fix preprocessing in th-bool

src/lra/sidekick_arith_lra.ml

@@ -381,7 +381,6 @@ module Make(A : ARG) : S with module A = A = struct
 
     | LRA_other t when A.has_ty_real t -> None
     | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
-      Log.debug 0 "LRA NONE";
       None
 
   let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =

src/sat/Solver.ml

@@ -1842,7 +1842,6 @@ module Make(Plugin : PLUGIN)
   let[@inline] proof st = st.proof
 
   let[@inline] add_lit self ?default_pol lit =
-    Log.debugf 0 (fun k->k"add lit %a" Lit.pp lit); (* XXX *)
     ignore (make_atom_ self lit ?default_pol : atom)
   let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit =
     let a = make_atom_ self lit ~default_pol:pol in

src/smt-solver/Sidekick_smt_solver.ml

@@ -251,7 +251,7 @@ module Make(A : ARG)
     (* actual preprocessing logic, acting on terms.
        this calls all the preprocessing hooks on subterms, ensuring
        a fixpoint. *)
-    let preprocess_term_ (self:t) (module A:PREPROCESS_ACTS) (t:term) : term =
+    let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term =
       let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
 
       (* compute and cache normal form [u] of [t].
@@ -261,19 +261,19 @@ module Make(A : ARG)
          next time we preprocess [t], we will have to re-emit the same
          proofs, even though we will not do any actual preprocessing work.
       *)
-      let rec aux t : term =
+      let rec preproc_rec t : term =
         match Term.Tbl.find self.preprocess_cache t with
         | u -> u
         | exception Not_found ->
           (* try rewrite at root *)
-          let t1 = aux_rec t self.preprocess in
+          let t1 = preproc_with_hooks t self.preprocess in
 
           (* map subterms *)
-          let t2 = Term.map_shallow self.tst aux t1 in
+          let t2 = Term.map_shallow self.tst preproc_rec t1 in
 
           let u =
             if not (Term.equal t t2) then (
-              aux t2 (* fixpoint *)
+              preproc_rec t2 (* fixpoint *)
             ) else (
               t2
             )
@@ -288,7 +288,7 @@ module Make(A : ARG)
             (* make a literal (already preprocessed) *)
             let lit = mk_lit_nopreproc u in
             (* ensure that SAT solver has a boolean atom for [u] *)
-            A.add_lit lit;
+            A0.add_lit lit;
 
             (* also map [sub] to this atom in the congruence closure, for propagation *)
             let cc = cc self in
@@ -305,39 +305,21 @@ module Make(A : ARG)
           u
 
       (* try each function in [hooks] successively *)
-      and aux_rec t hooks : term =
+      and preproc_with_hooks t hooks : term =
         match hooks with
         | [] -> t
         | h :: hooks_tl ->
-          match h self (module A) t with
+          (* call hook, using [pacts] which will ensure all new
-          | None -> aux_rec t hooks_tl
+             literals and clauses are also preprocessed *)
-          | Some u -> aux u
+          match h self (Lazy.force pacts) t with
-      in
+          | None -> preproc_with_hooks t hooks_tl
-
+          | Some u -> preproc_rec u
-      P.begin_subproof self.proof;
-
-      (* simplify the term *)
-      let t1 = simp_t self t in
-
-      (* preprocess *)
-      let u = aux t1 in
-      (* emit [|- t=u] *)
-      if not (Term.equal t u) then (
-        P.with_proof self.proof (P.lemma_preprocess t u);
-      );
-
-      P.end_subproof self.proof;
-      u
-
-    (* return preprocessed lit + proof they are equal *)
-    let preprocess_lit_ (self:t) (module A0:PREPROCESS_ACTS) (lit:lit) : lit =
 
       (* create literal and preprocess it with [pacts], which uses [A0]
          for the base operations, and preprocesses new literals and clauses
          recursively. *)
-      let rec mk_lit ?sign t =
+      and mk_lit ?sign t =
-        Log.debug 0 "A.MK_LIT";
+        let u = preproc_rec t in
-        let u = preprocess_term_ self (Lazy.force pacts) t in
         if not (Term.equal t u) then (
           Log.debugf 10
             (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
@@ -364,7 +346,27 @@ module Make(A : ARG)
         end : PREPROCESS_ACTS)
       ) in
 
