Normalizer (infer.Pulselib.PulseFormulaPhi.Normalizer)

val and_var_linarith : 
  Var.t ->
  LinArith.t ->
  (t * new_eqs) ->
  (t * new_eqs) SatUnsat.t

val and_var_term : Var.t -> Term.t -> (t * new_eqs) -> (t * new_eqs) SatUnsat.t

val and_var_var : Var.t -> Var.t -> (t * new_eqs) -> (t * new_eqs) SatUnsat.t

val normalize_atom : t -> Atom.t -> Atom.t list SatUnsat.t

val and_normalized_atoms : 
  (t * new_eqs) ->
  Atom.t list ->
  orig_atom:Atom.t list ->
  add_term:bool ->
  (t * new_eqs) SatUnsat.t

use with the result of normalize_atom in place of and_atom

val and_atom : 
  Atom.t ->
  (t * new_eqs) ->
  add_term:bool ->
  (t * new_eqs) SatUnsat.t

val and_dynamic_type : 
  Var.t ->
  IR.Typ.t ->
  ?source_file:IBase.SourceFile.t ->
  (t * new_eqs) ->
  (t * new_eqs) SatUnsat.t

val and_below : Var.t -> IR.Typ.t -> (t * new_eqs) -> (t * new_eqs) SatUnsat.t

val and_notbelow : 
  Var.t ->
  IR.Typ.t ->
  (t * new_eqs) ->
  (t * new_eqs) SatUnsat.t

val propagate_atom : Atom.t -> (t * new_eqs) -> (t * new_eqs) SatUnsat.t

and_atom atom (phi, new_eqs) is SatUnsat.(normalize_atom phi atom >>= and_normalized_atoms (phi, new_eqs))