Draft: Extend Truth based Solver/Prover Assertions#625
Draft: Extend Truth based Solver/Prover Assertions#625
Conversation
…tension based on Truth that allows for more than 1 BooleanFormula argument, intended for multiple assertions
…rgument, intended for multiple assertions
… multi BooleanFormula argument methods in some existing test-cases
kfriedberger
left a comment
kfriedberger
left a comment
There was a problem hiding this comment.
The idea to have a improved subject implementation is nice. I assume that the class is used in user-application, too, so we need to be carefully with API design.
We could support chained usage like:
assertThatFormulas(...).asConjunction().isSatisfiable().withModel(...)assertThatFormulas(...).asConjunction().isSatisfiable().withModelAssignment(x, 3).withModelAssignment(y, 5)assertThatFormulas(...).asConjunction().implies(...)assertThatFormulas(...).asDisjunction().implies(...)assertThatFormulas(...).asDisjunction().withTimeout(30).implies(...)- ...
Each command should read like natural language, and avoid technical parts.
I have not yet tried more examples, so I will not yet approve.
| constraints.add(imgr.lessOrEquals(symbol, four)); | ||
| } | ||
| assertThatFormula(bmgr.and(imgr.distinct(symbols), bmgr.and(constraints))).isSatisfiable(); | ||
| assertThatFormulas(imgr.distinct(symbols), bmgr.and(constraints)).isSatisfiable(); |
There was a problem hiding this comment.
I find that not very readable, because it seems to be a broken sentence:
assert that formulas A, B, C is satisfiable.
As a developer, I would need to look up whether one, any, all, or the conjunction of all formulas is actually checked.
Maybe find a new name for the method, such as assertThatConjunctionOf(...).isSatisfiable().
| */ | ||
| protected final BooleanFormulaSubjects assertThatFormulas( | ||
| BooleanFormula formula1, BooleanFormula formula2) { | ||
| return assertThatFormulas(ImmutableList.of(formula1, formula2)); |
There was a problem hiding this comment.
Why do we need the case for 2/3 formulas explicitly? Java allows var-args. Just use them.
|
|
||
| /** | ||
| * Use this for checking assertions about the conjunction of {@link BooleanFormula}s with Truth: | ||
| * <code>assertThatFormulas(Collection).are...()</code>. |
| smgr.prefix(prefix, concat), | ||
| smgr.suffix(suffix, concat), | ||
| imgr.equal(smgr.length(concat), imgr.add(smgr.length(prefix), smgr.length(suffix)))) | ||
| .imply(smgr.equal(concat, smgr.concat(prefix, suffix))); |
There was a problem hiding this comment.
The method imply points the developer towards any of those formulas implies, instead of conjunction of formula implies. Naming is not optimal here.
2 participants
I also noticed that it is helpful to have a
assertThat...implementation that actually uses multiple assertions, e.g. for HORN solving. A conjunction of multiple formulas is no equal to asserting them on their own for Z3! This PR is intended to discuss and implement extensions to our current API that only allows the assertion and solving/comparing of a singleBooleanFormula.Note: the current implementation is based on a
CollectionofBooleanFormulas. Instead, a conjunction could automatically be broken up using our conjunction flattening API. But i decided against this, as we might split formulas that we don't want to assert individually, and aCollectionbased approach seemed more easy to debug/maintain.Also, it is most likely a good idea to reflect how we add the assertions to the prover in the API name, but since the ending method, e.g.
isSatisfiable(), is actually controlling this, it seems weird to writeisSatisfiableAssertedIndiviually()or so. @kfriedberger do you know whether there is API to add in between? Something likeassertThatFormulas(collection).addedAsProverConstraintsIndividually().isSatisfiable()?Ideas: