Module Sidekick_base.Form

Formulas (boolean terms).

This module defines function symbols, constants, and views to manipulate boolean formulas in Sidekick_base. This is useful to have the ability to use boolean connectives instead of being limited to clauses; by using Sidekick_th_bool_static, the formulas are turned into clauses automatically for you.

type 'a view = 'a Sidekick_core.Bool_view.t =
  1. | B_bool of bool
  2. | B_not of 'a
  3. | B_and of 'a list
  4. | B_or of 'a list
  5. | B_imply of 'a * 'a
  6. | B_equiv of 'a * 'a
  7. | B_xor of 'a * 'a
  8. | B_eq of 'a * 'a
  9. | B_neq of 'a * 'a
  10. | B_ite of 'a * 'a * 'a
  11. | B_atom of 'a
val view : term -> term view
val bool : Sidekick_core.Term.store -> bool -> term
val not_ : Sidekick_core.Term.store -> term -> term
val and_ : Sidekick_core.Term.store -> term -> term -> term
val or_ : Sidekick_core.Term.store -> term -> term -> term
val imply : Sidekick_core.Term.store -> term -> term -> term
val equiv : Sidekick_core.Term.store -> term -> term -> term
val distinct_l : Sidekick_core.Term.store -> term list -> term
val const_decoders : Sidekick_core.Const.decoders
val and_l : Sidekick_core.Term.store -> term list -> term
val or_l : Sidekick_core.Term.store -> term list -> term
val imply_l : Sidekick_core.Term.store -> term list -> term -> term
val mk_of_view : Sidekick_core.Term.store -> term view -> term