feat(dyn-trans): first implementation, quite aggressive

src/base-solver/sidekick_base_solver.ml

@@ -118,6 +118,12 @@ end)
 
 module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct
     module Solver = Solver
+    type term = Solver.T.Term.t
+    let term_as_eqn _tst t =
+      match Term.view t with
+      | Term.Eq(a,b) -> Some (a,b)
+      | _ -> None
+    let mk_eqn tst t u : term = Term.make tst (Term.Eq (t,u))
     end)
 
 let th_bool : Solver.theory = Th_bool.theory

src/th-dyn-trans/Sidekick_th_dyn_trans.ml

@@ -51,33 +51,104 @@ module Make(A: ARG)
   module Inst_tbl = CCHashtbl.Make(Instantiation)
 
   type t = {
+    tstore: Term.store;
     cc: CC.t;
     sat: SAT.t;
     cpool: SAT.clause_pool_id;
     done_inst: unit Inst_tbl.t;
-    stat_cc_confl : int Stat.counter;
+    stat_cc_confl: int Stat.counter;
+    stat_inst: int Stat.counter;
   }
 
   (* TODO: some rate limiting system (a counter that goes up when cc conflict,
      goes down by 5 when a new axiom is instantiated, cannot go below 0?) *)
 
-  let on_conflict (self:t) (cc:CC.t) ~th lits : unit =
+  (* TODO: maybe the clause pool should automatically discard already present
+     clauses, so that theories don't have to remember what they did *)
+
+  let inst_from_conflict (self:t) (cc:CC.t) lits : unit =
     Log.debugf 50 (fun k->k "(@[dyn-trans.confl@ %a@])"
                      (Util.pp_list Lit.pp) lits);
     Stat.incr self.stat_cc_confl;
+
+    (* list of tuples [(t, u, v, (t=u), (u=v), (t=v))] where [t=u]
+       and [u=v] are in [lits] *)
+    let candidates = Vec.create () in
+    begin
+      (* table [term -> {lit \in lits | lit = (term=term')}] *)
+      let tbl = Term.Tbl.create 8 in
+
+      let on_eqn t u lit =
+        assert (not (Lit.sign lit));
+        begin match Term.Tbl.get tbl t with
+          | Some (u',lit') ->
+            if not (Term.equal u u') then (
+              (* see if [t=u, t=u' => u=u'] has not been instantiated yet *)
+              let concl = Lit.atom self.tstore (A.mk_eqn self.tstore u u') in
+              let inst =
+                Instantiation.make self.tstore
+                  (Lit.neg lit) (Lit.neg lit') concl in
+              if not (Inst_tbl.mem self.done_inst inst) then (
+                Vec.push candidates (t,u,u',lit,lit',concl)
+              )
+            )
+          | None -> Term.Tbl.add tbl t (u,lit);
+        end
+      in
+
+      Iter.of_list lits
+      |> Iter.filter (fun lit -> not (Lit.sign lit))
+      |> Iter.filter_map
+        (fun lit ->
+           match A.term_as_eqn self.tstore (Lit.term lit) with
+           | Some (t,u) when not (Term.equal t u) -> Some (t,u,lit)
+           | _ -> None)
+      |> Iter.iter
+        (fun (t,u,lit) ->
+           on_eqn t u lit;
+           on_eqn u t lit;
+        )
+    end;
+
+    if not (Vec.is_empty candidates) then (
+      let pp_cand out (t,u,v,l1,l2,concl) =
+        Fmt.fprintf out "(@[%a,@ %a,@ %a,@ %a,@ %a,@ ==> %a@])"
+          Term.pp t Term.pp u Term.pp v Lit.pp l1 Lit.pp l2 Lit.pp concl in
+      Log.debugf 20 (fun k->k "@[candidates: %a@]" (Vec.pp pp_cand) candidates);
+    );
+
+    begin
+      Vec.to_iter candidates
+      |> Iter.take 2 (* at most 2 for now *)
+      |> Iter.iter
+        (fun (_,_,_,l1,l2,concl) ->
+           let c = [l1; l2; concl] in
+           Stat.incr self.stat_inst;
+           Log.debugf 10 (fun k->k "add dyn-trans %a" (Fmt.Dump.list Lit.pp) c);
+           let emit_proof p = () in (* TODO *)
+           CC.add_clause ~pool:self.cpool cc c emit_proof)
+    end;
+
     (* TODO: find some potential dyn-trans axioms; add them to self.sat
        if they're not in done_inst *)
     ()
 
+  let on_conflict (self:t) (cc:CC.t) ~th lits : unit =
+    if not th then (
+      inst_from_conflict self cc lits
+    )
+
   let create_and_setup si sat : unit =
     Log.debugf 1 (fun k->k "(dyn-trans.setup)");
     let self = {
+      tstore=SI.tst si;
       cc=SI.cc si;
       sat;
       done_inst=Inst_tbl.create 32;
       cpool=SAT.new_clause_pool_gc_fixed_size
           ~descr:"dyn-trans clauses" ~size:200 sat;
       stat_cc_confl=Stat.mk_int (SI.stats si) "dyn-trans-confl";
+      stat_inst=Stat.mk_int (SI.stats si) "dyn-trans-inst";
     } in
     CC.on_conflict self.cc (on_conflict self);
     ()