From f83c60ef61c8939911edbc5776dc71dfe25143a7 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 11 Feb 2025 11:40:03 +0100 Subject: [PATCH 1/2] Fix issue 1023 --- src/lib/reasoners/satml_frontend.ml | 390 ++++++++++++--------- tests/smtlib/testfile-get-assignment3.smt2 | 2 +- 2 files changed, 218 insertions(+), 174 deletions(-) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 773efe1a2d..8fda3820ce 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -42,6 +42,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reset_refs () = Steps.reset_steps () + type 'a atom = { + lit: 'a; + neg: 'a; + } + type guards = { mutable current_guard: E.t; stack_guard: E.t Stack.t; @@ -64,6 +69,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct guards : guards; mutable last_saved_model : Models.t Lazy.t option; mutable last_saved_objectives : Objective.Model.t option; + mutable last_saved_bmodel : Shostak.Literal.t atom list option; + (** The boolean model saved in this field is intented for use by + [get_value]. This field can be updated in two situations: + - Just before returning [I_dont_know] in the [unsat_rec] function, it + is updated with the current boolean model of [env.satml]. + - After encountering a contradiction in [optimize_models], it is + updated with the lastest consistent boolean model produced by + SatML. This model must be consistent with the boolean model of + [env.satml] but it may be a strict extension of it. *) + mutable unknown_reason : Sat_solver_sig.unknown_reason option; (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) @@ -75,6 +90,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct stack is never empty. *) } + (* Helper function that produces an independent copy of the current boolean + model of [env.satml]. *) + let capture_bmodel env = + List.map + (fun Atom.{ lit; neg = { lit = nlit; _ }; _ } -> + { lit; neg = nlit } + ) (SAT.boolean_model env.satml) + let empty_guards () = { current_guard = Expr.vrai; stack_guard = Stack.create (); @@ -103,6 +126,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct add_inst = selector; last_saved_model = None; last_saved_objectives = None; + last_saved_bmodel = None; unknown_reason = None; declare_top = []; declare_tail = Stack.create (); @@ -116,7 +140,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct env.unknown_reason <- Some ur; raise I_dont_know - exception IUnsat of t * Explanation.t + exception IUnsat of Explanation.t let mk_gf f = { E.ff = f; @@ -860,7 +884,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (*update_lazy_cnf done inside assume at the right place *) SAT.assume env.satml unit nunit f ~cnumber:0 activate ~dec_lvl; with - | Satml.Unsat (lc) -> raise (IUnsat (env, make_explanation lc)) + | Satml.Unsat lc -> raise (IUnsat (make_explanation lc)) | Satml.Sat -> assert false let assume_aux_bis ~dec_lvl env l : bool * Atom.atom list = @@ -1009,151 +1033,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in env.last_saved_model <- Some model; env.last_saved_objectives <- Some objectives; + env.last_saved_bmodel <- Some (capture_bmodel env); with | Ex.Inconsistent (_expl, _classes) as e -> raise e | Util.Timeout -> i_dont_know env (Timeout ModelGen) - exception Give_up of (E.t * E.t * bool * bool) list - - (* Getting [unknown] after a query can mean two things: - - The problem is [unsat] but we didn't manage to find a contradiction; - - We produce a model of the formulas. - - In the latter case, we optimized our objective functions during the - exploration of this branch of the SAT solver. It doesn't mean there is no - other branch of the SAT solver in which all the formulas are satisfiable - and the objective functions have bigger values in some models of this - branch. - - For instance, consider the SMT-LIB problem: - (declare-const x Int) - (assert (or (<= x 2) (<= x 4))) - (assert (or (<= y 3)) - (maximize x) - (maximize y) - (check-sat) - (get-model) - - Assume that the solver explores the first branch (<= x 2) of the or gate: - (or (<= x 2) (<= x 4)). - - Let's imagine it discovers that [0] is a model of the first formula. After - optimization, it find that [2] is the best model for [x] and [3] is the - best model for [y] it can got in this branch. Still we have to explore - the second branch [(<= x 4)] to realize that [4] is actually the best - model for [x]. - - The following function ensures to explore adequate branches of the SAT - solver in order to get the best model, if the problem is SAT. - - In our running example, after getting the model [2], the below function - run again the SAT solver with the extra assert: - (assert (or (> x 2) (and (= x 2) (> y 3))) - - If this run produces the answer [unsat], we know that [2] was the best - model value for [x]. Otherwise, we got a better value for [x]. *) - - type ty_op = - { lt : E.t -> E.t -> E.t - ; le : E.t -> E.t -> E.t } - - let real_op = { lt = Expr.Reals.(<) ; le = Expr.Reals.(<=) } - - let int_op = { lt = Expr.Ints.(<) ; le = Expr.Reals.(<=) } - - let bitv_unsigned_op = { lt = Expr.BV.bvult ; le = Expr.BV.bvule } - - let mk_le { le ; _ } = le - - let mk_lt { lt ; _ } = lt - - let mk_ge { le ; _ } x y = le y x - - let mk_gt { lt ; _ } x y = lt y x - - let op ty is_max is_le = - let ty_op = - match ty with - | Ty.Treal -> real_op - | Tint -> int_op - | Tbitv _ -> bitv_unsigned_op - | _ -> Fmt.invalid_arg "cannot optimize for type: %a" Ty.print ty - in - if is_max then begin - if is_le then mk_le ty_op - else mk_lt ty_op - end - else begin - if is_le then mk_ge ty_op - else mk_gt ty_op - end - - (* 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 objs = - match env.last_saved_objectives with - | Some objs -> objs - | None -> raise I_dont_know - in - let acc = - try - Objective.Model.fold (fun { e; is_max; _ } value acc -> - match (value : Objective.Value.t) with - | Pinfinity | Minfinity -> - raise (Give_up acc) - | Value v -> - (e, v, is_max, true) :: acc - | Limit (_, v) -> - raise (Give_up ((e, v, is_max, false) :: acc)) - | Unknown -> - assert false - ) objs [] - with Give_up acc -> acc - in - begin match acc with - | [] -> - (* 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 I_dont_know; - | (e, tv, is_max, is_le) :: l -> - let neg = - List.fold_left - (fun acc (e, tv, is_max, is_le) -> - let eq = E.mk_eq e tv ~iff: false in - let acc = E.Core.and_ acc eq in - E.Core.(or_ acc (not ((op (E.type_info e) is_max is_le) e tv))) - ) (E.Core.not ((op (E.type_info e) is_max is_le) e tv)) l - in - if Options.get_debug_optimize () then - Printer.print_dbg - "The objective function %a has an optimum. We should continue \ - to explore other branches to try to find a better optimum than \ - %a." Expr.print e Expr.print tv; - let l = [mk_gf neg] in - (* TODO: Can we add the clause without 'cancel_until 0' ? *) - SAT.cancel_until env.satml 0; - if Options.get_debug_optimize () then - Printer.print_dbg - "We assert the formula %a to explore another branch." - E.print neg; - 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 \ - issue.@.@."; - assert false - end; - Options.Time.unset_timeout (); - Options.Time.set_timeout (Options.get_timelimit ()); - unsat_rec_prem env ~first_call:false - end - - let rec unsat_rec env ~first_call:_ : unit = + let rec unsat_rec env : unit = try SAT.solve env.satml; assert false with - | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Satml.Unsat lc -> raise (IUnsat (make_explanation lc)) | Util.Timeout -> i_dont_know env (Timeout ProofSearch) | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) | Satml.Sat -> @@ -1189,51 +1077,32 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in if not updated then ( if Options.get_produce_models () then update_model env; + env.last_saved_bmodel <- Some (capture_bmodel env); Options.Time.unset_timeout (); i_dont_know env Incomplete ); - unsat_rec env ~first_call:false + unsat_rec env with | Util.Timeout -> i_dont_know env (Timeout ProofSearch) | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) - | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Satml.Unsat lc -> raise (IUnsat (make_explanation lc)) | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*) begin try SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl); - unsat_rec env ~first_call:false + unsat_rec env with - | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Satml.Unsat lc -> raise (IUnsat (make_explanation lc)) | Util.Timeout -> i_dont_know env (Timeout ProofSearch) | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) end - let rec unsat_rec_prem env ~first_call : unit = - try - unsat_rec env ~first_call - with - | I_dont_know -> - begin - try analyze_unknown_for_objectives env unsat_rec_prem - with - | IUnsat (env, _) -> - assert (Option.is_some env.last_saved_objectives); - (* objectives is a ref, it's necessiraly updated as a - side-effect to best value *) - raise I_dont_know - end - | IUnsat (env, _) as e -> - if Option.is_none env.last_saved_objectives then raise e; - (* TODO: put the correct objectives *) - raise I_dont_know - (* copied from sat_solvers.ml *) let max_term_depth_in_sat env = let aux mx f = Stdlib.max mx (E.depth f) in ME.fold (fun f _ mx -> aux mx f) env.gamma 0 - let checks_implemented_features () = let fails msg = let msg = @@ -1299,6 +1168,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Steps.pop_steps (); env.last_saved_model <- None; env.last_saved_objectives <- None; + env.last_saved_bmodel <- None; env.inst <- inst; env.guards.current_guard <- b; let declare_top = @@ -1317,6 +1187,181 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let current_guard = env.guards.current_guard in {gf with E.ff = E.mk_imp current_guard gf.E.ff} + exception Give_up of (E.t * E.t * bool * bool) list + + (* Getting [unknown] after a query can mean two things: + - The problem is [unsat] but we didn't manage to find a contradiction; + - We produce a model of the formulas. + + In the latter case, we optimized our objective functions during the + exploration of this branch of the SAT solver. It doesn't mean there is no + other branch of the SAT solver in which all the formulas are satisfiable + and the objective functions have bigger values in some models of this + branch. + + For instance, consider the SMT-LIB problem: + (declare-const x Int) + (assert (or (<= x 2) (<= x 4))) + (assert (or (<= y 3)) + (maximize x) + (maximize y) + (check-sat) + (get-model) + + Assume that the solver explores the first branch (<= x 2) of the or gate: + (or (<= x 2) (<= x 4)). + + Let's imagine it discovers that [0] is a model of the first formula. After + optimization, it find that [2] is the best model for [x] and [3] is the + best model for [y] it can got in this branch. Still we have to explore + the second branch [(<= x 4)] to realize that [4] is actually the best + model for [x]. + + The following function ensures to explore adequate branches of the SAT + solver in order to get the best model, if the problem is SAT. + + In our running example, after getting the model [2], the below function + run again the SAT solver with the extra assert: + (assert (or (> x 2) (and (= x 2) (> y 3))) + + If this run produces the answer [unsat], we know that [2] was the best + model value for [x]. Otherwise, we got a better value for [x]. *) + + type ty_op = + { lt : E.t -> E.t -> E.t + ; le : E.t -> E.t -> E.t } + + let real_op = { lt = Expr.Reals.(<) ; le = Expr.Reals.(<=) } + + let int_op = { lt = Expr.Ints.(<) ; le = Expr.Reals.(<=) } + + let bitv_unsigned_op = { lt = Expr.BV.bvult ; le = Expr.BV.bvule } + + let mk_le { le ; _ } = le + + let mk_lt { lt ; _ } = lt + + let mk_ge { le ; _ } x y = le y x + + let mk_gt { lt ; _ } x y = lt y x + + let op ty is_max is_le = + let ty_op = + match ty with + | Ty.Treal -> real_op + | Tint -> int_op + | Tbitv _ -> bitv_unsigned_op + | _ -> Fmt.invalid_arg "cannot optimize for type: %a" Ty.print ty + in + if is_max then begin + if is_le then mk_le ty_op + else mk_lt ty_op + end + else begin + if is_le then mk_ge ty_op + else mk_gt ty_op + end + + let capture_models env = + (* Models must be saved before asserting a new formula in [optimize_models] + as they may be altered if a contradiction arises. More precisely, + - There is no need to force [env.last_saved_model], as this closure + has captured the correct theory environment in + [SAT.compute_concrete_model]. + - [env.last_saved_objectives] is pure and only needs to be saved + without additional precautions. + - The atoms of [env.last_saved_bmodel] are mutable and part of the SAT + solver state [env.satml], which means they may be altered after + popping an assertion level. *) + let fmdl = env.last_saved_model in + let omdl = + match env.last_saved_objectives with + | Some objs -> objs + | None -> assert false + in + fmdl, omdl, capture_bmodel env + + let rec optimize_models (fmdl, omdl, bmdl) env = + let acc = + try + Objective.Model.fold (fun { e; is_max; _ } value acc -> + match (value : Objective.Value.t) with + | Pinfinity | Minfinity -> + raise (Give_up acc) + | Value v -> + (e, v, is_max, true) :: acc + | Limit (_, v) -> + raise (Give_up ((e, v, is_max, false) :: acc)) + | Unknown -> + assert false + ) omdl [] + with Give_up acc -> acc + in + begin match acc with + | [] -> + (* The answer for the first objective is infinity. We stop here as + we cannot go beyond infinity and lower-priority objectives + cannot be optimized in the presence of infinity values. *) + fmdl, omdl, bmdl + | (e, tv, is_max, is_le) :: l -> + let neg = + List.fold_left + (fun acc (e, tv, is_max, is_le) -> + let eq = E.mk_eq e tv ~iff: false in + let acc = E.Core.and_ acc eq in + E.Core.(or_ acc (not ((op (E.type_info e) is_max is_le) e tv))) + ) (E.Core.not ((op (E.type_info e) is_max is_le) e tv)) l + in + Logs.debug ~src:Options.Sources.optimize + (fun k -> k + "The objective function %a has an optimum. We should continue \ + to explore other branches to try to find a better optimum than \ + %a." Expr.print e Expr.print tv); + Logs.debug ~src:Options.Sources.optimize + (fun k -> k + "We assert the formula %a to explore another branch." + E.print neg); + try + let gf = add_guard env @@ mk_gf neg in + let updated = assume_aux ~dec_lvl:0 env [gf] in + if not updated then + Fmt.failwith + "env not updated after injection of neg! termination issue"; + unsat_rec env; + assert false + with + | I_dont_know -> + optimize_models (capture_models env) env + | IUnsat _ex -> + (* The unsatisfability of [env] means that the objectives cannot + be further optimized. + + The explanation [_ex] can be discared, as we revert the assertion + of formulas that led to this contradiction in + [unsat_then_optimize]. *) + fmdl, omdl, bmdl + end + + let unsat_then_optimize env = + try + unsat_rec env + with + | I_dont_know -> + match env.last_saved_objectives with + | None -> raise I_dont_know + | Some omdl when Objective.Model.is_empty omdl -> raise I_dont_know + | Some _ -> + (* An additional assertion level is inserted around [optimize_models] + to revert to a consistent SAT environment after reaching an + unsatisfiable state in [optimize_models]. *) + push env 1; + let fmdl, omdl, bmdl = optimize_models (capture_models env) env in + pop env 1; + env.last_saved_model <- fmdl; + env.last_saved_objectives <- Some omdl; + env.last_saved_bmodel <- Some bmdl; + raise I_dont_know + let unsat env gf = assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml); checks_implemented_features (); @@ -1331,10 +1376,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let _updated = assume_aux ~dec_lvl:0 env [gf] in let max_t = max_term_depth_in_sat env in env.inst <- Inst.register_max_term_depth env.inst max_t; - unsat_rec_prem env ~first_call:true; + unsat_then_optimize env; assert false with - | IUnsat (_env, dep) -> + | IUnsat dep -> assert begin Ex.fold_atoms (fun e b -> match e with @@ -1349,7 +1394,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* dep currently not used. No unsat-cores in satML yet *) assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml); try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) - with | IUnsat (_env, dep) -> raise (Unsat dep) + with | IUnsat dep -> raise (Unsat dep) | Util.Timeout -> (* don't attempt to compute a model if timeout before calling unsat function *) @@ -1379,16 +1424,15 @@ 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 -> + match E.type_info t, env.last_saved_bmodel with + | Ty.Tbool, Some bmodel -> begin - let bmodel = SAT.boolean_model env.satml in Compat.List.find_map - (fun Atom.{lit; neg = {lit=neglit; _}; _} -> + (fun { lit; neg } -> let tlit = Shostak.Literal.make (LTerm t) in if Shostak.Literal.equal tlit lit then Some E.vrai - else if Shostak.Literal.equal tlit neglit then + else if Shostak.Literal.equal tlit neg then Some E.faux else None diff --git a/tests/smtlib/testfile-get-assignment3.smt2 b/tests/smtlib/testfile-get-assignment3.smt2 index 5aea879f79..e589daa44d 100644 --- a/tests/smtlib/testfile-get-assignment3.smt2 +++ b/tests/smtlib/testfile-get-assignment3.smt2 @@ -3,4 +3,4 @@ (declare-const x Int) (assert (! (= x 0) :named foo)) (check-sat) -(get-assignment) \ No newline at end of file +(get-assignment) From 457e43f52eade9b066f9d7e2244a0e9aa8be33fd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 20 Feb 2025 10:49:35 +0100 Subject: [PATCH 2/2] Remove lazy models --- src/lib/reasoners/fun_sat.ml | 5 ++--- src/lib/reasoners/satml.ml | 2 +- src/lib/reasoners/satml.mli | 2 +- src/lib/reasoners/satml_frontend.ml | 5 ++--- src/lib/reasoners/theory.ml | 15 +++++++-------- src/lib/reasoners/theory.mli | 2 +- tests/models/arith/arith11.default.expected | 2 +- 7 files changed, 15 insertions(+), 18 deletions(-) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 88c845c542..e4e98b5b0b 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -175,7 +175,7 @@ module Make (Th : Theory.S) = struct guards : guards; add_inst: E.t -> bool; unit_facts_cache : (E.gformula * Ex.t) ME.t ref; - last_saved_model : Models.t Lazy.t option ref; + last_saved_model : Models.t option ref; unknown_reason : Sat_solver_sig.unknown_reason option; declare_top : Id.typed list ref; @@ -1838,8 +1838,7 @@ module Make (Th : Theory.S) = struct {env with tbox = Th.assume_th_elt env.tbox th_elt dep} (** returns the latest model stored in the env if any *) - let get_model env = - Option.map Lazy.force !(env.last_saved_model) + let get_model env = !(env.last_saved_model) let get_unknown_reason env = env.unknown_reason diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 0d99069107..fe3383e1a5 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -94,7 +94,7 @@ module type SAT_ML = sig val compute_concrete_model : declared_ids:Id.typed list -> t -> - Models.t Lazy.t * Objective.Model.t + Models.t * Objective.Model.t val set_new_proxies : t -> FF.proxies -> unit diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index e3b91a919e..85b03c19c2 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -48,7 +48,7 @@ module type SAT_ML = sig val compute_concrete_model : declared_ids:Id.typed list -> t -> - Models.t Lazy.t * Objective.Model.t + Models.t * Objective.Model.t val set_new_proxies : t -> Flat_Formula.proxies -> unit diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 8fda3820ce..dcec710ae1 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -67,7 +67,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct mutable skolems : E.gformula ME.t; (* key <-> f *) add_inst : E.t -> bool; guards : guards; - mutable last_saved_model : Models.t Lazy.t option; + mutable last_saved_model : Models.t option; mutable last_saved_objectives : Objective.Model.t option; mutable last_saved_bmodel : Shostak.Literal.t atom list option; (** The boolean model saved in this field is intented for use by @@ -1418,8 +1418,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let optimize env fn = SAT.optimize env.satml fn - let get_model env = - Option.map Lazy.force env.last_saved_model + let get_model env = env.last_saved_model let get_unknown_reason env = env.unknown_reason diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962a..105674520a 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -70,7 +70,7 @@ module type S = sig val extract_concrete_model : declared_ids:Id.typed list -> t -> - Models.t Lazy.t * Objective.Model.t + Models.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -894,12 +894,11 @@ module Main_Default : S = struct let { gamma_finite; assumed_set; objectives; _ }, _ = do_case_split_aux env ~for_model:true in - lazy ( - CC_X.extract_concrete_model - ~prop_model:assumed_set - ~declared_ids - gamma_finite - ), objectives + CC_X.extract_concrete_model + ~prop_model:assumed_set + ~declared_ids + gamma_finite + , objectives let assume_th_elt t th_elt dep = { t with gamma = CC_X.assume_th_elt t.gamma th_elt dep } @@ -953,7 +952,7 @@ module Main_Empty : S = struct let add_term env _ ~add_in_cs:_ = env let compute_concrete_model ~acts:_ _env = () let extract_concrete_model ~declared_ids:_ _env = - lazy Models.empty, Objective.Model.empty + Models.empty, Objective.Model.empty let assume_th_elt e _ _ = e let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, [] diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index f8c4e115d3..4b5545ad21 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -61,7 +61,7 @@ module type S = sig val extract_concrete_model : declared_ids:Id.typed list -> t -> - Models.t Lazy.t * Objective.Model.t + Models.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : diff --git a/tests/models/arith/arith11.default.expected b/tests/models/arith/arith11.default.expected index 216672887e..366bab5ddf 100644 --- a/tests/models/arith/arith11.default.expected +++ b/tests/models/arith/arith11.default.expected @@ -2,7 +2,7 @@ unknown ( (define-fun x () Real 2.0) - (define-fun y () Real (as @a0 Real)) + (define-fun y () Real (as @a4 Real)) (define-fun p1 () Bool false) (define-fun p2 () Bool true) )