feat(CDCL): Add ability to decide on semantic literals

src/bin/common/parse_command.ml

@@ -272,7 +272,7 @@ module Debug = struct
            ~doc:full_doc)
 end
 
-let mk_case_split_opt case_split_policy enable_adts_cs max_split
+let mk_case_split_opt case_split_policy enable_adts_cs max_split ()
   =
   let res =
     match case_split_policy with
@@ -577,6 +577,14 @@ let parse_case_split_opt =
     let doc = "Enable case-split for Algebraic Datatypes theory." in
     Arg.(value & flag & info ["enable-adts-cs"] ~docs ~doc) in
 
+  let enable_sat_cs =
+    let doc = "Enable case-split in the SAT solver (Experts only)" in
+    Term.(
+      const set_enable_sat_cs $
+      Arg.(value & flag & info ["enable-sat-cs"] ~docs ~doc)
+    )
+  in
+
   let max_split =
     let dv = Numbers.Q.to_string (get_max_split ()) in
     let doc =
@@ -585,7 +593,7 @@ let parse_case_split_opt =
     Arg.(value & opt string dv & info ["max-split"] ~docv ~docs ~doc) in
 
   Term.(ret (const mk_case_split_opt $
-             case_split_policy $ enable_adts_cs $ max_split))
+             case_split_policy $ enable_adts_cs $ max_split $ enable_sat_cs))
 
 let parse_context_opt =
 

src/lib/dune

@@ -55,7 +55,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap Id Objective
+    Expr Var Ty Typed Xliteral ModelMap Id Objective Literal
     ; util
     Emap Gc_debug Hconsing Hstring Heap Lists Loc
     MyUnix Numbers

src/lib/reasoners/adt_rel.ml

@@ -267,7 +267,7 @@ let deduce_is_constr uf r h eqs env ex =
                 ~module_name:"Adt_rel"
                 ~function_name:"deduce_is_constr"
                 "%a" E.print is_c;
-            (Sig_rel.LTerm is_c, ex, Th_util.Other) :: eqs
+            (Literal.LTerm is_c, ex, Th_util.Other) :: eqs
         in
         begin
           match E.term_view t with
@@ -291,7 +291,7 @@ let deduce_is_constr uf r h eqs env ex =
                 ~module_name:"Adt_rel"
                 ~function_name:"deduce equal to constr"
                 "%a" E.print eq;
-            let eqs = (Sig_rel.LTerm eq, ex, Th_util.Other) :: eqs in
+            let eqs = (Literal.LTerm eq, ex, Th_util.Other) :: eqs in
             env, eqs
           | _ -> env, eqs
         end
@@ -407,7 +407,7 @@ let add_guarded_destr env uf t hs e t_ty =
   let r_e, ex_e = try Uf.find uf e with Not_found -> assert false in
   if trivial_tester r_e c || seen_tester r_e c env then
     {env with pending_deds =
-                (Sig_rel.LTerm eq, ex_e, Th_util.Other) :: env.pending_deds}
+                (Literal.LTerm eq, ex_e, Th_util.Other) :: env.pending_deds}
   else
     let m_e = try MX.find r_e env.selectors with Not_found -> MHs.empty in
     let old = try MHs.find c m_e with Not_found -> [] in
@@ -570,7 +570,7 @@ let assume_is_constr uf hs r dep env eqs =
       let eqs =
         List.fold_left
           (fun eqs (ded, dep') ->
-             (Sig_rel.LTerm ded, Ex.union dep dep', Th_util.Other) :: eqs
+             (Literal.LTerm ded, Ex.union dep dep', Th_util.Other) :: eqs
           )eqs deds
       in
       let env = update_tester r hs env in
@@ -710,7 +710,7 @@ let update_cs_modulo_eq r1 r2 ex env eqs =
                  X.print r2 Hs.print hs;
              List.iter
                (fun (a, dep) ->
-                  eqs := (Sig_rel.LTerm a, dep, Th_util.Other) :: !eqs) l;
+                  eqs := (Literal.LTerm a, dep, Th_util.Other) :: !eqs) l;
            end;
            let l = List.rev_map (fun (a, dep) -> a, Ex.union ex dep) l in
            MHs.add hs l mhs
@@ -791,7 +791,7 @@ let assume env uf la =
     Debug.print_env "after assume" env;
     let print fmt (a,_,_) =
       match a with
-      | Sig_rel.LTerm a -> Format.fprintf fmt "%a" E.print a;
+      | Literal.LTerm a -> Format.fprintf fmt "%a" E.print a;
       | _ -> assert false
     in
     if Options.get_debug_adt () then

src/lib/reasoners/arrays_rel.ml

@@ -426,7 +426,7 @@ let assume env uf la =
   Debug.new_equalities atoms;
   let l =
     Conseq.fold (fun (a,ex) l ->
-        ((Sig_rel.LTerm a, ex, Th_util.Other)::l)) atoms []
+        ((Literal.LTerm a, ex, Th_util.Other)::l)) atoms []
   in
   env, { Sig_rel.assume = l; remove = [] }
 

src/lib/reasoners/bitv_rel.ml

@@ -619,7 +619,7 @@ let assume env uf la =
       raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf)
   in
   let assume =
