diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 1dba8541a..2be577eff 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -95,6 +95,47 @@ let enable_maxsmt b = else DStd.Extensions.Smtlib2.(disable maxsmt) +(* Dolmen util *) + +(** Adds the named terms of the term [term] to the map accumulator [acc] *) +let get_named_of_term + (acc : DStd.Expr.term Util.MS.t) + (term : DStd.Expr.term) = + let rec loop acc terms_to_check = + match terms_to_check with + | [] -> acc + | [] :: rest -> loop acc rest + | (term :: tl) :: rest -> + let terms_to_check = tl :: rest in + let terms_to_check = + match term.DStd.Expr.term_descr with + | DStd.Expr.Var _ | Cst _ -> terms_to_check + | App (t, _, tl) -> (t :: tl) :: terms_to_check + | Binder (_b, t) -> + (* TODO: consider catching the terms in the binder *) + [t] :: terms_to_check + | Match (t, plt) -> (t :: (List.map snd plt)) :: terms_to_check + in + match DStd.Expr.Term.get_tag term DStd.Expr.Tags.named with + | None -> loop acc terms_to_check + | Some name -> loop (Util.MS.add name term acc) terms_to_check + in + loop acc [[term]] + +(** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) +let get_named_of_stmt + ~(acc : DStd.Expr.term Util.MS.t) + (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) = + match stmt.contents with + | `Hyp f | `Goal f -> get_named_of_term acc f + | `Clause l -> List.fold_left get_named_of_term acc l + | `Solve (l1, l2) -> + List.fold_left + get_named_of_term + (List.fold_left get_named_of_term acc l1) + l2 + | _ -> acc + (* We currently use the full state of the solver as model. *) type model = Model : 'a sat_module * 'a -> model @@ -297,6 +338,14 @@ let main () = State.create_key ~pipe:"" "optimize" in + let produce_assignment: bool State.key = + State.create_key ~pipe:"" "produce_assignment" + in + + let named_terms: DStd.Expr.term Util.MS.t State.key = + State.create_key ~pipe:"" "named_terms" + in + let debug_parsed_pipe st c = if State.get State.debug st then Format.eprintf "[logic][parsed][%a] @[%a@]@." @@ -409,6 +458,8 @@ let main () = |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key partial_model |> State.set optimize_key (O.get_optimize ()) + |> State.set produce_assignment false + |> State.set named_terms Util.MS.empty |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file |> Parser.init @@ -536,10 +587,18 @@ let main () = solver; st ) + | ":produce-assignments", Symbol { name = Simple b; _ } -> + begin + match bool_of_string_opt b with + | None -> + print_wrn_opt ~name:":verbosity" st_loc "boolean" value; + st + | Some b -> + State.set produce_assignment b st + end | (":global-declarations" | ":interactive-mode" | ":produce-assertions" - | ":produce-assignments" | ":produce-proofs" | ":produce-unsat-assumptions" | ":print-success" @@ -650,6 +709,45 @@ let main () = unsupported_opt name in + (* Fetches the term value in the current model. *) + let evaluate_term get_value name term = + let ae_form = + D_cnf.make_form + name + term + Loc.dummy + ~decl_kind:Expr.Dgoal + in + match get_value ae_form with + | None -> "unknown" (* Not in the standard, but useful for recording when + Alt-Ergo fails to guess the value of a term. *) + | Some v -> Fmt.to_to_string Expr.print v + in + + let print_terms_assignments = + Fmt.list + ~sep:Fmt.cut + (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v) + in + + let handle_get_assignment ~get_value st = + let assignments = + Util.MS.fold + (fun name term acc -> + if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then + (name, evaluate_term get_value name term) :: acc + else + acc + ) + (State.get named_terms st) + [] + in + Printer.print_std + "(@[%a@])@," + print_terms_assignments + assignments + in + let handle_stmt : Frontend.used_context -> State.t -> _ D_loop.Typer_Pipe.stmt -> State.t = @@ -657,6 +755,12 @@ let main () = fun all_context st td -> let file_loc = (State.get State.logic_file st).loc in let solver_ctx = State.get solver_ctx_key st in + let st = + let named_terms_map = + get_named_of_stmt ~acc:(State.get named_terms st) td + in + State.set named_terms named_terms_map st + in match td with (* When the next statement is a goal, the solver is called and provided the goal and the current context *) @@ -763,6 +867,8 @@ let main () = |> State.set partial_model_key None |> State.set solver_ctx_key empty_solver_ctx |> State.set optimize_key (O.get_optimize ()) + |> State.set produce_assignment false + |> State.set named_terms Util.MS.empty | {contents = `Exit; _} -> raise Exit @@ -778,6 +884,26 @@ let main () = handle_get_info st kind; st + | {contents = `Get_assignment; _} -> + begin + match State.get partial_model_key st with + | Some Model ((module SAT), partial_model) -> + if State.get produce_assignment st then + handle_get_assignment + ~get_value:(SAT.get_value partial_model) + st + else + recoverable_error + "Produce assignments disabled; \ + add (set-option :produce-assignments true)"; + st + | None -> + (* TODO: add the location of the statement. *) + recoverable_error + "No model produced, cannot execute get-assignment."; + st + end + | {contents = `Other (custom, args); _} -> handle_custom_statement custom args st diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index 1d32e6414..b835e735f 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -31,6 +31,13 @@ val clear_cache : unit -> unit (** Empties the internal cache of the module. *) +val make_form : + string -> + D_loop.DStd.Expr.term -> + Loc.t -> + decl_kind:Expr.decl_kind -> + Expr.t + val make : D_loop.DStd.Loc.file -> Commands.sat_tdecl list -> diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index c9fa2acdd..9df7efe6a 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1847,6 +1847,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let get_unknown_reason env = env.unknown_reason + let get_value env t = + match E.type_info t with + | Ty.Tbool -> + begin + match ME.find_opt t env.gamma with + | None -> Some E.faux + | Some _ -> Some E.vrai + end + | _ -> None + let reinit_ctx () = (* all_models_sat_env := None; *) (* latest_saved_env := None; diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index f53c0ab22..49da92aab 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -89,6 +89,10 @@ module type S = sig (** [get_unknown_reason t] returns the reason Alt-Ergo raised [I_dont_know] if it did. If it did not, returns None. *) val get_unknown_reason : t -> unknown_reason option + + (** [get_value t e] returns the value of [e] as a constant expression + in the current model generated. Returns [None] if can't decide. *) + val get_value : t -> Expr.t -> Expr.t option end diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 53282e144..90b89b4ca 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -90,6 +90,10 @@ module type S = sig (** [get_unknown_reason t] returns the reason Alt-Ergo raised [I_dont_know] if it did. If it did not, returns None. *) val get_unknown_reason : t -> unknown_reason option + + (** [get_value t e] returns the value of [e] as a constant expression + in the current model generated. Returns [None] if can't decide. *) + val get_value : t -> Expr.t -> Expr.t option end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 4967f4d8d..832229ffd 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1249,6 +1249,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let get_unknown_reason env = env.unknown_reason + let get_value env t = + match E.type_info t with + | Ty.Tbool -> + begin + match ME.find_opt t env.gamma with + | None -> Some E.faux + | Some _ -> Some E.vrai + end + | _ -> None + let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index fb796fd78..fdbe3b2ba 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -52,6 +52,8 @@ module MI = Map.Make(struct type t = int module SI = Set.Make(struct type t = int let compare (x: int) y = Stdlib.compare x y end) +module MS = Map.Make(String) + module SS = Set.Make(String) diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 92458b95f..9a6d6e115 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -36,6 +36,7 @@ exception Not_implemented of string module MI : Map.S with type key = int module SI : Set.S with type elt = int +module MS : Map.S with type key = string module SS : Set.S with type elt = string (** Different values for -case-split-policy option: diff --git a/tests/dune.inc b/tests/dune.inc index 8d0936388..0491f2e6e 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -192910,6 +192910,28 @@ ; Auto-generated part begin (subdir models/bool + (rule + (target bool3.models_tableaux.output) + (deps (:input bool3.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps bool3.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff bool3.models.expected bool3.models_tableaux.output))) (rule (target bool2.models_tableaux.output) (deps (:input bool2.models.smt2)) @@ -204047,6 +204069,69 @@ (package alt-ergo) (action (diff testfile-get-info1.dolmen.expected testfile-get-info1.dolmen_dolmen.output))) + (rule + (target testfile-get-assignment3.dolmen_dolmen.output) + (deps (:input testfile-get-assignment3.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-get-assignment3.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-get-assignment3.dolmen.expected testfile-get-assignment3.dolmen_dolmen.output))) + (rule + (target testfile-get-assignment2.err.dolmen_dolmen.output) + (deps (:input testfile-get-assignment2.err.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 1 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-get-assignment2.err.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-get-assignment2.err.dolmen.expected testfile-get-assignment2.err.dolmen_dolmen.output))) + (rule + (target testfile-get-assignment1.err.dolmen_dolmen.output) + (deps (:input testfile-get-assignment1.err.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 1 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-get-assignment1.err.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-get-assignment1.err.dolmen.expected testfile-get-assignment1.err.dolmen_dolmen.output))) (rule (target testfile-exit_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-exit.smt2)) diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected index 9766bb1d8..3a9def340 100644 --- a/tests/models/bool/bool1.models.expected +++ b/tests/models/bool/bool1.models.expected @@ -3,9 +3,15 @@ unknown ( (define-fun q () Bool false) ) +((notp false) + (notnq true)) + unknown ( (define-fun p () Bool true) (define-fun q () Bool true) ) +((notp false) + (notnq false)) + diff --git a/tests/models/bool/bool1.models.smt2 b/tests/models/bool/bool1.models.smt2 index a7fde5136..d6d90b5a8 100644 --- a/tests/models/bool/bool1.models.smt2 +++ b/tests/models/bool/bool1.models.smt2 @@ -1,10 +1,11 @@ (set-logic QF_UF) (set-option :produce-models true) ; enable model generation +(set-option :produce-assignments true) ; enable get assignment (declare-const p Bool) (declare-const q Bool) ; (declare-const t Int) (define-fun nq () Bool q) -(assert (=> (not p) (not nq))) +(assert (=> (! (not p) :named notp) (! (not nq) :named notnq))) (check-sat) (get-model) (get-assignment) diff --git a/tests/models/bool/bool2.models.expected b/tests/models/bool/bool2.models.expected index 4726de3b1..8ccd511e6 100644 --- a/tests/models/bool/bool2.models.expected +++ b/tests/models/bool/bool2.models.expected @@ -2,3 +2,5 @@ unknown ( ) +((notx false)) + diff --git a/tests/models/bool/bool2.models.smt2 b/tests/models/bool/bool2.models.smt2 index 1b5ae3bbb..30321c945 100644 --- a/tests/models/bool/bool2.models.smt2 +++ b/tests/models/bool/bool2.models.smt2 @@ -1,8 +1,9 @@ (set-logic QF_UF) (set-option :produce-models true) +(set-option :produce-assignments true) (declare-const x Bool) (declare-const y Bool) -(assert (or x (not x))) +(assert (or x (! (not x) :named notx))) (check-sat) (get-model) (get-assignment) diff --git a/tests/models/bool/bool3.models.expected b/tests/models/bool/bool3.models.expected new file mode 100644 index 000000000..341a2df7e --- /dev/null +++ b/tests/models/bool/bool3.models.expected @@ -0,0 +1,9 @@ + +unknown +( + (define-fun x () Bool true) + (define-fun y () Bool true) +) +((foo true) + (bar false)) + diff --git a/tests/models/bool/bool3.models.smt2 b/tests/models/bool/bool3.models.smt2 new file mode 100644 index 000000000..759cd3bb2 --- /dev/null +++ b/tests/models/bool/bool3.models.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-option :produce-assignments true) +(set-option :produce-models true) +(declare-const x Bool) +(declare-const y Bool) +(assert (or (! (and x y) :named foo) (! (and (not x) (not y)) :named bar))) +(check-sat) +(get-model) +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.expected b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected new file mode 100644 index 000000000..6cb130a54 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected @@ -0,0 +1 @@ +(error "No model produced, cannot execute get-assignment.") diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 new file mode 100644 index 000000000..2d8e91c82 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 @@ -0,0 +1,3 @@ +(set-logic ALL) +; The next instruction should fail because we did not generate a model +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.expected b/tests/smtlib/testfile-get-assignment2.err.dolmen.expected new file mode 100644 index 000000000..964245cf0 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment2.err.dolmen.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () Int 0) +) +(error "Produce assignments disabled; add (set-option :produce-assignments true)") diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 new file mode 100644 index 000000000..b5133db07 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(assert (! (= x 0) :named foo)) +(check-sat) +(get-model) +; The next instruction should fail because we did not activate the option +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment3.dolmen.expected b/tests/smtlib/testfile-get-assignment3.dolmen.expected new file mode 100644 index 000000000..a90ec1898 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment3.dolmen.expected @@ -0,0 +1,4 @@ + +unknown +((foo true)) + diff --git a/tests/smtlib/testfile-get-assignment3.dolmen.smt2 b/tests/smtlib/testfile-get-assignment3.dolmen.smt2 new file mode 100644 index 000000000..ad1960cbd --- /dev/null +++ b/tests/smtlib/testfile-get-assignment3.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-assignments true) +(declare-const x Int) +(assert (! (= x 0) :named foo)) +(check-sat) +(get-assignment) \ No newline at end of file