Add Proper Yices2 Quantifier Support #447
Conversation
…k most solvers (now 152 tests run over all solvers compared to 89 before)
…bles for quantifiers
|
Note: this PR was created on 5.0.1, so that we can merge it into older feature branches. |
|
I could not find a canonical way of discerning the quantifier types from a quantified term. I currently use the string representation, which is not good. Maybe any one of you @kfriedberger or @daniel-raffler wants to try his luck? Note: you can get the type, but thats always |
…sable all tests without assertions or printouts
…che the free vars in the creator as retrieval by name from the solver is not reliable for variables that are also used in quantifiers
| + "as it would omit a variable with type '%s'", | ||
| name, yices_type_to_string(type), yices_type_to_string(termFromNameType))); | ||
| } | ||
| } |
There was a problem hiding this comment.
it looks like some ELSE-cases are missing. Is this intentional?
There was a problem hiding this comment.
This is intentional. I added documentation for it.
Essentially: Names work like a stack in Yices2. If we associate a term with a name, we get that term if we ask yices_get_term_by_name(). However, if we create bound variables, we associate them with the same name as the free variable (so that it has the same name). This pushes the name stack, and we get the bound var when asking yices_get_term_by_name(). That's why i added a cache for free vars. So this way we can re-use bound variables, and don't clash with free vars.
| } | ||
| BooleanFormula body = encapsulateBoolean(yices_term_child(pF, children - 1)); | ||
| Quantifier quant = Quantifier.EXISTS; | ||
| if (yices_term_to_string(pF).startsWith("(forall")) { |
There was a problem hiding this comment.
Yices is open source. We could find out, how Yices computes the string and check for the flag that tells the difference from FORALL to EXISTS:
There was a problem hiding this comment.
Yices does not seem to have a separate term for exists:
term_t mk_exists(term_manager_t *manager, uint32_t n, const term_t var[], term_t body) {
if (body == true_term) return body;
if (body == false_term) return body;
// (not (forall ... (not body))
return opposite_term(forall_term(manager->terms, n, var, opposite_term(body)));
}
To see if we have a forall or an exists we'd have to check the polarity of the term. Yices does this internally with a simple bitmask:
static inline uint32_t polarity_of(term_t x) {
return ((uint32_t) x) & 1;
}
I couldn't find any public API for this, but we could probably just keep track of the polarity in the visitor.
There was a problem hiding this comment.
No actually that is the solution! Thank you very much!
exists is negated and we can check that.
This opens another questions however: do we traverse and/or rebuild terms correctly with this?
Do we have a test for exists that manipulates the formula? If not, we need to add one!
There was a problem hiding this comment.
(I fear that the visitor might rebuild a formula exists x x=y into not(forall x x=y), which is not equal.)
| @@ -201,6 +204,8 @@ public void rationalError() { | |||
| System.out.println(rat); // "use" variable | |||
| } | |||
|
|
|||
| // TODO: what is this test supposed to be doing? And remove print. | |||
| @Ignore | |||
There was a problem hiding this comment.
Most of those tests are simply tests for loading and running Yices. They serves as examples and were helpful for debugging initial issues. If the tests do no longer bring benefit, please remove them, and do not just disable them.
There was a problem hiding this comment.
I reworked all tests with printouts into assertions and re-enabled all. I also found some issues and fixed them, added documentation and 2 more native tests.
| int var = yices_new_uninterpreted_term(type); | ||
| yices_set_term_name(var, name); | ||
| return var; | ||
| } |
There was a problem hiding this comment.
This IF-THEN-ELSE logic seems to be used twice. Can we refactor it into a proper utility method?
There was a problem hiding this comment.
Only parts of the structure is reused. This version is for tests and for free variables only. The other one is for bound variables and has additional logic. (I reworked the creation of free vars and its not similar to this one anymore)
This PR adds proper support for quantified formulas in Yices2.
Proper substitution of unbound with bound variables was added.
The
QuantifiedFormulaManageris now available publicly.Also, the quantifier tests were refactored, so that the automatic setup does not block most tests.