From 201957ed44ef0206fa714fbd047dcf2c858f58d0 Mon Sep 17 00:00:00 2001 From: Stevendeo Date: Thu, 23 Nov 2023 16:17:39 +0100 Subject: [PATCH] Imperative API (#962) Tackles #899 by making both Sat API imperative. The imperative is made... well, imperative; it still relies on Satml_frontend for properly wrapping calls to Satml. We should be able to merge them, but I choosed not to in this PR to avoid spaghettification. The functional sat now has an imperative frontend upadting a reference to the environment. --- src/bin/common/solving_loop.ml | 11 +- src/bin/js/worker_js.ml | 16 +- src/lib/dune | 2 +- src/lib/frontend/frontend.ml | 154 +++++----- src/lib/frontend/frontend.mli | 14 +- src/lib/reasoners/fun_sat.ml | 2 +- src/lib/reasoners/fun_sat.mli | 35 ++- src/lib/reasoners/fun_sat_frontend.ml | 74 +++++ src/lib/reasoners/fun_sat_frontend.mli | 31 ++ src/lib/reasoners/sat_solver.ml | 2 +- src/lib/reasoners/sat_solver_sig.ml | 14 +- src/lib/reasoners/sat_solver_sig.mli | 14 +- src/lib/reasoners/satml_frontend.ml | 279 ++++++++---------- .../smtlib/testfile-get-info1.dolmen.expected | 2 +- 14 files changed, 382 insertions(+), 268 deletions(-) create mode 100644 src/lib/reasoners/fun_sat_frontend.ml create mode 100644 src/lib/reasoners/fun_sat_frontend.mli diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 8ec88de99..ea8f4b753 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -136,10 +136,10 @@ let main () = Options.Time.set_timeout (Options.get_timelimit ()); end; SAT.reset_refs (); - let ftdn_env = - List.fold_left - (FE.process_decl ~hook_on_status:Frontend.print_status) - (FE.init_env used_context) + let ftdn_env = FE.init_env used_context in + let () = + List.iter + (FE.process_decl ~hook_on_status:Frontend.print_status ftdn_env) cnf in if Options.get_timelimit_per_goal() then @@ -152,8 +152,9 @@ let main () = we have to drop the partial model in order to prevent printing wrong model. *) match ftdn_env.FE.res with - | `Sat partial_model | `Unknown partial_model -> + | `Sat | `Unknown -> begin + let partial_model = ftdn_env.sat_env in let mdl = Model ((module SAT), partial_model) in if Options.(get_interpretation () && get_dump_models ()) then begin let ur = SAT.get_unknown_reason partial_model in diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index b66f946fc..7b6a1c46c 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -124,21 +124,21 @@ let main worker_id content = let used_context = Frontend.choose_used_context all_context ~goal_name in SAT.reset_refs (); let sat_env = SAT.empty_with_inst add_inst in - let ftnd_env = - List.fold_left - (FE.process_decl ~hook_on_status:get_status_and_print) - (FE.init_env ~sat_env used_context) - cnf - in + let ftnd_env = FE.init_env ~sat_env used_context in + List.iter + (FE.process_decl ~hook_on_status:get_status_and_print ftnd_env) + cnf; if Options.get_unsat_core () then begin unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl; end; let () = match ftnd_env.FE.res with - | `Sat partial_model | `Unknown partial_model -> + | `Sat | `Unknown -> begin if Options.(get_interpretation () && get_dump_models ()) then - FE.print_model (Options.Output.get_fmt_models ()) partial_model; + FE.print_model + (Options.Output.get_fmt_models ()) + ftnd_env.sat_env; end | `Unsat -> () in diff --git a/src/lib/dune b/src/lib/dune index 259918818..2d98a19bd 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -39,7 +39,7 @@ Models ; reasoners Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel - Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel + Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index b69d7265c..ecf5ec02e 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -129,20 +129,20 @@ module type S = sig type sat_env type res = [ - | `Sat of sat_env - | `Unknown of sat_env + | `Sat + | `Unknown | `Unsat ] - type env = { + type env = private { used_context : used_context; consistent_dep_stack: (res * Explanation.t) Stack.t; sat_env : sat_env; - res : res; - expl : Explanation.t + mutable res : res; + mutable expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> env + type 'a process = ?loc : Loc.t -> env -> 'a -> unit val init_env : ?sat_env:sat_env -> used_context -> env @@ -162,7 +162,7 @@ module type S = sig ?hook_on_status: (sat_env status -> int -> unit) -> env -> sat_tdecl -> - env + unit val print_model: sat_env Fmt.t end @@ -213,8 +213,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct type sat_env = SAT.t type res = [ - | `Sat of sat_env - | `Unknown of sat_env + | `Sat + | `Unknown | `Unsat ] @@ -222,18 +222,18 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct used_context : used_context; consistent_dep_stack: (res * Explanation.t) Stack.t; sat_env : sat_env; - res : res; - expl : Explanation.t + mutable res : res; + mutable expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> env + type 'a process = ?loc : Loc.t -> env -> 'a -> unit let init_env ?(sat_env=SAT.empty ()) used_context = { used_context; consistent_dep_stack = Stack.create (); sat_env; - res = `Unknown (SAT.empty ()); + res = `Unknown; expl = Explanation.empty } @@ -255,10 +255,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (Ex.print_unsat_core ~tab:false) dep; try let pb = E.Set.elements (Ex.formulas_of dep) in - let env = - List.fold_left - (fun env f -> - SAT.assume env + let satenv = SAT.empty () in + let () = + List.iter + (fun f -> + SAT.assume satenv {E.ff=f; origin_name = ""; gdist = -1; @@ -272,10 +273,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct from_terms = []; theory_elim = true; } Ex.empty - ) (SAT.empty ()) pb + ) + pb in ignore (SAT.unsat - env + satenv {E.ff=E.vrai; origin_name = ""; gdist = -1; @@ -292,76 +294,72 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct Errors.run_error Errors.Failed_check_unsat_core with | SAT.Unsat _ -> () - | (SAT.Sat _ | SAT.I_dont_know _) as e -> raise e + | (SAT.Sat | SAT.I_dont_know) as e -> raise e let mk_root_dep name f loc = if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty - let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : env = + let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : unit = ignore loc; Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack) ~max:n ~elt:(env.res, env.expl) ~init:(); - {env with sat_env = SAT.push env.sat_env n} + SAT.push env.sat_env n - let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : env = + let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : unit = ignore loc; let res, expl = Util.loop ~f:(fun _n () _env -> Stack.pop env.consistent_dep_stack) ~max:n ~elt:() ~init:(env.res, env.expl) in - let sat_env = SAT.pop env.sat_env n in - {env with sat_env; res; expl} + SAT.pop env.sat_env n; + env.res <- res; + env.expl <- expl let internal_assume ?(loc = Loc.dummy) (env : env) ((name, f, mf) : string * E.t * bool) = let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in - if not is_hyp && unused_context name env.used_context then - env - else + if is_hyp || not (unused_context name env.used_context) then let expl = if is_hyp then Ex.empty else mk_root_dep name f loc in - let sat_env = - match env.res with - | `Sat _ | `Unknown _ -> - SAT.assume env.sat_env - {E.ff=f; - origin_name = name; - 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; - } - expl - | `Unsat -> env.sat_env - in - {env with sat_env; expl} + match env.res with + | `Sat | `Unknown -> + SAT.assume env.sat_env + {E.ff=f; + origin_name = name; + 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; + } + expl; + env.expl <- expl; + | `Unsat -> + env.expl <- expl let internal_pred_def ?(loc = Loc.dummy) env (name, f) = - if unused_context name env.used_context then - env - else + if not (unused_context name env.used_context) then let expl = mk_root_dep name f loc in - let sat_env = SAT.pred_def env.sat_env f name expl loc in - {env with sat_env; expl} + SAT.pred_def env.sat_env f name expl loc; + env.expl <- expl let internal_query ?(loc = Loc.dummy) env (n, f, sort) = ignore loc; let expl = match env.res with - | `Sat _ | `Unknown _ -> + | `Sat | `Unknown -> let expl' = SAT.unsat env.sat_env {E.ff=f; origin_name = n; @@ -382,27 +380,29 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct in if get_debug_unsat_core () then check_produced_unsat_core expl; if get_save_used_context () then output_used_context n expl; - {env with res = `Unsat; expl} + env.res <- `Unsat; + env.expl <- expl let internal_th_assume ?(loc = Loc.dummy) env ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) = - if unused_context ax_name env.used_context then - env - else + if not (unused_context ax_name env.used_context) then match env.res with - | `Sat _ | `Unknown _ -> + | `Sat | `Unknown -> let expl = mk_root_dep ax_name ax_form loc in - let sat_env = SAT.assume_th_elt env.sat_env th_elt expl in - {env with sat_env; expl} - | `Unsat -> env + SAT.assume_th_elt env.sat_env th_elt expl; + env.expl <- expl + | `Unsat -> () let handle_sat_exn f ?loc env x = try f ?loc env x with - | SAT.Sat t -> {env with res = `Sat t} - | SAT.Unsat expl -> {env with res = `Unsat; expl = Ex.union expl env.expl} - | SAT.I_dont_know t -> {env with res = `Unknown t} + | SAT.Sat -> env.res <- `Sat + | SAT.Unsat expl -> + env.res <- `Unsat; + env.expl <- Ex.union expl env.expl + | SAT.I_dont_know -> + env.res <- `Unknown (* The SAT.Timeout exception is not catched. *) let push = handle_sat_exn internal_push @@ -427,20 +427,19 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | RwtDef _ -> assert false | Query (n, f, sort) -> begin - let env = internal_query ~loc:d.st_loc env (n, f, sort) in + internal_query ~loc:d.st_loc env (n, f, sort); match env.res with | `Unsat -> - hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()); - env + hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()) | _ -> assert false end | ThAssume th_elt -> internal_th_assume ~loc:d.st_loc env th_elt with - | SAT.Sat t -> + | SAT.Sat -> (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) - hook_on_status (Sat (d,t)) (Steps.get_steps ()); - {env with res = `Sat t} + hook_on_status (Sat (d, env.sat_env)) (Steps.get_steps ()); + env.res <- `Sat | SAT.Unsat expl' -> (* This case should mainly occur when a new assumption results in an unsat @@ -449,20 +448,21 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let expl = Ex.union env.expl expl' in if get_debug_unsat_core () then check_produced_unsat_core expl; (* print_status (Inconsistent d) (Steps.get_steps ()); *) - {env with res = `Unsat; expl} + env.res <- `Unsat; + env.expl <- expl - | SAT.I_dont_know t -> + | SAT.I_dont_know -> (* TODO: always print Unknown for why3 ? *) - let ur = SAT.get_unknown_reason t in + let ur = SAT.get_unknown_reason env.sat_env in let status = match ur with | Some (Sat_solver_sig.Timeout _) -> Timeout (Some d) - | _ -> Unknown (d, t) + | _ -> Unknown (d, env.sat_env) in hook_on_status status (Steps.get_steps ()); (* TODO: Is it an appropriate behaviour? *) (* if timeout != NoTimeout then raise Util.Timeout; *) - {env with res = `Unknown t} + env.res <- `Unknown | Util.Timeout as e -> (* In this case, we obviously want to print the status, diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index b16bd7821..b79fa819a 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -49,17 +49,17 @@ module type S = sig type sat_env type res = [ - | `Sat of sat_env - | `Unknown of sat_env + | `Sat + | `Unknown | `Unsat ] - type env = { + type env = private { used_context : used_context; consistent_dep_stack: (res * Explanation.t) Stack.t; sat_env : sat_env; - res : res; - expl : Explanation.t + mutable res : res; + mutable expl : Explanation.t } val init_env : ?sat_env:sat_env -> used_context -> env @@ -68,7 +68,7 @@ module type S = sig They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the frontend environment, but not the [Timeout] exception which is raised to the user. *) - type 'a process = ?loc:Loc.t -> env -> 'a -> env + type 'a process = ?loc:Loc.t -> env -> 'a -> unit val push : int process @@ -86,7 +86,7 @@ module type S = sig ?hook_on_status:(sat_env status -> int -> unit) -> env -> Commands.sat_tdecl -> - env + unit val print_model: sat_env Fmt.t end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 90c67dcd3..b67c4965f 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -33,7 +33,7 @@ module SE = E.Set module ME = E.Map module Ex = Explanation -module Make (Th : Theory.S) : Sat_solver_sig.S = struct +module Make (Th : Theory.S) = struct module Inst = Instances.Make(Th) module CDCL = Satml_frontend_hybrid.Make(Th) diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index 7cd3ab726..953aaeac1 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/src/lib/reasoners/fun_sat.mli @@ -28,4 +28,37 @@ (* *) (**************************************************************************) -include Sat_solver_sig.SatContainer +(** A functional SAT solver implementation. *) +module Make (Th : Theory.S) : sig + type t + + exception Sat of t + exception Unsat of Explanation.t + exception I_dont_know of t + + val empty : unit -> t + + val empty_with_inst : (Expr.t -> bool) -> t + + val push : t -> int -> t + + val pop : t -> int -> t + + val assume : t -> Expr.gformula -> Explanation.t -> t + + val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t + + val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + + val unsat : t -> Expr.gformula -> Explanation.t + + val reset_refs : unit -> unit + + val reinit_ctx : unit -> unit + + val get_model: t -> Models.t Lazy.t option + + val get_unknown_reason : t -> Sat_solver_sig.unknown_reason option + + val get_value : t -> Expr.t -> Expr.t option +end diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml new file mode 100644 index 000000000..e0a89fe3f --- /dev/null +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -0,0 +1,74 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module Make (Th : Theory.S) : Sat_solver_sig.S = struct + exception Sat + exception Unsat of Explanation.t + exception I_dont_know + + module FS = Fun_sat.Make(Th) + + type t = FS.t ref + + let empty () = ref (FS.empty ()) + + let empty_with_inst f = ref (FS.empty_with_inst f) + + let exn_handler f env = + try f !env with + | FS.Sat e -> env := e; raise Sat + | FS.Unsat expl -> raise (Unsat expl) + | FS.I_dont_know e -> env := e; raise I_dont_know + + let push t i = exn_handler (fun env -> t := FS.push env i) t + + let pop t i = exn_handler (fun env -> t := FS.pop env i) t + + let assume t g expl = exn_handler (fun env -> t := FS.assume env g expl) t + + let assume_th_elt t th expl = + exn_handler (fun env -> t := FS.assume_th_elt env th expl) t + + let pred_def t expr n expl loc = + exn_handler (fun env -> t := FS.pred_def env expr n expl loc) t + + let unsat t g = + exn_handler (fun env -> FS.unsat env g) t + + let reset_refs = FS.reset_refs + + let reinit_ctx = FS.reinit_ctx + + let get_model t = FS.get_model !t + + let get_unknown_reason t = FS.get_unknown_reason !t + + let get_value t expr = FS.get_value !t expr +end diff --git a/src/lib/reasoners/fun_sat_frontend.mli b/src/lib/reasoners/fun_sat_frontend.mli new file mode 100644 index 000000000..7cd3ab726 --- /dev/null +++ b/src/lib/reasoners/fun_sat_frontend.mli @@ -0,0 +1,31 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +include Sat_solver_sig.SatContainer diff --git a/src/lib/reasoners/sat_solver.ml b/src/lib/reasoners/sat_solver.ml index ce12d75b4..8a0ac3884 100644 --- a/src/lib/reasoners/sat_solver.ml +++ b/src/lib/reasoners/sat_solver.ml @@ -34,7 +34,7 @@ let get = function Printer.print_dbg ~module_name:"Sat_solver" "use Tableaux-like solver"; - (module Fun_sat : Sat_solver_sig.SatContainer) + (module Fun_sat_frontend : Sat_solver_sig.SatContainer) | Util.CDCL | Util.CDCL_Tableaux -> if Options.get_verbose () then Printer.print_dbg diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 9caf2c457..5c3559a09 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -54,9 +54,9 @@ let pp_unknown_reason_opt ppf = function module type S = sig type t - exception Sat of t + exception Sat exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know (* the empty sat-solver context *) val empty : unit -> t @@ -67,21 +67,21 @@ module type S = sig assertion level. Ie. assuming e after the push will become g -> e, a g will be forced to be true (but not propagated at level 0) *) - val push : t -> int -> t + val push : t -> int -> unit (** [pop env n] remove an assertion level. Internally, the guard g introduced in the push correponsding to this pop will be propagated to false (at level 0) *) - val pop : t -> int -> t + val pop : t -> int -> unit (* [assume env f] assume a new formula [f] in [env]. Raises Unsat if [f] is unsatisfiable in [env] *) - val assume : t -> Expr.gformula -> Explanation.t -> t + val assume : t -> Expr.gformula -> Explanation.t -> unit - val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t + val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit (* [pred_def env f] assume a new predicate definition [f] in [env]. *) - val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit (* [unsat env f size] checks the unsatisfiability of [f] in [env]. Raises I_dont_know when the proof tree's height reaches diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 4b1b7e703..a8d7a0fdb 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -44,9 +44,9 @@ val pp_unknown_reason_opt : unknown_reason option Fmt.t module type S = sig type t - exception Sat of t + exception Sat exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know (** the empty sat-solver context *) val empty : unit -> t @@ -57,23 +57,23 @@ module type S = sig assertion level. Ie. assuming e after the push will become g -> e, a g will be forced to be true (but not propagated at level 0) *) - val push : t -> int -> t + val push : t -> int -> unit (** [pop env n] remove an assertion level. Internally, the guard g introduced in the push correponsding to this pop will be propagated to false (at level 0) *) - val pop : t -> int -> t + val pop : t -> int -> unit (** [assume env f] assume a new formula [f] in [env]. Raises Unsat if [f] is unsatisfiable in [env] *) - val assume : t -> Expr.gformula -> Explanation.t -> t + val assume : t -> Expr.gformula -> Explanation.t -> unit (** [assume env f exp] assume a new formula [f] with the explanation [exp] in the theories environment of [env]. *) - val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t + val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit (** [pred_def env f] assume a new predicate definition [f] in [env]. *) - val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit (** [unsat env f size] checks the unsatisfiability of [f] in [env]. Raises I_dont_know when the proof tree's height reaches diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index dfa04d6e4..071d5bcaa 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -41,32 +41,32 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reset_refs () = Steps.reset_steps () type guards = { - current_guard: E.t; + mutable current_guard: E.t; stack_guard: E.t Stack.t; } type t = { satml : SAT.t; - ff_hcons_env : FF.hcons_env; - nb_mrounds : int; - last_forced_normal : int; - last_forced_greedy : int; - gamma : (int * FF.t option) ME.t; - conj : (int * SE.t) FF.Map.t; - abstr_of_axs : (FF.t * Atom.atom) ME.t; - axs_of_abstr : (E.t * Atom.atom) ME.t; - proxies : (Atom.atom * Atom.atom list * bool) Util.MI.t; - inst : Inst.t; - skolems : E.gformula ME.t; (* key <-> f *) + mutable ff_hcons_env : FF.hcons_env; + mutable nb_mrounds : int; + mutable last_forced_normal : int; + mutable last_forced_greedy : int; + mutable gamma : (int * FF.t option) ME.t; + mutable conj : (int * SE.t) FF.Map.t; + mutable abstr_of_axs : (FF.t * Atom.atom) ME.t; + mutable axs_of_abstr : (E.t * Atom.atom) ME.t; + mutable proxies : (Atom.atom * Atom.atom list * bool) Util.MI.t; + mutable inst : Inst.t; + mutable skolems : E.gformula ME.t; (* key <-> f *) add_inst : E.t -> bool; guards : guards; - last_saved_model : Models.t Lazy.t option ref; - model_gen_phase : bool ref; - unknown_reason : Sat_solver_sig.unknown_reason option; + mutable last_saved_model : Models.t Lazy.t option; + mutable model_gen_phase : bool; + mutable unknown_reason : Sat_solver_sig.unknown_reason option; (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) - objectives : Th_util.optimized_split Util.MI.t option ref + mutable objectives : Th_util.optimized_split Util.MI.t option } let empty_guards () = { @@ -94,21 +94,22 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct skolems = ME.empty; guards = init_guards (); add_inst = (fun _ -> true); - last_saved_model = ref None; - model_gen_phase = ref false; + last_saved_model = None; + model_gen_phase = false; unknown_reason = None; - objectives = ref None + objectives = None } let empty_with_inst add_inst = { (empty ()) with add_inst = add_inst } - exception Sat of t + exception Sat exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know let i_dont_know env ur = - raise (I_dont_know {env with unknown_reason = Some ur}) + env.unknown_reason <- Some ur; + raise I_dont_know exception IUnsat of t * Explanation.t @@ -421,7 +422,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in let l2 = List.rev_append (List.rev gd2) ngd2 in if Options.get_profiling() then Profiling.instances l2; - (*let env = assume env l2 in*) let gd1, ngd1 = Inst.m_lemmas menv env.inst tbox (selector env) env.nb_mrounds in @@ -448,12 +448,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* dep currently not used. No unsat-cores in satML yet *) Debug.pred_def f; let guard = env.guards.current_guard in - { env with - inst = - Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep } + env.inst <- Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep let axiom_def env gf ex = - {env with inst = Inst.add_lemma env.inst gf ex} + env.inst <- Inst.add_lemma env.inst gf ex let internal_axiom_def ax a at inst = Debug.internal_axiom_def ax a at; @@ -461,7 +459,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let ex = Ex.singleton (Ex.Literal at) in Inst.add_lemma inst gax ex - let register_abstraction (env, new_abstr_vars) (f, (af, at)) = + let register_abstraction env new_abstr_vars (f, (af, at)) = if Options.(get_debug_sat () && get_verbose ()) then Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"register_abstraction" @@ -472,18 +470,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in assert (not (ME.mem f env.abstr_of_axs)); assert (not (ME.mem lat env.axs_of_abstr)); - let env = - if Atom.eq_atom at Atom.vrai_atom || Atom.eq_atom at Atom.faux_atom + let () = + if not (Atom.eq_atom at Atom.vrai_atom || Atom.eq_atom at Atom.faux_atom) then - env - else - { env with - abstr_of_axs = ME.add f (af, at) env.abstr_of_axs; - axs_of_abstr = ME.add lat (f, at) env.axs_of_abstr } + begin + env.abstr_of_axs <- ME.add f (af, at) env.abstr_of_axs; + env.axs_of_abstr <- ME.add lat (f, at) env.axs_of_abstr + end in if Atom.level at = 0 then (* at is necessarily assigned if lvl = 0 *) if Atom.is_true at then - axiom_def env (mk_gf f) Ex.empty, new_abstr_vars + let () = axiom_def env (mk_gf f) Ex.empty in + new_abstr_vars else begin assert (Atom.is_true (Atom.neg at)); assert false (* FF.simplify invariant: should not happen *) @@ -500,7 +498,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let f = E.mk_or lat ded false in let nlat = E.neg lat in (* semantics: nlat ==> f *) - {env with skolems = ME.add nlat (mk_gf f) env.skolems}, + env.skolems <- ME.add nlat (mk_gf f) env.skolems; new_abstr_vars end @@ -741,26 +739,24 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct updated : bool; } - let pre_assume (env, acc) gf = + let pre_assume env acc gf = let { E.ff = f; _ } = gf in if Options.(get_debug_sat () && get_verbose ()) then Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"pre_assume" "Entry of pre_assume: Given %a" E.print f; - if SE.mem f acc.seen_f then env, acc + if SE.mem f acc.seen_f then acc else let acc = {acc with seen_f = SE.add f acc.seen_f} in try let _, ff = ME.find f env.gamma in match ff with - | None -> - env, acc + | None -> + acc [@ocaml.ppwarning "TODO: should be assert failure?"] - | Some ff -> - if SAT.exists_in_lazy_cnf env.satml ff then env, acc + if SAT.exists_in_lazy_cnf env.satml ff then acc else - env, {acc with activate = FF.Map.add ff None acc.activate; updated = true} @@ -772,13 +768,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let _, old_sf = try FF.Map.find ff env.conj with Not_found -> 0, SE.empty in - let env = - {env with - gamma = ME.add f (env.nb_mrounds, None) env.gamma; - conj = FF.Map.add ff (env.nb_mrounds, SE.add f old_sf) env.conj } - in + env.gamma <- ME.add f (env.nb_mrounds, None) env.gamma; + env.conj <- FF.Map.add ff (env.nb_mrounds, SE.add f old_sf) env.conj; (* This assert is not true assert (dec_lvl = 0); *) - axiom_def env gf Ex.empty, {acc with updated = true} + axiom_def env gf Ex.empty; + {acc with updated = true} | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> @@ -791,25 +785,20 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let _, old_sf = try FF.Map.find ff env.conj with Not_found -> 0, SE.empty in - let env = - {env with - gamma = ME.add f (env.nb_mrounds, Some ff) env.gamma; - conj = FF.Map.add ff (env.nb_mrounds, SE.add f old_sf) env.conj } - in + env.gamma <- ME.add f (env.nb_mrounds, Some ff) env.gamma; + env.conj <- FF.Map.add ff (env.nb_mrounds, SE.add f old_sf) env.conj; Debug.simplified_form f ff; - let env, new_abstr_vars = - List.fold_left register_abstraction (env, acc.new_abstr_vars) axs + let new_abstr_vars = + List.fold_left (register_abstraction env) acc.new_abstr_vars axs in let acc = { acc with new_abstr_vars } in - - if FF.equal ff FF.vrai then env, acc + if FF.equal ff FF.vrai then acc else if cnf_is_in_cdcl then (* this means that there exists another E.t that is equivalent to f. These two formulas have the same ff *) - if SAT.exists_in_lazy_cnf env.satml ff then env, acc + if SAT.exists_in_lazy_cnf env.satml ff then acc else - env, {acc with activate = FF.Map.add ff None acc.activate; updated = true} @@ -817,7 +806,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let ff_abstr,new_proxies,proxies_mp, new_vars = FF.cnf_abstr env.ff_hcons_env ff env.proxies acc.new_vars in - let env = {env with proxies = proxies_mp} in + env.proxies <- proxies_mp; let nunit = List.fold_left FF.expand_proxy_defn acc.nunit new_proxies in @@ -830,7 +819,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct updated = true } in - env, acc + acc let cdcl_assume env pending ~dec_lvl = let { seen_f; activate; new_vars; unit; nunit; updated; _ } = pending in @@ -864,7 +853,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Satml.Unsat (lc) -> raise (IUnsat (env, make_explanation lc)) | Satml.Sat -> assert false - let assume_aux_bis ~dec_lvl env l = + let assume_aux_bis ~dec_lvl env l : bool * Atom.atom list = let pending = { seen_f = SE.empty; activate = FF.Map.empty; new_vars = []; unit = []; nunit = []; updated = false; @@ -872,12 +861,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct } in (*fprintf fmt "@.assume aux: %d@." (List.length l);*) - let env, pending = List.fold_left pre_assume (env, pending) l in + let pending = List.fold_left (pre_assume env) pending l in cdcl_assume env pending ~dec_lvl; - env, pending.updated, pending.new_abstr_vars + pending.updated, pending.new_abstr_vars let rec assume_aux ~dec_lvl env l = - let env, updated, new_abstr_vars = assume_aux_bis ~dec_lvl env l in + let updated, new_abstr_vars = assume_aux_bis ~dec_lvl env l in let bot_abstr_vars = (* try to immediately expand newly added skolems *) List.fold_left (fun acc at -> let neg_at = Atom.neg at in @@ -885,13 +874,13 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct )[] new_abstr_vars in match bot_abstr_vars with - | [] -> env, updated + | [] -> updated | _ -> let res = expand_skolems env [] bot_abstr_vars (fun _ -> true) in - if res == [] then env, updated + if res == [] then updated else - let env, updated' = assume_aux ~dec_lvl env res in - env, updated || updated' + let updated' = assume_aux ~dec_lvl env res in + updated || updated' let frugal_mconf () = @@ -939,8 +928,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let l = instantiate_ground_preds env [] sa in let l = expand_skolems env l sa inst_quantif in let l = new_instances mconf env sa inst_quantif l in - let env, updated = assume_aux ~dec_lvl env l in - env, updated + assume_aux ~dec_lvl env l type instantiation_strat = | Auto @@ -953,27 +941,29 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct match inst_strat with | Force_normal -> let mconf = frugal_mconf () in (* take frugal_mconf if normal is forced *) - let env = {env with last_forced_normal = nb_mrounds} in + env.last_forced_normal <- nb_mrounds; let sa, inst_quantif = instantiation_context env ~greedy_round:false ~frugal:false in do_instantiation env sa inst_quantif mconf "normal-inst (forced)" ~dec_lvl | Force_greedy -> let mconf = normal_mconf () in (*take normal_mconf if greedy is forced*) - let env = {env with last_forced_greedy = nb_mrounds} in + env.last_forced_greedy <- nb_mrounds; let sa, inst_quantif = instantiation_context env ~greedy_round:true ~frugal:true in do_instantiation env sa inst_quantif mconf "greedy-inst (forced)" ~dec_lvl | Auto -> List.fold_left - (fun ((env, updated) as acc) (mconf, debug, greedy_round, frugal) -> - if updated then acc + (fun updated (mconf, debug, greedy_round, frugal) -> + if updated then updated + (* TODO: stop here with an exception *) else let sa, inst_quantif = instantiation_context env ~greedy_round ~frugal in do_instantiation env sa inst_quantif mconf debug ~dec_lvl - )(env, false) + ) + false (match Options.get_instantiation_heuristic () with | INormal -> [ frugal_mconf (), "frugal-inst", false, true ; @@ -988,35 +978,32 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let do_case_split env policy = match SAT.do_case_split env.satml policy with - | C_none -> env + | C_none -> () | C_bool _ -> assert false | C_theory expl -> raise (Ex.Inconsistent (expl, [])) let may_update_last_saved_model env compute = let compute = if not (Options.get_first_interpretation ()) then compute - else !(env.last_saved_model) == None + else env.last_saved_model == None in - if not compute then env - else begin + if compute then begin try (* also performs case-split and pushes pending atoms to CS *) let model = Th.compute_concrete_model (SAT.current_tbox env.satml) in - env.last_saved_model := model; - env + env.last_saved_model <- model; with Ex.Inconsistent (_expl, _classes) as e -> raise e - end let update_model_and_return_unknown env compute_model ~unknown_reason = try - let env = may_update_last_saved_model env compute_model in + may_update_last_saved_model env compute_model; Options.Time.unset_timeout (); i_dont_know env unknown_reason (* Timeout -> I_dont_know conversions temporarily disabled https://github.com/OCamlPro/alt-ergo/issues/946 *) - with Util.Timeout when !(env.model_gen_phase) && false -> + with Util.Timeout when env.model_gen_phase && false -> (* In this case, timeout reason becomes 'ModelGen' *) i_dont_know env (Timeout ModelGen) @@ -1091,10 +1078,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct else Expr.Reals.(>) end - let analyze_unknown_for_objectives env unknown_exn unsat_rec_prem : unit = + (* This function is called after receiving an `I_dont_know` exception from + unsat_rec. It may re-raise this exception. *) + let analyze_unknown_for_objectives env unsat_rec_prem : unit = let obj = Th.get_objectives (SAT.current_tbox env.satml) in - if Util.MI.is_empty obj then raise unknown_exn; - env.objectives := Some obj; + if Util.MI.is_empty obj then raise I_dont_know; + env.objectives <- Some obj; let acc = try Util.MI.fold @@ -1116,8 +1105,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* The answer for the first objective is infinity. We stop here as we cannot go beyond infinity and the next objectives with lower priority cannot be optimized in presence of infinity values. *) - raise unknown_exn; - + raise I_dont_know; | (e, tv, is_max, is_le) :: l -> let neg = List.fold_left @@ -1139,7 +1127,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Printer.print_dbg "We assert the formula %a to explore another branch." E.print neg; - let env, updated = assume_aux ~dec_lvl:0 env l in + let updated = assume_aux ~dec_lvl:0 env l in if not updated then begin Printer.print_dbg "env not updated after injection of neg! termination \ @@ -1151,7 +1139,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unsat_rec_prem env ~first_call:false end - let rec unsat_rec env ~first_call:_ : unit = try SAT.solve env.satml; assert false with @@ -1159,17 +1146,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* Timeout -> I_dont_know conversions temporarily disabled https://github.com/OCamlPro/alt-ergo/issues/946 *) (* | Util.Timeout -> model_gen_on_timeout env *) - | Satml.Sat -> try - let env = do_case_split env Util.BeforeMatching in - let env = - may_update_last_saved_model env - (Options.get_every_interpretation ()) - in - let env = {env with nb_mrounds = env.nb_mrounds + 1} - [@ocaml.ppwarning - "TODO: first intantiation a la DfsSAT before searching ..."] + do_case_split env Util.BeforeMatching; + may_update_last_saved_model env (Options.get_every_interpretation ()); + let () = + env.nb_mrounds <- env.nb_mrounds + 1 + [@ocaml.ppwarning + "TODO: first intantiation a la DfsSAT before \ + searching ..."] in if Options.get_profiling() then Profiling.instantiation env.nb_mrounds; let strat = @@ -1180,20 +1165,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in (*let strat = Auto in*) let dec_lvl = SAT.decision_level env.satml in - let env, updated = instantiation env strat dec_lvl in - let env = do_case_split env Util.AfterMatching in - let env, updated = + let updated = instantiation env strat dec_lvl in + do_case_split env Util.AfterMatching; + let updated = if not updated && strat != Auto then instantiation env Auto dec_lvl - else env, updated + else updated in let dec_lvl' = SAT.decision_level env.satml in - let env = + let () = if strat == Auto && dec_lvl' = dec_lvl then (* increase chances of forcing Normal each time Auto instantiation doesn't allow to backjump *) - {env with last_forced_normal = env.last_forced_normal - 1} - else - env + env.last_forced_normal <- env.last_forced_normal - 1 in if not updated then update_model_and_return_unknown @@ -1222,21 +1205,20 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct try unsat_rec env ~first_call with - | I_dont_know env as e -> + | I_dont_know -> begin - try analyze_unknown_for_objectives env e unsat_rec_prem + try analyze_unknown_for_objectives env unsat_rec_prem with | IUnsat (env, _) -> - assert (!(env.objectives) != None); + assert (env.objectives != None); (* objectives is a ref, it's necessiraly updated as a side-effect to best value *) - raise (I_dont_know env) + raise I_dont_know end - | IUnsat (env, _) as e -> - if !(env.objectives) == None then raise e; + if env.objectives == None then raise e; (* TODO: put the correct objectives *) - raise (I_dont_know env) + raise I_dont_know (* copied from sat_solvers.ml *) let max_term_depth_in_sat env = @@ -1277,37 +1259,34 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | _ -> assert false let push env to_push = - Util.loop ~f:(fun _n () acc -> - let expr_guard, atom_guard = create_guard acc in - SAT.push acc.satml atom_guard; - Stack.push expr_guard acc.guards.stack_guard; + Util.loop ~f:(fun _n () () -> + let expr_guard, atom_guard = create_guard env in + SAT.push env.satml atom_guard; + Stack.push expr_guard env.guards.stack_guard; Steps.push_steps (); - {acc with guards = - {acc.guards with - current_guard = expr_guard;} } + env.guards.current_guard <- expr_guard ) ~max:to_push ~elt:() - ~init:env + ~init:() let pop env to_pop = Util.loop - ~f:(fun _n () acc -> - SAT.pop acc.satml; - let guard_to_neg = Stack.pop acc.guards.stack_guard in + ~f:(fun _n () () -> + SAT.pop env.satml; + let guard_to_neg = Stack.pop env.guards.stack_guard in let inst = Inst.pop ~guard:guard_to_neg env.inst in - assert (not (Stack.is_empty acc.guards.stack_guard)); - let b = Stack.top acc.guards.stack_guard in + assert (not (Stack.is_empty env.guards.stack_guard)); + let b = Stack.top env.guards.stack_guard in Steps.pop_steps (); - acc.model_gen_phase := false; - env.last_saved_model := None; - {acc with inst; - guards = - { acc.guards with - current_guard = b;}}) + env.model_gen_phase <- false; + env.last_saved_model <- None; + env.inst <- inst; + env.guards.current_guard <- b + ) ~max:to_pop ~elt:() - ~init:env + ~init:() let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1319,16 +1298,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Debug.unsat gf; (*fprintf fmt "FF.unsat@.";*) (* In dfs_sat goals' terms are added to env.inst *) - let env = - {env with inst = - Inst.add_terms env.inst - (E.max_ground_terms_rec_of_form gf.E.ff) gf} - in + env.inst <- + Inst.add_terms env.inst + (E.max_ground_terms_rec_of_form gf.E.ff) gf; try assert (SAT.decision_level env.satml == 0); - let env, _updated = assume_aux ~dec_lvl:0 env [gf] in + let _updated = assume_aux ~dec_lvl:0 env [gf] in let max_t = max_term_depth_in_sat env in - let env = {env with inst = Inst.register_max_term_depth env.inst max_t} in + env.inst <- Inst.register_max_term_depth env.inst max_t; unsat_rec_prem env ~first_call:true; assert false with @@ -1342,7 +1319,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct )dep true end; dep - | (Util.Timeout | I_dont_know _ ) as e -> raise e + | (Util.Timeout | I_dont_know ) as e -> raise e | e -> Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"unsat" @@ -1352,7 +1329,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let assume env gf _dep = (* dep currently not used. No unsat-cores in satML yet *) assert (SAT.decision_level env.satml == 0); - try fst (assume_aux ~dec_lvl:0 env [add_guard env gf]) + try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) (* Timeout -> I_dont_know conversions temporarily disabled https://github.com/OCamlPro/alt-ergo/issues/946 *) @@ -1367,9 +1344,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct else try Timers.exec_timer_start Timers.M_Sat Timers.F_assume; - let t = assume t ff dep in + assume t ff dep; Timers.exec_timer_pause Timers.M_Sat Timers.F_assume; - t with exn -> Timers.exec_timer_pause Timers.M_Sat Timers.F_assume; raise exn @@ -1387,10 +1363,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct raise exn let assume_th_elt env th_elt dep = - SAT.assume_th_elt env.satml th_elt dep; - env + SAT.assume_th_elt env.satml th_elt dep - let get_model env = !(env.last_saved_model) + let get_model env = env.last_saved_model let get_unknown_reason env = env.unknown_reason diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index 5b23cbed9..97c90a910 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -1,7 +1,7 @@ unknown ( - :steps 8) + :steps 7) unsupported