Module Pulselib__PulseFormula
module Var = Pulselib.PulseAbstractValue
Arithmetic solver
Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.
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
Notations
include sig ... end
module SatUnsatMonad : sig ... end
Useful notations to deal with normalized formulas