From 98c30bf0cc61250c64d37f8c6e99b43038956249 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 14 Feb 2022 10:46:08 -0500 Subject: [PATCH] updates and cleanup --- doc/guide.md | 7 ++- src/cc/Sidekick_cc.ml | 2 +- src/lra/sidekick_arith_lra.ml | 79 ++++++--------------------- src/simplex/sidekick_simplex.ml | 22 ++++---- src/smt-solver/Sidekick_smt_solver.ml | 6 +- src/smtlib/Typecheck.ml | 5 +- 6 files changed, 39 insertions(+), 82 deletions(-) diff --git a/doc/guide.md b/doc/guide.md index 0477788e..c68f50a9 100644 --- a/doc/guide.md +++ b/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 diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index c7790c18..d4c6bf7e 100644 --- a/src/cc/Sidekick_cc.ml +++ b/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) -> diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 25ec7765..141180df 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/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 _ -> () - (* - NOTE: we don't need to do anything for rational subterms, at least + | LRA_op _ | LRA_mult _ -> + (* 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 -> - (* 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_const _n -> () | 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 diff --git a/src/simplex/sidekick_simplex.ml b/src/simplex/sidekick_simplex.ml index 51117896..ea53e28d 100644 --- a/src/simplex/sidekick_simplex.ml +++ b/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 - if not (Q.is_int n) then ( - (* 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); + begin match Subst.eval m x_i.var with + | 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)) - ) + raise (Found (x_i, n)) + + | _ -> () + end ) ); Ok() diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 71a68161..62034103 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/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 = - Lit.atom self.si.tst ?sign t + let mk_lit_t (self:t) ?sign (t:term) : lit = + 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} *) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 9a67a726..c538bb7a 100644 --- a/src/smtlib/Typecheck.ml +++ b/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 = - match T.view t with - | T.LRA _ -> true - | _ -> Ty.equal (T.ty t) (Ty.real()) +let[@inline] is_real t = 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 =