Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use fresh names for all the abstract values #811

Merged
merged 2 commits into from
Sep 12, 2023
Merged

Use fresh names for all the abstract values #811

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
23c17a5
Use fresh names for all abstract values
Halbaroth Sep 12, 2023
59752b9
Call fresh_string in pp_abstract_value_of_type
Halbaroth Sep 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 6 additions & 9 deletions src/lib/frontend/models.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,9 +236,9 @@ module SmtlibCounterExample = struct
else
E.print fmt t

let pp_abstract_value_of_type ppf (name, ty) =
let pp_abstract_value_of_type ppf ty =
if not @@ Options.get_interpretation_use_underscore () then
Fmt.pf ppf "(as @@%s %a)" name Ty.pp_smtlib ty
Fmt.pf ppf "(as @@%s %a)" (Hstring.fresh_string ()) Ty.pp_smtlib ty
else
Fmt.pf ppf "_ "

Expand All @@ -264,8 +264,7 @@ module SmtlibCounterExample = struct
let destr = Hstring.view destr in
match find_destrs destr destrs with
| None ->
let name = Hstring.fresh_string () in
pp_abstract_value_of_type fmt (name, ty_destr)
pp_abstract_value_of_type fmt ty_destr
| Some rep -> fprintf fmt "%s " rep
) lbs
in
Expand Down Expand Up @@ -388,8 +387,7 @@ module SmtlibCounterExample = struct

let rec reps_aux reps =
match reps with
| [] -> dprintf "%a" pp_abstract_value_of_type
(Symbols.to_string f, ty)
| [] -> dprintf "%a" pp_abstract_value_of_type ty
| [srep,xs_values_list] ->
if Options.get_interpretation_use_underscore () then
dprintf "(@[<hv>ite %t@ %a@ %t)@]"
Expand Down Expand Up @@ -476,9 +474,8 @@ let rec pp_value ppk ppf = function
| Constant (sy, t) -> ppk ppf (sy, t)
| Value (_, s) -> Format.pp_print_string ppf s

let pp_constant ppf (sy, t) =
Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type
(Symbols.to_string sy, t)
let pp_constant ppf (_sy, t) =
Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t

let output_concrete_model fmt props ~functions ~constants ~arrays =
if ModelMap.(is_suspicious functions || is_suspicious constants
Expand Down
2 changes: 1 addition & 1 deletion tests/cram.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ appropriate here.

unknown
(
(define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
(define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
(define-fun x () Int 0)
(define-fun y () Int 0)
)
Expand Down
2 changes: 1 addition & 1 deletion tests/issues/555.models.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

unknown
(
(define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
(define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
(define-fun x () Int 0)
(define-fun y () Int 0)
)
Loading