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

Jump to bottom

Remove uses of mkTypedTerm #728

Merged
merged 9 commits into from
Aug 4, 2020
Merged

Remove uses of mkTypedTerm #728

merged 9 commits into from
Aug 4, 2020

Conversation

brianhuffman
Copy link
Contributor

See #718.

Brian Huffman added 7 commits May 18, 2020 22:11
Remove unnecessary calls to mkTypedTerm.
f7bb948 
This is a step toward fixing #718.

The use of mkTypedTerm is redundant in these cases in the
SAWScript.Prover modules, as the computed schema in all cases
is only used to check that the return type is Bool, and the
prior calls to `propToPredicate` already ensure that.
Remove completely unnecessary call to mkTypedTerm.
3747a88
Reimplement some java-related code to avoid mkTypedTerm.
1ecb24c
Remove uses of mkTypedTerm in case{Proof,Sat}ResultPrim.
0686429
Rewrite crucible llvm/jvm extract functions to avoid mkTypedTerm.
ea5fd43
Merge branch 'master' into mkTypedTerm
a01e467
Adapt to changes in FirstOrderType datatype from saw-core.
faadf26 
This makes saw-script compile successfully again, after being
broken by the most recent merge.
@brianhuffman brianhuffman marked this pull request as ready for review August 3, 2020 22:19
@brianhuffman
Copy link
Contributor Author

Some uses of mkTypedTerm still remain, but there's no need to remove them all at once.

Brian Huffman added 2 commits August 4, 2020 12:57
Make readAIG return input and output bitwidths along with term.
f3801fa 
This lets us remove another use of `mkTypedTerm` from `readAIGPrim`.
Remove unused import.
99d15ff
atomb
atomb approved these changes Aug 4, 2020
View reviewed changes
Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

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

This seems like an improvement to me. One question: in several of the proof backends, you removed the call to checkBooleanSchema and didn't replace it with anything else. How do these functions behave now if you give them non-boolean terms? Do they yield reasonable error messages?

@brianhuffman
Copy link
Contributor Author

This was explained in the commit message for f7bb948:

The use of mkTypedTerm is redundant in these cases in the SAWScript.Prover modules, as the computed schema in all cases is only used to check that the return type is Bool, and the prior calls to propToPredicate already ensure that.

@atomb
Copy link
Contributor

atomb commented Aug 4, 2020

This was explained in the commit message for f7bb948:

The use of mkTypedTerm is redundant in these cases in the SAWScript.Prover modules, as the computed schema in all cases is only used to check that the return type is Bool, and the prior calls to propToPredicate already ensure that.

Ah, right. I should have read the commit messages. :) 👍

@brianhuffman brianhuffman merged commit b1c50b0 into master Aug 4, 2020
This was referenced Aug 7, 2020
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@atomb atomb atomb approved these changes

@andreistefanescu andreistefanescu Awaiting requested review from andreistefanescu

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 @atomb