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

Apply simplification to Imp and Iff connectives #4533

Merged
merged 37 commits into from
Apr 2, 2024
Merged
Changes from 1 commit
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
4235832
Optimize uses clauses added by Translator.cs
zafer-esen Aug 16, 2023
7ac0fbe
Add trigger to an axiom that was incorrectly being pruned away.
zafer-esen Aug 16, 2023
943ade9
Revert change in Translator for Boogie compatibility.
zafer-esen Aug 16, 2023
b52e014
Update integration tests. Minor changes in the prelude.
zafer-esen Aug 17, 2023
99a24cc
Simplify certain formulas with literals.
zafer-esen Aug 21, 2023
0f76db6
Fixes some issues introduced during merge with upstream.
zafer-esen Sep 8, 2023
81ce40e
Fixes another issue introduced during merge.
zafer-esen Sep 8, 2023
1224fd2
Simplify F in BplAnd.
zafer-esen Sep 8, 2023
80bde0a
Make BplIff static.
zafer-esen Sep 8, 2023
09dcb06
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 8, 2023
ec7b088
Adds a few more and replacements.
zafer-esen Sep 8, 2023
56ebbf7
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 11, 2023
7234e99
More simplification for BplIff
zafer-esen Sep 11, 2023
4228f5c
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 25, 2023
4dc1c0e
Consider Lit when simplifying and update expected test results.
zafer-esen Sep 25, 2023
4ffe6d0
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Nov 8, 2023
bd17def
Merge branch 'master' into simplify-imp-iff
atomb Nov 15, 2023
915c68e
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Jan 31, 2024
1ce4aeb
Fix overzealous conversion to BplImp, BplAnd
atomb Jan 31, 2024
85f0ee1
Fix some expected test outputs
atomb Jan 31, 2024
493b912
Get one more test to pass
atomb Feb 1, 2024
33b2b97
Fix misunderstanding of for-each-compiler
atomb Feb 1, 2024
30677dd
Make dafny4/gcd.dfy less brittle
atomb Feb 1, 2024
3289695
Make VSComp2010/Problem2-Invert.dfy less brittle
atomb Feb 1, 2024
082e19a
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Feb 9, 2024
2d973cf
Fix tests
atomb Feb 10, 2024
77443c1
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Feb 10, 2024
16b77c2
Merge branch 'master' into simplify-imp-iff
atomb Mar 28, 2024
e6bda87
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Mar 29, 2024
fad1c8d
Fix CI
atomb Mar 29, 2024
b08ffef
One more test fix
atomb Apr 1, 2024
0c3c0a3
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Apr 1, 2024
9ed2257
Remove unneeded resource limit increase
atomb Apr 2, 2024
e7ee237
Merge branch 'master' into simplify-imp-iff
atomb Apr 2, 2024
2b769f9
Rebuild standard libraries
atomb Apr 2, 2024
08daf27
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Apr 2, 2024
e53ed77
Update expected test output
atomb Apr 2, 2024
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
Prev Previous commit
Next Next commit
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb committed Mar 29, 2024

Verified

This commit was signed with the committer’s verified signature.
jorisv Joris Vaillant
commit e6bda87b931dfbe809b38b9318ec9dad667ef37e

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.