Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Improved support for IntMod type in symbolic backends #93

Merged
merged 12 commits into from
Nov 3, 2020
Merged

Improved support for IntMod type in symbolic backends #93

merged 12 commits into from
Nov 3, 2020

Conversation

brianhuffman
Copy link
Contributor

This fixes some of the problems mentioned as part of GaloisInc/saw-script#745, specifically the ones involving uninterpreted functions over the integers-mod-n type: GaloisInc/saw-script#745 (comment)

@brianhuffman
Copy link
Contributor Author

There is still a bit more work to do here, related to the Labeler datatype. I realized that the getLabelValues function in saw-script uses the Labeler values to build FirstOrderValues from solver counterexamples. But currently this will produce a FOVInt constructor for any IntMod-typed variable, which doesn't have the right type. It will work well enough if we're just printing out the counterexamples, but if we try to build saw-core terms from them, they won't be type correct.

To get this in a better state, we first need to add a FOVIntMod constructor to the FirstOrderValue datatype. Then we need to move the definition of getLabelValues from saw-script into saw-core-what4 (which will allow us to keep type Labeler abstract) and modify it (and the Labeler type as needed) to produce the right values for IntMod variables.

@brianhuffman brianhuffman marked this pull request as draft October 23, 2020 16:21
Brian Huffman added 9 commits November 2, 2020 17:27
Add TValue constructor for IntMod type.
aa768b7 
Also reimplement `IntMod` type in simulator backends
to use it.
Avoid using error within what4 backend.
69707b4
Add VIntMod constructor to Value datatype.
337aa80 
Also convert primitive implementations to use it.
Add scIntModType to SharedTerm library.
7fd75f9
Add function asIntModType to Recognizer library.
5a5d430
Add constructor FOTIntMod to FirstOrderType datatype.
8a80a19 
Quantified variables of type `IntMod n` should work again in
the what4/sbv backends.
Correctly handle uninterpreted functions on IntMod in sbv/what4 backe…
f01e444 
…nds.

When we generate an uninterpreted function in a symbolic backend that
takes an argument of type `IntMod n`, we normalize the symbolic integer
argument by reducing mod n. This ensures that the resulting expression
will respect the underlying equivalence relation for the `IntMod n` type.
Remove duplicated code.
80c40b5
Add function scToIntMod to SharedTerm library.
e2f714d
Brian Huffman added 2 commits November 2, 2020 18:51
Add FOVIntMod constructor to FirstOrderValue datatype.
363437f
saw-core-what4: Add IntModLabel to Labeler type.
7b6167e 
Also add `getLabelValues` function from saw-script to saw-core-what4.
@brianhuffman brianhuffman marked this pull request as ready for review November 3, 2020 04:20
@brianhuffman
Copy link
Contributor Author

I think this is ready to merge now. There are some additional refactorings that could be done to the Labeler type, but I think those can wait until we switch saw-script to use the getLabelValues function from saw-core-what4 instead of its own version of that function; at that point we can make the Labeler type abstract and then we can refactor it freely.

robdockins
robdockins approved these changes Nov 3, 2020
View reviewed changes
Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks OK to me.

@brianhuffman brianhuffman merged commit 7b04d2e into master Nov 3, 2020
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Nov 7, 2020
Update saw-core submodule and adapt to GaloisInc/saw-core#93.
b2fd263 
The What4 prover interface now uses `getLabelValues` from the
saw-core-what4 package.
@brianhuffman brianhuffman mentioned this pull request Nov 24, 2020
Closed
brianhuffman pushed a commit that referenced this pull request Nov 24, 2020
Fix implementation of fromIntMod in concrete evaluation backend.
2d04786 
It had been broken since #93 introduced a separate value constructor
for the `IntMod` type.

(GaloisInc/saw-script#936)
@brianhuffman brianhuffman mentioned this pull request Nov 24, 2020
Merged
brianhuffman pushed a commit that referenced this pull request Dec 10, 2020
Fix incorrect implementation of intModUnOp in sbv backend.
56f6585 
This was an unintentional omission from PR #93, which correctly
updated `intModUnOp` in the what4 backend, but not in sbv.

Fixes #114.
@brianhuffman brianhuffman mentioned this pull request Dec 10, 2020
Merged
@brianhuffman brianhuffman deleted the intmod branch January 22, 2021 12:32
@brianhuffman brianhuffman mentioned this pull request May 5, 2021
Merged
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@robdockins robdockins robdockins approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@brianhuffman @robdockins