| Age | Commit message (Collapse) | Author |
|---|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.
Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
There was a way to use a row twice in the construction of the conflicts.
This was violating an assumption in the Tableau when constructing the intermediate rows.
Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
before they are converted to externally understandable conflicts and propagations in the form
of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
to the impliedByX (and similar functions).
For example,this is now longer both:
void setAssertedToTheTheory(TNode witness);
void setAssertedToTheTheoryWithNegationTrue(TNode witness);
There is just:
void setAssertedToTheTheory(TNode witness, bool inConflict);
|
|
|
|
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
|
|
|
|
removing an ugly forward declaration that was needed to get error set bound information on basic variables.
|
|
|
