- This increases the number of substitutions that ppAssert can solve on integer equations.
if(l.leadingCoefficientIsPositive()){ // (< x c)
return UpperBound;
}else{
- return LowerBound; // (< (-x) c)
+ return LowerBound; // (< (-x) c)
}
}
case GT:
}else{
pair<SortedConstraintMapIterator, bool> negInsertAttempt;
negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
- Assert(negInsertAttempt.second);
+ Assert(negInsertAttempt.second
+ || ! negInsertAttempt.first->second.hasConstraintOfType(negC->getType()));
negPos = negInsertAttempt.first;
}
bool isUpperBound() const{
return d_type == UpperBound;
}
+ bool isStrictUpperBound() const{
+ Assert(isUpperBound());
+ return getValue().infinitesimalSgn() < 0;
+ }
+
+ bool isStrictLowerBound() const{
+ Assert(isLowerBound());
+ return getValue().infinitesimalSgn() > 0;
+ }
bool isSplit() const {
return d_split;
/**
* Light wrapper for calling setCanBePropagated(),
- * on this and this-d_negation.
+ * on this and this->d_negation.
*/
void setPreregistered(){
setCanBePropagated();
Assert(d_tableau.isBasic(basic));
Assert(c->getVariable() == basic);
Assert(!c->assertedToTheTheory());
- Assert(c->canBePropagated());
+ //Assert(c->canBePropagated());
Assert(!c->hasProof());
Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
if(upperBound){
if(sgn < 0){
bound = d_partialModel.getLowerBoundConstraint(nonbasic);
- //d_partialModel.explainLowerBound(nonbasic, output);
- //bound = d_partialModel.explainLowerBound(nonbasic);
}else{
Assert(sgn > 0);
bound = d_partialModel.getUpperBoundConstraint(nonbasic);
- //d_partialModel.explainUpperBound(nonbasic, output);
- //bound = d_partialModel.explainUpperBound(nonbasic);
}
}else{
if(sgn < 0){
bound = d_partialModel.getUpperBoundConstraint(nonbasic);
- //d_partialModel.explainUpperBound(nonbasic, output);
- //bound = d_partialModel.explainUpperBound(nonbasic);
}else{
Assert(sgn > 0);
bound = d_partialModel.getLowerBoundConstraint(nonbasic);
- //d_partialModel.explainLowerBound(nonbasic, output);
- //bound = d_partialModel.explainLowerBound(nonbasic);
}
}
Assert(bound != NullConstraint);
Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
bounds.push_back(bound);
- //Assert(!bound.isNull());
- // Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
- // << endl;
- // output << bound;
}
- c->propagate(bounds);
+ c->impliedBy(bounds);
Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
<< basic << ") done" << endl;
}
static const uint32_t VARORDER_CHECK_PERIOD = 200;
SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) :
+ d_conflictVariable(ARITHVAR_SENTINEL),
d_linEq(linEq),
d_partialModel(d_linEq.getPartialModel()),
d_tableau(d_linEq.getTableau()),
bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime);
+ Assert(d_successes.empty());
switch(type){
case BeforeDiffSearch: ++(d_statistics.d_attemptBeforeDiffSearch); break;
case AfterVarOrderSearch: ++(d_statistics.d_attemptAfterVarOrderSearch); break;
}
- bool success = false;
ArithPriorityQueue::const_iterator i = d_queue.begin();
ArithPriorityQueue::const_iterator end = d_queue.end();
for(; i != end; ++i){
ArithVar x_i = *i;
- if(d_tableau.isBasic(x_i)){
+ if(x_i != d_conflictVariable && d_tableau.isBasic(x_i) && !d_successes.isMember(x_i)){
Node possibleConflict = checkBasicForConflict(x_i);
if(!possibleConflict.isNull()){
- success = true;
+ d_successes.add(x_i);
reportConflict(possibleConflict);
}
}
}
- if(success){
+ if(!d_successes.empty()){
switch(type){
case BeforeDiffSearch: ++(d_statistics.d_successBeforeDiffSearch); break;
case DuringDiffSearch: ++(d_statistics.d_successDuringDiffSearch); break;
case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break;
case AfterVarOrderSearch: ++(d_statistics.d_successAfterVarOrderSearch); break;
}
+ d_successes.purge();
+ return true;
+ }else{
+ return false;
}
- return success;
}
bool SimplexDecisionProcedure::findModel(){
+ Assert(d_conflictVariable == ARITHVAR_SENTINEL);
+
if(d_queue.empty()){
return false;
}
// means that the assignment we can always empty these queues.
d_queue.clear();
d_pivotsInRound.purge();
+ d_conflictVariable = ARITHVAR_SENTINEL;
Assert(!d_queue.inCollectionMode());
d_queue.transitionToCollectionMode();
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
Node conflict = generateConflictBelowLowerBound(x_i); //unsat
+ d_conflictVariable = x_i;
reportConflict(conflict);
return true;
}
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
Node conflict = generateConflictAboveUpperBound(x_i); //unsat
+
+ d_conflictVariable = x_i;
reportConflict(conflict);
return true;
}
if(CHECK_AFTER_PIVOT){
Node possibleConflict = checkBasicForConflict(x_j);
if(!possibleConflict.isNull()){
+ d_conflictVariable = x_j;
reportConflict(possibleConflict);
return true; // unsat
}
class SimplexDecisionProcedure {
private:
+ ArithVar d_conflictVariable;
+ DenseSet d_successes;
/** Linear equality module. */
LinearEqualityModule& d_linEq;
TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
+//TODO: Handle this better
+// FAIL: preprocess_10.cvc (exit: 1)
+// =================================
+
+// running /home/taking/ws/cvc4/branches/arithmetic/infer-bounds/builds/x86_64-unknown-linux-gnu/debug-staticbinary/src/main/cvc4 --lang=cvc4 --segv-nospin preprocess_10.cvc [from working dir /home/taking/ws/cvc4/branches/arithmetic/infer-bounds/builds/x86_64-unknown-linux-gnu/debug-staticbinary/../../../test/regress/regress0/preprocess]
+// run_regression: error: differences between expected and actual output on stdout
+// --- /tmp/cvc4_expect_stdout.20298.5Ga5123F4L 2012-04-30 12:27:16.136684359 -0400
+// +++ /tmp/cvc4_stdout.20298.oZwTuIYuF3 2012-04-30 12:27:16.176685543 -0400
+// @@ -1 +1,3 @@
+// +TheoryArith::solve(): substitution x |-> IF b THEN 10 ELSE -10 ENDIF
+// +minVar is integral 0right 0
+// sat
+
+
// Solve equalities
Rational minConstant = 0;
Node minMonomial;
if (m.getVarList().singleton()){
VarList vl = m.getVarList();
Node var = vl.getNode();
- if (var.getKind() == kind::VARIABLE && !vl.isIntegral()) {
- minVar = var;
+ if (var.getKind() == kind::VARIABLE){
+ // if vl.isIntegral then m.getConstant().isOne()
+ if(!vl.isIntegral() || m.getConstant().isOne()){
+ minVar = var;
+ }
}
}
- //Assert(in[1].getKind() == kind::CONST_RATIONAL);
- // Find the variable with the smallest coefficient
- //Polynomial p = Polynomial::parsePolynomial(in[0]);
-
- // Polynomial::iterator it = p.begin(), it_end = p.end();
- // for (; it != it_end; ++ it) {
- // Monomial m = *it;
- // // Skip the constant
- // if (m.isConstant()) continue;
- // // This is a ''variable''
- // nVars ++;
- // // Skip the non-linear stuff
- // if (!m.getVarList().singleton()) continue;
- // // Get the minimal one
- // Rational constant = m.getConstant().getValue();
- // Rational absSconstant = constant > 0 ? constant : -constant;
- // if (minVar.isNull() || absSconstant < minConstant) {
- // Node var = m.getVarList().getNode();
- // if (var.getKind() == kind::VARIABLE) {
- // minVar = var;
- // minMonomial = m.getNode();
- // minConstant = constant;
- // }
- // }
- //}
-
// Solve for variable
if (!minVar.isNull()) {
Polynomial right = cmp.getRight();
- Node eliminateVar = right.getNode();
+ Node elim = right.getNode();
// ax + p = c -> (ax + p) -ax - c = -ax
- // Node eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, in[0], minMonomial);
- // if (in[1].getConst<Rational>() != 0) {
- // eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, eliminateVar, in[1]);
- // }
- // // x = (p - ax - c) * -1/a
- // eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse()));
- // // Add the substitution if not recursive
- Node rewritten = eliminateVar;
- Assert(rewritten == Rewriter::rewrite(eliminateVar));
- if (!rewritten.hasSubterm(minVar)) {
- Node elim = Rewriter::rewrite(eliminateVar);
- if (!minVar.getType().isInteger() || elim.getType().isInteger()) {
- // cannot eliminate integers here unless we know the resulting
- // substitution is integral
- Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
- outSubstitutions.addSubstitution(minVar, elim);
- return PP_ASSERT_STATUS_SOLVED;
- } else {
- Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
- }
+ // x = (p - ax - c) * -1/a
+ // Add the substitution if not recursive
+ Assert(elim == Rewriter::rewrite(elim));
+ Assert(!elim.hasSubterm(minVar));
+
+ if (!minVar.getType().isInteger() || right.isIntegral()) {
+ // cannot eliminate integers here unless we know the resulting
+ // substitution is integral
+ Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
+
+ outSubstitutions.addSubstitution(minVar, elim);
+ return PP_ASSERT_STATUS_SOLVED;
+ } else {
+ Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
}
}
}
}
+bool TheoryArith::rowImplication(ArithVar v, bool upperBound, const DeltaRational& r){
+ Unimplemented();
+ return false;
+}
+
bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
++d_statistics.d_boundComputations;
*/
class TheoryArith : public Theory {
private:
+ bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
/**
* This counter is false if nothing has been done since the last cut.