You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
47 lines
1.4 KiB
47 lines
1.4 KiB
(*
|
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
|
*
|
|
* This source code is licensed under the MIT license found in the
|
|
* LICENSE file in the root directory of this source tree.
|
|
*)
|
|
open! IStd
|
|
module F = Format
|
|
|
|
(** Concrete interval domain (CItv) *)
|
|
|
|
type t [@@deriving compare]
|
|
|
|
val equal_to : IntLit.t -> t
|
|
|
|
val is_equal_to_zero : t -> bool
|
|
|
|
val as_int : t -> int option
|
|
(** [as_int v] returns [Some x] if [v] is known to be [x] *)
|
|
|
|
val pp : F.formatter -> t -> unit
|
|
|
|
type abduction_result =
|
|
| Unsatisfiable (** the assertion is never true given the parameters *)
|
|
| Satisfiable of t option * t option
|
|
(** the assertion is satisfiable and when it is true then the lhs and rhs can be optionally
|
|
refined to the given new intervals *)
|
|
|
|
val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> abduction_result
|
|
(** given [arith_lhs_opt bop arith_rhs_opt] and if not [negated], return either
|
|
|
|
- [Unsatisfiable] iff lhs bop rhs = ∅
|
|
|
|
- [Satisfiable (abduced_lhs_opt,abduced_rhs_opt)] iff lhs bop rhs ≠ ∅, such that (taking
|
|
lhs=true if lhs_opt is [None], same for rhs) [abduced_lhs_opt=Some alhs] if (lhs bop rhs ≠
|
|
∅ => alhs⇔lhs) (and similarly for rhs)
|
|
|
|
If [negated] then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa. *)
|
|
|
|
val binop : Binop.t -> t -> t -> t option
|
|
|
|
val unop : Unop.t -> t -> t option
|
|
|
|
val zero_inf : t
|
|
|
|
val ge_to : IntLit.t -> t
|