Module Pulselib.PulseFormula

module F = Stdlib.Format
module Var = PulseAbstractValue

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

type t
val pp : F.formatter -> t -> unit
val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit

only used for unit tests

type 'a normalized =
| Unsat
| Sat of 'a
type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

val ttrue : t
val and_equal : operand -> operand -> t -> t normalized
val and_less_equal : operand -> operand -> t -> t normalized
val and_less_than : operand -> operand -> t -> t normalized
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> t normalized
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> t normalized
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t normalized

Operations

val normalize : t -> t normalized

think a bit harder about the formula

val simplify : keep:Var.Set.t -> t -> t normalized
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t) normalized
val is_known_zero : t -> Var.t -> bool
val as_int : t -> Var.t -> int option
val has_no_assumptions : t -> bool

Notations

include sig ... end
module SatUnsatMonad : sig ... end

Useful notations to deal with normalized formulas