fix(tseitin): use final check to push axioms

src/cc/Congruence_closure.ml

@@ -842,9 +842,9 @@ module Make(A: ARG) = struct
     let sign = A.Lit.sign lit in
     begin match T.cc_view t with
       | Eq (a,b) when sign ->
-        (* merge [a] and [b] *)
         let a = add_term cc a in
         let b = add_term cc b in
+        (* merge [a] and [b] *)
         push_combine cc a b (Expl.mk_lit lit)
       | _ ->
         (* equate t and true/false *)

src/smt/Theory_combine.ml

@@ -42,8 +42,8 @@ let[@inline] theories (self:t) : theory_state Sequence.t =
 (* handle a literal assumed by the SAT solver *)
 let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit =
   Msat.Log.debugf 2
-    (fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}@ %a@])"
+    (fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
-        (Util.pp_seq ~sep:";" Lit.pp) lits);
+        (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
   (* transmit to CC *)
   Vec.clear self.new_merges;
   let cc = cc self in

src/th-bool/Sidekick_th_bool.ml

@@ -162,7 +162,9 @@ type t = {
   tst: Term.state;
 }
 
-let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit =
+let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
+
+let tseitin ~final (self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit =
   let (module A) = acts in
   Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
   match v with
@@ -172,9 +174,16 @@ let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term vie
     let l = IArray.to_list l in
     if Lit.sign lit then (
       A.propagate_distinct l ~neq:lit_t lit
-    ) else (
+    ) else if final then (
-      (* TODO: propagate pairwise equalities? *)
+      (* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
-      Error.errorf "cannot process negative distinct lit %a" Lit.pp lit;
+      let c =
+        Sequence.diagonal_l l
+        |> Sequence.map (fun (t,u) -> Lit.eq self.tst t u)
+        |> Sequence.to_rev_list
+      in
+      let c = Lit.neg lit :: c in
+      Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c);
+      A.add_local_axiom c
     )
   | B_and subs ->
     if Lit.sign lit then (
@@ -182,35 +191,35 @@ let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term vie
       IArray.iter
         (fun sub ->
            let sublit = Lit.atom sub in
-           A.add_local_axiom [Lit.neg lit; sublit])
+           A.propagate sublit [lit])
         subs
-    ) else (
+    ) else if final then (
-      (* propagate [¬lit => ∨_i ¬ subs_i] *)
+      (* axiom [¬lit => ∨_i ¬ subs_i] *)
       let subs = IArray.to_list subs in
       let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
       A.add_local_axiom c
     )
   | B_or subs ->
-    if Lit.sign lit then (
+    if not @@ Lit.sign lit then (
-      (* propagate [lit => ∨_i subs_i] *)
-      let subs = IArray.to_list subs in
-      let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
-      A.add_local_axiom c
-    ) else (
       (* propagate [¬lit => ¬subs_i] *)
       IArray.iter
         (fun sub ->
            let sublit = Lit.atom ~sign:false sub in
            A.add_local_axiom [Lit.neg lit; sublit])
         subs
+    ) else if final then (
+      (* axiom [lit => ∨_i subs_i] *)
+      let subs = IArray.to_list subs in
+      let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
+      A.add_local_axiom c
     )
   | B_imply (guard,concl) ->
-    if Lit.sign lit then (
+    if Lit.sign lit && final then (
-      (* propagate [lit => ∨_i ¬guard_i ∨ concl] *)
+      (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
       let guard = IArray.to_list guard in
       let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
       A.add_local_axiom c
-    ) else (
+    ) else if not @@ Lit.sign lit then (
       (* propagate [¬lit => ¬concl] *)
       A.propagate (Lit.atom ~sign:false concl) [lit];
       (* propagate [¬lit => ∧_i guard_i] *)
@@ -221,15 +230,19 @@ let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term vie
         guard
     )
 
-let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
+let check_ ~final self acts lits =
   lits
     (fun lit ->
        let t = Lit.term lit in
        match view t with
-       | B_atom _ -> ()
+       | B_atom _ | B_eq _ -> ()
-       | v -> tseitin self acts lit t v)
+       | v -> tseitin ~final self acts lit t v)
 
-let final_check _ _ _ : unit = ()
+let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
+  check_ ~final:false self acts lits
+
+let final_check (self:t) acts (lits:Lit.t Sequence.t) =
+  check_ ~final:true self acts lits
 
 let th =
   Theory.make