-    List.rev_map (fun (lit, ex) -> Sig_rel.LSem lit, ex, Th_util.Other) eqs
+    List.rev_map (fun (lit, ex) -> Literal.LSem lit, ex, Th_util.Other) eqs
   in
   let result =
     { result with assume = List.rev_append assume result.assume }

src/lib/reasoners/ccx.ml

@@ -273,7 +273,7 @@ module Main : S = struct
           let ex = List.fold_left2 (explain_equality env) Ex.empty xs1 xs2 in
           let a = E.mk_eq ~iff:false t1 t2 in
           Debug.congruent a ex;
-          Q.push (Sig_rel.LTerm a, ex, Th_util.Other) facts.equas
+          Q.push (Literal.LTerm a, ex, Th_util.Other) facts.equas
         with Exit -> ()
 
   let congruents env (facts: r Sig_rel.facts) t1 s =
@@ -352,7 +352,7 @@ module Main : S = struct
                    | Some (ex_r, _) ->
                      let a = E.mk_distinct ~iff:false [x; y] in
                      Debug.contra_congruence a ex_r;
-                     Q.push (Sig_rel.LTerm a, ex_r, Th_util.Other) facts.diseqs
+                     Q.push (Literal.LTerm a, ex_r, Th_util.Other) facts.diseqs
                    | None -> assert false
                  end
              | _ -> ()
@@ -615,7 +615,7 @@ module Main : S = struct
         | A.Distinct (false, lr) -> assume_dist env facts lr ex
         | A.Distinct (true, _) -> assert false
         | A.Pred _ ->
-          Q.push (Sig_rel.LSem sa, ex, orig) facts.equas;
+          Q.push (Literal.LSem sa, ex, orig) facts.equas;
           env
         | _ -> assert false
       in

src/lib/reasoners/enum_rel.ml

@@ -164,7 +164,7 @@ let add_diseq hss sm1 sm2 dep env eqs =
       if HSS.cardinal enum = 1 then
         let h' = HSS.choose enum in
         env,
