unit,nunit

src/lib/reasoners/satml.ml

@@ -100,12 +100,12 @@ module type SAT_ML = sig
     t ->
     nbv : int -> (* nb made vars *)
     Atom.var list ->
-    Atom.atom list list -> Atom.atom list list ->
-    Atom.atom list list * Atom.atom list list
+    Atom.atom list list ->
+    Atom.atom list list
 
   val assume :
     t ->
-    Atom.atom list list -> Atom.atom list list -> E.t ->
+    Atom.atom list list -> E.t ->
     cnumber : int ->
     FF.Set.t -> dec_lvl:int ->
     unit
@@ -2062,29 +2062,29 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           env all_propagations (ref 0) Auto;
     end
 
-  let new_vars env ~nbv new_v unit_cnf nunit_cnf  =
+  let new_vars env ~nbv new_v cnf =
     match new_v with
-    | [] -> unit_cnf, nunit_cnf
+    | [] -> cnf
     | _ ->
       let tenv0 = env.unit_tenv in
       Vec.grow_to_by_double env.vars nbv;
       Vheap.grow_to_by_double env.order nbv;
       let accu =
         List.fold_left
-          (fun ((unit_cnf, nunit_cnf) as accu) (v : Atom.var) ->
+          (fun cnf (v : Atom.var) ->
              Vec.push env.vars v;
              assert (not (is_semantic v.pa));
              insert_var_order env v;
              match th_entailed tenv0 v.pa with
-             | None -> accu
+             | None -> cnf
              | Some (c, sz) ->
                assert (sz >= 1);
-               if sz = 1 then c :: unit_cnf, nunit_cnf
-               else unit_cnf, c :: nunit_cnf
+               if sz = 1 then c :: cnf
+               else c :: cnf
                     [@ocaml.ppwarning
                       "Issue: BAD decision_level, in particular, \
                        if minimal-bj is ON"]
-          ) (unit_cnf, nunit_cnf) new_v
+          ) cnf new_v
       in
       (* This assert is no longer true because some of the vars in the
          [hcons_env] are now semantic literals.
@@ -2125,19 +2125,18 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       if Options.get_cdcl_tableaux () then
         better_bj env sff
 
-  let assume env unit_cnf nunit_cnf f ~cnumber sff ~dec_lvl =
+  let assume env cnf f ~cnumber sff ~dec_lvl =
     begin
-      match unit_cnf, nunit_cnf with
-      | [], [] -> ()
-      | _, _ ->
+      match cnf with
+      | [] -> ()
+      | _ ->
         let nbc =
-          env.nb_init_clauses + List.length unit_cnf + List.length nunit_cnf in
+          env.nb_init_clauses + List.length cnf in
         Vec.grow_to_by_double env.clauses nbc;
         Vec.grow_to_by_double env.learnts nbc;
         env.nb_init_clauses <- nbc;
 
-        List.iter (add_clause env f ~cnumber) unit_cnf;
-        List.iter (add_clause env f ~cnumber) nunit_cnf;
+        List.iter (add_clause env f ~cnumber) cnf;
 
         if Options.get_verbose () then
           Printer.print_dbg

src/lib/reasoners/satml.mli

@@ -54,13 +54,12 @@ module type SAT_ML = sig
     t ->
     nbv : int -> (* nb made vars *)
     Satml_types.Atom.var list ->
-    Satml_types.Atom.atom list list -> Satml_types.Atom.atom list list ->
-    Satml_types.Atom.atom list list * Satml_types.Atom.atom list list
+    Satml_types.Atom.atom list list ->
+    Satml_types.Atom.atom list list
 
   val assume :
     t ->
     Satml_types.Atom.atom list list ->
-    Satml_types.Atom.atom list list ->
     Expr.t ->
     cnumber : int ->
     Flat_Formula.Set.t -> dec_lvl:int ->

src/lib/reasoners/satml_frontend.ml

@@ -745,8 +745,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     seen_f : SE.t;
     activate : FF.Set.t;
     new_vars : Atom.var list;
-    unit : Atom.atom list list;
-    nunit : Atom.atom list list;
+    cnf : Atom.atom list list;
     new_abstr_vars : Atom.atom list;
     updated : bool;
   }
@@ -818,22 +817,21 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
             let ff_abstr,new_proxies, new_vars =
               FF.cnf_abstr env.ff_hcons_env ff env.proxies acc.new_vars
             in
-            let nunit =
-              List.fold_left FF.expand_proxy_defn acc.nunit new_proxies
+            let cnf =
+              List.fold_left FF.expand_proxy_defn acc.cnf new_proxies
             in
             let acc =
               {acc with
                new_vars;
-               nunit;
-               unit = [ff_abstr] :: acc.unit;
+               cnf = [ff_abstr] :: cnf;
                activate = FF.Set.add ff acc.activate;
                updated = true
               }
             in
             acc
 
   let cdcl_assume' env pending ~dec_lvl =
-    let { seen_f; activate; new_vars; unit; nunit; updated; _ } = pending in
+    let { seen_f; activate; new_vars; cnf; updated; _ } = pending in
     (*
     fprintf fmt "pending : %d distinct forms@." (SE.cardinal seen_f);
     fprintf fmt "pending : %d to activate@." (SFF.cardinal activate);
@@ -845,8 +843,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     if SE.is_empty seen_f then begin
       assert (FF.Set.is_empty activate);
       assert (new_vars == []);
-      assert (unit == []);
-      assert (nunit == []);
+      assert (cnf == []);
       assert (not updated);
     end
     else
@@ -855,17 +852,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
                 [@ocaml.ppwarning "TODO: should fix for unsat cores generation"]
         in
         let nbv = FF.nb_made_vars env.ff_hcons_env in
-        let unit, nunit = SAT.new_vars env.satml ~nbv new_vars unit nunit in
+        let cnf = SAT.new_vars env.satml ~nbv new_vars cnf in
         (*update_lazy_cnf done inside assume at the right place *)
-        SAT.assume env.satml unit nunit f ~cnumber:0 activate ~dec_lvl;
+        SAT.assume env.satml cnf f ~cnumber:0 activate ~dec_lvl;
       with
       | Satml.Unsat (lc) -> raise (IUnsat (env, make_explanation lc))
       | Satml.Sat -> assert false
 
   let assume_aux_bis ~dec_lvl env l : bool * Atom.atom list =
     let pending = {
       seen_f = SE.empty; activate = FF.Set.empty;
-      new_vars = []; unit = []; nunit = []; updated = false;
+      new_vars = []; cnf = []; updated = false;
       new_abstr_vars = [];
     }
     in
@@ -1267,8 +1264,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       let nbv = FF.nb_made_vars env.ff_hcons_env in
       (* Need to use new_vars function to add the new_var corresponding to
          the atom atom_guard in the satml env *)
-      let u, nu = SAT.new_vars env.satml ~nbv new_vars [] [] in
-      assert (u == [] && nu == []);
+      let c = SAT.new_vars env.satml ~nbv new_vars [] in
+      assert (c == []);
       expr_guard, atom_guard
     | _ -> assert false
 

src/lib/reasoners/satml_frontend_hybrid.ml

@@ -158,7 +158,7 @@ module Make (Th : Theory.S) = struct
           try
             let _ =
               SAT.new_vars env.sat ~nbv:(Atom.nb_made_vars env.hcons_env)
-                new_vars [] []
+                new_vars []
             in
             SAT.assume_simple env.sat cnf;
             SAT.assume_simple env.sat pfl;