From 3fdb07b5339df3d9dffadd17735a23389160be21 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 2 Feb 2022 15:51:44 -0500 Subject: [PATCH] feat: handle get-model/get-value from smtlib inputs --- src/base/Base_types.ml | 7 + src/core/Sidekick_core.ml | 3 + src/lia/Sidekick_arith_lia.ml | 4 +- src/lra/sidekick_arith_lra.ml | 6 +- src/smt-solver/Sidekick_smt_solver.ml | 275 ++++++++++++++------------ src/smtlib/Process.ml | 32 ++- src/smtlib/Typecheck.ml | 6 +- 7 files changed, 192 insertions(+), 141 deletions(-) diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 07ab98a9..5387bdb1 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -328,6 +328,8 @@ type statement = | Stmt_assert of term | Stmt_assert_clause of term list | Stmt_check_sat of (bool * term) list + | Stmt_get_model + | Stmt_get_value of term list | Stmt_exit let[@inline] term_equal_ (a:term) b = a==b @@ -1382,6 +1384,8 @@ module Statement = struct | Stmt_assert of term | Stmt_assert_clause of term list | Stmt_check_sat of (bool * term) list + | Stmt_get_model + | Stmt_get_value of term list | Stmt_exit (** Pretty print a statement *) @@ -1404,5 +1408,8 @@ module Statement = struct | Stmt_exit -> Fmt.string out "(exit)" | Stmt_data l -> Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data.pp) l + | Stmt_get_model -> Fmt.string out "(get-model)" + | Stmt_get_value l -> + Fmt.fprintf out "(@[get-value@ (@[%a@])@])" (Util.pp_list pp_term) l | Stmt_define _ -> assert false (* TODO *) end diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index d31d65a1..7bd2bdd2 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -1238,6 +1238,9 @@ module type SOLVER = sig must stop (returning [Unknown]), [false] if solving can proceed. @param on_exit functions to be run before this returns *) + val last_res : t -> res option + (** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *) + val push_assumption : t -> lit -> unit (** Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by {!pop_assumptions}. *) diff --git a/src/lia/Sidekick_arith_lia.ml b/src/lia/Sidekick_arith_lia.ml index 06cd80b5..b4f4b7a2 100644 --- a/src/lia/Sidekick_arith_lia.ml +++ b/src/lia/Sidekick_arith_lia.ml @@ -90,10 +90,10 @@ module Make(A : ARG) : S with module A = A = struct | LIA_other t when A.has_ty_int t -> SI.declare_pb_is_incomplete si; None - | LIA_const _ | LIA_op _ | LIA_mult _ -> + | LIA_op _ | LIA_mult _ -> SI.declare_pb_is_incomplete si; None (* TODO: theory combination?*) - | LIA_other _ -> + | LIA_const _ | LIA_other _ -> None let create_and_setup si = diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 78b082bc..88235e59 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -244,11 +244,11 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: define proxy *) self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; Log.debugf 50 - (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); + (fun k->k "(@[lra.encode-linexp@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); (* it's actually 0 *) if LE_.Comb.is_empty le_comb then ( - Log.debug 50 "(lra.encode-le.is-trivially-0)"; + Log.debug 50 "(lra.encode-linexp.is-trivially-0)"; SimpSolver.add_constraint self.simplex ~on_propagate:(fun _ ~reason:_ -> ()) (SimpSolver.Constraint.leq proxy A.Q.zero) Tag.By_def; @@ -409,7 +409,7 @@ module Make(A : ARG) : S with module A = A = struct ((A.Q.minus_one, proxy) :: LE_.Comb.to_list le_comb); Log.debugf 50 - (fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])" + (fun k->k "(@[lra.encode-linexp.with-offset@ %a@ :var %a@ :diff-var %a@])" LE_.Comb.pp le_comb T.pp proxy T.pp proxy2); declare_term_to_cc proxy; diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 02f13be9..fdbd3334 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -674,20 +674,7 @@ module Make(A : ARG) (** the parametrized SAT Solver *) module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal) - (* main solver state *) - type t = { - si: Solver_internal.t; - solver: Sat_solver.t; - stat: Stat.t; - proof: P.t; - count_clause: int Stat.counter; - count_solve: int Stat.counter; - (* config: Config.t *) - } - type solver = t - module Registry = Solver_internal.Registry - let[@inline] registry self = Solver_internal.registry self.si module type THEORY = sig type t @@ -700,93 +687,6 @@ module Make(A : ARG) type theory = (module THEORY) type 'a theory_p = (module THEORY with type t = 'a) - (** {2 Main} *) - - let add_theory_p (type a) (self:t) (th:a theory_p) : a = - let (module Th) = th in - Log.debugf 2 - (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name); - let st = Th.create_and_setup self.si in - (* add push/pop to the internal solver *) - begin - let open Solver_internal in - self.si.th_states <- Ths_cons { - st; - push_level=Th.push_level; - pop_levels=Th.pop_levels; - next=self.si.th_states; - }; - end; - st - - let add_theory (self:t) (th:theory) : unit = - let (module Th) = th in - ignore (add_theory_p self (module Th)) - - let add_theory_l self = List.iter (add_theory self) - - (* create a new solver *) - let create ?(stat=Stat.global) ?size ~proof ~theories tst ty_st () : t = - Log.debug 5 "smt-solver.create"; - let si = Solver_internal.create ~stat ~proof tst ty_st () in - let self = { - si; proof; - solver=Sat_solver.create ~proof ?size ~stat si; - stat; - count_clause=Stat.mk_int stat "solver.add-clause"; - count_solve=Stat.mk_int stat "solver.solve"; - } in - add_theory_l self theories; - (* assert [true] and [not false] *) - begin - let tst = Solver_internal.tst self.si in - let t_true = Term.bool tst true in - Sat_solver.add_clause self.solver - [Lit.atom tst t_true] - (P.lemma_true t_true self.proof) - end; - self - - let[@inline] solver self = self.solver - let[@inline] cc self = Solver_internal.cc self.si - let[@inline] stats self = self.stat - let[@inline] tst self = Solver_internal.tst self.si - let[@inline] ty_st self = Solver_internal.ty_st self.si - let[@inline] proof self = self.si.proof - - let preprocess_acts_of_solver_ - (self:t) : (module Solver_internal.PREPROCESS_ACTS) = - (module struct - let proof = self.proof - let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t - let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None - let add_lit ?default_pol lit = - Sat_solver.add_lit self.solver ?default_pol lit - let add_clause c pr = - Sat_solver.add_clause self.solver c pr - end) - - (* preprocess literal *) - let preprocess_lit_ ~steps (self:t) (lit:lit) : lit = - let pacts = preprocess_acts_of_solver_ self in - Solver_internal.preprocess_lit_ ~steps self.si pacts lit - - (* preprocess clause, return new proof *) - let preprocess_clause_ (self:t) - (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step = - let steps = ref [] in - let c = IArray.map (preprocess_lit_ self ~steps) c in - let pr = - P.lemma_rw_clause pr - ~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof - in - c, pr - - (* make a literal from a term, ensuring it is properly preprocessed *) - let mk_lit_t (self:t) ?sign (t:term) : lit = - let pacts = preprocess_acts_of_solver_ self in - Solver_internal.mk_plit self.si pacts ?sign t - (** {2 Result} *) module Unknown = struct @@ -837,6 +737,110 @@ module Make(A : ARG) | Unknown of Unknown.t (** Result of solving for the current set of clauses *) + (* main solver state *) + type t = { + si: Solver_internal.t; + solver: Sat_solver.t; + mutable last_res: res option; + stat: Stat.t; + proof: P.t; + count_clause: int Stat.counter; + count_solve: int Stat.counter; + (* config: Config.t *) + } + type solver = t + + (** {2 Main} *) + + let add_theory_p (type a) (self:t) (th:a theory_p) : a = + let (module Th) = th in + Log.debugf 2 + (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name); + let st = Th.create_and_setup self.si in + (* add push/pop to the internal solver *) + begin + let open Solver_internal in + self.si.th_states <- Ths_cons { + st; + push_level=Th.push_level; + pop_levels=Th.pop_levels; + next=self.si.th_states; + }; + end; + st + + let add_theory (self:t) (th:theory) : unit = + let (module Th) = th in + ignore (add_theory_p self (module Th)) + + let add_theory_l self = List.iter (add_theory self) + + (* create a new solver *) + let create ?(stat=Stat.global) ?size ~proof ~theories tst ty_st () : t = + Log.debug 5 "smt-solver.create"; + let si = Solver_internal.create ~stat ~proof tst ty_st () in + let self = { + si; proof; last_res=None; + solver=Sat_solver.create ~proof ?size ~stat si; + stat; + count_clause=Stat.mk_int stat "solver.add-clause"; + count_solve=Stat.mk_int stat "solver.solve"; + } in + add_theory_l self theories; + (* assert [true] and [not false] *) + begin + let tst = Solver_internal.tst self.si in + let t_true = Term.bool tst true in + Sat_solver.add_clause self.solver + [Lit.atom tst t_true] + (P.lemma_true t_true self.proof) + end; + self + + let[@inline] solver self = self.solver + let[@inline] cc self = Solver_internal.cc self.si + let[@inline] stats self = self.stat + let[@inline] tst self = Solver_internal.tst self.si + let[@inline] ty_st self = Solver_internal.ty_st self.si + let[@inline] proof self = self.si.proof + let[@inline] last_res self = self.last_res + let[@inline] registry self = Solver_internal.registry self.si + + let reset_last_res_ self = self.last_res <- None + + let preprocess_acts_of_solver_ + (self:t) : (module Solver_internal.PREPROCESS_ACTS) = + (module struct + let proof = self.proof + let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t + let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None + let add_lit ?default_pol lit = + Sat_solver.add_lit self.solver ?default_pol lit + let add_clause c pr = + Sat_solver.add_clause self.solver c pr + end) + + (* preprocess literal *) + let preprocess_lit_ ~steps (self:t) (lit:lit) : lit = + let pacts = preprocess_acts_of_solver_ self in + Solver_internal.preprocess_lit_ ~steps self.si pacts lit + + (* preprocess clause, return new proof *) + let preprocess_clause_ (self:t) + (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step = + let steps = ref [] in + let c = IArray.map (preprocess_lit_ self ~steps) c in + let pr = + P.lemma_rw_clause pr + ~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof + in + c, pr + + (* make a literal from a term, ensuring it is properly preprocessed *) + let mk_lit_t (self:t) ?sign (t:term) : lit = + let pacts = preprocess_acts_of_solver_ self in + Solver_internal.mk_plit self.si pacts ?sign t + (** {2 Main} *) let pp_stats out (self:t) : unit = @@ -845,6 +849,7 @@ module Make(A : ARG) (* add [c], without preprocessing its literals *) let add_clause_nopreproc_ (self:t) (c:lit IArray.t) (proof:proof_step) : unit = Stat.incr self.count_clause; + reset_last_res_ self; Log.debugf 50 (fun k-> k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Lit.pp) c); @@ -944,42 +949,51 @@ module Make(A : ARG) in self.si.on_progress <- on_progress; - match - Stat.incr self.count_solve; - Sat_solver.solve ~on_progress ~assumptions (solver self) - with - | Sat_solver.Sat _ when not self.si.complete -> - Log.debugf 1 - (fun k->k "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason incomplete-fragment@])"); - Unknown Unknown.U_incomplete + let res = + match + Stat.incr self.count_solve; + Sat_solver.solve ~on_progress ~assumptions (solver self) + with + | Sat_solver.Sat _ when not self.si.complete -> + Log.debugf 1 + (fun k->k "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason incomplete-fragment@])"); + Unknown Unknown.U_incomplete - | Sat_solver.Sat (module SAT) -> - Log.debug 1 "(sidekick.smt-solver: SAT)"; + | Sat_solver.Sat (module SAT) -> + Log.debug 1 "(sidekick.smt-solver: SAT)"; - Log.debugf 50 - (fun k-> - let ppc out n = - Fmt.fprintf out "{@[class@ %a@]}" (Util.pp_iter N.pp) (N.iter_class n) in - k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" - (Util.pp_iter ppc) (CC.all_classes @@ Solver_internal.cc self.si)); + Log.debugf 50 + (fun k-> + let ppc out n = + Fmt.fprintf out "{@[class@ %a@]}" (Util.pp_iter N.pp) (N.iter_class n) in + k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" + (Util.pp_iter ppc) (CC.all_classes @@ Solver_internal.cc self.si)); - let _lits f = SAT.iter_trail f in - let m = mk_model self _lits in - (* TODO: check model *) - let _ = check in + let _lits f = SAT.iter_trail f in + let m = mk_model self _lits in + (* TODO: check model *) + let _ = check in - do_on_exit (); - Sat m + do_on_exit (); + Sat m - | Sat_solver.Unsat (module UNSAT) -> - let unsat_core () = UNSAT.unsat_assumptions () in - let unsat_proof_step () = Some (UNSAT.unsat_proof()) in - do_on_exit (); - Unsat {unsat_core; unsat_proof_step} - | exception Should_stop -> Unknown Unknown.U_asked_to_stop + | Sat_solver.Unsat (module UNSAT) -> + let unsat_core () = UNSAT.unsat_assumptions () in + let unsat_proof_step () = Some (UNSAT.unsat_proof()) in + do_on_exit (); + Unsat {unsat_core; unsat_proof_step} + | exception Should_stop -> Unknown Unknown.U_asked_to_stop + in + self.last_res <- Some res; + res - let push_assumption self a = Sat_solver.push_assumption self.solver a - let pop_assumptions self n = Sat_solver.pop_assumptions self.solver n + let push_assumption self a = + reset_last_res_ self; + Sat_solver.push_assumption self.solver a + + let pop_assumptions self n = + reset_last_res_ self; + Sat_solver.pop_assumptions self.solver n type propagation_result = | PR_sat @@ -991,6 +1005,7 @@ module Make(A : ARG) } let check_sat_propagations_only ~assumptions self : propagation_result = + reset_last_res_ self; match Sat_solver.check_sat_propagations_only ~assumptions self.solver with diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 2c872f4f..1a03cc66 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -147,7 +147,7 @@ let solve ?(check=false) ?time:_ ?memory:_ ?(progress=false) ~assumptions - s : unit = + s : Solver.res = let t1 = Sys.time() in let on_progress = if progress then Some (mk_progress s) else None in @@ -208,7 +208,8 @@ let solve | Solver.Unknown reas -> Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas - end + end; + res let known_logics = [ "QF_UF"; @@ -260,11 +261,11 @@ let process_stmt (fun (sign,t) -> Solver.mk_lit_t solver ~sign t) l in - solve + ignore (solve ?gc ?restarts ~check ?pp_model ?proof_file ?time ?memory ?progress ~assumptions - solver; + solver : Solver.res); E.return() | Statement.Stmt_ty_decl (id,n) -> decl_sort id n; @@ -300,6 +301,29 @@ let process_stmt Solver.add_clause solver (IArray.of_list c) pr; E.return() + | Statement.Stmt_get_model -> + begin match Solver.last_res solver with + | Some (Solver.Sat m) -> + Fmt.printf "(@[model@ %a@])@." Solver.Model.pp m + | _ -> Error.errorf "cannot access model" + end; + E.return () + + | Statement.Stmt_get_value l -> + begin match Solver.last_res solver with + | Some (Solver.Sat m) -> + let l = List.map + (fun t -> match Solver.Model.eval m t with + | None -> Error.errorf "cannot evaluate %a" Term.pp t + | Some u -> t, u) + l + in + let pp_pair out (t,u) = Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Term.pp u in + Fmt.printf "(@[%a@])@." (Util.pp_list pp_pair) l + | _ -> Error.errorf "cannot access model" + end; + E.return () + | Statement.Stmt_data _ -> E.return() | Statement.Stmt_define _ -> diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index fec13b85..51cc5722 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -573,10 +573,13 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = l in [Stmt.Stmt_check_sat l] + | PA.Stmt_get_model -> [Stmt.Stmt_get_model] + | PA.Stmt_get_value l -> + let l = List.map (conv_term ctx) l in + [Stmt.Stmt_get_value l] | PA.Stmt_get_assertions | PA.Stmt_get_option _ | PA.Stmt_get_info _ - | PA.Stmt_get_model | PA.Stmt_get_proof | PA.Stmt_get_unsat_core | PA.Stmt_get_unsat_assumptions @@ -585,7 +588,6 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = | PA.Stmt_reset_assertions | PA.Stmt_push _ | PA.Stmt_pop _ - | PA.Stmt_get_value _ -> (* TODO: handle more of these *) errorf_ctx ctx "cannot handle statement %a" PA.pp_stmt stmt