Module Pulselib.PulseFormulaTerm

module F = Stdlib.Format
module L = IBase.Logging
module CItv = PulseCItv
module SatUnsat = PulseSatUnsat
module Debug = PulseFormulaDebug
module Var = PulseFormulaVar
module Q = QSafeCapped
module Z = ZSafe
module LinArith = PulseFormulaLinArit
type function_symbol =
  1. | Unknown of Var.t
  2. | Procname of IR.Procname.t
val compare_function_symbol : function_symbol -> function_symbol -> int
val equal_function_symbol : function_symbol -> function_symbol -> bool
val yojson_of_function_symbol : function_symbol -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp_function_symbol : Var.F.formatter -> function_symbol -> unit
type operand =
  1. | AbstractValueOperand of Var.t
  2. | ConstOperand of IR.Const.t
  3. | FunctionApplicationOperand of {
    1. f : function_symbol;
    2. actuals : Var.t list;
    }
val compare_operand : operand -> operand -> int
val equal_operand : operand -> operand -> bool
val pp_operand : Var.F.formatter -> operand -> unit
type 'term_t subst_target = 'term_t LinArith.subst_target =
  1. | QSubst of Q.t
  2. | ConstantSubst of 'term_t * Var.t option
  3. | VarSubst of Var.t
  4. | LinSubst of LinArith.t
  5. | NonLinearTermSubst of 'term_t
val targetted_subst_var : Var.Map.key Var.Map.t -> Var.Map.key -> 'a subst_target

Expressive term structure to be able to express all of SIL, but the main smarts of the formulas are for the equality between variables and linear arithmetic subsets. Terms (and atoms, below) are kept as a last-resort for when outside that fragment.

type t =
  1. | Const of Q.t
  2. | String of string
  3. | Var of Var.t
  4. | Procname of IR.Procname.t
  5. | FunctionApplication of {
    1. f : t;
    2. actuals : t list;
    }
  6. | Linear of LinArith.t
  7. | Add of t * t
  8. | Minus of t
  9. | LessThan of t * t
  10. | LessEqual of t * t
  11. | Equal of t * t
  12. | NotEqual of t * t
  13. | Mult of t * t
  14. | DivI of t * t
  15. | DivF of t * t
  16. | And of t * t
  17. | Or of t * t
  18. | Not of t
  19. | Mod of t * t
  20. | BitAnd of t * t
  21. | BitOr of t * t
  22. | BitNot of t
  23. | BitShiftLeft of t * t
  24. | BitShiftRight of t * t
  25. | BitXor of t * t
  26. | StringConcat of t * t
  27. | IsInstanceOf of {
    1. var : Var.t;
    2. typ : IR.Typ.t;
    3. nullable : bool;
    }
  28. | IsInt of t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val equal_syntax : t -> t -> bool
val needs_paren : t -> bool
val pp_paren : (F.formatter -> LinArith.Var.t -> unit) -> needs_paren:(t -> bool) -> F.formatter -> t -> unit
val pp_no_paren : (F.formatter -> LinArith.Var.t -> unit) -> F.formatter -> t -> unit
val pp : (F.formatter -> LinArith.Var.t -> unit) -> F.formatter -> t -> unit
val of_q : Q.t -> t
val of_intlit : IR.IntLit.t -> t
val of_const : IR.Const.t -> t
val of_operand : operand -> t
val of_subst_target : t subst_target -> t
val one : t
val zero : t
val of_bool : bool -> t
val of_unop : IR.Unop.t -> t -> t
val of_binop : IR.Binop.t -> t -> t -> t
val is_zero : t -> bool
val is_non_zero_const : t -> bool
val has_known_non_boolean_type : t -> bool
val fold_map_direct_subterms : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t

Fold f on the strict sub-terms of t, if any. Preserve physical equality if f does.

val map_direct_subterms : t -> f:(t -> t) -> t
val satunsat_map_direct_subterms : t -> f:(t -> t SatUnsat.Import.sat_unsat_t) -> t SatUnsat.Import.sat_unsat_t
val fold_subst_variables : init:'a -> f_subst:('a -> LinArith.Var.t -> 'a * t LinArith.subst_target) -> ?f_post:(prev:t -> 'a -> t -> 'a * t) -> t -> 'a * t
val fold_variables : init:'a -> f:('a -> LinArith.Var.t -> 'a) -> ?f_post:(prev:t -> 'a -> t -> 'a * t) -> t -> 'a
val iter_variables : t -> f:(LinArith.Var.t -> unit) -> unit
val subst_variables : f:(LinArith.Var.t -> t LinArith.subst_target) -> ?f_post:(prev:t -> unit -> t -> unit * t) -> t -> t
val has_var_notin : Var.Set.t -> t -> bool
val eval_const_shallow_ : t -> t option

reduce to a constant when the direct sub-terms are constants

val eval_const_shallow : t -> t SatUnsat.Import.sat_unsat_t
val simplify_shallow : t -> t SatUnsat.Import.sat_unsat_t
val linearize : t -> t

more or less syntactic attempt at detecting when an arbitrary term is a linear formula; call Atom.eval_term first for best results

val simplify_linear : t -> t
val get_as_isinstanceof : t -> (Var.t * IR.Typ.t * bool) option
val get_as_var : t -> Var.t option
val get_as_const : t -> Q.t option
val is_non_numeric_constant : t -> bool
val get_as_linear : t -> LinArith.t option
val to_subst_target : t -> t subst_target
module VarMap : sig ... end
module Set : sig ... end