Module Pulselib.PulseFormulaAtom

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
module Term = PulseFormulaTerm

Basically boolean terms, used to build the part of a formula that is not equalities between linear arithmetic.

type t =
  1. | LessEqual of Term.t * Term.t
  2. | LessThan of Term.t * Term.t
  3. | Equal of Term.t * Term.t
  4. | NotEqual of Term.t * Term.t
val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp_with_pp_var : (Term.F.formatter -> Term.LinArith.Var.t -> unit) -> F.formatter -> t -> unit
val get_terms : t -> Term.t * Term.t
val fold_map_terms : t -> init:'a -> f:('a -> Term.t -> 'a * Term.t) -> 'a * t

preserve physical equality if f does

val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
val fold_variables : t -> init:'a -> f:('a -> Term.LinArith.Var.t -> 'a) -> 'a
val equal : Term.t -> Term.t -> t
val not_equal : Term.t -> Term.t -> t
val less_equal : Term.t -> Term.t -> t
val less_than : Term.t -> Term.t -> t
val nnot : t -> t
val map_terms : t -> f:(Term.t -> Term.t) -> t
val to_term : t -> Term.t
type eval_result =
  1. | True
  2. | False
  3. | Atom of t
val eval_result_of_bool : bool -> eval_result
val nnot_if : bool -> t -> t
val atoms_of_term : is_neq_zero:(Term.t -> bool) -> negated:bool -> ?force_to_atom:bool -> Term.t -> t list option

atoms_of_term ~negated t is Some [atom1; ..; atomN] if t (or ¬t if negated) is (mostly syntactically) equivalent to atom1 ∧ .. ∧ atomN. For example atoms_of_term ~negated:false (Equal (Or (x, Not y), 0)) should be [Equal (x, 0); NotEqual (y, 0)]. When the term y is known as a boolean, it generates a preciser atom Equal (y, 1).

is_neq_zero is a function that can tell if a term is known to be ≠0, and force_to_atom can be used to force converting the term into an atom even if it does not make it simpler or stronger.

val get_as_embedded_atoms : is_neq_zero:(Term.t -> bool) -> t -> t list option

similar to atoms_of_term but takes an atom and "flattens" it to possibly several atoms whose conjunction is equivalent to the original atom

val eval_const_shallow : t -> eval_result
val var_terms_to_linear : t -> t
val get_as_linear : t -> t option
val eval_syntactically_equal_terms : t -> eval_result
val eval_with_normalized_terms : is_neq_zero:(Term.t -> bool) -> t -> t list option SatUnsat.Import.sat_unsat_t
val eval_atoms_with_normalized_terms : is_neq_zero:(Term.t -> bool) -> t list -> t list SatUnsat.t
val eval_term : is_neq_zero:(Term.t -> bool) -> Term.t -> Term.t Term.SatUnsat.Import.sat_unsat_t
val eval : is_neq_zero:(Term.t -> bool) -> t -> t list Pulselib__PulseSatUnsat.t
val fold_subst_variables : init:'a -> f_subst:('a -> Term.LinArith.Var.t -> 'a * Term.t Term.LinArith.subst_target) -> ?f_post:(prev:Term.t -> 'a -> Term.t -> 'a * Term.t) -> t -> 'a * t
val subst_variables : t -> f:(Term.LinArith.Var.t -> Term.t Term.LinArith.subst_target) -> t
val has_var_notin : Term.Var.Set.t -> t -> bool
val get_as_var_neq_zero : t -> Term.Var.t option
val get_as_disequal_vars : t -> (Term.Var.t * Term.Var.t) option
val simplify_linear : t -> t
module Set : sig ... end
module Map : sig ... end