-        (Sig_rel.LSem (LR.mkv_eq r (Sh.is_mine (Cons(h',ty)))),
+        (Literal.LSem (LR.mkv_eq r (Sh.is_mine (Cons(h',ty)))),
          ex, Th_util.Other)::eqs
       else env, eqs
 
@@ -177,7 +177,7 @@ let add_diseq hss sm1 sm2 dep env eqs =
         let ex = Ex.union dep ex1 in
         let h' = HSS.choose enum1 in
         let ty = X.type_info r1 in
-        (Sig_rel.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
+        (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
          ex, Th_util.Other)::eqs
       else eqs
     in
@@ -186,7 +186,7 @@ let add_diseq hss sm1 sm2 dep env eqs =
         let ex = Ex.union dep ex2 in
         let h' = HSS.choose enum2 in
         let ty = X.type_info r2 in
-        (Sig_rel.LSem (LR.mkv_eq r2 (Sh.is_mine (Cons(h',ty)))),
+        (Literal.LSem (LR.mkv_eq r2 (Sh.is_mine (Cons(h',ty)))),
          ex, Th_util.Other)::eqs
       else eqs
     in
@@ -226,7 +226,7 @@ let add_eq hss sm1 sm2 dep env eqs =
     if HSS.cardinal diff = 1 then
       let h' = HSS.choose diff in
       let ty = X.type_info r1 in
-      env, (Sig_rel.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
+      env, (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
             ex, Th_util.Other)::eqs
     else env, eqs
 

src/lib/reasoners/fun_sat.ml

@@ -846,9 +846,11 @@ module Make (Th : Theory.S) = struct
                  "%a is not ground" E.print a;
                assert false
              end;
-             let facts = (a, ex, dlvl, plvl) :: facts in
+             let alit = Shostak.Literal.make (LTerm a) in
+             let facts = (alit, Th_util.Other, ex, dlvl, plvl) :: facts in
              let ufacts =
-               if Ex.has_no_bj ex then (a, ex, dlvl, plvl) :: ufacts
+               if Ex.has_no_bj ex then
+                 (alit, Th_util.Other, ex, dlvl, plvl) :: ufacts
                else ufacts
              in
              if not ff.E.mf then begin
@@ -1129,9 +1131,8 @@ module Make (Th : Theory.S) = struct
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
-        let model, _ =
-          Th.compute_concrete_model ~declared_ids:!(env.declare_top) env.tbox
-        in
+        let declared_ids = !(env.declare_top) in
+        let model, _ = Th.extract_concrete_model ~declared_ids env.tbox in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->

src/lib/reasoners/intervalCalculus.ml

@@ -552,7 +552,7 @@ module Debug = struct
   let implied_equalities l =
     if get_debug_fm () then
       let pp_literal ppf = function
-        | Sig_rel.LTerm e -> Expr.print ppf e
+        | Literal.LTerm e -> Expr.print ppf e
         | LSem ra -> LR.print ppf (LR.make ra)
       in
       let print fmt (ra, ex, _) =
@@ -1996,9 +1996,10 @@ let case_split env uf ~for_model =
   | _ -> res
 
 (* Helper function used in [optimizing_objective] to pick a value
-   for the polynomial [p] in its interval. We use this function in the case
-   the value produced by the optimization procedure doesn't satisfy some
-   constraints that involve strict inequalities or the problem is unbounded. *)
+   for the polynomial [p] in its interval. We use this function to split the
+   search space and bias it towards the optimum in the case the value produced
+   by the optimization procedure doesn't satisfy some constraints that involve
+   strict inequalities or the problem is unbounded. *)
 let middle_value env ~is_max ty p bound =
   let interval =
     match MP0.find_opt p env.polynomes, bound with
@@ -2070,11 +2071,16 @@ let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
             Objective.Value.Minfinity
         in
         (* As the problem is unbounded, we need to produce a value for the
-           objective function. In this case, we pick a value in the domain
-           of the polynomial [p]. *)
+           objective function. Rather than picking a value directly, we add a
+           constraint to let the case split mechanism pick a "large" (or
+           "small") value in the interval (otherwise, later objectives are
+           computed while assuming that the middle value is forced, which is
+           incorrect). *)
         let case_split =
-          LR.mkv_eq r1 (middle_value env ~is_max ty p None), true, Th_util.CS
-            (Th_util.Th_arith, Q.one)
+          LR.mkv_builtin false LT
+            [r1; middle_value env ~is_max ty p None],
+          true,
+          Th_util.CS (Th_util.Th_arith, Q.one)
         in
         Some Th_util.{ value; case_split }
 

src/lib/reasoners/ite_rel.ml

@@ -172,7 +172,7 @@ let extract_pending_deductions env =
              ~module_name:"Ite_rel" ~function_name:"assume"
              "deduce that %a with expl %a"
              E.print a Ex.print ex;
-         (Sig_rel.LTerm a, ex, Th_util.Other) :: acc)
+         (Literal.LTerm a, ex, Th_util.Other) :: acc)
       env.pending_deds []
   in
   {env with pending_deds = ME2.empty}, l

src/lib/reasoners/rel_utils.ml

@@ -40,7 +40,7 @@ let assume_nontrivial_eqs
          if SR.mem sa m then acc else e :: eqs, SR.add sa m
       )([], la) eqs
   in
-  List.rev_map (fun (sa, _, ex, orig) -> Sig_rel.LSem sa, ex, orig) eqs
+  List.rev_map (fun (sa, _, ex, orig) -> Literal.LSem sa, ex, orig) eqs
 
 (* The type of delayed functions. A delayed function is given an [Uf.t] instance
    for resolving expressions to semantic values, the operator to compute, and a