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.

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

Fix model generation for records #792

Closed
wants to merge 1 commit into from

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Sep 4, 2023

Before this PR, it seems the model generation for records didn't work on next. The reason is simple. If we want to produce a value for a declared record, we need to accumulate all the accesses to this record. For instance, the following input file:

(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)

didn't produce a correct model. It assigned 0 for any field of type Int.

Note: for functional arrays, we can use the ModelMap.t structure to accumulate the store instructions as functional arrays can be seen as a map. We cannot do the same thing for records since each destructor of the record can return a different type.

@bclement-ocp
Copy link
Collaborator

bclement-ocp commented Sep 4, 2023

Hmm I believe this should be dealt with by purification? In fact if you run your example with -d uf you get:

a --> {first = 5; second = 0}

in the representative maps, so this is probably either a printing issue or the specialized code for records in model generation. I have seen that code do dubious things in the past (I didn't look into it too much because my understanding is that records in models are not officially supported).

@bclement-ocp
Copy link
Collaborator

Ah, I did not see this was a PR and not an issue, sorry. I think the fix works, but it would be better to exploit the information we have from the semantic values instead (in contrast, functional arrays don't have semantic values).

@bclement-ocp
Copy link
Collaborator

(Discussed offline; #776 changes this code quite a bit so we are going for the simplest possible fix in #793 )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants