--- /dev/null
+/********************* */
+/*! \file arith_rewriter.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/rewriter.h"
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arith_static_learner.h"
+
+#include "util/propositional_query.h"
+
+#include <vector>
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+
+ArithStaticLearner::ArithStaticLearner():
+ d_miplibTrick(),
+ d_statistics()
+{}
+
+ArithStaticLearner::Statistics::Statistics():
+ d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
+ d_iteConstantApplications("theory::arith::iteConstantApplications", 0),
+ d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
+ d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues")
+{
+ StatisticsRegistry::registerStat(&d_iteMinMaxApplications);
+ StatisticsRegistry::registerStat(&d_iteConstantApplications);
+ StatisticsRegistry::registerStat(&d_miplibtrickApplications);
+ StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
+}
+
+ArithStaticLearner::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications);
+ StatisticsRegistry::unregisterStat(&d_iteConstantApplications);
+ StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
+ StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
+}
+
+void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
+
+ vector<TNode> workList;
+ workList.push_back(n);
+ TNodeSet processed;
+
+ //Contains an underapproximation of nodes that must hold.
+ TNodeSet defTrue;
+
+ defTrue.insert(n);
+
+ while(!workList.empty()) {
+ n = workList.back();
+
+ bool unprocessedChildren = false;
+ for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+ if(processed.find(*i) == processed.end()) {
+ // unprocessed child
+ workList.push_back(*i);
+ unprocessedChildren = true;
+ }
+ }
+ if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
+ for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+ defTrue.insert(*i);
+ }
+ }
+
+ if(unprocessedChildren) {
+ continue;
+ }
+
+ workList.pop_back();
+ // has node n been processed in the meantime ?
+ if(processed.find(n) != processed.end()) {
+ continue;
+ }
+ processed.insert(n);
+
+ process(n,learned, defTrue);
+
+ }
+
+ postProcess(learned);
+}
+
+void ArithStaticLearner::clear(){
+ d_miplibTrick.clear();
+}
+
+
+void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
+ Debug("arith::static") << "===================== looking at" << n << endl;
+
+ switch(n.getKind()){
+ case ITE:
+ if(n[0].getKind() != EQUAL &&
+ isRelationOperator(n[0].getKind()) ){
+ iteMinMax(n, learned);
+ }
+
+ if((n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
+ (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
+ iteConstant(n, learned);
+ }
+ break;
+ case IMPLIES:
+ // == 3-FINITE VALUE SET : Collect information ==
+ if(n[1].getKind() == EQUAL &&
+ n[1][0].getMetaKind() == metakind::VARIABLE &&
+ defTrue.find(n) != defTrue.end()){
+ Node eqTo = n[1][1];
+ Node rewriteEqTo = Rewriter::rewrite(eqTo);
+ if(rewriteEqTo.getKind() == CONST_RATIONAL){
+
+ TNode var = n[1][0];
+ if(d_miplibTrick.find(var) == d_miplibTrick.end()){
+ d_miplibTrick.insert(make_pair(var, set<Node>()));
+ }
+ d_miplibTrick[var].insert(n);
+ Debug("arith::miplib") << "insert " << var << " const " << n << endl;
+ }
+ }
+ break;
+ default: // Do nothing
+ break;
+ }
+}
+
+void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
+ Assert(n.getKind() == kind::ITE);
+ Assert(n[0].getKind() != EQUAL);
+ Assert(isRelationOperator(n[0].getKind()));
+
+ TNode c = n[0];
+ Kind k = simplifiedKind(c);
+ TNode t = n[1];
+ TNode e = n[2];
+ TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
+ TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
+
+ if((t == cright) && (e == cleft)){
+ TNode tmp = t;
+ t = e;
+ e = tmp;
+ k = reverseRelationKind(k);
+ }
+ if(t == cleft && e == cright){
+ // t == cleft && e == cright
+ Assert( t == cleft );
+ Assert( e == cright );
+ switch(k){
+ case LT: // (ite (< x y) x y)
+ case LEQ: { // (ite (<= x y) x y)
+ Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
+ Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+ Debug("arith::static") << n << "is a min =>" << nLeqX << nLeqY << endl;
+ learned << nLeqX << nLeqY;
+ ++(d_statistics.d_iteMinMaxApplications);
+ break;
+ }
+ case GT: // (ite (> x y) x y)
+ case GEQ: { // (ite (>= x y) x y)
+ Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
+ Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+ Debug("arith::static") << n << "is a max =>" << nGeqX << nGeqY << endl;
+ learned << nGeqX << nGeqY;
+ ++(d_statistics.d_iteMinMaxApplications);
+ break;
+ }
+ default: Unreachable();
+ }
+ }
+}
+
+void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
+ Assert(n.getKind() == ITE);
+ Assert(n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER );
+ Assert(n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER );
+
+ Rational t = coerceToRational(n[1]);
+ Rational e = coerceToRational(n[2]);
+ TNode min = (t <= e) ? n[1] : n[2];
+ TNode max = (t >= e) ? n[1] : n[2];
+
+ Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
+ Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
+ Debug("arith::static") << n << " iteConstant" << nGeqMin << nLeqMax << endl;
+ learned << nGeqMin << nLeqMax;
+ ++(d_statistics.d_iteConstantApplications);
+}
+
+
+void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
+
+ // == 3-FINITE VALUE SET ==
+ VarToNodeSetMap::iterator i = d_miplibTrick.begin();
+ VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
+ for(; i != endMipLibTrick; ++i){
+ TNode var = i->first;
+ const set<Node>& imps = i->second;
+
+ Assert(!imps.empty());
+ vector<Node> conditions;
+ set<Rational> values;
+ set<Node>::const_iterator j=imps.begin(), impsEnd=imps.end();
+ for(; j != impsEnd; ++j){
+ TNode imp = *j;
+ Assert(imp.getKind() == IMPLIES);
+ Assert(imp[1].getKind() == EQUAL);
+
+ Node eqTo = imp[1][1];
+ Node rewriteEqTo = Rewriter::rewrite(eqTo);
+ Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
+
+ conditions.push_back(imp[0]);
+ values.insert(rewriteEqTo.getConst<Rational>());
+ }
+
+ Node possibleTaut = Node::null();
+ if(conditions.size() == 1){
+ possibleTaut = conditions.front();
+ }else{
+ NodeBuilder<> orBuilder(OR);
+ orBuilder.append(conditions);
+ possibleTaut = orBuilder;
+ }
+
+
+ Debug("arith::miplib") << "var: " << var << endl;
+ Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
+
+ Result isTaut = PropositionalQuery::isTautology(possibleTaut);
+ if(isTaut == Result(Result::VALID)){
+ miplibTrick(var, values, learned);
+ }
+ }
+}
+
+
+void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuilder<>& learned){
+
+ Debug("arith::miplib") << var << " found a tautology!"<< endl;
+
+ const Rational& min = *(values.begin());
+ const Rational& max = *(values.rbegin());
+
+ Debug("arith::miplib") << "min: " << min << endl;
+ Debug("arith::miplib") << "max: " << max << endl;
+
+ Assert(min <= max);
+ ++(d_statistics.d_miplibtrickApplications);
+ (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
+
+ Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
+ Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
+ Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
+ learned << nGeqMin << nLeqMax;
+ set<Rational>::iterator valuesIter = values.begin();
+ set<Rational>::iterator valuesEnd = values.end();
+ set<Rational>::iterator valuesPrev = valuesIter;
+ ++valuesIter;
+ for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
+ const Rational& prev = *valuesPrev;
+ const Rational& curr = *valuesIter;
+ Assert(prev < curr);
+
+ //The interval (last,curr) can be excluded:
+ //(not (and (> var prev) (< var curr))
+ //<=> (or (not (> var prev)) (not (< var curr)))
+ //<=> (or (<= var prev) (>= var curr))
+ Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
+ Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
+ Node excludedMiddle = NodeBuilder<2>(OR) << leqPrev << geqCurr;
+ Debug("arith::miplib") << excludedMiddle << endl;
+ learned << excludedMiddle;
+ }
+}
TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
Theory(THEORY_ARITH, c, out),
- d_constants(NodeManager::currentNM()),
d_partialModel(c),
d_userVariables(),
d_diseq(c),
d_tableauResetDensity(2.0),
d_tableauResetPeriod(10),
d_propagator(c, out),
- d_simplex(d_constants, d_partialModel, d_out, d_tableau),
+ d_simplex(d_partialModel, d_out, d_tableau),
+ d_DELTA_ZERO(0),
d_statistics()
{}
d_staticLearningTimer("theory::arith::staticLearningTimer"),
d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
d_presolveTime("theory::arith::presolveTime"),
- d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
- d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"),
d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
d_tableauResets("theory::arith::tableauResets", 0),
StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
StatisticsRegistry::registerStat(&d_presolveTime);
- StatisticsRegistry::registerStat(&d_miplibtrickApplications);
- StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
StatisticsRegistry::registerStat(&d_initialTableauDensity);
StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
StatisticsRegistry::unregisterStat(&d_presolveTime);
- StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
- StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
StatisticsRegistry::unregisterStat(&d_restartTimer);
}
-#include "util/propositional_query.h"
void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
- vector<TNode> workList;
- workList.push_back(n);
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
-
- //Contains an underapproximation of nodes that must hold.
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> defTrue;
-
- /* Maps a variable, x, to the set of defTrue nodes of the form
- * (=> _ (= x c))
- * where c is a constant.
- */
- typedef __gnu_cxx::hash_map<TNode, set<TNode>, TNodeHashFunction> VarToNodeSetMap;
- VarToNodeSetMap miplibTrick;
-
- defTrue.insert(n);
-
- while(!workList.empty()) {
- n = workList.back();
-
- bool unprocessedChildren = false;
- for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
- if(processed.find(*i) == processed.end()) {
- // unprocessed child
- workList.push_back(*i);
- unprocessedChildren = true;
- }
- }
- if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
- for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
- defTrue.insert(*i);
- }
- }
-
- if(unprocessedChildren) {
- continue;
- }
-
- workList.pop_back();
- // has node n been processed in the meantime ?
- if(processed.find(n) != processed.end()) {
- continue;
- }
- processed.insert(n);
-
- // == MINS ==
-
- Debug("mins") << "===================== looking at" << endl << n << endl;
- if(n.getKind() == kind::ITE && n[0].getKind() != EQUAL && isRelationOperator(n[0].getKind()) ){
- TNode c = n[0];
- Kind k = simplifiedKind(c);
- TNode t = n[1];
- TNode e = n[2];
- TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
- TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
-
- if((t == cright) && (e == cleft)){
- TNode tmp = t;
- t = e;
- e = tmp;
- k = reverseRelationKind(k);
- }
- if(t == cleft && e == cright){
- // t == cleft && e == cright
- Assert( t == cleft );
- Assert( e == cright );
- switch(k){
- case LT: // (ite (< x y) x y)
- case LEQ: { // (ite (<= x y) x y)
- Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
- Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
- Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl;
- learned << nLeqX << nLeqY;
- break;
- }
- case GT: // (ite (> x y) x y)
- case GEQ: { // (ite (>= x y) x y)
- Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
- Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
- Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl;
- learned << nGeqX << nGeqY;
- break;
- }
- default: Unreachable();
- }
- }
- }
- // == 2-CONSTANTS ==
-
- if(n.getKind() == ITE &&
- (n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
- (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
- Rational t = coerceToRational(n[1]);
- Rational e = coerceToRational(n[2]);
- TNode min = (t <= e) ? n[1] : n[2];
- TNode max = (t >= e) ? n[1] : n[2];
-
- Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
- Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
- Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl;
- learned << nGeqMin << nLeqMax;
- }
- // == 3-FINITE VALUE SET : Collect information ==
- if(n.getKind() == IMPLIES &&
- n[1].getKind() == EQUAL &&
- n[1][0].getMetaKind() == metakind::VARIABLE &&
- defTrue.find(n) != defTrue.end()){
- Node eqTo = n[1][1];
- Node rewriteEqTo = Rewriter::rewrite(eqTo);
- if(rewriteEqTo.getKind() == CONST_RATIONAL){
-
- TNode var = n[1][0];
- if(miplibTrick.find(var) == miplibTrick.end()){
- miplibTrick.insert(make_pair(var, set<TNode>()));
- }
- miplibTrick[var].insert(n);
- Debug("arith::miplib") << "insert " << var << " const " << n << endl;
- }
- }
- }
-
- // == 3-FINITE VALUE SET ==
- VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end();
- for(; i != endMipLibTrick; ++i){
- TNode var = i->first;
- const set<TNode>& imps = i->second;
-
- Assert(!imps.empty());
- vector<Node> conditions;
- vector<Rational> valueCollection;
- set<TNode>::const_iterator j=imps.begin(), impsEnd=imps.end();
- for(; j != impsEnd; ++j){
- TNode imp = *j;
- Assert(imp.getKind() == IMPLIES);
- Assert(defTrue.find(imp) != defTrue.end());
- Assert(imp[1].getKind() == EQUAL);
-
-
- Node eqTo = imp[1][1];
- Node rewriteEqTo = Rewriter::rewrite(eqTo);
- Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
-
- conditions.push_back(imp[0]);
- valueCollection.push_back(rewriteEqTo.getConst<Rational>());
- }
-
- Node possibleTaut = Node::null();
- if(conditions.size() == 1){
- possibleTaut = conditions.front();
- }else{
- NodeBuilder<> orBuilder(OR);
- orBuilder.append(conditions);
- possibleTaut = orBuilder;
- }
-
-
- Debug("arith::miplib") << "var: " << var << endl;
- Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
-
- Result isTaut = PropositionalQuery::isTautology(possibleTaut);
- if(isTaut == Result(Result::VALID)){
- Debug("arith::miplib") << var << " found a tautology!"<< endl;
-
- set<Rational> values(valueCollection.begin(), valueCollection.end());
- const Rational& min = *(values.begin());
- const Rational& max = *(values.rbegin());
-
- Debug("arith::miplib") << "min: " << min << endl;
- Debug("arith::miplib") << "max: " << max << endl;
-
- Assert(min <= max);
- ++(d_statistics.d_miplibtrickApplications);
- (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
-
- Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
- Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
- Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
- learned << nGeqMin << nLeqMax;
- set<Rational>::iterator valuesIter = values.begin();
- set<Rational>::iterator valuesEnd = values.end();
- set<Rational>::iterator valuesPrev = valuesIter;
- ++valuesIter;
- for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
- const Rational& prev = *valuesPrev;
- const Rational& curr = *valuesIter;
- Assert(prev < curr);
-
- //The interval (last,curr) can be excluded:
- //(not (and (> var prev) (< var curr))
- //<=> (or (not (> var prev)) (not (< var curr)))
- //<=> (or (<= var prev) (>= var curr))
- Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
- Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
- Node excludedMiddle = NodeBuilder<2>(OR) << leqPrev << geqCurr;
- Debug("arith::miplib") << excludedMiddle << endl;
- learned << excludedMiddle;
- }
- }
- }
+ learner.staticLearning(n, learned);
}
ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
ArithVar bestBasic = ARITHVAR_SENTINEL;
- unsigned rowLength = 0;
+ uint64_t rowLength = std::numeric_limits<uint64_t>::max();
- for(ArithVarSet::iterator basicIter = d_tableau.begin();
- basicIter != d_tableau.end();
- ++basicIter){
+ Column::iterator basicIter = d_tableau.beginColumn(variable);
+ Column::iterator end = d_tableau.endColumn(variable);
+ for(; basicIter != end; ++basicIter){
ArithVar x_j = *basicIter;
ReducedRowVector& row_j = d_tableau.lookup(x_j);
- if(row_j.has(variable)){
- if((bestBasic == ARITHVAR_SENTINEL) ||
- (bestBasic != ARITHVAR_SENTINEL && row_j.size() < rowLength)){
- bestBasic = x_j;
- rowLength = row_j.size();
- }
+ Assert(row_j.has(variable));
+ if((row_j.size() < rowLength) ||
+ (row_j.size() == rowLength && x_j < bestBasic)){
+ bestBasic = x_j;
+ rowLength = row_j.size();
}
}
return bestBasic;
setupInitialValue(varN);
}
-
- //TODO is an atom
if(isRelationOperator(k)){
Assert(Comparison::isNormalAtom(n));
setArithVar(x,varX);
- //d_basicManager.init(varX,basic);
d_userVariables.init(varX, !basic);
d_tableau.increaseSize();
void TheoryArith::setupInitialValue(ArithVar x){
if(!d_tableau.isBasic(x)){
- d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
+ d_partialModel.initialize(x, d_DELTA_ZERO);
}else{
//If the variable is basic, assertions may have already happened and updates
//may have occured before setting this variable up.
DeltaRational assignment = d_simplex.computeRowValue(x, false);
d_partialModel.initialize(x,safeAssignment);
d_partialModel.setAssignment(x,assignment);
-
-
- //d_simplex.checkBasicVariable(x);
- //Conciously violating unneeded check
-
- //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;
};
return DeltaRational(noninf, inf);
}
+void TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
+
+ NodeBuilder<3> conflict(kind::AND);
+ conflict << eq << lb << ub;
+ ++(d_statistics.d_statDisequalityConflicts);
+ d_out->conflict((TNode)conflict);
+
+}
+
bool TheoryArith::assertionCases(TNode assertion){
Kind simpKind = simplifiedKind(assertion);
Assert(simpKind != UNDEFINED_KIND);
if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
Node diseq = assertion[0].eqNode(assertion[1]).notNode();
if (d_diseq.find(diseq) != d_diseq.end()) {
- NodeBuilder<3> conflict(kind::AND);
- conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i);
- ++(d_statistics.d_statDisequalityConflicts);
- d_out->conflict((TNode)conflict);
+ disequalityConflict(diseq, d_partialModel.getLowerConstraint(x_i) , assertion);
return true;
}
}
if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
Node diseq = assertion[0].eqNode(assertion[1]).notNode();
if (d_diseq.find(diseq) != d_diseq.end()) {
- NodeBuilder<3> conflict(kind::AND);
- conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i);
- ++(d_statistics.d_statDisequalityConflicts);
- d_out->conflict((TNode)conflict);
+ disequalityConflict(diseq, assertion, d_partialModel.getUpperConstraint(x_i));
return true;
}
}
Assert(rhs.getKind() == CONST_RATIONAL);
ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
- if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) &&
- d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) {
- NodeBuilder<3> conflict(kind::AND);
- conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar);
- d_out->conflict((TNode)conflict);
+ if (d_partialModel.hasLowerBound(lhsVar) &&
+ d_partialModel.hasUpperBound(lhsVar) &&
+ d_partialModel.getLowerBound(lhsVar) == rhsValue &&
+ d_partialModel.getUpperBound(lhsVar) == rhsValue) {
+ Node lb = d_partialModel.getLowerConstraint(lhsVar);
+ Node ub = d_partialModel.getUpperConstraint(lhsVar);
+ disequalityConflict(assertion, lb, ub);
+ return true;
}
}
return false;
}
}
+
+
void TheoryArith::check(Effort effortLevel){
Debug("arith") << "TheoryArith::check begun" << std::endl;
while(!done()){
Node assertion = get();
-
- //d_propagator.assertLiteral(assertion);
bool conflictDuringAnAssert = assertionCases(assertion);
if(conflictDuringAnAssert){
}
if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
- Debug("arith::print_assertions") << "Assertions:" << endl;
- for (ArithVar i = 0; i < d_variables.size(); ++ i) {
- if (d_partialModel.hasLowerBound(i)) {
- Node lConstr = d_partialModel.getLowerConstraint(i);
- Debug("arith::print_assertions") << lConstr.toString() << endl;
- }
-
- if (d_partialModel.hasUpperBound(i)) {
- Node uConstr = d_partialModel.getUpperConstraint(i);
- Debug("arith::print_assertions") << uConstr.toString() << endl;
- }
- }
- context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
- context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
- for(; it != it_end; ++ it) {
- Debug("arith::print_assertions") << *it << endl;
- }
+ debugPrintAssertions();
}
Node possibleConflict = d_simplex.updateInconsistentVars();
d_partialModel.revertAssignmentChanges();
- if(Debug.isOn("arith::print-conflict"))
- Debug("arith_conflict") << (possibleConflict) << std::endl;
-
d_out->conflict(possibleConflict);
-
- Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
}else{
d_partialModel.commitAssignmentChanges();
if (fullEffort(effortLevel)) {
- context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
- context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
- for(; it != it_end; ++ it) {
- TNode eq = (*it)[0];
- Assert(eq.getKind() == kind::EQUAL);
- TNode lhs = eq[0];
- TNode rhs = eq[1];
- Assert(rhs.getKind() == CONST_RATIONAL);
- ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
- DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
- DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
- if (lhsValue == rhsValue) {
- Debug("arith_lemma") << "Splitting on " << eq << endl;
- Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
- Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
- 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.andNode(impClosure));
- }
- }
+ splitDisequalities();
}
}
- if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+ if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
Debug("arith") << "TheoryArith::check end" << std::endl;
+}
- if(Debug.isOn("arith::print_model")) {
- Debug("arith::print_model") << "Model:" << endl;
+void TheoryArith::splitDisequalities(){
+ context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+ context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+ for(; it != it_end; ++ it) {
+ TNode eq = (*it)[0];
+ Assert(eq.getKind() == kind::EQUAL);
+ TNode lhs = eq[0];
+ TNode rhs = eq[1];
+ Assert(rhs.getKind() == CONST_RATIONAL);
+ ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+ DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
+ DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+ if (lhsValue == rhsValue) {
+ Debug("arith_lemma") << "Splitting on " << eq << endl;
+ Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
+ Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
+ 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);
+ }
+ }
+}
- for (ArithVar i = 0; i < d_variables.size(); ++ i) {
- Debug("arith::print_model") << d_variables[i] << " : " <<
- d_partialModel.getAssignment(i);
- if(d_tableau.isBasic(i))
- Debug("arith::print_model") << " (basic)";
- Debug("arith::print_model") << endl;
+/**
+ * Should be guarded by at least Debug.isOn("arith::print_assertions").
+ * Prints to Debug("arith::print_assertions")
+ */
+void TheoryArith::debugPrintAssertions() {
+ Debug("arith::print_assertions") << "Assertions:" << endl;
+ for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+ if (d_partialModel.hasLowerBound(i)) {
+ Node lConstr = d_partialModel.getLowerConstraint(i);
+ Debug("arith::print_assertions") << lConstr.toString() << endl;
}
+
+ if (d_partialModel.hasUpperBound(i)) {
+ Node uConstr = d_partialModel.getUpperConstraint(i);
+ Debug("arith::print_assertions") << uConstr.toString() << endl;
+ }
+ }
+ context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+ context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+ for(; it != it_end; ++ it) {
+ Debug("arith::print_assertions") << *it << endl;
+ }
+}
+
+void TheoryArith::debugPrintModel(){
+ Debug("arith::print_model") << "Model:" << endl;
+
+ for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+ Debug("arith::print_model") << d_variables[i] << " : " <<
+ d_partialModel.getAssignment(i);
+ if(d_tableau.isBasic(i))
+ Debug("arith::print_model") << " (basic)";
+ Debug("arith::print_model") << endl;
}
}
void TheoryArith::explain(TNode n) {
- // Node explanation = d_propagator.explain(n);
- // Debug("arith") << "arith::explain("<<explanation<<")->"
- // << explanation << endl;
- // d_out->explanation(explanation, true);
}
void TheoryArith::propagate(Effort e) {
d_out->lemma(lemma);
}
}
- // if(quickCheckOrMore(e)){
- // std::vector<Node> implied = d_propagator.getImpliedLiterals();
- // for(std::vector<Node>::iterator i = implied.begin();
- // i != implied.end();
- // ++i){
- // d_out->propagate(*i);
- // }
- // }
}
Node TheoryArith::getValue(TNode n, Valuation* valuation) {
mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
case kind::PLUS: { // 2+ args
- Rational value = d_constants.d_ZERO;
+ Rational value(0);
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
}
case kind::MULT: { // 2+ args
- Rational value = d_constants.d_ONE;
+ Rational value(1);
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
static int callCount = 0;
Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+ learner.clear();
+
check(FULL_EFFORT);
}
projects / cvc5.git / commitdiff