diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/N/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/N/index.html index 751a5430..7a8895c8 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/N/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/N/index.html @@ -1,2 +1,2 @@ -
CC.NCC.NSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endCC.NCC.NSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endCC.NCC.NSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endCC.NCC.NSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endSolver_internal.CCmodule T : sig ... endmodule P : sig ... endmodule Lit : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endval term_store : t -> term_storeval find : t -> node -> reprval add_term : t -> term -> nodeval mem_term : t -> term -> booltype ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unittype ev_on_post_merge = t -> actions -> N.t -> N.t -> unittype ev_on_new_term = t -> N.t -> term -> unittype ev_on_conflict = t -> th:bool -> lit list -> unittype ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unittype ev_on_is_subterm = N.t -> term -> unitval create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Big | `Small ] -> term_store -> tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval set_as_lit : t -> N.t -> lit -> unitval find_t : t -> term -> reprval add_seq : t -> term Iter.t -> unitval all_classes : t -> repr Iter.tval assert_lit : t -> lit -> unitval assert_lits : t -> lit Iter.t -> unitval explain_eq : t -> N.t -> N.t -> lit listval raise_conflict_from_expl : t -> actions -> Expl.t -> 'aval n_true : t -> N.tval n_false : t -> N.tval n_bool : t -> bool -> N.tval merge : t -> N.t -> N.t -> Expl.t -> unitval merge_t : t -> term -> term -> Expl.t -> unitval check : t -> actions -> unitval new_merges : t -> boolval push_level : t -> unitval pop_levels : t -> int -> unitval get_model : t -> N.t Iter.t Iter.tmodule Debug_ : sig ... endCC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Make.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
Make.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Sidekick_cc.Makemodule T = A.Tmodule P = A.Pmodule Lit = A.Litmodule Actions = A.Actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Sidekick_cc.Makemodule T = A.Tmodule P = A.Pmodule Lit = A.Litmodule Actions = A.Actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
S.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
S.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Sidekick_cc.Smodule T : Sidekick_core.TERMmodule P : Sidekick_core.PROOF with type term = T.Term.tmodule Lit : Sidekick_core.LIT with module T = Ttype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Sidekick_cc.Smodule T : Sidekick_core.TERMmodule P : Sidekick_core.PROOF with type term = T.Term.tmodule Lit : Sidekick_core.LIT with module T = Ttype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
SI.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
SI.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Sidekick_coreTheories and concrete solvers rely on an environment that defines several important types:
In this module we define most of the main signatures used throughout Sidekick.
module CC_view : sig ... endView terms through the lens of the Congruence Closure
module type TERM = sig ... endMain representation of Terms and Types
module type PROOF = sig ... endProofs of unsatisfiability
module type LIT = sig ... endLiterals
module type CC_ACTIONS = sig ... endActions provided to the congruence closure.
module type CC_ARG = sig ... endArguments to a congruence closure's implementation
module type CC_S = sig ... endSignature of the congruence closure
module type SOLVER_INTERNAL = sig ... endA view of the solver from a theory's point of view.
module type SOLVER = sig ... endUser facing view of the solver
module type MONOID_ARG = sig ... endHelper for the congruence closure
module Monoid_of_repr : functor (M : MONOID_ARG) -> sig ... endState for a per-equivalence-class monoid.
Sidekick_coreTheories and concrete solvers rely on an environment that defines several important types:
In this module we define most of the main signatures used throughout Sidekick.
module CC_view : sig ... endView terms through the lens of the Congruence Closure
module type TERM = sig ... endMain representation of Terms and Types
module type PROOF = sig ... endProofs of unsatisfiability
module type LIT = sig ... endLiterals
module type CC_ACTIONS = sig ... endActions provided to the congruence closure.
module type CC_ARG = sig ... endArguments to a congruence closure's implementation
module type CC_S = sig ... endMain congruence closure.
module type SOLVER_INTERNAL = sig ... endA view of the solver from a theory's point of view.
module type SOLVER = sig ... endUser facing view of the solver
module type MONOID_ARG = sig ... endHelper for the congruence closure
module Monoid_of_repr : functor (M : MONOID_ARG) -> sig ... endState for a per-equivalence-class monoid.
CC_S.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC_S.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Sidekick_core.CC_SSignature of the congruence closure
type term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Sidekick_core.CC_SMain congruence closure.
The congruence closure handles the theory QF_UF (uninterpreted function symbols). It is also responsible for theory combination, and provides a general framework for equality reasoning that other theories piggyback on.
For example, the theory of datatypes relies on the congruence closure to do most of the work, and "only" adds injectivity/disjointness/acyclicity lemmas when needed.
Similarly, a theory of arrays would hook into the congruence closure and assert (dis)equalities as needed.
type term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
SI.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
SI.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
SOLVER_INTERNAL.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
SOLVER_INTERNAL.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
CC.NAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termval equal : t -> t -> boolval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
CC.NEquivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
type tAn equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
val term : t -> termTerm contained in this equivalence class. If is_root n, then term n is the class' representative term.
val equal : t -> t -> boolAre two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
val iter_class : t -> t Iter.tTraverse the congruence class. Precondition: is_root n (see find below)
val iter_parents : t -> t Iter.tTraverse the parents of the class. Precondition: is_root n (see find below)
type bitfieldA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See Sidekick_core.CC_S.allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tState of the congruence closure
module N : sig ... endAn equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new bitfield for the nodes. See N.bitfield.
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
Solver_internal.CCCongruence closure instance
module T = Tmodule P = Pmodule Lit = Litmodule Actions : Sidekick_core.CC_ACTIONS with module T = T and module Lit = Lit and module P = P and type t = actionstype term_store = T.Term.storetype term = T.Term.ttype fun_ = T.Fun.ttype lit = Lit.ttype proof = P.ttype actions = Actions.ttype tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tval term_store : t -> term_storeval find : t -> node -> reprCurrent representative
Events triggered by the congruence closure, to which other plugins can subscribe.
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unitev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unitev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
type ev_on_new_term = t -> N.t -> term -> unitev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
type ev_on_conflict = t -> th:bool -> lit list -> unitev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See Sidekick_core.CC_ACTIONS.propagate.
type ev_on_is_subterm = N.t -> term -> unitev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create : ?stat:Sidekick_util.Stat.t -> ?on_pre_merge:ev_on_pre_merge list -> ?on_post_merge:ev_on_post_merge list -> ?on_new_term:ev_on_new_term list -> ?on_conflict:ev_on_conflict list -> ?on_propagate:ev_on_propagate list -> ?on_is_subterm:ev_on_is_subterm list -> ?size:[ `Small | `Big ] -> term_store -> tCreate a new congruence closure.
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
val find_t : t -> term -> reprCurrent representative of the term.
if the term is not already add-ed.
val all_classes : t -> repr Iter.tAll current classes. This is costly, only use if there is no other solution
val assert_lit : t -> lit -> unitGiven a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> lit listExplain why the two nodes are equal. Fails if they are not, in an unspecified way
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'aRaise a conflict with the given explanation it must be a theory tautology that expl ==> absurd. To be used in theories.
val merge : t -> N.t -> N.t -> Expl.t -> unitMerge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val check : t -> actions -> unitPerform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.