Module Pulselib__PulseFormula
module Var = Pulselib.PulseAbstractValueArithmetic solver
Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.
val pp : F.formatter -> t -> unitval pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unitonly used for unit tests
type 'a normalized=|Unsat|Sat of 'atype operand=|LiteralOperand of IR.IntLit.t|AbstractValueOperand of Var.t
Build formulas
val ttrue : tval and_equal : operand -> operand -> t -> t normalizedval and_less_equal : operand -> operand -> t -> t normalizedval and_less_than : operand -> operand -> t -> t normalizedval and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> t normalizedval and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> t normalizedval prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t normalized
Operations
val normalize : t -> t normalizedthink a bit harder about the formula
Notations
include sig ... end
module SatUnsatMonad : sig ... endUseful notations to deal with normalized formulas