updates and cleanup

doc/guide.md

@@ -329,7 +329,7 @@ val b : Term.t = b
 # Term.ty a;;
 - : Ty.t = Real
 
-# let a_leq_b = Term.LRA.(leq tstore (var tstore a) (var tstore b));;
+# let a_leq_b = Term.LRA.(leq tstore a b);;
 val a_leq_b : Term.t = (<= a b)
 ```
 
@@ -367,7 +367,10 @@ val res : Solver.res =
 
 This just showed that `a=1, b=1/2, a>=b` is unsatisfiable.
 The junk assumption `p` was not used during the proof
-and therefore doesn't appear in the unsat core we extract from `res`.
+and therefore doesn't appear in the unsat core we extract from `res`;
+the assertion `a<=b` isn't in the core either because it was asserted
+using `(assert …)` rather than passed as a local assumption,
+so it's "background" knowledge.
 
 ## Functions and congruence closure
 

src/cc/Sidekick_cc.ml

@@ -679,7 +679,7 @@ module Make (A: CC_ARG)
         if same_class a b then (
           let expl = Expl.mk_merge a b in
           Log.debugf 5
-            (fun k->k "(@[pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b);
+            (fun k->k "(@[cc.pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b);
           merge_classes cc n (n_true cc) expl
         )
       | Some (Not u) ->

src/lra/sidekick_arith_lra.ml

@@ -460,70 +460,15 @@ module Make(A : ARG) : S with module A = A = struct
       Log.debugf 50 (fun k->k "(@[lra.preproc@ :t %a@ :to-constr %a@])"
                         T.pp t SimpSolver.Constraint.pp constr);
 
-    | LRA_op _ | LRA_mult _ -> ()
+    | LRA_op _ | LRA_mult _ ->
-      (*
+      (* NOTE: we don't need to do anything for rational subterms, at least
-      NOTE: we don't need to do anything for rational subterms, at least
          not at first. Only when theory combination mandates we compare
          two terms (by deciding [t1 = t2]) do they impact the simplex; and
-         then they're moved into an equation, which means
+         then they're moved into an equation, which means they are
-
+         preprocessed in the LRA_pred case above. *)
-      let le = as_linexp t in
-
-      (* [t] is [le_comb + le_const], where [le_comb] is a linear expression
-         without constant. *)
-      let le_comb, le_const = LE.comb le, LE.const le in
-      LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
-
-      if A.Q.(le_const = zero) then (
-        (* if there is no constant, define [t] as [t := le_comb] *)
-        declare_term_to_cc ~sub:false t;
-        SimpSolver.define self.simplex t (LE_.Comb.to_list le_comb);
-
-      ) else (
-        (* a bit more complicated: we cannot just define [t := le_comb]
-           because of the coefficient, and the simplex doesn't like offsets.
-
-           Instead we assert [t := le_comb + proxy2] using a secondary
-           variable [proxy2], and assert [proxy2 = le_const] in
-           the simplex *)
-
-        let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
-
-        SimpSolver.add_var self.simplex proxy2;
-        LE_.Comb.iter (fun v _ ->
-            declare_term_to_cc ~sub:true v;
-            SimpSolver.add_var self.simplex v;
-          ) le_comb;
-        SimpSolver.define self.simplex t
-          ((A.Q.one, proxy2) :: LE_.Comb.to_list le_comb);
-
-        Log.debugf 50
-          (fun k->k "(@[lra.encode-linexp.with-offset@ `@[%a@]`@ :var %a@ :const-var %a@])"
-              LE_.Comb.pp le_comb T.pp t T.pp proxy2);
-
-        declare_term_to_cc ~sub:false t;
-        declare_term_to_cc ~sub:true proxy2;
-
-        (* can only work at level 0 *)
-        assert (Backtrack_stack.n_levels self.local_eqs = 0);
-        SimpSolver.declare_bound self.simplex
-          (SimpSolver.Constraint.mk proxy2 Leq le_const) Tag.By_def;
-        SimpSolver.declare_bound self.simplex
-          (SimpSolver.Constraint.mk proxy2 Geq le_const) Tag.By_def;
-
       ()
-      )
-      *)
 
-    | LRA_const n ->
+    | LRA_const _n -> ()
-      (* add to simplex, make sure it's always itself *)
-      SimpSolver.add_var self.simplex t;
-
-      assert (n_levels self=0); (* otherwise this will be backtracked but not re-done *)
-      SimpSolver.declare_bound self.simplex
-        (SimpSolver.Constraint.mk t Leq n) Tag.By_def;
-      SimpSolver.declare_bound self.simplex
-        (SimpSolver.Constraint.mk t Geq n) Tag.By_def;
 
     | LRA_other t when A.has_ty_real t -> ()
     | LRA_other _ ->
@@ -683,6 +628,11 @@ module Make(A : ARG) : S with module A = A = struct
             (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
     );
 
+    let eval_in_subst_ subst t = match A.view_as_lra t with
+      | LRA_const n -> n
+      | _ -> Subst.eval subst t |> CCOpt.get_or ~default:A.Q.zero
+    in
+
     let n = ref 0 in
     (* theory combination: for [t1,t2] terms in [self.needs_th_combination]
        that have same value, but are not provably equal, push
@@ -690,7 +640,7 @@ module Make(A : ARG) : S with module A = A = struct
     begin
       let by_val: T.t list Q_map.t =
         T.Tbl.keys self.needs_th_combination
-        |> Iter.map (fun t -> Subst.eval subst t, t)
+        |> Iter.map (fun t -> eval_in_subst_ subst t, t)
         |> Iter.fold
           (fun m (q,t) ->
              let l = Q_map.get_or ~default:[] q m in
@@ -816,7 +766,10 @@ module Make(A : ARG) : S with module A = A = struct
     begin match self.last_res with
       | Some (SimpSolver.Sat m) ->
         Log.debugf 50 (fun k->k "(@[lra.model-ask@ %a@])" T.pp t);
-        SimpSolver.V_map.get t m |> CCOpt.map (t_const self)
+        begin match A.view_as_lra t with
+          | LRA_const n -> Some n (* always eval constants to themselves *)
+          | _ -> SimpSolver.V_map.get t m
+        end |> CCOpt.map (t_const self)
       | _ -> None
     end
 

src/simplex/sidekick_simplex.ml

@@ -73,7 +73,7 @@ module type S = sig
 
   module Subst : sig
     type t = num V_map.t
-    val eval : t -> V.t -> Q.t
+    val eval : t -> V.t -> Q.t option
     val pp : t Fmt.printer
     val to_string : t -> string
   end
@@ -210,7 +210,7 @@ module Make(Arg: ARG)
 
   module Subst = struct
     type t = num V_map.t
-    let eval self t = try V_map.find t self with Not_found -> Q.zero
+    let eval self t = V_map.get t self
     let pp out (self:t) : unit =
       let pp_pair out (v,n) =
         Fmt.fprintf out "(@[%a := %a@])" V.pp v pp_q_dbg n in
@@ -1170,15 +1170,17 @@ module Make(Arg: ARG)
         Matrix.iter_rows self.matrix
           (fun _i x_i ->
              if x_i.is_int then (
-               let n = Subst.eval m x_i.var in
+               begin match Subst.eval m x_i.var with
-               if not (Q.is_int n) then (
+                 | Some n when not (Q.is_int n) ->
                    (* found one! *)
                    Log.debugf 10
                      (fun k->k "(@[simplex.int-var-assigned-to-non-int@ %a := %a@])"
                          Var_state.pp x_i Q.pp n);
 
                    raise (Found (x_i, n))
-               )
+
+                 | _ -> ()
+               end
              )
           );
         Ok()

src/smt-solver/Sidekick_smt_solver.ml

@@ -787,8 +787,10 @@ module Make(A : ARG)
       (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
     Solver_internal.preprocess_clause_iarray_ self.si c pr
 
-  let[@inline] mk_lit_t (self:t) ?sign (t:term) : lit =
+  let mk_lit_t (self:t) ?sign (t:term) : lit =
-    Lit.atom self.si.tst ?sign t
+    let lit = Lit.atom self.si.tst ?sign t in
+    let lit, _ = Solver_internal.simplify_and_preproc_lit_ self.si lit in
+    lit
 
   (** {2 Main} *)
 

src/smtlib/Typecheck.ml

@@ -127,10 +127,7 @@ let t_as_z t = match Term.view t with
   | T.LIA (Const n) -> Some n
   | _ -> None
 
-let is_real t =
+let[@inline] is_real t = Ty.equal (T.ty t) (Ty.real())
-  match T.view t with
-  | T.LRA _ -> true
-  | _ -> Ty.equal (T.ty t) (Ty.real())
 
 (* convert [t] to a real term *)
 let cast_to_real (ctx:Ctx.t) (t:T.t) : T.t =