diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 0849ff6c88..1c843ed7f1 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -243,7 +243,7 @@ module SmtlibCounterExample = struct | Ty.Tbool -> Fmt.pf ppf "false" | Ty.Tfarray (_, rty) -> Fmt.pf ppf "((as const %a) %a)" Ty.pp_smtlib ty pp_dummy_value_of_type rty - | _ -> Fmt.pf ppf "@@%a" pp_term (Expr.fresh_name ty) + | _ -> Fmt.pf ppf "(as @@%a %a)" pp_term (Expr.fresh_name ty) Ty.pp_smtlib ty let pp_dummy_value_of_type fmt ty = if not (Options.get_interpretation_use_underscore ()) then @@ -457,6 +457,8 @@ type value_defn = | Value of X.r * string (* A leaf semantic value. This must be an actual value, i.e. it must not contain any uninterpreted terms. *) + | Abstract of string + (* An unique abstract value *) let value (r, s) = match X.term_extract r with @@ -476,6 +478,7 @@ let rec pp_value ppk ppf = function (pp_value ppk) v | Constant (sy, t) -> ppk ppf (sy, t) | Value (_, s) -> Format.pp_print_string ppf s + | Abstract s -> Format.pp_print_string ppf s let pp_constant ppf (_, t) = Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t @@ -494,6 +497,13 @@ let output_concrete_model fmt props ~functions ~constants ~arrays = end; let values = Hashtbl.create 17 in + let find_or_add sy f = + try Hashtbl.find values sy + with Not_found -> + let value = f () in + Hashtbl.replace values sy value; + value + in (* Add the constants *) ModelMap.iter (fun (f, xs_ty, _) st -> assert (Lists.is_empty xs_ty); @@ -516,8 +526,16 @@ let output_concrete_model fmt props ~functions ~constants ~arrays = arrays; let pp_value = - pp_value (fun ppf (sy, _) -> - pp_value pp_constant ppf (Hashtbl.find values sy)) + pp_value (fun ppf (sy, ty) -> + let v = + find_or_add sy @@ fun () -> + (* NB: It is important that we call `pp_dummy_value_of_type` + immediately (not in a delayed fashion) so that we make sure that + the same abstract value will get printed each time. *) + Abstract ( + Fmt.to_to_string SmtlibCounterExample.pp_dummy_value_of_type ty) + in + pp_value pp_constant ppf v) in let pp_x ppf xs = pp_value ppf (value xs) in diff --git a/tests/dune.inc b/tests/dune.inc index dc64ad5059..2b26613f9a 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -117958,9 +117958,8 @@ (ignore-stderr (with-accepted-exit-codes 0 (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions --output=smtlib2 + --timelimit=2 --frontend dolmen %{input}))))))) (rule @@ -173288,6 +173287,71 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir issues/854 + (rule + (target twice_eq.models_tableaux.output) + (deps (:input twice_eq.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 twice_eq.models.expected twice_eq.models_tableaux.output))) + (rule + (target original.models_tableaux.output) + (deps (:input original.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 original.models.expected original.models_tableaux.output))) + (rule + (target function.models_tableaux.output) + (deps (:input function.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 function.models.expected function.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + ; Auto-generated part begin (subdir ite (rule diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected new file mode 100644 index 0000000000..0245fd7dfa --- /dev/null +++ b/tests/issues/854/function.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k2 intref)) + (define-fun f ((arg_0 Int)) Int 0) + (define-fun a () Int 0) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/function.models.smt2 b/tests/issues/854/function.models.smt2 new file mode 100644 index 0000000000..65e42142bc --- /dev/null +++ b/tests/issues/854/function.models.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun a () Int) +(declare-fun f (Int) Int) +(define-fun aqtunused ((x Int)) intref (intrefqtmk (f a))) +(assert (= (aqtunused 0) (aqtunused 1))) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected new file mode 100644 index 0000000000..fce880b2f6 --- /dev/null +++ b/tests/issues/854/original.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k1 intref)) + (define-fun a () Int 0) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/original.models.smt2 b/tests/issues/854/original.models.smt2 new file mode 100644 index 0000000000..fd66489a18 --- /dev/null +++ b/tests/issues/854/original.models.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun a () Int) +(define-fun aqtunused () intref (intrefqtmk a)) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected new file mode 100644 index 0000000000..e981535425 --- /dev/null +++ b/tests/issues/854/twice_eq.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k1 intref)) + (define-fun another_mk ((arg_0 Int)) intref (as @!k1 intref)) + (define-fun a () Int 0) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/twice_eq.models.smt2 b/tests/issues/854/twice_eq.models.smt2 new file mode 100644 index 0000000000..eaac2b8d6b --- /dev/null +++ b/tests/issues/854/twice_eq.models.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun another_mk (Int) intref) +(declare-fun a () Int) +(define-fun aqtunused () intref (intrefqtmk a)) +(assert (= aqtunused (another_mk a))) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model)