From 1e1bcb5417e2f97433f406c634d14dc2dc2409e3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 24 Aug 2023 10:07:28 +0200 Subject: [PATCH 1/5] Return the right environment --- src/lib/frontend/frontend.ml | 2 +- tests/dune.inc | 20 ++++++++++++++++++++ tests/issues/777.models.expected | 0 tests/issues/777.models.smt2 | 7 +++++++ tests/models/bool/bool1.models.expected | 1 + 5 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 tests/issues/777.models.expected create mode 100644 tests/issues/777.models.smt2 diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 5b7c4b02a..bb6f819f3 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -244,7 +244,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct and not a simple bool. *) print_status (Unknown (d, t)) (Steps.get_steps ()); (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*) - env , consistent, dep + t, consistent, dep | Util.Timeout as e -> (* In this case, we obviously want to print the status, since we exit right after *) diff --git a/tests/dune.inc b/tests/dune.inc index a19c2a508..7660e372c 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -170907,6 +170907,26 @@ ; Auto-generated part begin (subdir issues + (rule + (target 777.models_tableaux.output) + (deps (:input 777.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver Tableaux + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 777.models.expected 777.models_tableaux.output))) (rule (target 696_ci_cdcl_no_minimal_bj.output) (deps (:input 696.ae)) diff --git a/tests/issues/777.models.expected b/tests/issues/777.models.expected new file mode 100644 index 000000000..e69de29bb diff --git a/tests/issues/777.models.smt2 b/tests/issues/777.models.smt2 new file mode 100644 index 000000000..7116c6ba2 --- /dev/null +++ b/tests/issues/777.models.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const i Int) +(define-fun C ((j Int)) Bool (> j 0)) +(assert (C i)) +(check-sat) +(get-model) diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected index 0ccd1ace6..9766bb1d8 100644 --- a/tests/models/bool/bool1.models.expected +++ b/tests/models/bool/bool1.models.expected @@ -1,6 +1,7 @@ unknown ( + (define-fun q () Bool false) ) unknown From 1ae7c7cb6f281efdb3b9c8a66ce031115f887e04 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 24 Aug 2023 10:18:56 +0200 Subject: [PATCH 2/5] Promote tests --- tests/issues/777.models.expected | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/issues/777.models.expected b/tests/issues/777.models.expected index e69de29bb..1a3477493 100644 --- a/tests/issues/777.models.expected +++ b/tests/issues/777.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun i () Int 2) +) From ad9d4f0c505d3011941dddf6f542662721d364c3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Sep 2023 11:26:11 +0200 Subject: [PATCH 3/5] Use an adt to save the results of queries --- src/lib/frontend/frontend.ml | 88 +++++++++++++++++++++-------------- src/lib/frontend/frontend.mli | 13 ++++-- 2 files changed, 62 insertions(+), 39 deletions(-) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index bb6f819f3..4b0436e07 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -39,6 +39,12 @@ module type S = sig type sat_env type used_context + type res = [ + | `Sat of sat_env + | `Unknown of sat_env + | `Unsat + ] + type status = | Unsat of Commands.sat_tdecl * Ex.t | Inconsistent of Commands.sat_tdecl @@ -50,10 +56,10 @@ module type S = sig val process_decl: (status -> int -> unit) -> used_context -> - (bool * Ex.t) Stack.t -> - sat_env * bool * Ex.t -> + (res * Ex.t) Stack.t -> + sat_env * res * Ex.t -> Commands.sat_tdecl -> - sat_env * bool * Ex.t + sat_env * res * Ex.t val print_status : status -> int -> unit @@ -65,9 +71,14 @@ end module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct type sat_env = SAT.t - type used_context = Util.SS.t option + type res = [ + | `Sat of sat_env + | `Unknown of sat_env + | `Unsat + ] + type status = | Unsat of Commands.sat_tdecl * Ex.t | Inconsistent of Commands.sat_tdecl @@ -149,12 +160,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct match d.st_decl with | Push n -> Util.loop ~f:(fun _n env () -> Stack.push env consistent_dep_stack) - ~max:n ~elt:(consistent,dep) ~init:(); + ~max:n ~elt:(consistent, dep) ~init:(); SAT.push env n, consistent, dep | Pop n -> - let consistent,dep = + let consistent, dep = Util.loop ~f:(fun _n () _env -> Stack.pop consistent_dep_stack) - ~max:n ~elt:() ~init:(consistent,dep) + ~max:n ~elt:() ~init:(consistent, dep) in SAT.pop env n, consistent, dep | Assume(n, f, mf) -> @@ -163,23 +174,27 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct acc else let dep = if is_hyp then Ex.empty else mk_root_dep n f d.st_loc in - if consistent then - SAT.assume env - {E.ff=f; - origin_name = n; - gdist = -1; - hdist = (if is_hyp then 0 else -1); - trigger_depth = max_int; - nb_reductions = 0; - age=0; - lem=None; - mf=mf; - gf=false; - from_terms = []; - theory_elim = true; - } dep, - consistent, dep - else env, consistent, dep + begin + match consistent with + | `Sat _ | `Unknown _ -> + SAT.assume env + {E.ff=f; + origin_name = n; + gdist = -1; + hdist = (if is_hyp then 0 else -1); + trigger_depth = max_int; + nb_reductions = 0; + age=0; + lem=None; + mf=mf; + gf=false; + from_terms = []; + theory_elim = true; + } dep, + consistent, dep + | `Unsat -> + env, consistent, dep + end | PredDef (f, name) -> if unused_context name used_context then acc else @@ -190,7 +205,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | Query(n, f, sort) -> let dep = - if consistent then + match consistent with + | `Sat _ | `Unknown _ -> let dep' = SAT.unsat env {E.ff=f; origin_name = n; @@ -206,22 +222,24 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct theory_elim = true; } in Ex.union dep' dep - else dep + | `Unsat -> dep in if get_debug_unsat_core () then check_produced_unsat_core dep; if get_save_used_context () then output_used_context n dep; print_status (Unsat (d, dep)) (Steps.get_steps ()); - env, false, dep + env, `Unsat, dep | ThAssume ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) -> if unused_context ax_name used_context then acc else - if consistent then - let dep = mk_root_dep ax_name ax_form d.st_loc in - let env = SAT.assume_th_elt env th_elt dep in - env, consistent, dep - else env, consistent, dep + match consistent with + | `Sat _ | `Unknown _ -> + let dep = mk_root_dep ax_name ax_form d.st_loc in + let env = SAT.assume_th_elt env th_elt dep in + env, consistent, dep + | `Unsat -> + env, consistent, dep with | SAT.Sat t -> @@ -229,7 +247,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct so we want to print the status in this case. *) print_status (Sat (d,t)) (Steps.get_steps ()); (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*) - env , consistent, dep + env, `Sat t, dep | SAT.Unsat dep' -> (* This case should mainly occur when a new assumption results in an unsat env, in which case we do not want to print status, since the correct @@ -237,14 +255,14 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let dep = Ex.union dep dep' in if get_debug_unsat_core () then check_produced_unsat_core dep; (* print_status (Inconsistent d) (Steps.get_steps ()); *) - env , false, dep + env, `Unsat, dep | SAT.I_dont_know t -> (* In this case, it's not clear whether we want to print the status. Instead, it'd be better to accumulate in `consistent` a 3-case adt and not a simple bool. *) print_status (Unknown (d, t)) (Steps.get_steps ()); (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*) - t, consistent, dep + env, `Unknown t, dep | Util.Timeout as e -> (* In this case, we obviously want to print the status, since we exit right after *) diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index 8a583ac7c..cbdbd3bd1 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -31,9 +31,14 @@ module type S = sig type sat_env - type used_context + type res = [ + | `Sat of sat_env + | `Unknown of sat_env + | `Unsat + ] + type status = | Unsat of Commands.sat_tdecl * Explanation.t | Inconsistent of Commands.sat_tdecl @@ -45,10 +50,10 @@ module type S = sig val process_decl: (status -> int -> unit) -> used_context -> - (bool * Explanation.t) Stack.t -> - sat_env * bool * Explanation.t -> + (res * Explanation.t) Stack.t -> + sat_env * res * Explanation.t -> Commands.sat_tdecl -> - sat_env * bool * Explanation.t + sat_env * res * Explanation.t val print_status : status -> int -> unit From b4501b46b22e11a51ecc2726a6c0e785f24fb116 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Sep 2023 11:32:18 +0200 Subject: [PATCH 4/5] Use an adt to save the results of queries (bis) --- src/bin/common/solving_loop.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 04445bb99..44d67bd5b 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -81,10 +81,10 @@ let main () = Options.Time.set_timeout (Options.get_timelimit ()); end; SAT.reset_refs (); - let partial_model, consistent, _ = + let _, consistent, _ = List.fold_left (FE.process_decl FE.print_status used_context consistent_dep_stack) - (SAT.empty (), true, Explanation.empty) cnf + (SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty) cnf in if Options.get_timelimit_per_goal() then Options.Time.unset_timeout (); @@ -96,9 +96,10 @@ let main () = (* If the status of the SAT environment is inconsistent, we have to drop the partial model in order to prevent printing wrong model. *) - if consistent then + match consistent with + | `Sat partial_model | `Unknown partial_model -> Some partial_model - else None + | `Unsat -> None with Util.Timeout -> if not (Options.get_timelimit_per_goal()) then exit 142; None From cbd5e1b9eb87c6b78bfcc1c152a9d2a5d4ccf498 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Sep 2023 13:28:46 +0200 Subject: [PATCH 5/5] Fix lib_usage and worker_js --- examples/dune | 16 ++++++++++++++++ examples/lib_usage.ml | 19 +++++++++++-------- src/bin/js/worker_js.ml | 3 ++- 3 files changed, 29 insertions(+), 9 deletions(-) create mode 100644 examples/dune diff --git a/examples/dune b/examples/dune new file mode 100644 index 000000000..52d46d10b --- /dev/null +++ b/examples/dune @@ -0,0 +1,16 @@ +(executable + (name Lib_usage) + (libraries AltErgoLib) + (modules Lib_usage) +) + +(rule + (alias runtest) + (action + (ignore-stdout + (ignore-stderr + (run ./Lib_usage.exe) + ) + ) + ) +) diff --git a/examples/lib_usage.ml b/examples/lib_usage.ml index 850158060..762e74199 100644 --- a/examples/lib_usage.ml +++ b/examples/lib_usage.ml @@ -65,7 +65,7 @@ open AltErgoLib module PA = Parsed_interface -let x = PA.mk_var_type Loc.dummy "'a" +let _x = PA.mk_var_type Loc.dummy "'a" let one = PA.mk_int_const Loc.dummy "1" let two = PA.mk_int_const Loc.dummy "2" @@ -80,7 +80,7 @@ let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1) let parsed = [goal_1; goal_2; goal_3] -let typed, env = Typechecker.type_file parsed +let typed, _env = Typechecker.type_file parsed let pbs = Typechecker.split_goals_and_cnf typed @@ -89,16 +89,19 @@ module FE = Frontend.Make(SAT) let () = List.iter - (fun (pb, goal_name) -> + (fun (pb, _goal_name) -> let ctxt = FE.init_all_used_context () in - let acc0 = SAT.empty (), true, Explanation.empty in + let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in let s = Stack.create () in - let _, consistent, ex = + let _env, consistent, _ex = List.fold_left (fun acc d -> FE.process_decl (fun _ _ -> ()) ctxt s acc d - )acc0 pb + ) acc0 pb in - Format.printf "%s@." - (if consistent then "unknown" else "unsat") + match consistent with + | `Sat _ | `Unknown _ -> + Format.printf "unknown" + | `Unsat -> + Format.printf "unsat" )pbs diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 5b3d2939e..b77131464 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -130,11 +130,12 @@ let main worker_id content = let used_context = FE.choose_used_context all_context ~goal_name in let consistent_dep_stack = Stack.create () in SAT.reset_refs (); + let env = SAT.empty_with_inst add_inst in let _,_,dep = List.fold_left (FE.process_decl get_status_and_print used_context consistent_dep_stack) - (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in + (env, `Unknown env, Explanation.empty) cnf in if Options.get_unsat_core () then begin unsat_core := Explanation.get_unsat_core dep;