From 1fed4cea13d1a1e7e2354a766aa79eeb6723c92d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Sep 2023 16:17:28 +0200 Subject: [PATCH] accumulate record accesses --- src/lib/frontend/models.ml | 28 +++++++++++-------- src/lib/frontend/models.mli | 3 ++ src/lib/reasoners/shostak.ml | 8 +++--- src/lib/reasoners/uf.ml | 31 ++++++++++++++++----- tests/dune.inc | 25 +++++++++++++++++ tests/models/record/record1.models.expected | 5 ++++ tests/models/record/record1.models.smt2 | 8 ++++++ 7 files changed, 85 insertions(+), 23 deletions(-) create mode 100644 tests/models/record/record1.models.expected create mode 100644 tests/models/record/record1.models.smt2 diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 0849ff6c8..48704e2dc 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -261,29 +261,33 @@ module SmtlibCounterExample = struct MS.add record_name destrs records let mk_records_constr records record_name - { Ty.name = _n; record_constr = cstr; lbs = lbs; _} = + { Ty.record_constr = cstr; lbs; _ } = let find_destrs destr destrs = try let rep = MS.find destr destrs in Some rep with Not_found -> None in - let print_destr fmt (destrs,lbs) = - List.iter (fun (destr, ty_destr) -> - let destr = Hstring.view destr in - match find_destrs destr destrs with - | None -> - pp_dummy_value_of_type fmt ty_destr - | Some rep -> fprintf fmt "%s " rep - ) lbs + let pp_destr destrs ppf (destr, ty_destr) = + match find_destrs (Hstring.view destr) destrs with + | None -> + Fmt.pf ppf "%a" + pp_dummy_value_of_type ty_destr + | Some rep -> + Fmt.pf ppf "%s" rep in + + let pp_destrs destrs = + Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf " ") (pp_destr destrs) + in + let destrs = try MS.find (Sy.to_string record_name) records with Not_found -> MS.empty in asprintf "%s %a" (Hstring.view cstr) - print_destr (destrs,lbs) + (pp_destrs destrs) lbs let add_record_constr records record_name { Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values = @@ -480,7 +484,7 @@ let rec pp_value ppk ppf = function let pp_constant ppf (_, t) = Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t -let output_concrete_model fmt props ~functions ~constants ~arrays = +let output_concrete_model fmt props ~functions ~constants ~arrays ~records = if ModelMap.(is_suspicious functions || is_suspicious constants || is_suspicious arrays) then Format.fprintf fmt "; This model is a best-effort. It includes symbols @@ -524,7 +528,7 @@ let output_concrete_model fmt props ~functions ~constants ~arrays = (* Functions *) let records = SmtlibCounterExample.output_functions_counterexample - pp_x fmt MS.empty functions + pp_x fmt records functions in (* Constants *) diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index dcbe944a3..178ecc1a3 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -28,6 +28,8 @@ (* *) (**************************************************************************) +module MS : Map.S with type key = string + (** {1 Models module} *) (** Print the given counterexample on the given formatter with the @@ -42,4 +44,5 @@ val output_concrete_model : functions:ModelMap.t -> constants:ModelMap.t -> arrays:ModelMap.t -> + records:string MS.t MS.t -> unit diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 455c6374f..3f7a3421a 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -330,10 +330,10 @@ struct let is_solvable_theory_symbol sb ty = X1.is_mine_symb sb ty || not (Options.get_restricted ()) && - (X2.is_mine_symb sb ty || - X3.is_mine_symb sb ty || - X4.is_mine_symb sb ty || - X5.is_mine_symb sb ty) + ((*X2.is_mine_symb sb ty || *) + X3.is_mine_symb sb ty || + X4.is_mine_symb sb ty || + X5.is_mine_symb sb ty) let is_a_leaf r = match r.v with diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 81dd4095a..032223f39 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -36,6 +36,7 @@ module Ex = Explanation module Sy = Symbols module E = Expr module ME = Expr.Map +module MS = Models.MS module SE = Expr.Set module LX = @@ -1024,7 +1025,7 @@ let model_repr_of_term t env mrepr = let compute_concrete_model ({ make; _ } as env) = ME.fold - (fun t _mk ((fprofs, cprofs, carrays, mrepr) as acc) -> + (fun t _mk ((fprofs, cprofs, carrays, crecords, mrepr) as acc) -> let { E.f; xs; ty; _ } = E.term_view t in if X.is_solvable_theory_symbol f ty || E.is_fresh t || E.is_fresh_skolem t @@ -1045,6 +1046,22 @@ let compute_concrete_model ({ make; _ } as env) = let rep, mrepr = model_repr_of_term t env mrepr in assert (is_a_good_model_value rep); match f, xs, ty with + | Sy.Op Sy.Record, _, _ -> acc + + | Sy.Op Sy.Access field, [(_, (_, srep))], _ -> + let fields = + let fields = + try MS.find srep crecords + with Not_found -> MS.empty + in + MS.add (Hstring.view field) (snd rep) fields + in + fprofs, + cprofs, + carrays, + MS.add srep fields crecords, + mrepr + | Sy.Op Sy.Set, _, _ -> acc | Sy.Op Sy.Get, [(_,(a,_));((_,(i,_)) as e)], _ -> @@ -1056,6 +1073,7 @@ let compute_concrete_model ({ make; _ } as env) = fprofs, cprofs, ModelMap.add (f_ta,[X.type_info i], ty) ([e], rep) carrays, + crecords, mrepr | _ -> assert false @@ -1064,19 +1082,18 @@ let compute_concrete_model ({ make; _ } as env) = | _ -> if tys == [] then fprofs, ModelMap.add (f, tys, ty) (xs, rep) cprofs, carrays, - mrepr + crecords, mrepr else ModelMap.add (f, tys, ty) (xs, rep) fprofs, cprofs, carrays, - mrepr + crecords, mrepr ) make - (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty) + (ModelMap.empty, ModelMap.empty, ModelMap.empty, MS.empty, ME.empty) let output_concrete_model fmt ~prop_model env = if Options.get_interpretation () then - let functions, constants, arrays, _ = - compute_concrete_model env in - Models.output_concrete_model fmt prop_model ~functions ~constants ~arrays + let functions, constants, arrays, records, _ = compute_concrete_model env in + Models.output_concrete_model fmt prop_model ~functions ~constants ~arrays ~records let save_cache () = LX.save_cache () diff --git a/tests/dune.inc b/tests/dune.inc index a19c2a508..4945d05e7 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -186808,6 +186808,31 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir models/record + (rule + (target record1.models_tableaux.output) + (deps (:input record1.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 record1.models.expected record1.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + ; Auto-generated part begin (subdir models/uf (rule diff --git a/tests/models/record/record1.models.expected b/tests/models/record/record1.models.expected new file mode 100644 index 000000000..da5e88f8f --- /dev/null +++ b/tests/models/record/record1.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () Pair (pair 5 0)) +) diff --git a/tests/models/record/record1.models.smt2 b/tests/models/record/record1.models.smt2 new file mode 100644 index 000000000..2739fc71d --- /dev/null +++ b/tests/models/record/record1.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-const a Pair) +(assert (= (first a) 5)) +(check-sat) +(get-model)