-
Notifications
You must be signed in to change notification settings - Fork 17
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
incomplete detection of EPR axioms #143
Comments
By default the EPR solver is not enabled. You can enable it with The default quantifier theory is based on the almost uninterpreted fragment, which doesn't support positive equalities between variables (negated equalities can be eliminated with DER). |
I'm kind of getting confused. The almost uninterpreted fragment (AUF) is supposed to be an extension of EPR. At least the paper claims that. Independently of that, Section 4.1 of the paper discusses equality with uninterpreted sorts. This should cover the example. The gist is that equality with uninterpreted sorts can be axiomatized within AUF. However, as solvers understand equality we can rely on that. For fun, here is a version with the axiomatization
SMTInterpol works fine on it. |
I'm not completely sure what the answer is here. The models we want to use for the almost uninterpreted fragment would not work, if we allow equalities between quantified variables. E.g., you can encode injectivity: Now if a function is injective and monotone, it is strict monotone. If the function is over integer then the additional constraint You can axiomatise an equiv predicate as you did in your second example, but we would compute a model where equiv is not equality, e.g. it would be true for almost all pairs of integer. But for uninterpreted sorts it may work. |
Very good point. I need some time (and some spare cycles) to think about this. I'll let you know if I have some idea about that. |
Hi @jhoenicke,
while playing around with SMTInterpol and quantifiers, I found the following funny example:
I expected SMTInerpol to return
unsat
. However, it returnsunknown
. Unless I'm mistaken, that should be an EPR formula (variables occurring only below relations). So SMTInterpol should be complete there.Looking at the solver's output, it complains that:
If you don't have the time to take a look, I can give it a shot. But I'll need your help to confirm my analysis. My best guess is that there is a case missing in getQuantEquality.
The text was updated successfully, but these errors were encountered: