Merge branch 'wip-fix-lra' into wip-lra-simplex-unsat-core

Makefile

@@ -44,6 +44,9 @@ $(TESTTOOL)-smt-QF_DT: snapshots
 $(TESTTOOL)-smt-QF_LRA: snapshots
 	$(TESTTOOL) run $(TESTOPTS) \
 	  --csv snapshots/smt-QF_LRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_LRA
+$(TESTTOOL)-smt-QF_UFLRA: snapshots
+	$(TESTTOOL) run $(TESTOPTS) \
+	  --csv snapshots/smt-QF_UFLRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_UFLRA
 
 install: build-install
 	@dune install

sidekick-bin.opam

@@ -15,7 +15,7 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter"
   "zarith"
-  "smtlib-utils" { >= "0.1" & < "0.2" }
+  "smtlib-utils" { >= "0.1" & < "0.3" }
   "sidekick" { = version }
   "menhir"
   "msat" { >= "0.8" < "0.9" }

src/arith/base-term/Base_types.ml

@@ -914,6 +914,8 @@ end = struct
     | Eq (a,b) -> C.Eq (a, b)
     | Not u -> C.Not u
     | Ite (a,b,c) -> C.If (a,b,c)
+    | LRA (LRA_pred (Eq, a, b)) ->
+      C.Eq (a,b) (* need congruence closure on this one, for theory combination *)
     | LRA _ -> C.Opaque t (* no congruence here *)
 
   module As_key = struct

src/arith/lra/sidekick_arith_lra.ml

@@ -43,6 +43,9 @@ module type ARG = sig
 
   val ty_lra : S.T.Term.state -> ty
 
+  val has_ty_real : term -> bool
+  (** Does this term have the type [Real] *)
+
   module Gensym : sig
     type t
 
@@ -73,18 +76,37 @@ module Make(A : ARG) : S with module A = A = struct
   module T = A.S.T.Term
   module Lit = A.S.Solver_internal.Lit
   module SI = A.S.Solver_internal
+  module N = A.S.Solver_internal.CC.N
+
+  module Tag = struct
+    type t =
+      | By_def
+      | Lit of Lit.t
+      | CC_eq of N.t * N.t
+
+    let pp out = function
+      | By_def -> Fmt.string out "<bydef>"
+      | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
+      | CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2
+
+    let to_lits si = function
+      | By_def -> []
+      | Lit l -> [l]
+      | CC_eq (n1,n2) ->
+        SI.CC.explain_eq (SI.cc si) n1 n2
+  end
 
   module SimpVar
     : Linear_expr.VAR_GEN
       with type t = A.term
        and type Fresh.t = A.Gensym.t
-       and type lit = Lit.t
+       and type lit = Tag.t
   = struct
     type t = A.term
     let pp = A.S.T.Term.pp
     let compare = A.S.T.Term.compare
-    type lit = Lit.t
-    let pp_lit = Lit.pp
+    type lit = Tag.t
+    let pp_lit = Tag.pp
     module Fresh = struct
       type t = A.Gensym.t
       let copy = A.Gensym.copy
@@ -101,14 +123,17 @@ module Make(A : ARG) : S with module A = A = struct
   module LE = SimpSolver.L.Expr
   module LConstr = SimpSolver.L.Constr
 
+  type proxy = T.t
   type state = {
     tst: T.state;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     neq_encoded: unit T.Tbl.t;
     (* if [a != b] asserted and not in this table, add clause [a = b \/ a<b \/ a>b] *)
-    mutable t_defs: (T.t * LE.t) list; (* term definitions *)
-    pred_defs: (pred * LE.t * LE.t) T.Tbl.t; (* predicate definitions *)
+    needs_th_combination: LE.t T.Tbl.t; (* terms that require theory combination *)
+    t_defs: LE.t T.Tbl.t; (* term definitions *)
+    pred_defs: (pred * LE.t * LE.t * T.t * T.t) T.Tbl.t; (* predicate definitions *)
+    local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *)
   }
 
   let create tst : state =
