if(d_partialModel.belowLowerBound(x_i, c_i, true)){
return Node::null();
}
- // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){
- // TNode prevConstraint = d_partialModel.getLowerConstraint(x_i);
- // if(prevConstraint.getKind() == EQUAL){
- // return Node::null();
- // }else{
- // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl;
- // Assert(prevConstraint.getKind() == AND);
- // d_partialModel.setLowerConstraint(x_i,original);
- // return Node::null();
- // }
- // }
if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
Node ubc = d_partialModel.getUpperConstraint(x_i);
return Node::null(); //sat
}
- // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){
- // TNode prevConstraint = d_partialModel.getUpperConstraint(x_i);
- // if(prevConstraint.getKind() == EQUAL){
- // return Node::null();
- // }else{
- // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl;
- // Assert(prevConstraint.getKind() == AND);
- // d_partialModel.setUpperConstraint(x_i,original);
- // return Node::null();
- // }
- // }
if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
Node lbc = d_partialModel.getLowerConstraint(x_i);
Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original);
}
void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){
bool success = false;
- if(d_partialModel.strictlyAboveLowerBound(basic) &&
- (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) &&
- hasLowerBounds(basic)){
+ if(d_partialModel.strictlyAboveLowerBound(basic) && hasLowerBounds(basic)){
++d_statistics.d_boundComputations;
success |= propagateCandidateLowerBound(basic);
}
- if(d_partialModel.strictlyBelowUpperBound(basic) &&
- (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) &&
- hasUpperBounds(basic)){
+ if(d_partialModel.strictlyBelowUpperBound(basic) && hasUpperBounds(basic)){
++d_statistics.d_boundComputations;
success |= propagateCandidateUpperBound(basic);
}
if(!possibleConflict.isNull()){
return possibleConflict;
}
- // if(selectSlackUpperBound<pf>(x_j) == ARITHVAR_SENTINEL){
- // Node possibleConflict = deduceUpperBound(x_j);
- // if(!possibleConflict.isNull()){
- // return possibleConflict;
- // }
- // }
- // if(selectSlackLowerBound<pf>(x_j) == ARITHVAR_SENTINEL){
- // Node possibleConflict = deduceLowerBound(x_j);
- // if(!possibleConflict.isNull()){
- // return possibleConflict;
- // }
- // }
}
}
Assert(remainingIterations == 0);
}
-// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){
-// TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
-
-// bool anyWeakenings = false;
-// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-// Assert(d_partialModel.hasLowerBound(basicVar));
-// Assert(assignment < d_partialModel.getLowerBound(basicVar));
-
-// DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment;
-
-// vector<WeakeningElem> weakeningElements;
-// queue<uint32_t> potentialWeakingings;
-// for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
-// const TableauEntry& entry = *i;
-// ArithVar v = entry.getColVar();
-// const Rational& coeff = entry.getCoefficient();
-
-// int sgn = coeff.sgn();
-// bool ub = (sgn > 0);
-// Node exp = ub ?
-// d_partialModel.getUpperConstraint(v) :
-// d_partialModel.getLowerConstraint(v);
-// DeltaRational bound = ub?
-// d_partialModel.getUpperBound(v) :
-// d_partialModel.getLowerBound(v);
-// potentialWeakingings.push(weakeningElements.size());
-// weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp));
-// }
-
-// vector<Node> conflict;
-
-// Debug("weak") << "weakenLowerBoundConflict" << endl;
-// while(!potentialWeakingings.empty()){
-// uint32_t pos = potentialWeakingings.front();
-// potentialWeakingings.pop();
-
-// WeakeningElem& curr = weakeningElements[pos];
-
-// Node weaker = curr.upperBound?
-// d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound):
-// d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound);
-
-// bool weakened = false;
-// if(!weaker.isNull()){
-// DeltaRational weakerBound = asDeltaRational(weaker);
-// DeltaRational diff = weakerBound - curr.bound;
-// //if var == basic, weakerBound < curr.bound
-// // multiply by -1
-// diff = diff * (*curr.coeff);
-
-// if(surplus > diff){
-// ++d_statistics.d_weakenings;
-// anyWeakenings = true;
-// weakened = true;
-// surplus = surplus - diff;
-
-// Debug("weak") << "found:" << endl;
-// if(curr.var == basicVar){
-// Debug("weak") << " basic: ";
-// }
-// Debug("weak") << " " << surplus << " "<< diff << endl
-// << " " << curr.bound << weakerBound << endl
-// << " " << curr.explanation << weaker << endl;
-
-// if(curr.explanation.getKind() == AND){
-// Debug("weak") << "VICTORY" << endl;
-// }
-
-// Assert(diff > d_DELTA_ZERO);
-// curr.explanation = weaker;
-// curr.bound = weakerBound;
-// }
-// }
-
-// if(weakened){
-// potentialWeakingings.push(pos);
-// }else{
-// if(curr.explanation.getKind() == AND){
-// Debug("weak") << "boo: " << curr.explanation << endl;
-// }
-// conflict.push_back(curr.explanation);
-// }
-// }
-
-// ++d_statistics.d_weakeningAttempts;
-// if(anyWeakenings){
-// ++d_statistics.d_weakeningSuccesses;
-// }
-
-// NodeBuilder<> nb(AND);
-// nb.append(conflict);
-// return nb;
-// }
-
-// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){
-// Assert(d_tableau.isBasic(basicVar));
-// Assert(selectSlackUpperBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
-
-// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-
-// Assert(assignment.getInfinitesimalPart() <= 0);
-
-// if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){
-// NodeBuilder<> nb(kind::AND);
-// explainNonbasicsUpperBound(basicVar, nb);
-// Node explanation = maybeUnaryConvert(nb);
-// Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl;
-// Node res = AssertUpper(basicVar, assignment, explanation);
-// if(res.isNull()){
-// d_propManager.propagateArithVar(true, basicVar, assignment, explanation);
-// }
-// return res;
-// }else{
-// return Node::null();
-// }
-// }
-
-// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){
-// Assert(d_tableau.isBasic(basicVar));
-// Assert(selectSlackLowerBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
-// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-
-// if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
-
-// Assert(assignment.getInfinitesimalPart() >= 0);
-
-// if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){
-// NodeBuilder<> nb(kind::AND);
-// explainNonbasicsLowerBound(basicVar, nb);
-// Node explanation = maybeUnaryConvert(nb);
-// Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl;
-// Node res = AssertLower(basicVar, assignment, explanation);
-// if(res.isNull()){
-// d_propManager.propagateArithVar(false, basicVar, assignment, explanation);
-// }
-// return res;
-// }else{
-// return Node::null();
-// }
-// }
-
Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){
return weakenConflict(true, conflictVar);
}
if(!possibleConflict.isNull()){
d_partialModel.revertAssignmentChanges();
- //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict);
-
Debug("arith::conflict") << "conflict " << possibleConflict << endl;
-
d_simplex.clearUpdates();
d_out->conflict(possibleConflict);
return;
if(possibleConflict != Node::null()){
d_partialModel.revertAssignmentChanges();
d_simplex.clearUpdates();
-
- //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict);
-
Debug("arith::conflict") << "conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
-
- // // < => !>
- // Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode();
- // // < => !=
- // Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode();
- // // > => !=
- // Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode();
- // // All the implication
- // Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
-
++(d_statistics.d_statDisequalitySplits);
d_out->lemma(lemma);
}
}
}
-/*
-bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){
- Node varAsNode = asNode(var);
- const DeltaRational& ub = d_partialModel.getUpperBound(var);
- Assert(ub.getInfinitesimalPart() <= 0 );
- Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ;
- Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart());
- Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode);
-
- return bestImplied == exp;
-}
-
-bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){
- Node varAsNode = asNode(var);
- const DeltaRational& lb = d_partialModel.getLowerBound(var);
- Assert(lb.getInfinitesimalPart() >= 0 );
- Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ;
- Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart());
- Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq);
- return bestImplied == exp;
-}
-*/
-
void TheoryArith::explain(TNode n) {
Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
- //Assert(n.hasAttribute(Propagated()));
- //NodeBuilder<> explainBuilder(AND);
- //internalExplain(n,explainBuilder);
Assert(d_propManager.isPropagated(n));
Node explanation = d_propManager.explain(n);
- //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation);
-
d_out->explanation(explanation, true);
}
-/*
-void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){
- Assert(n.hasAttribute(Propagated()));
- Node bound = n.getAttribute(Propagated());
-
- AlwaysAssert(bound.getKind() == kind::AND);
-
- for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){
- Node lit = *i;
- if(lit.hasAttribute(Propagated())){
- cout << "hoop the sadjklasdj" << endl;
- internalExplain(lit, explainBuilder);
- }else{
- explainBuilder << lit;
- }
- }
-}
-*/
-/*
-static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false;
-void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){
- Node varAsNode = asNode(var);
- const DeltaRational& b = upperbound ?
- d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var);
-
- Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
- Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
- Kind kind;
- if(upperbound){
- kind = b.getInfinitesimalPart() < 0 ? LT : LEQ;
- } else{
- kind = b.getInfinitesimalPart() > 0 ? GT : GEQ;
- }
-
- Node bAsNode = NodeBuilder<2>(kind) << varAsNode
- << mkRationalNode(b.getNoninfinitesimalPart());
-
- Node bestImplied = upperbound ?
- d_propagator.getBestImpliedUpperBound(bAsNode):
- d_propagator.getBestImpliedLowerBound(bAsNode);
-
- if(!bestImplied.isNull()){
- Node satValue = d_valuation.getSatValue(bestImplied);
- if(satValue.isNull()){
-
- Node reason = upperbound ?
- d_partialModel.getUpperConstraint(var) :
- d_partialModel.getLowerConstraint(var);
-
- //cout << getContext()->getLevel() << " " << bestImplied << " " << reason << endl;
- if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){
- Node lemma = NodeBuilder<2>(IMPLIES) << reason
- << bestImplied;
-
- //Temporary
- Node clause = BooleanSimplification::simplifyHornClause(lemma);
- d_out->lemma(clause);
- }else{
- Assert(!bestImplied.hasAttribute(Propagated()));
- bestImplied.setAttribute(Propagated(), reason);
- d_reasons.push_back(reason);
- d_out->propagate(bestImplied);
- }
- }else{
- Assert(!satValue.isNull());
- Assert(satValue.getKind() == CONST_BOOLEAN);
- Assert(satValue.getConst<bool>());
- }
- }
-}
-*/
void TheoryArith::propagate(Effort e) {
if(quickCheckOrMore(e)){
if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
++d_restartsCounter;
- /*
- if(d_restartsCounter % d_tableauResetPeriod == 0){
- double currentDensity = d_tableau.densityMeasure();
- d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity);
- if(currentDensity >= d_tableauResetDensity * d_initialDensity){
-
- ++d_statistics.d_tableauResets;
- d_tableauResetPeriod += s_TABLEAU_RESET_INCREMENT;
- d_tableauResetDensity += .2;
- d_tableau = d_initialTableau;
- }
- }
- */
+
static const bool debugResetPolicy = false;
uint32_t currSize = d_tableau.size();
projects / cvc5.git / commitdiff