feat: more expressive theories, also plug distinct in

src/cc/Congruence_closure.ml

@@ -324,6 +324,7 @@ module Make(A: ARG) = struct
     combine: combine_task Vec.t;
     undo: (unit -> unit) Backtrack_stack.t;
     mutable theories: theory IM.t;
+    mutable on_merge: (t -> N.t -> N.t -> Expl.t -> unit) list;
     mutable ps_lits: lit list; (* TODO: thread it around instead? *)
     (* proof state *)
     ps_queue: (node*node) Vec.t;
@@ -734,6 +735,8 @@ module Make(A: ARG) = struct
       merge_bool rb b ra a;
       (* perform [union r_from r_into] *)
       Log.debugf 15 (fun k->k "(@[cc.merge@ :from %a@ :into %a@])" N.pp r_from N.pp r_into);
+      (* call [on_merge] functions *)
+      List.iter (fun f -> f cc r_into r_from e_ab) cc.on_merge;
       (* call micro theories *)
       begin
         let th_into = r_into.n_th_data in
@@ -986,13 +989,16 @@ module Make(A: ARG) = struct
     Log.debugf 3 (fun k->k "(@[@{<green>cc.add-theory@} %a@])" Key.pp Th.key);
     self.theories <- IM.add Th.key_id th self.theories
 
-  let create ?th:(theories=[]) ?(size=`Big) (tst:term_state) : t =
+  let on_merge cc f = cc.on_merge <- f :: cc.on_merge
+
+  let create ?th:(theories=[]) ?(on_merge=[]) ?(size=`Big) (tst:term_state) : t =
     let size = match size with `Small -> 128 | `Big -> 2048 in
     let rec cc = {
       tst;
       tbl = T_tbl.create size;
       signatures_tbl = Sig_tbl.create size;
       theories=IM.empty;
+      on_merge;
       pending=Vec.create();
       combine=Vec.create();
       ps_lits=[];

src/cc/Congruence_closure_intf.ml

@@ -152,6 +152,7 @@ module type S = sig
 
   val create :
     ?th:Theory.t list ->
+    ?on_merge:(t -> N.t -> N.t -> Expl.t -> unit) list ->
     ?size:[`Small | `Big] ->
     term_state ->
     t
@@ -162,6 +163,9 @@ module type S = sig
       @raise Error.Error if there is already a theory with
       the same key. *)
 
+  val on_merge : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit
+  (** Add a function to be called when two classes are merged *)
+
   val set_as_lit : t -> N.t -> lit -> unit
   (** map the given node to a literal. *)
 

src/main/main.ml

@@ -117,7 +117,9 @@ let main () =
         (* TODO: eager CNF conversion *)
         [Sidekick_th_bool.th_dynamic_tseitin]
       | Smtlib ->
-        [Sidekick_th_bool.th_dynamic_tseitin] (* TODO: more theories *)
+        [ Sidekick_th_bool.th_dynamic_tseitin;
+          Sidekick_th_distinct.th;
+        ] (* TODO: more theories *)
     in
     Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
   in

src/smt/Term.ml

@@ -102,6 +102,7 @@ module As_key = struct
 end
 
 module Map = CCMap.Make(As_key)
+module Set = CCSet.Make(As_key)
 module Tbl = CCHashtbl.Make(As_key)
 
 let to_seq t yield =

src/smt/Term.mli

@@ -56,3 +56,4 @@ val as_cst_undef : t -> (cst * Ty.Fun.t) option
 
 module Tbl : CCHashtbl.S with type key = t
 module Map : CCMap.S with type key = t
+module Set : CCSet.S with type elt = t

src/smt/Theory.ml

@@ -36,6 +36,10 @@ module type ACTIONS = sig
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
+  val add_lit : Lit.t -> unit
+  (** Add the given literal to the SAT solver, so it gets assigned
+      a boolean value *)
+
   val add_local_axiom: Lit.t list -> unit
   (** Add local clause to the SAT solver. This clause will be
       removed when the solver backtracks. *)
@@ -56,10 +60,11 @@ module type S = sig
   val create : Term.state -> t
   (** Instantiate the theory's state *)
 
-  (* TODO: instead pass Congruence_closure.theory to [create] 
+  val on_new_term : t -> actions -> Term.t -> unit
+  (** Called when a new term is added *)
+
   val on_merge: t -> actions -> CC_eq_class.t -> CC_eq_class.t -> CC_expl.t -> unit
   (** Called when two classes are merged *)
-     *)
 
   val partial_check : t -> actions -> Lit.t Sequence.t -> unit
   (** Called when a literal becomes true *)
@@ -87,6 +92,7 @@ type 'a t1 = (module S with type t = 'a)
 let make
   (type st)
     ?(check_invariants=fun _ -> ())
+    ?(on_new_term=fun _ _ _ -> ())
     ?(on_merge=fun _ _ _ _ _ -> ())
     ?(partial_check=fun _ _ _ -> ())
     ?(mk_model=fun _ _ m -> m)
@@ -100,6 +106,7 @@ let make
     type nonrec t = st
     let name = name
     let create = create
+    let on_new_term = on_new_term
     let on_merge = on_merge
     let partial_check = partial_check
     let final_check = final_check

src/smt/Theory_combine.ml

@@ -60,6 +60,7 @@ let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit =
       acts.Msat.acts_add_clause ~keep:false lits Proof_default
     let[@inline] add_persistent_axiom lits : unit =
       acts.Msat.acts_add_clause ~keep:true lits Proof_default
+    let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit
   end in
   let acts = (module A : Theory.ACTIONS) in
   theories self

src/smtlib/Process.ml

@@ -8,7 +8,7 @@ type 'a or_error = ('a, string) CCResult.t
 module E = CCResult
 module A = Ast
 module Form = Sidekick_th_bool.Bool_term
-module Distinct = Sidekick_th_distinct
+module Th_distinct = Sidekick_th_distinct
 module Fmt = CCFormat
 module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver))
 
@@ -138,7 +138,7 @@ module Conv = struct
           in
           Form.and_l tst (curry_eq l)
         | A.Op (A.Distinct, l) ->
-          Distinct.distinct_l tst @@ List.map (aux subst) l
+          Th_distinct.distinct_l tst @@ List.map (aux subst) l
         | A.Not f -> Form.not_ tst (aux subst f)
         | A.Bool true -> Term.true_ tst
         | A.Bool false -> Term.false_ tst