@@ -116,10 +141,20 @@ module Make(A : ARG) : S with module A = A = struct
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       neq_encoded=T.Tbl.create 16;
-      t_defs=[];
+      needs_th_combination=T.Tbl.create 8;
+      t_defs=T.Tbl.create 8;
       pred_defs=T.Tbl.create 16;
+      local_eqs = Backtrack_stack.create();
     }
 
+  let push_level self =
+    Backtrack_stack.push_level self.local_eqs;
+    ()
+
+  let pop_levels self n =
+    Backtrack_stack.pop_levels self.local_eqs n ~f:(fun _ -> ());
+    ()
+
   (* FIXME
   let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
     let tst = self.tst in
@@ -191,73 +226,118 @@ module Make(A : ARG) : S with module A = A = struct
       LE.( n * t )
     | LRA_const q -> LE.of_const q
 
+  let as_linexp_id = as_linexp ~f:CCFun.id
+
   (* TODO: keep the linexps until they're asserted;
      TODO: but use simplification in preprocess
      *)
 
   (* preprocess linear expressions away *)
-  let preproc_lra self si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
+  let preproc_lra (self:state) si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
     Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
-    let _tst = SI.tst si in
+    let tst = SI.tst si in
     match A.view_as_lra t with
+    | LRA_pred ((Eq|Neq) as pred, t1, t2) ->
+      (* keep equality as is, needed for congruence closure *)
+      let t1 = recurse t1 in
+      let t2 = recurse t2 in
+      let u = A.mk_lra tst (LRA_pred (pred, t1, t2)) in
+      if T.equal t u then None else Some u
     | LRA_pred (pred, t1, t2) ->
       let l1 = as_linexp ~f:recurse t1 in
       let l2 = as_linexp ~f:recurse t2 in
       let proxy = fresh_term self ~pre:"_pred_lra_" Ty.bool in
-      T.Tbl.add self.pred_defs proxy (pred, l1, l2);
+      T.Tbl.add self.pred_defs proxy (pred, l1, l2, t1, t2);
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy pp_pred_def (pred,l1,l2));
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
-      self.t_defs <- (proxy, le) :: self.t_defs;
+      T.Tbl.add self.t_defs proxy le;
+      T.Tbl.add self.needs_th_combination proxy le;
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy LE.pp le);
       Some proxy
+    | LRA_other t when A.has_ty_real t ->
+      let le = LE.monomial1 t in
+      T.Tbl.replace self.needs_th_combination t le;
+      None
     | LRA_const _ | LRA_other _ -> None
 
-  (* partial check: just ensure [a != b] triggers the clause
+  (* ensure that [a != b] triggers the clause
      [a=b \/ a<b \/ a>b] *)
-  let partial_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
+  let encode_neq self si acts trail : unit =
     let tst = self.tst in
     begin
       trail
-      |> Iter.filter (fun lit -> not (Lit.sign lit))
       |> Iter.filter_map
         (fun lit ->
            let t = Lit.term lit in
-           match A.view_as_lra t with
-           | LRA_pred (Eq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
-             Some (lit, a,b)
-           | _ -> None)
+           Log.debugf 50 (fun k->k "@[lra: check lit %a@ :t %a@ :sign %B@]"
+                             Lit.pp lit T.pp t (Lit.sign lit));
+
+           let check_pred pred a b =
+             let pred = if Lit.sign lit then pred else Predicate.neg pred in
+             Log.debugf 50 (fun k->k "pred = `%s`" (Predicate.to_string pred));
+             if pred = Neq && not (T.Tbl.mem self.neq_encoded t) then (
+               Some (lit, a, b)
+             ) else None
+           in
+
+           begin match T.Tbl.find self.pred_defs t with
+             | (pred, _, _, ta, tb) -> check_pred pred ta tb
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) -> check_pred pred a b
+                 | _ -> None
+               end
+           end)
       |> Iter.iter
         (fun (lit,a,b) ->
+           Log.debugf 50 (fun k->k "encode neq in %a" Lit.pp lit);
            let c = [
-             Lit.abs lit;
+             Lit.neg lit;
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, a, b)));
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, b, a)));
            ] in
            SI.add_clause_permanent si acts c;
-           T.Tbl.add self.neq_encoded (Lit.term lit) ();
+           T.Tbl.add self.neq_encoded (Lit.term (Lit.abs lit)) ();
         )
     end
 
+  let dedup_lits lits : _ list =
+    let module LTbl = CCHashtbl.Make(Lit) in
+    let tbl = LTbl.create 16 in
+    List.iter (fun l -> LTbl.replace tbl l ()) lits;
+    LTbl.keys_list tbl
+
+  module Q_map = CCMap.Make(Q)
+
   let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
     let simplex = SimpSolver.create self.gensym in
+    encode_neq self si acts trail;
     (* first, add definitions *)
     begin
-      List.iter
-        (fun (t,le) ->
+      T.Tbl.iter
+        (fun t le ->
            let open LE.Infix in
            let le = le - LE.monomial1 t in
            let c = LConstr.eq0 le in
-           let lit = assert false (* TODO: find the lit *) in
+           let lit = Tag.By_def in
            SimpSolver.add_constr simplex c lit
-           )
+        )
         self.t_defs
     end;
+    (* add congruence closure equalities *)
+    Backtrack_stack.iter self.local_eqs
+      ~f:(fun (n1,n2) ->
+         let t1 = N.term n1 |> as_linexp_id in
+         let t2 = N.term n2 |> as_linexp_id in
+         let c = LConstr.eq0 LE.(t1 -  t2) in
+         let lit = Tag.CC_eq (n1,n2) in
+         SimpSolver.add_constr simplex c lit);
     (* add trail *)
     begin
       trail
@@ -265,26 +345,78 @@ module Make(A : ARG) : S with module A = A = struct
         (fun lit ->
            let sign = Lit.sign lit in
            let t = Lit.term lit in
+           let assert_pred pred a b =
+             let pred = if sign then pred else Predicate.neg pred in
+             if pred = Neq then (
+               Log.debugf 50 (fun k->k "(@[LRA.skip-neq@ :in %a@])" T.pp t);
+             ) else (
+               let c = LConstr.of_expr LE.(a-b) pred in
+               SimpSolver.add_constr simplex c (Tag.Lit lit);
+             )
+           in
            begin match T.Tbl.find self.pred_defs t with
-             | exception Not_found -> ()
-             | (pred, a, b) ->
-               (* FIXME: generic negation+printer in Linear_expr_intf;
-                  actually move predicates to their own module *)
-               let pred = if sign then pred else Predicate.neg pred in
-               if pred = Neq then (
-                 Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
-               ) else (
-                 (* TODO: tag *)
-                 let c = LConstr.of_expr LE.(a-b) pred in
-                 SimpSolver.add_constr simplex c lit;
-               )
+             | (pred, a, b, _, _) -> assert_pred pred a b
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) ->
+                   let a = try T.Tbl.find self.t_defs a with _ -> as_linexp_id a in
+                   let b = try T.Tbl.find self.t_defs b with _ -> as_linexp_id b in
+                   assert_pred pred a b
+                 | _ -> ()
+               end
            end)
     end;
     Log.debug 5 "lra: call arith solver";
     begin match SimpSolver.solve simplex with
       | SimpSolver.Solution _m ->
         Log.debug 5 "lra: solver returns SAT";
