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

Smt changes #70

Merged
merged 101 commits into from
Feb 26, 2024
Merged

Smt changes #70

merged 101 commits into from
Feb 26, 2024

Conversation

rozlynd
Copy link
Contributor

@rozlynd rozlynd commented Jan 9, 2023

New version of the SMT encoding. The encoding is simpler but performs similarly. The previous version is still available; it can be invoked with the debug flag "oldsmt".

adef and others added 23 commits November 15, 2022 16:02
Replaced test/fast/smt_tests bu unit/ and bugs/
b230794
Made hyp_hint available
07f71e4
Facts may be named and marked as axioms, hyps,...
7724ee3
SMT-LIB patterns
e8c54bc
Made ssnoc and app_hyps from Expr.Subst visible
bbf5f1f
New expression visitors: foldmap and fold
557bb55
Option.fold
88a71ae
Sets and Maps of integers
291ce04
builtin_to_string
f93c594
Expr.Collect for computing sets of free variables
1d7f8ee
Fixed a bug in smt.ml that made verbosity ignored
289a573
Display obligation number in isabelle output
30fed8c
Package Type: type system utilities
2480ac7
Package Encode: new SMT and TPTP encoding
b39335b
New translation to SMT-LIB
8b13372 
The old version is still here, use it with the flag
    --debug oldsmt
New translation to TPTP + Support Zipperposition
3842f53 
Usage:
- 'BY Zipper' or 'BY Zipper(T)' in TLAPS
- '--method zipper' in command-line
FIXUP: SMT translation
3f08478
Improved obligation display in temp files
81695a3
Heuristics for set extensionality (SMT)
7caaa98
Mode "ext" for SMT is default
39a981d
Compare all pairs of refinement sets (heuristics)
8450a8c
Use flag --smt-logic for new SMT encoding
7a1f96a
Use CVC4 for one regression test
0bdb217
damiendoligez
damiendoligez reviewed Mar 2, 2023
View reviewed changes
Copy link
Contributor

@damiendoligez damiendoligez left a comment

Choose a reason for hiding this comment

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

First part of my review.

src/backend/fpfile.ml Show resolved Hide resolved
test/bugs/sndord_test.tla Outdated Show resolved Hide resolved
src/util/util.ml Outdated Show resolved Hide resolved
src/type/t_visit.mlt Outdated Show resolved Hide resolved
src/type/t_visit.mli Outdated Show resolved Hide resolved
src/encode/n_axioms.ml Outdated Show resolved Hide resolved
src/encode/n_axioms.ml Outdated Show resolved Hide resolved
src/encode/n_axioms.ml Outdated Show resolved Hide resolved
src/encode/n_axioms.mli Outdated Show resolved Hide resolved
src/encode/n_axioms.mlt Outdated Show resolved Hide resolved
adef-inr and others added 6 commits March 24, 2023 13:58
@damiendoligez
Update src/util/util.ml
a97d4f9 
Co-authored-by: Damien Doligez <[email protected]>
@damiendoligez
Update src/type/t_visit.mlt
c10b19d 
Co-authored-by: Damien Doligez <[email protected]>
@damiendoligez
Update src/type/t_visit.mli
0e323ce 
Co-authored-by: Damien Doligez <[email protected]>
@damiendoligez
Update src/encode/n_axioms.ml
194f684 
Co-authored-by: Damien Doligez <[email protected]>
@damiendoligez
Update src/type/t_t.ml
b887a09 
Co-authored-by: Damien Doligez <[email protected]>
@damiendoligez
Update src/encode/n_axioms.ml
9835c02 
Co-authored-by: Damien Doligez <[email protected]>
rozlynd added 14 commits January 25, 2024 16:57
@rozlynd
Removed unused module Encode.Hints
7c13511
@rozlynd
Fixed polarities in Encode.Rewriting
159f728
@rozlynd
Fix: And/Or lists with one member collapse
7b76a69 
This raised an error with cvc5
@rozlynd
Clarification that tla_smb_desc is NOT injective
54915f6 
Renamed the function, previously "tla_smb_to_string"
@rozlynd
Fix: Infinity is not a real
2e2ee94
@rozlynd
Fix duplicate case in T.Synth
fdb9c09
@rozlynd
Use subclass of Subst.map insteadof duplicate code
93ca710
@rozlynd
Factor special characters replacement in Thf/SMT
01e2e61
@rozlynd
Fixed contradictory assert in Expr.Subst
198a64a
@rozlynd
Factored expansion of set extensionality fcn
11922d8
@rozlynd
Set equalities in negative contexts are unchanged
378fd47
@rozlynd
Fixed/Rephrased some comments
ac759fa
@rozlynd
Fixed exponentation symbol for SMT
035c39d 
m^n is specified for m,n:int iff m # 0 OR n > 0

The operator has no counterpart in SMT, and no axiom is provided for
reasoning, but at least we cannot prove statements like 0^(-1) \in Int.
@rozlynd
Removed global use of debug flags in encode/
86ffa20 
Flag "nonewqut" not supported anymore

Flag "noarith" renamed to "disable_arithmetic"; always true for
Zipperposition

Flag "no_smt_set_extensionality" disables the special use of SMT
triggers for the axiom of set extensionality
@rozlynd
Copy link
Contributor Author

rozlynd commented Jan 26, 2024

I just pushed a bunch of commits. Most of them are changes that address something @damiendoligez pointed out. A few are fixes to bugs I found along the way. Anyway, I think I'm done now.

@rozlynd
Copy link
Contributor Author

rozlynd commented Jan 26, 2024

Should I try to merge now?

@kape1395 kape1395 mentioned this pull request Jan 28, 2024
Merged
@damiendoligez
Copy link
Contributor

@kape1395

@damiendoligez, maybe it is enough to merge instead of rebase? That's usually simpler. I could do the main -> smt-changes merge. Then, the opposite will be a non-conflicting merge.

Yes, merging is fine if it's easier than rebasing.

@damiendoligez
Copy link
Contributor

@adef-inr We have a few more conflicts, but they should be easy to resolve.

@damiendoligez
Copy link
Contributor

I have pushed a trivial change to make the source compatible with Ocaml 5. Let's see what CI says now.

@damiendoligez
Copy link
Contributor

Pushed two very small changes in the failed tests, and a change to the test harness to get more feedback from CI when a test fails.

@adef-inr you may want to have a look at commit 783df0a : why does a useless quantifier throw the SMT prover off track? Is it caused by your back-end processor somehow?

@kape1395
Copy link
Collaborator

Maybe this branch can be merged already and the why does a useless quantifier throw the SMT prover off track? Is it caused by your back-end processor somehow? could be tracked as a separate branch/issue?

@damiendoligez damiendoligez merged commit d53d147 into main Feb 26, 2024
12 of 13 checks passed
@damiendoligez
Copy link
Contributor

Merged and opened #121 to track the issue with the quantifier.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@muenchnerkindl muenchnerkindl muenchnerkindl left review comments

@damiendoligez damiendoligez damiendoligez approved these changes

Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@rozlynd @damiendoligez @kape1395 @muenchnerkindl