diff options
| -rw-r--r-- | src/theory/arith/Makefile.am | 3 | ||||
| -rw-r--r-- | src/theory/arith/arith_constants.h | 67 | ||||
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 27 | ||||
| -rw-r--r-- | src/theory/arith/arith_rewriter.h | 16 | ||||
| -rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 298 | ||||
| -rw-r--r-- | src/theory/arith/arith_static_learner.h | 63 | ||||
| -rw-r--r-- | src/theory/arith/normal_form.h | 1 | ||||
| -rw-r--r-- | src/theory/arith/simplex.cpp | 6 | ||||
| -rw-r--r-- | src/theory/arith/simplex.h | 14 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 431 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 39 |
11 files changed, 524 insertions, 441 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 48be16f90..2c00f5d4d 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -9,10 +9,11 @@ libarith_la_SOURCES = \ theory_arith_type_rules.h \ arith_rewriter.h \ arith_rewriter.cpp \ + arith_static_learner.h \ + arith_static_learner.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ - arith_constants.h \ delta_rational.h \ delta_rational.cpp \ partial_model.h \ diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h deleted file mode 100644 index 98a202207..000000000 --- a/src/theory/arith/arith_constants.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file arith_constants.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H -#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "util/rational.h" -#include "theory/arith/delta_rational.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -class ArithConstants { -public: - Rational d_ZERO; - Rational d_ONE; - Rational d_NEGATIVE_ONE; - - DeltaRational d_ZERO_DELTA; - - Node d_ZERO_NODE; - Node d_ONE_NODE; - Node d_NEGATIVE_ONE_NODE; - - ArithConstants(NodeManager* nm) : - d_ZERO(0,1), - d_ONE(1,1), - d_NEGATIVE_ONE(-1,1), - d_ZERO_DELTA(d_ZERO), - d_ZERO_NODE(nm->mkConst(d_ZERO)), - d_ONE_NODE(nm->mkConst(d_ONE)), - d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE)) - {} - - ~ArithConstants() { - d_ZERO_NODE = Node::null(); - d_ONE_NODE = Node::null(); - d_NEGATIVE_ONE_NODE = Node::null(); - } -};/* class ArithConstants */ - -}/* namespace CVC4::theory::arith */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ - -#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index cc80e2dd8..941394138 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -30,8 +30,6 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -arith::ArithConstants* ArithRewriter::s_constants = NULL; - bool isVariable(TNode t){ return t.getMetaKind() == kind::metakind::VARIABLE; } @@ -52,7 +50,11 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){ RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ Assert(t.getKind()== kind::MINUS); - if(t[0] == t[1]) return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); + if(t[0] == t[1]){ + Rational zero(0); + Node zeroNode = mkRationalNode(zero); + return RewriteResponse(REWRITE_DONE, zeroNode); + } Node noMinus = makeSubtractionNode(t[0],t[1]); if(pre){ @@ -121,17 +123,19 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ // Rewrite multiplications with a 0 argument and to 0 Integer intZero; + Rational qZero(0); + for(TNode::iterator i = t.begin(); i != t.end(); ++i) { if((*i).getKind() == kind::CONST_RATIONAL) { - if((*i).getConst<Rational>() == s_constants->d_ZERO) { - return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); + if((*i).getConst<Rational>() == qZero) { + return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero)); } } else if((*i).getKind() == kind::CONST_INTEGER) { if((*i).getConst<Integer>() == intZero) { if(t.getType().isInteger()) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero)); } else { - return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); + return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero)); } } } @@ -222,7 +226,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ }else{ //Transform this to: (left - right) |><| 0 Node diff = makeSubtractionNode(left, right); - Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE); + Rational qZero(0); + Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, mkRationalNode(qZero)); return RewriteResponse(REWRITE_AGAIN_FULL, reduction); } } @@ -246,7 +251,8 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ //Transform this to: (left - right) |><| 0 Node diff = makeSubtractionNode(left, right); - reduction = currNM->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE); + Rational qZero(0); + reduction = currNM->mkNode(atom.getKind(), diff, mkRationalNode(qZero)); } if(reduction.getKind() == kind::GT){ @@ -291,7 +297,8 @@ RewriteResponse ArithRewriter::preRewrite(TNode t){ } Node ArithRewriter::makeUnaryMinusNode(TNode n){ - return NodeManager::currentNM()->mkNode(kind::MULT,s_constants->d_NEGATIVE_ONE_NODE,n); + Rational qNegOne(-1); + return NodeManager::currentNM()->mkNode(kind::MULT, mkRationalNode(qNegOne),n); } Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ @@ -311,7 +318,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ const Rational& den = right.getConst<Rational>(); - Assert(den != s_constants->d_ZERO); + Assert(den != Rational(0)); Rational div = den.inverse(); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 3a8fc191a..d88a7ae92 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -23,7 +23,6 @@ #define __CVC4__THEORY__ARITH__ARITH_REWRITER_H #include "theory/theory.h" -#include "theory/arith/arith_constants.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" @@ -37,8 +36,6 @@ class ArithRewriter { private: - static arith::ArithConstants* s_constants; - static Node makeSubtractionNode(TNode l, TNode r); static Node makeUnaryMinusNode(TNode n); @@ -67,18 +64,9 @@ public: static RewriteResponse preRewrite(TNode n); static RewriteResponse postRewrite(TNode n); - static void init() { - if (s_constants == NULL) { - s_constants = new arith::ArithConstants(NodeManager::currentNM()); - } - } + static void init() { } - static void shutdown() { - if (s_constants != NULL) { - delete s_constants; - s_constants = NULL; - } - } + static void shutdown() { } private: diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp new file mode 100644 index 000000000..6fb538fac --- /dev/null +++ b/src/theory/arith/arith_static_learner.cpp @@ -0,0 +1,298 @@ +/********************* */ +/*! \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; + } +} diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h new file mode 100644 index 000000000..02274318f --- /dev/null +++ b/src/theory/arith/arith_static_learner.h @@ -0,0 +1,63 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H +#define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H + + +#include "util/stats.h" +#include "theory/arith/arith_utilities.h" +#include <set> + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithStaticLearner { +private: + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + + /* 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<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap; + VarToNodeSetMap d_miplibTrick; + +public: + ArithStaticLearner(); + void staticLearning(TNode n, NodeBuilder<>& learned); + + void clear(); + +private: + void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue); + + void postProcess(NodeBuilder<>& learned); + + void iteMinMax(TNode n, NodeBuilder<>& learned); + void iteConstant(TNode n, NodeBuilder<>& learned); + + void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); + + /** These fields are designed to be accessable to ArithStaticLearner methods. */ + class Statistics { + public: + IntStat d_iteMinMaxApplications; + IntStat d_iteConstantApplications; + + IntStat d_miplibtrickApplications; + AverageStat d_avgNumMiplibtrickValues; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + +};/* class ArithStaticLearner */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index aa4e8bc13..5d6ca27e9 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -26,7 +26,6 @@ #include "expr/node_self_iterator.h" #include "util/rational.h" #include "theory/theory.h" -#include "theory/arith/arith_constants.h" #include "theory/arith/arith_utilities.h" #include <list> diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index dc451288b..1e7b5c028 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -618,7 +618,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ if(nonbasic == conflictVar) continue; const Rational& a_ij = (*nbi).getCoefficient(); - Assert(a_ij != d_constants.d_ZERO); + Assert(a_ij != d_ZERO); int sgn = a_ij.sgn(); Assert(sgn != 0); @@ -662,7 +662,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ const Rational& a_ij = (*nbi).getCoefficient(); int sgn = a_ij.sgn(); - Assert(a_ij != d_constants.d_ZERO); + Assert(a_ij != d_ZERO); Assert(sgn != 0); if(sgn < 0){ @@ -691,7 +691,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ */ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){ Assert(d_tableau.isBasic(x)); - DeltaRational sum = d_constants.d_ZERO_DELTA; + DeltaRational sum(0); ReducedRowVector& row = d_tableau.lookup(x); for(ReducedRowVector::const_iterator i = row.begin(), end = row.end(); diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index c6bc3c434..6f3ff073f 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -25,9 +25,6 @@ namespace arith { class SimplexDecisionProcedure { private: - /** Stores system wide constants to avoid unnessecary reconstruction. */ - const ArithConstants& d_constants; - /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -44,23 +41,22 @@ private: std::vector<Node> d_delayedLemmas; uint32_t d_delayedLemmasPos; + Rational d_ZERO; + public: - SimplexDecisionProcedure(const ArithConstants& constants, - ArithPartialModel& pm, + SimplexDecisionProcedure(ArithPartialModel& pm, OutputChannel* out, Tableau& tableau) : - d_constants(constants), d_partialModel(pm), d_out(out), d_tableau(tableau), d_queue(pm, tableau), d_numVariables(0), d_delayedLemmas(), - d_delayedLemmasPos(0) + d_delayedLemmasPos(0), + d_ZERO(0) {} - -public: /** * Assert*(n, orig) takes an bound n that is implied by orig. * and asserts that as a new bound if it is tighter than the current bound diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c0e7057c2..726bfc210 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -57,7 +57,6 @@ typedef expr::Attribute<SlackAttrID, Node> Slack; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : Theory(THEORY_ARITH, c, out), - d_constants(NodeManager::currentNM()), d_partialModel(c), d_userVariables(), d_diseq(c), @@ -67,7 +66,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : 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() {} @@ -81,8 +81,6 @@ TheoryArith::Statistics::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), @@ -97,8 +95,6 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); StatisticsRegistry::registerStat(&d_presolveTime); - StatisticsRegistry::registerStat(&d_miplibtrickApplications); - StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues); StatisticsRegistry::registerStat(&d_initialTableauDensity); StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart); @@ -116,8 +112,6 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); StatisticsRegistry::unregisterStat(&d_presolveTime); - StatisticsRegistry::unregisterStat(&d_miplibtrickApplications); - StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues); StatisticsRegistry::unregisterStat(&d_initialTableauDensity); StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart); @@ -125,228 +119,29 @@ TheoryArith::Statistics::~Statistics(){ 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; @@ -369,8 +164,6 @@ void TheoryArith::preRegisterTerm(TNode n) { setupInitialValue(varN); } - - //TODO is an atom if(isRelationOperator(k)){ Assert(Comparison::isNormalAtom(n)); @@ -402,7 +195,6 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ setArithVar(x,varX); - //d_basicManager.init(varX,basic); d_userVariables.init(varX, !basic); d_tableau.increaseSize(); @@ -458,7 +250,7 @@ void TheoryArith::setupSlack(TNode left){ 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. @@ -469,15 +261,6 @@ void TheoryArith::setupInitialValue(ArithVar x){ 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; }; @@ -525,6 +308,15 @@ DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ 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); @@ -539,10 +331,7 @@ bool TheoryArith::assertionCases(TNode assertion){ 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; } } @@ -552,10 +341,7 @@ bool TheoryArith::assertionCases(TNode assertion){ 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; } } @@ -574,11 +360,14 @@ bool TheoryArith::assertionCases(TNode assertion){ 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; @@ -588,14 +377,14 @@ bool TheoryArith::assertionCases(TNode assertion){ } } + + 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){ @@ -605,23 +394,7 @@ void TheoryArith::check(Effort effortLevel){ } 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(); @@ -629,72 +402,92 @@ void TheoryArith::check(Effort effortLevel){ 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) { @@ -704,14 +497,6 @@ 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) { @@ -741,7 +526,7 @@ 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; @@ -752,7 +537,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { } 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; @@ -897,5 +682,7 @@ void TheoryArith::presolve(){ static int callCount = 0; Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; + learner.clear(); + check(FULL_EFFORT); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1dcdceab0..ef93b7d64 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -35,6 +35,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/unate_propagator.h" #include "theory/arith/simplex.h" +#include "theory/arith/arith_static_learner.h" #include "util/stats.h" @@ -54,26 +55,22 @@ namespace arith { class TheoryArith : public Theory { private: - /* TODO Everything in the chopping block needs to be killed. */ - /* Chopping block begins */ - - std::vector<Node> d_splits; - //This stores the eager splits sent out of the theory. - - /* Chopping block ends */ + /** Static learner. */ + ArithStaticLearner learner; + /** + * List of the variables in the system. + * This is needed to keep a positive ref count on slack variables. + */ std::vector<Node> d_variables; /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that - * can be used to determine the value of n uysing getValue(). + * can be used to determine the value of n using getValue(). */ std::map<ArithVar, Node> d_removedRows; - /** Stores system wide constants to avoid unnessecary reconstruction. */ - ArithConstants d_constants; - /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -178,9 +175,17 @@ public: d_simplex.notifyOptions(opt); } private: + /** The constant zero. */ + DeltaRational d_DELTA_ZERO; + /** + * Using the simpleKind return the ArithVar associated with the + * left hand side of assertion. + */ ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); + /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */ + void splitDisequalities(); /** * This requests a new unique ArithVar value for x. @@ -203,6 +208,11 @@ private: bool assertionCases(TNode assertion); /** + * This is used for reporting conflicts caused by disequalities during assertionCases. + */ + void disequalityConflict(TNode eq, TNode lb, TNode ub); + + /** * Returns the basic variable with the shorted row containg a non-basic variable. * If no such row exists, return ARITHVAR_SENTINEL. */ @@ -225,6 +235,10 @@ private: std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) const; + /** Routine for debugging. Print the assertions the theory is aware of. */ + void debugPrintAssertions(); + /** Debugging only routine. Prints the model. */ + void debugPrintModel(); /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { @@ -237,9 +251,6 @@ private: IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; - IntStat d_miplibtrickApplications; - AverageStat d_avgNumMiplibtrickValues; - BackedStat<double> d_initialTableauDensity; AverageStat d_avgTableauDensityAtRestart; IntStat d_tableauResets; |