diff options
author | Tim King <taking@cs.nyu.edu> | 2015-04-17 15:22:53 +0200 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2015-04-18 13:32:28 +0200 |
commit | 174e03832db4325d79880a2048aaad5c405ff699 (patch) | |
tree | f739b2428a8a2e9262e0d0b1fc77c04b5ec707ea /src/theory/arith/simplex.cpp | |
parent | 4d359ce4470c44c3e7532edb6b60bcb61b51f862 (diff) |
Farkas proof coefficients.
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);
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 46 |
1 files changed, 31 insertions, 15 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index b37f24d14..49664e0ea 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -20,12 +20,14 @@ #include "theory/arith/options.h" #include "theory/arith/constraint.h" + using namespace std; namespace CVC4 { namespace theory { namespace arith { + SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) : d_conflictVariables() , d_linEq(linEq) @@ -34,14 +36,23 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, , d_errorSet(errors) , d_numVariables(0) , d_conflictChannel(conflictChannel) + , d_conflictBuilder(NULL) , d_arithVarMalloc(tvmalloc) , d_errorSize(0) , d_zero(0) + , d_posOne(1) + , d_negOne(-1) { d_heuristicRule = options::arithErrorSelectionRule(); d_errorSet.setSelectionRule(d_heuristicRule); + d_conflictBuilder = new FarkasConflictBuilder(); } +SimplexDecisionProcedure::~SimplexDecisionProcedure(){ + delete d_conflictBuilder; +} + + bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) { TimerStat::CodeTimer codeTimer(timer); Assert( d_conflictVariables.empty() ); @@ -77,37 +88,34 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& void SimplexDecisionProcedure::reportConflict(ArithVar basic){ Assert(!d_conflictVariables.isMember(basic)); Assert(checkBasicForConflict(basic)); - RaiseConflict rc( d_conflictChannel); - generateConflictForBasic(basic, rc); + ConstraintCP conflicted = generateConflictForBasic(basic); + Assert(conflicted != NullConstraint); + d_conflictChannel.raiseConflict(conflicted); - // static bool verbose = false; - // if(verbose) { Message() << "conflict " << basic << " " << conflict << endl; } - // Assert(!conflict.isNull()); - //d_conflictChannel(conflict); - rc.commitConflict(); d_conflictVariables.add(basic); } -void SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic, RaiseConflict& rc) const { +ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const { Assert(d_tableau.isBasic(basic)); Assert(checkBasicForConflict(basic)); if(d_variables.cmpAssignmentLowerBound(basic) < 0){ Assert(d_linEq.nonbasicsAtUpperBounds(basic)); - return d_linEq.generateConflictBelowLowerBound(basic, rc); + return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder); }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){ Assert(d_linEq.nonbasicsAtLowerBounds(basic)); - return d_linEq.generateConflictAboveUpperBound(basic, rc); + return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder); }else{ Unreachable(); + return NullConstraint; } } bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const { if(checkBasicForConflict(basic)){ - RaiseConflict rc(d_conflictChannel); - generateConflictForBasic(basic, rc); + ConstraintCP conflicted = generateConflictForBasic(basic); + d_conflictChannel.raiseConflict(conflicted); return true; }else{ return false; @@ -183,9 +191,12 @@ void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar i } ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){ + Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl; + TimerStat::CodeTimer codeTimer(timer); Assert(!d_errorSet.focusEmpty()); - + Assert(debugIsASet(set)); + ArithVar inf = requestVariable(); Assert(inf != ARITHVAR_SENTINEL); @@ -199,8 +210,13 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time Assert(!d_variables.assignmentIsConsistent(e)); int sgn = d_errorSet.getSgn(e); - coeffs.push_back(Rational(sgn)); + Assert(sgn == -1 || sgn == 1); + const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne; + coeffs.push_back(violatedCoeff); variables.push_back(e); + + Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl; + } d_tableau.addRow(inf, coeffs, variables); DeltaRational newAssignment = d_linEq.computeRowValue(inf, false); @@ -210,7 +226,7 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf)); Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl; - + Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl; return inf; } |