-        () (* TODO: get a model + model combination *)
+        Log.debugf 50
+          (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
+              (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
+        (* FIXME: theory combination
+        let lazy model = model in
+        Log.debugf 30 (fun k->k "(@[LRA.model@ %a@])" FM_A.pp_model model);
+
+        (* theory combination: for [t1,t2] terms in [self.needs_th_combination]
+           that have same value, but are not provably equal, push
+           decision [t1=t2] into the SAT solver. *)
+        begin
+          let by_val: T.t list Q_map.t =
+            T.Tbl.to_iter self.needs_th_combination
+            |> Iter.map (fun (t,le) -> FM_A.eval_model model le, t)
+            |> Iter.fold
+              (fun m (q,t) ->
+                 let l = Q_map.get_or ~default:[] q m in
+                 Q_map.add q (t::l) m)
+              Q_map.empty
+          in
+          Q_map.iter
+            (fun _q ts ->
+               begin match ts with
+                 | [] | [_] -> ()
+                 | ts ->
+                   (* several terms! see if they are already equal *)
+                   CCList.diagonal ts
+                   |> List.iter
+                     (fun (t1,t2) ->
+                        Log.debugf 50
+                          (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])"
+                              Q.pp_print _q T.pp t1 T.pp t2);
+                        (* FIXME: we need these equalities to be considered
+                           by the congruence closure *)
+                        if not (SI.cc_are_equal si t1 t2) then (
+                          Log.debug 50 "LRA.th-comb.must-decide-equal";
+                          let t = A.mk_lra (SI.tst si) (LRA_pred (Eq, t1, t2)) in
+                          let lit = SI.mk_lit si acts t in
+                          SI.push_decision si acts lit
+                        )
+                     )
+               end)
+            by_val;
+          ()
+        end;
+           *)
+        ()
       | SimpSolver.Unsatisfiable cert ->
         let unsat_core =
           match SimpSolver.check_cert simplex cert with
@@ -292,9 +424,15 @@ module Make(A : ARG) : S with module A = A = struct
           | _ -> assert false (* some kind of fatal error ? *)
         in
         Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
-                         (Fmt.Dump.list Lit.pp) unsat_core);
+                         (Fmt.Dump.list Tag.pp) unsat_core);
         (* TODO: produce and store a proper LRA resolution proof *)
-        let confl = List.rev_map Lit.neg unsat_core in
+        let confl =
+          unsat_core
+          |> Iter.of_list
+          |> Iter.flat_map_l (fun tag -> Tag.to_lits si tag)
+          |> Iter.map Lit.neg
+          |> Iter.to_rev_list
+        in
         SI.raise_conflict si acts confl SI.P.default
     end;
     ()
@@ -304,8 +442,12 @@ module Make(A : ARG) : S with module A = A = struct
     let st = create (SI.tst si) in
     (* TODO    SI.add_simplifier si (simplify st); *)
     SI.add_preprocess si (preproc_lra st);
-    SI.on_partial_check si (partial_check_ st);
     SI.on_final_check si (final_check_ st);
+    SI.on_cc_post_merge si
+      (fun _ _ n1 n2 ->
+         if A.has_ty_real (N.term n1) then (
+           Backtrack_stack.push st.local_eqs (n1, n2)
+         ));
     (*     SI.add_preprocess si (cnf st); *)
     (* TODO: theory combination *)
     st
@@ -313,6 +455,6 @@ module Make(A : ARG) : S with module A = A = struct
   let theory =
     A.S.mk_theory
       ~name:"th-lra"
-      ~create_and_setup
+      ~create_and_setup ~push_level ~pop_levels
       ()
 end

src/cc/Sidekick_cc.ml

@@ -835,6 +835,10 @@ module Make (A: CC_ARG)
   let[@inline] merge_t cc t1 t2 expl =
     merge cc (add_term cc t1) (add_term cc t2) expl
 
+  let explain_eq cc n1 n2 : lit list =
+    let th = ref true in
+    explain_pair cc ~th [] n1 n2
+
   let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
   let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge
   let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term

src/core/Sidekick_core.ml

@@ -280,6 +280,10 @@ module type CC_S = sig
   val assert_lits : t -> lit Iter.t -> unit
   (** Addition of many literals *)
 
+  val explain_eq : t -> N.t -> N.t -> lit list
+  (** Explain why the two nodes are equal.
+      Fails if they are not, in an unspecified way *)
+
   val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
   (** Raise a conflict with the given explanation
       it must be a theory tautology that [expl ==> absurd].
@@ -390,10 +394,19 @@ module type SOLVER_INTERNAL = sig
   (** {3 hooks for the theory} *)
 
   val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
+  (** Propagate a literal for a reason. This is similar to asserting
+      the clause [reason => lit], but more lightweight, and in a way
+      that is backtrackable. *)
 
   val raise_conflict : t -> actions -> lit list -> proof -> 'a
   (** Give a conflict clause to the solver *)
 
+  val push_decision : t -> actions -> lit -> unit
+  (** Ask the SAT solver to decide the given literal in an extension of the
+      current trail. This is useful for theory combination.
+      If the SAT solver backtracks, this (potential) decision is removed
+      and forgotten. *)
+
   val propagate: t -> actions -> lit -> (unit -> lit list) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
@@ -429,6 +442,9 @@ module type SOLVER_INTERNAL = sig
   val cc_find : t -> CC.N.t -> CC.N.t
   (** Find representative of the node *)
 
+  val cc_are_equal : t -> term -> term -> bool
+  (** Are these two terms equal in the congruence closure? *)
+
   val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].

src/main/main.ml

@@ -78,6 +78,7 @@ let argspec = Arg.align [
     "--no-p", Arg.Clear p_progress, " no progress bar";
     "--size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
     "--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
+    "-t", Arg.String (int_arg time_limit), " short for --time";
     "--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit";
     "-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
     "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";

src/msat-solver/Sidekick_msat_solver.ml

@@ -202,6 +202,10 @@ module Make(A : ARG)
 
     let add_preprocess self f = self.preprocess <- f :: self.preprocess
 
+    let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
+      let sign = Lit.sign lit in
+      acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
+
     let[@inline] raise_conflict self acts c : 'a =
       Stat.incr self.count_conflict;
       acts.Msat.acts_raise_conflict c P.default
@@ -279,6 +283,10 @@ module Make(A : ARG)
 
     let cc_add_term self t = CC.add_term (cc self) t
     let cc_find self n = CC.find (cc self) n
+    let cc_are_equal self t1 t2 =
+      let n1 = cc_add_term self t1 in
+      let n2 = cc_add_term self t2 in
+      N.equal (cc_find self n1) (cc_find self n2)
     let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
     let cc_merge_t self acts t1 t2 e =
       cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e
@@ -578,7 +586,7 @@ module Make(A : ARG)
 
   let add_clause (self:t) (c:Atom.t IArray.t) : unit =
     Stat.incr self.count_clause;
-    Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c);
+    Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c);
     Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default
 
   let add_clause_l self c = add_clause self (IArray.of_list c)

src/smtlib/Process.ml

@@ -315,6 +315,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
     | _ -> LRA_other t
 
   let ty_lra _st = Ty.real
+  let has_ty_real t = Ty.equal (T.ty t) Ty.real
 
   module Gensym = struct
     type t = {

src/smtlib/Typecheck.ml

@@ -280,6 +280,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
       | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
       | PA.Add, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l
+      | PA.Minus, [a] ->
+        begin match t_as_q a with
+          | Some a -> T.lra ctx.tst (LRA_const (Q.neg a))
+          | None ->
+            T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a))
+        end
       | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
       | PA.Minus, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l

src/util/Backtrack_stack.ml

@@ -34,3 +34,5 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
     done;
     Vec.shrink self.lvls new_lvl
   )
+
+let iter ~f self = Vec.iter f self.vec

src/util/Backtrack_stack.mli

@@ -19,3 +19,5 @@ val push_level : _ t -> unit
 
 val pop_levels : 'a t -> int -> f:('a -> unit) -> unit
 (** [pop_levels st n ~f] removes [n] levels, calling [f] on every removed item *)
+
+val iter : f:('a -> unit) -> 'a t -> unit