d_hasSafeAssignment[x] = true;
d_history.push_back(x);
}
+
+ d_deltaIsSafe = false;
d_assignment[x] = r;
}
void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
d_history.push_back(x);
}
}
+
+ d_deltaIsSafe = false;
d_assignment[x] = r;
}
/** Must know that the bound exists both calling this! */
const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
Assert(inMaps(x));
- Assert(!d_upperConstraint[x].isNull());
+ Assert(hasUpperBound(x));
return d_upperBound[x];
}
const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
Assert(inMaps(x));
- Assert(!d_lowerConstraint[x].isNull());
+ Assert(hasLowerBound(x));
return d_lowerBound[x];
}
}
}
+const DeltaRational& ArithPartialModel::getAssignment(ArithVar x, bool safe) const{
+ Assert(inMaps(x));
+ if(safe && d_hasSafeAssignment[x]){
+ return d_safeAssignment[x];
+ }else{
+ return d_assignment[x];
+ }
+}
+
const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
Assert(inMaps(x));
return d_assignment[x];
TNode ArithPartialModel::getLowerConstraint(ArithVar x){
Assert(inMaps(x));
- Assert(!d_lowerConstraint[x].isNull());
+ Assert(hasLowerBound(x));
return d_lowerConstraint[x];
}
TNode ArithPartialModel::getUpperConstraint(ArithVar x){
Assert(inMaps(x));
- Assert(!d_upperConstraint[x].isNull());
+ Assert(hasUpperBound(x));
return d_upperConstraint[x];
}
bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
- if(d_lowerConstraint[x].isNull()){
+ if(!hasLowerBound(x)){
// l = -\intfy
// ? c < -\infty |- _|_
return false;
}
bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
- if(d_upperConstraint[x].isNull()){
+ if(!hasUpperBound(x)){
// u = \intfy
// ? c > \infty |- _|_
return false;
return c >= d_upperBound[x];
}
}
-
-bool ArithPartialModel::hasBounds(ArithVar x){
- return !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
+bool ArithPartialModel::hasEitherBound(ArithVar x){
+ return hasLowerBound(x) || hasUpperBound(x);
}
bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
Assert(inMaps(x));
- if(d_upperConstraint[x].isNull()){ // u = \infty
+ if(!hasUpperBound(x)){ // u = \infty
return true;
}
return d_assignment[x] < d_upperBound[x];
bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
Assert(inMaps(x));
- if(d_lowerConstraint[x].isNull()){ // l = -\infty
+ if(!hasLowerBound(x)){ // l = -\infty
return true;
}
return d_lowerBound[x] < d_assignment[x];
}
}
+ if(revert && !d_history.empty()){
+ d_deltaIsSafe = true;
+ }
+
d_history.clear();
}
void ArithPartialModel::printModel(ArithVar x){
Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
- if(d_lowerConstraint[x].isNull()){
+ if(!hasLowerBound(x)){
Debug("model") << "no lb ";
}else{
Debug("model") << getLowerBound(x) << " ";
Debug("model") << getLowerConstraint(x) << " ";
}
- if(d_upperConstraint[x].isNull()){
+ if(!hasUpperBound(x)){
Debug("model") << "no ub ";
}else{
Debug("model") << getUpperBound(x) << " ";
for(ArithVar x = 0; x < d_mapSize; ++x){
const DeltaRational& a = getAssignment(x);
- if(!d_lowerConstraint[x].isNull()){
+ if(hasLowerBound(x)){
const DeltaRational& l = getLowerBound(x);
deltaIsSmallerThan(l,a);
}
- if(!d_upperConstraint[x].isNull()){
+ if(hasUpperBound(x)){
const DeltaRational& u = getUpperBound(x);
deltaIsSmallerThan(a,u);
}
bool TheoryArith::shouldEject(ArithVar var){
- if(d_partialModel.hasBounds(var)){
+ if(d_partialModel.hasEitherBound(var)){
return false;
}else if(d_tableau.isEjected(var)) {
return false;
d_tableau.reinjectBasic(x);
- DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x);
- DeltaRational assignment = computeRowValueUsingAssignment(x);
+ DeltaRational safeAssignment = computeRowValue(x, true);
+ DeltaRational assignment = computeRowValue(x, false);
d_partialModel.setAssignment(x,safeAssignment,assignment);
}
//This can go away if the tableau creation is done at preregister
//time instead of register
- DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x);
- DeltaRational assignment = computeRowValueUsingAssignment(x);
+ DeltaRational safeAssignment = computeRowValue(x, true);
+ DeltaRational assignment = computeRowValue(x, false);
d_partialModel.initialize(x,safeAssignment);
d_partialModel.setAssignment(x,assignment);
//lower bound. This is done to strongly enforce the notion that basic
//variables should not be changed without begin checked.
- //Strictly speaking checking x is unnessecary as it cannot have an upper or
- //lower bound. This is done to strongly enforce the notion that basic
- //variables should not be changed without begin checked.
-
}
Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
};
/**
* Computes the value of a basic variable using the current assignment.
*/
-DeltaRational TheoryArith::computeRowValueUsingAssignment(ArithVar x){
+DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
Assert(d_basicManager.isBasic(x));
DeltaRational sum = d_constants.d_ZERO_DELTA;
for(Row::iterator i = row->begin(); i != row->end();++i){
ArithVar nonbasic = i->first;
const Rational& coeff = i->second;
- const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic);
- sum = sum + (assignment * coeff);
- }
- return sum;
-}
-
-/**
- * Computes the value of a basic variable using the current assignment.
- */
-DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(ArithVar x){
- Assert(d_basicManager.isBasic(x));
- DeltaRational sum = d_constants.d_ZERO_DELTA;
- Row* row = d_tableau.lookup(x);
- for(Row::iterator i = row->begin(); i != row->end();++i){
- ArithVar nonbasic = i->first;
- const Rational& coeff = i->second;
- const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic);
+ const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
sum = sum + (assignment * coeff);
}
return sum;
}
+
RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
return d_nextRewriter.preRewrite(n);
}
}
/* procedure AssertUpper( x_i <= c_i) */
-bool TheoryArith::AssertUpper(TNode n, TNode original){
- TNode nodeX_i = n[0];
- ArithVar x_i = asArithVar(nodeX_i);
- Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
- DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
-
+bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
}
/* procedure AssertLower( x_i >= c_i ) */
-bool TheoryArith::AssertLower(TNode n, TNode original){
- TNode nodeX_i = n[0];
- ArithVar x_i = asArithVar(nodeX_i);
- Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
- DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
-
+bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
}
/* procedure AssertLower( x_i == c_i ) */
-bool TheoryArith::AssertEquality(TNode n, TNode original){
- Assert(n.getKind() == EQUAL);
- TNode nodeX_i = n[0];
- ArithVar x_i = asArithVar(nodeX_i);
- DeltaRational c_i(n[1].getConst<Rational>());
+bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
return false;
}
-void TheoryArith::update(ArithVar x_i, DeltaRational& v){
+void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
Assert(!d_basicManager.isBasic(x_i));
DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
++(d_statistics.d_statUpdates);
return conflict;
}
+template <bool selectLeft>
+TNode getSide(TNode assertion, Kind simpleKind){
+ switch(simpleKind){
+ case LT:
+ case GT:
+ case DISTINCT:
+ return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
+ case LEQ:
+ case GEQ:
+ case EQUAL:
+ return selectLeft ? assertion[0] : assertion[1];
+ default:
+ Unreachable();
+ return TNode::null();
+ }
+}
-//TODO get rid of this!
-Node TheoryArith::simulatePreprocessing(TNode n){
- if(n.getKind() == NOT){
- Node sub = simulatePreprocessing(n[0]);
- Assert(sub.getKind() != NOT);
- return NodeManager::currentNM()->mkNode(NOT,sub);
+ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
+ TNode left = getSide<true>(assertion, simpleKind);
+ if(isTheoryLeaf(left)){
+ return asArithVar(left);
}else{
- Assert(isNormalAtom(n));
- Kind k = n.getKind();
-
- Assert(isRelationOperator(k));
- if(n[0].getMetaKind() == metakind::VARIABLE){
- return n;
- }else {
- TNode left = n[0];
- TNode right = n[1];
- Assert(left.hasAttribute(Slack()));
- Node slack = left.getAttribute(Slack());
- return NodeManager::currentNM()->mkNode(k,slack,right);
- }
+ Assert(left.hasAttribute(Slack()));
+ TNode slack = left.getAttribute(Slack());
+ return asArithVar(slack);
}
}
-bool TheoryArith::assertionCases(TNode original, TNode assertion){
- switch(assertion.getKind()){
+DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
+ TNode right = getSide<false>(assertion, simpleKind);
+
+ Assert(right.getKind() == CONST_RATIONAL);
+ const Rational& noninf = right.getConst<Rational>();
+
+ Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
+ return DeltaRational(noninf, inf);
+}
+
+bool TheoryArith::assertionCases(TNode assertion){
+ Kind simpKind = simplifiedKind(assertion);
+ Assert(simpKind != UNDEFINED_KIND);
+ ArithVar x_i = determineLeftVariable(assertion, simpKind);
+ DeltaRational c_i = determineRightConstant(assertion, simpKind);
+
+ Debug("arith_assertions") << "arith assertion(" << assertion
+ << " \\-> "
+ <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
+ switch(simpKind){
case LEQ:
- return AssertUpper(assertion, original);
+ case LT:
+ return AssertUpper(x_i, c_i, assertion);
+ case GT:
case GEQ:
- return AssertLower(assertion, original);
+ return AssertLower(x_i, c_i, assertion);
case EQUAL:
- return AssertEquality(assertion,original);
- case NOT:
- {
- TNode atom = assertion[0];
- switch(atom.getKind()){
- case LEQ: //(not (LEQ x c)) <=> (GT x c)
- {
- Node pushedin = pushInNegation(assertion);
- return AssertLower(pushedin,original);
- }
- case GEQ: //(not (GEQ x c) <=> (LT x c)
- {
- Node pushedin = pushInNegation(assertion);
- return AssertUpper(pushedin,original);
- }
- case EQUAL:
- d_diseq.push_back(assertion);
- return false;
- default:
- Unreachable();
- return false;
- }
- }
+ return AssertEquality(x_i, c_i, assertion);
+ case DISTINCT:
+ d_diseq.push_back(assertion);
+ return false;
default:
Unreachable();
return false;
while(!done()){
- Node original = get();
- Node assertion = simulatePreprocessing(original);
- Debug("arith_assertions") << "arith assertion(" << original
- << " \\-> " << assertion << ")" << std::endl;
-
- d_propagator.assertLiteral(original);
- bool conflictDuringAnAssert = assertionCases(original, assertion);
+ Node assertion = get();
+ d_propagator.assertLiteral(assertion);
+ bool conflictDuringAnAssert = assertionCases(assertion);
if(conflictDuringAnAssert){
d_partialModel.revertAssignmentChanges();
*
* returns true if a conflict was asserted.
*/
- bool AssertLower(TNode n, TNode orig);
- bool AssertUpper(TNode n, TNode orig);
+ bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+ bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+ bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+
+ ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
- bool AssertEquality(TNode n, TNode orig);
/**
* Updates the assignment of a nonbasic variable x_i to v.
* Also updates the assignment of basic variables accordingly.
*/
- void update(ArithVar x_i, DeltaRational& v);
+ void update(ArithVar x_i, const DeltaRational& v);
/**
* Updates the value of a basic variable x_i to v,
/** Initial (not context dependent) sets up for a new slack variable.*/
void setupSlack(TNode left);
-
- /** Computes the value of a row in the tableau using the current assignment.*/
- DeltaRational computeRowValueUsingAssignment(ArithVar x);
-
- /** Computes the value of a row in the tableau using the safe assignment.*/
- DeltaRational computeRowValueUsingSavedAssignment(ArithVar x);
+ /**
+ * Computes the value of a basic variable using the assignments
+ * of the values of the variables in the basic variable's row tableau.
+ * This can compute the value using either:
+ * - the the current assignment (useSafe=false) or
+ * - the safe assignment (useSafe = true).
+ */
+ DeltaRational computeRowValue(ArithVar x, bool useSafe);
/** Checks to make sure the assignment is consistent with the tableau. */
void checkTableau();
* Handles the case splitting for check() for a new assertion.
* returns true if their is a conflict.
*/
- bool assertionCases(TNode original, TNode assertion);
+ bool assertionCases(TNode assertion);
ArithVar findBasicRow(ArithVar variable);
bool shouldEject(ArithVar var);
void ejectInactiveVariables();
void reinjectVariable(ArithVar x);
- //TODO get rid of this!
- Node simulatePreprocessing(TNode n);
-
void asVectors(Polynomial& p,
std::vector<Rational>& coeffs,
std::vector<ArithVar>& variables) const;
projects / cvc5.git / commitdiff