-      preprocess_lit lit
+      P.begin_subproof self.proof;
+
+      (* simplify the term *)
+      let t1 = simp_t self t in
+
+      (* preprocess *)
+      let u = preproc_rec t1 in
+      (* emit [|- t=u] *)
+      if not (Term.equal t u) then (
+        P.with_proof self.proof (P.lemma_preprocess t u);
+      );
+
+      P.end_subproof self.proof;
+      u
+
+    (* return preprocessed lit *)
+    let preprocess_lit_ (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
+      let t = Lit.term lit in
+      let sign = Lit.sign lit in
+      let u = preprocess_term_ self pacts t in
+      Lit.atom self.tst ~sign u
 
     (* add a clause using [acts] *)
     let add_clause_ self acts lits (proof:dproof) : unit =

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -216,29 +216,37 @@ module Make(A : ARG) : S with module A = A = struct
 
   (* TODO: polarity? *)
   let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
-    let rec get_lit (t:T.t) : Lit.t =
+    Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
+
+    let mk_lit = PA.mk_lit in
+
+    let rec get_lit_opt (t:T.t) : Lit.t option =
       let t_abs, t_sign = T.abs self.tst t in
       let lit_abs =
         match T.Tbl.find self.cnf t_abs with
-        | lit -> lit (* cached *)
+        | lit -> Some lit (* cached *)
         | exception Not_found ->
-          (* compute and cache *)
+          (* compute and cache, if present *)
           let lit = get_lit_uncached si t_abs in
-          if not (T.equal (Lit.term lit) t_abs) then (
+          begin match lit with
-            T.Tbl.add self.cnf t_abs lit;
+            | None -> ()
-            Log.debugf 20
+            | Some lit ->
-              (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
+              if not (T.equal (Lit.term lit) t_abs) then (
-                  Lit.pp lit T.pp t_abs);
+                T.Tbl.add self.cnf t_abs lit;
-          );
+                Log.debugf 20
+                  (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
+                      Lit.pp lit T.pp t_abs);
+              );
+          end;
           lit
       in
 
-      let lit = if t_sign then lit_abs else Lit.neg lit_abs in
+      let lit = if t_sign then lit_abs else CCOpt.map Lit.neg lit_abs in
       lit
 
-    and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t =
+    and equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
-      let a = get_lit t_a in
+      let a = mk_lit t_a in
-      let b = get_lit t_b in
+      let b = mk_lit t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
       let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
 
@@ -266,17 +274,17 @@ module Make(A : ARG) : S with module A = A = struct
       proxy
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
-    and get_lit_uncached si t : Lit.t =
+    and get_lit_uncached si t : Lit.t option =
       match A.view_as_bool t with
-      | B_bool b -> PA.mk_lit (T.bool self.tst b)
+      | B_opaque_bool _ -> None
-      | B_opaque_bool t -> PA.mk_lit t
+      | B_bool b -> Some (PA.mk_lit (T.bool self.tst b))
       | B_not u ->
-        let lit = get_lit u in
+        let lit = get_lit_opt u in
-        Lit.neg lit
+        CCOpt.map Lit.neg lit
 
       | B_and l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map get_lit t_subs in
+        let subs = List.map mk_lit t_subs in
         let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
         SI.with_proof si (SI.P.define_term t_proxy t);
@@ -289,11 +297,11 @@ module Make(A : ARG) : S with module A = A = struct
           t_subs subs;
         PA.add_clause (proxy :: List.map Lit.neg subs)
           (A.lemma_bool_c "and-i" [t_proxy]);
-        proxy
+        Some proxy
 
       | B_or l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map get_lit t_subs in
+        let subs = List.map mk_lit t_subs in
         let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
         SI.with_proof si (SI.P.define_term t_proxy t);
@@ -305,13 +313,13 @@ module Make(A : ARG) : S with module A = A = struct
           t_subs subs;
         PA.add_clause (Lit.neg proxy :: subs)
           (A.lemma_bool_c "or-e" [t_proxy]);
-        proxy
+        Some proxy
 
       | B_imply (t_args, t_u) ->
         (* transform into [¬args \/ u] on the fly *)
         let t_args = Iter.to_list t_args in
-        let args = List.map (fun t -> Lit.neg (get_lit t)) t_args in
+        let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in
-        let u = get_lit t_u in
+        let u = mk_lit t_u in
         let subs = u :: args in
 
         (* now the or-encoding *)
@@ -327,19 +335,22 @@ module Make(A : ARG) : S with module A = A = struct
           (t_u::t_args) subs;
         PA.add_clause (Lit.neg proxy :: subs)
           (A.lemma_bool_c "imp-e" [t_proxy]);
-        proxy
+        Some proxy
 
-      | B_ite _ | B_eq _ | B_neq _ -> PA.mk_lit t
+      | B_ite _ | B_eq _ | B_neq _ -> None
-      | B_equiv (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:false a b
+      | B_equiv (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:false a b)
-      | B_xor  (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:true a b
+      | B_xor  (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:true a b)
-      | B_atom u -> PA.mk_lit u
+      | B_atom _ -> None
     in
 
-    let lit = get_lit t in
+    begin match get_lit_opt t with
-    let u = Lit.term lit in
+      | None -> None
-    (* put sign back as a "not" *)
+      | Some lit ->
-    let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
+        let u = Lit.term lit in
-    if T.equal u t then None else Some u
+        (* put sign back as a "not" *)
+        let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
+        if T.equal u t then None else Some u
+    end
 
   (* check if new terms were added to the congruence closure, that can be turned
      into clauses *)