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

CVC5 Interpolation #293

Closed
baierd opened this issue Feb 1, 2023 · 7 comments · Fixed by #320
Closed

CVC5 Interpolation #293

baierd opened this issue Feb 1, 2023 · 7 comments · Fixed by #320

Comments

@baierd
Copy link
Collaborator

baierd commented Feb 1, 2023

CVC5 uses a different interpolation interpretation than what we support in our API. However, they can be transformed into one another.

We use the following definition of Craig-Interpolation:

For a pair of formulas φ− and φ+ such that φ− ∧ φ+ is
unsatisfiable, a Craig interpolant ψ is a formula that fulfills
the following requirements:

  1. the implication φ− ⇒ ψ holds,
  2. the conjunction ψ ∧ φ+ is unsatisfiable, and
  3. ψ only contains symbols that occur in both φ− and φ+.

In CVC5 φ− ⇒ ψ and ψ ⇒ φ+ are with φ+ and φ- being valid.
(Does valid mean SAT or UNSAT?!)

This means that if we negate φ+, we receive the correct interpolant under the assumption that its the same interpretation of satisfiablity.

We should test this.

@kfriedberger
Copy link
Member

In SMT theory, the validity of a formula is defined as "there is at least one satisfying model for it".

For this context, it might be better not to test it, but to proof it. Someones life might depend on it. 😃

@baierd
Copy link
Collaborator Author

baierd commented Mar 13, 2023

@nianzelee your input would be much appreciated.

@Po-Chun-Chien
Copy link
Member

In CVC5 φ− ⇒ ψ and ψ ⇒ φ+ are with φ+ and φ- being valid. (Does valid mean SAT or UNSAT?!)

@baierd What you have written here seems to deviate from their API documentation.

From the Javadoc of Solver#getInterpolant:

Returns:
A Term I such that A->I and I->B are valid, where A is the current set of assertions and B is given in the input by conj, or the null term if such a term cannot be found.

So, it should be the case that both A->I and I->B are valid, but NOT A and B are valid.
And in this context, a formula is valid iff it is true under every interpretation (cf. tautologies in propositional logic).

@baierd
Copy link
Collaborator Author

baierd commented Jul 11, 2023

I think that's how we interpreted it in our internal discussion.

Update on this issue: we are certain that the proposed changes above lead to the same interpolation procedure. @RSoegtrop currently works on implementing it the way described above.

@Po-Chun-Chien
Copy link
Member

I think that's how we interpreted it in our internal discussion.

Update on this issue: we are certain that the proposed changes above lead to the same interpolation procedure. @RSoegtrop currently works on implementing it the way described above.

Good to know. I really look forward to it.

@RSoegtrop
Copy link
Contributor

RSoegtrop commented Jul 13, 2023

@baierd Could you please review my take on CVC5InterpolatingProver? Interpolation and SequentialInterpolation should work. I left some ideas on TreeInterpolation and marked them as experimental.
Some Tests in InterpolatingProverTest fail to terminate (seem to get stuck in the CVC5 Interpolation API Call).

@kfriedberger
Copy link
Member

kfriedberger commented Jul 13, 2023

@RSoegtrop Could you create a proper pull-request for the code changes in your branch, such that a review can be performed via Github?

A first look: There is nearly no documentation, i.e., no comment on complex code and no JavaDoc for methods.

@RSoegtrop RSoegtrop linked a pull request Jul 18, 2023 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging a pull request may close this issue.

4 participants