From b34cdc14238b5d215e6014d6b3db2971859a0b9d Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 19 Oct 2011 17:25:00 +0000 Subject: [PATCH] Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 into trunk. Arithmetic should now be closer to being able to support push and pop. --- src/theory/arith/arith_utilities.h | 5 + src/theory/arith/theory_arith.cpp | 336 +++++++++++------- src/theory/arith/theory_arith.h | 50 ++- .../regress0/arith/integers/Makefile.am | 82 ++++- 4 files changed, 325 insertions(+), 148 deletions(-) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 838285f42..42f4704df 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -26,6 +26,7 @@ #include "expr/node.h" #include "expr/attribute.h" #include "theory/arith/delta_rational.h" +#include "context/cdset.h" #include #include #include @@ -44,6 +45,10 @@ typedef uint32_t ArithVar; typedef __gnu_cxx::hash_map NodeToArithVarMap; typedef __gnu_cxx::hash_map ArithVarToNodeMap; +//Sets of Nodes +typedef __gnu_cxx::hash_set NodeSet; +typedef context::CDSet CDNodeSet; + inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 066eb85b5..289d5ace4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,12 +56,10 @@ using namespace CVC4::theory::arith; static const uint32_t RESET_START = 2; -struct SlackAttrID; -typedef expr::Attribute Slack; - TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, c, u, out, valuation), - learner(d_pbSubstitutions), + d_atomsInContext(c), + d_learner(d_pbSubstitutions), d_nextIntegerCheckVar(0), d_partialModel(c), d_userVariables(), @@ -92,7 +90,6 @@ TheoryArith::Statistics::Statistics(): d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), d_initialTableauSize("theory::arith::initialTableauSize", 0), - //d_tableauSizeHistory("theory::arith::tableauSizeHistory"), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), d_restartTimer("theory::arith::restartTimer") @@ -109,7 +106,6 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_initialTableauSize); - //StatisticsRegistry::registerStat(&d_tableauSizeHistory); StatisticsRegistry::registerStat(&d_currSetToSmaller); StatisticsRegistry::registerStat(&d_smallerSetToCurr); StatisticsRegistry::registerStat(&d_restartTimer); @@ -128,7 +124,6 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_initialTableauSize); - //StatisticsRegistry::unregisterStat(&d_tableauSizeHistory); StatisticsRegistry::unregisterStat(&d_currSetToSmaller); StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); StatisticsRegistry::unregisterStat(&d_restartTimer); @@ -142,15 +137,18 @@ Node TheoryArith::preprocess(TNode atom) { if (a != atom) { Debug("pb") << "arith::preprocess() : after pb substitutions: " << a << endl; a = Rewriter::rewrite(a); - Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; - Debug("arith::preprocess") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; + Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: " + << a << endl; + Debug("arith::preprocess") << "arith::preprocess() :" + << "after pb substitutions and rewriting: " << a << endl; } if (a.getKind() == kind::EQUAL) { Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1]; Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1]; Node rewritten = Rewriter::rewrite(leq.andNode(geq)); - Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; + Debug("arith::preprocess") << "arith::preprocess() : returning " + << rewritten << endl; return rewritten; } @@ -225,7 +223,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio case kind::GEQ: case kind::GT: if (in[0].getMetaKind() == kind::metakind::VARIABLE) { - learner.addBound(in); + d_learner.addBound(in); } break; default: @@ -239,7 +237,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); - learner.staticLearning(n, learned); + d_learner.staticLearning(n, learned); } @@ -264,58 +262,117 @@ ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){ return bestBasic; } +void TheoryArith::setupVariable(const Variable& x){ + Node n = x.getNode(); -void TheoryArith::preRegisterTerm(TNode n) { - Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; - Kind k = n.getKind(); + Assert(!isSetup(n)); + + ++(d_statistics.d_statUserVariables); + ArithVar varN = requestArithVar(n,false); + setupInitialValue(varN); + + markSetup(n); +} + +void TheoryArith::setupVariableList(const VarList& vl){ + Assert(!vl.empty()); - /* BREADCRUMB: I am using this bool to compile time enable testing for arbitrary equalities. */ - static bool turnOffEqualityPreRegister = false; - if(turnOffEqualityPreRegister){ - if(k == LEQ || k == LT || k == GT || k == GEQ){ - TNode left = n[0]; - delayedSetupPolynomial(left); + TNode vlNode = vl.getNode(); + Assert(!isSetup(vlNode)); + Assert(!d_arithvarNodeMap.hasArithVar(vlNode)); - d_atomDatabase.addAtom(n); + for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){ + Variable var = *i; + + if(!isSetup(var.getNode())){ + setupVariable(var); } - return; } - bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n); - - if(isStrictlyVarList){ + if(!vl.singleton()){ + // vl is the product of at least 2 variables + // vl : (* v1 v2 ...) d_out->setIncomplete(); - } - if((Variable::isMember(n) || isStrictlyVarList) && !d_arithvarNodeMap.hasArithVar(n)){ ++(d_statistics.d_statUserVariables); - ArithVar varN = requestArithVar(n,false); - setupInitialValue(varN); + ArithVar av = requestArithVar(vlNode, false); + setupInitialValue(av); + + markSetup(vlNode); } - if(isRelationOperator(k) && (!d_atomDatabase.leftIsSetup(n[0]) || !d_atomDatabase.containsAtom(n))) { - Assert(Comparison::isNormalAtom(n)); + /* Note: + * Only call markSetup if the VarList is not a singleton. + * See the comment in setupPolynomail for more. + */ +} - d_atomDatabase.addAtom(n); +void TheoryArith::setupPolynomial(const Polynomial& poly) { + Assert(!poly.containsConstant()); + TNode polyNode = poly.getNode(); + Assert(!isSetup(polyNode)); + Assert(!d_arithvarNodeMap.hasArithVar(polyNode)); + + for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){ + Monomial mono = *i; + const VarList& vl = mono.getVarList(); + if(!isSetup(vl.getNode())){ + setupVariableList(vl); + } + } - TNode left = n[0]; - TNode right = n[1]; - if(left.getKind() == PLUS){ - //We may need to introduce a slack variable. - Assert(left.getNumChildren() >= 2); - if(!left.getAttribute(Slack())){ - setupSlack(left); - } - } else { - if (theoryOf(left) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(left)) { - // The only way not to get it through pre-register is if it's a foreign term - ++(d_statistics.d_statUserVariables); - ArithVar av = requestArithVar(left, false); - setupInitialValue(av); - } + if(polyNode.getKind() == PLUS){ + d_rowHasBeenAdded = true; + + vector variables; + vector coefficients; + asVectors(poly, coefficients, variables); + + ArithVar varSlack = requestArithVar(polyNode, true); + d_tableau.addRow(varSlack, coefficients, variables); + setupInitialValue(varSlack); + + ++(d_statistics.d_statSlackVariables); + markSetup(polyNode); + } + + /* Note: + * It is worth documenting that polyNode should only be marked as + * being setup by this function if it has kind PLUS. + * Other kinds will be marked as being setup by lower levels of setup + * specifically setupVariableList. + */ +} + +void TheoryArith::setupAtom(TNode atom, bool addToDatabase) { + Assert(isRelationOperator(atom.getKind())); + Assert(Comparison::isNormalAtom(atom)); + Assert(!isSetup(atom)); + + Node left = atom[0]; + if(!isSetup(left)){ + Polynomial poly = Polynomial::parsePolynomial(left); + setupPolynomial(poly); + } + + if(addToDatabase){ + d_atomDatabase.addAtom(atom); + } + + markSetup(atom); +} + +void TheoryArith::preRegisterTerm(TNode n) { + Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; + + if(isRelationOperator(n.getKind())){ + if(!isSetup(n)){ + setupAtom(n, true); } + addToContext(n); } - Debug("arith_preregister") << "end arith::preRegisterTerm(" << n <<")" << endl; + + Debug("arith::preregister") << "end arith::preRegisterTerm(" << n <<")" << endl; } @@ -341,7 +398,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ return varX; } -void TheoryArith::asVectors(Polynomial& p, std::vector& coeffs, std::vector& variables) { +void TheoryArith::asVectors(const Polynomial& p, std::vector& coeffs, std::vector& variables) { for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){ const Monomial& mono = *i; const Constant& constant = mono.getConstant(); @@ -354,6 +411,7 @@ void TheoryArith::asVectors(Polynomial& p, std::vector& coeffs, std::v Assert(isLeaf(n)); Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n)); + Assert(d_arithvarNodeMap.hasArithVar(n)); ArithVar av; if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) { // The only way not to get it through pre-register is if it's a foreign term @@ -364,31 +422,33 @@ void TheoryArith::asVectors(Polynomial& p, std::vector& coeffs, std::v // Otherwise, we already have it's variable av = d_arithvarNodeMap.asArithVar(n); } - + coeffs.push_back(constant.getValue()); variables.push_back(av); } } -void TheoryArith::setupSlack(TNode left){ - Assert(!left.getAttribute(Slack())); +// void TheoryArith::setupSlack(TNode left){ +// //Assert(!left.getAttribute(Slack())); +// Assert(!isSlack(left)); - ++(d_statistics.d_statSlackVariables); - left.setAttribute(Slack(), true); - d_rowHasBeenAdded = true; +// ++(d_statistics.d_statSlackVariables); +// left.setAttribute(Slack(), true); - Polynomial polyLeft = Polynomial::parsePolynomial(left); +// d_rowHasBeenAdded = true; - vector variables; - vector coefficients; +// Polynomial polyLeft = Polynomial::parsePolynomial(left); - asVectors(polyLeft, coefficients, variables); +// vector variables; +// vector coefficients; - ArithVar varSlack = requestArithVar(left, true); - d_tableau.addRow(varSlack, coefficients, variables); - setupInitialValue(varSlack); -} +// asVectors(polyLeft, coefficients, variables); + +// ArithVar varSlack = requestArithVar(left, true); +// d_tableau.addRow(varSlack, coefficients, variables); +// setupInitialValue(varSlack); +// } /* Requirements: * For basic variables the row must have been added to the tableau. @@ -408,18 +468,13 @@ void TheoryArith::setupInitialValue(ArithVar x){ d_partialModel.initialize(x,safeAssignment); d_partialModel.setAssignment(x,assignment); } - Debug("arithgc") << "setupVariable("<(assertion, simpleKind); - if(isLeaf(left)){ - return d_arithvarNodeMap.asArithVar(left); - }else{ - Assert(left.hasAttribute(Slack())); - return d_arithvarNodeMap.asArithVar(left); - } + return d_arithvarNodeMap.asArithVar(left); } @@ -430,63 +485,63 @@ Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){ return conflict; } -void TheoryArith::delayedSetupMonomial(const Monomial& mono){ +// void TheoryArith::delayedSetupMonomial(const Monomial& mono){ - Debug("arith::delay") << "delayedSetupMonomial(" << mono.getNode() << ")" << endl; +// Debug("arith::delay") << "delayedSetupMonomial(" << mono.getNode() << ")" << endl; - Assert(!mono.isConstant()); - VarList vl = mono.getVarList(); +// Assert(!mono.isConstant()); +// VarList vl = mono.getVarList(); - if(!d_arithvarNodeMap.hasArithVar(vl.getNode())){ - for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){ - Variable var = *i; - Node n = var.getNode(); +// if(!d_arithvarNodeMap.hasArithVar(vl.getNode())){ +// for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){ +// Variable var = *i; +// Node n = var.getNode(); - ++(d_statistics.d_statUserVariables); - ArithVar varN = requestArithVar(n,false); - setupInitialValue(varN); - } - - if(!vl.singleton()){ - d_out->setIncomplete(); - - Node n = vl.getNode(); - ++(d_statistics.d_statUserVariables); - ArithVar varN = requestArithVar(n,false); - setupInitialValue(varN); - } - } -} - -void TheoryArith::delayedSetupPolynomial(TNode polynomial){ - Debug("arith::delay") << "delayedSetupPolynomial(" << polynomial << ")" << endl; - - Assert(Polynomial::isMember(polynomial)); - // if d_nodeMap.hasArithVar() all of the variables and it are setup - if(!d_arithvarNodeMap.hasArithVar(polynomial)){ - Polynomial poly = Polynomial::parsePolynomial(polynomial); - Assert(!poly.containsConstant()); - for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){ - Monomial mono = *i; - delayedSetupMonomial(mono); - } - - if(polynomial.getKind() == PLUS){ - Assert(!polynomial.getAttribute(Slack()), - "Polynomial has slack attribute but not does not have arithvar"); - setupSlack(polynomial); - } - } -} - -void TheoryArith::delayedSetupEquality(TNode equality){ - Debug("arith::delay") << "delayedSetupEquality(" << equality << ")" << endl; +// ++(d_statistics.d_statUserVariables); +// ArithVar varN = requestArithVar(n,false); +// setupInitialValue(varN); +// } + +// if(!vl.singleton()){ +// d_out->setIncomplete(); + +// Node n = vl.getNode(); +// ++(d_statistics.d_statUserVariables); +// ArithVar varN = requestArithVar(n,false); +// setupInitialValue(varN); +// } +// } +// } + +// void TheoryArith::delayedSetupPolynomial(TNode polynomial){ +// Debug("arith::delay") << "delayedSetupPolynomial(" << polynomial << ")" << endl; + +// Assert(Polynomial::isMember(polynomial)); +// // if d_nodeMap.hasArithVar() all of the variables and it are setup +// if(!d_arithvarNodeMap.hasArithVar(polynomial)){ +// Polynomial poly = Polynomial::parsePolynomial(polynomial); +// Assert(!poly.containsConstant()); +// for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){ +// Monomial mono = *i; +// delayedSetupMonomial(mono); +// } + +// if(polynomial.getKind() == PLUS){ +// Assert(!polynomial.getAttribute(Slack()), +// "Polynomial has slack attribute but not does not have arithvar"); +// setupSlack(polynomial); +// } +// } +// } + +// void TheoryArith::delayedSetupEquality(TNode equality){ +// Debug("arith::delay") << "delayedSetupEquality(" << equality << ")" << endl; - Assert(equality.getKind() == EQUAL); +// Assert(equality.getKind() == EQUAL); - TNode left = equality[0]; - delayedSetupPolynomial(left); -} +// TNode left = equality[0]; +// delayedSetupPolynomial(left); +// } bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){ Assert(equality.getKind() == EQUAL); @@ -498,9 +553,13 @@ Node TheoryArith::assertionCases(TNode assertion){ Assert(simpKind != UNDEFINED_KIND); if(simpKind == EQUAL || simpKind == DISTINCT){ Node eq = (simpKind == DISTINCT) ? assertion[0] : assertion; - - if(!canSafelyAvoidEqualitySetup(eq)){ - delayedSetupEquality(eq); + + if(!isSetup(eq)){ + //The previous code was equivalent to: + setupAtom(eq, false); + //We can try: + //setupAtom(eq, true); + addToContext(eq); } } @@ -509,7 +568,7 @@ Node TheoryArith::assertionCases(TNode assertion){ Debug("arith::assertions") << "arith assertion(" << assertion << " \\-> " - < d_variables; + /** + * The map between arith variables to nodes. + */ ArithVarNodeMap d_arithvarNodeMap; + + NodeSet d_setupNodes; + bool isSetup(Node n){ + return d_setupNodes.find(n) != d_setupNodes.end(); + } + void markSetup(Node n){ + Assert(!isSetup(n)); + d_setupNodes.insert(n); + } + + void setupVariable(const Variable& x); + void setupVariableList(const VarList& vl); + void setupPolynomial(const Polynomial& poly); + void setupAtom(TNode atom, bool addToDatabase); + + /** * List of the types of variables in the system. * "True" means integer, "false" means (non-integer) real. @@ -225,10 +262,10 @@ private: * preregistered. * Currently these MUST be introduced by combination. */ - void delayedSetupEquality(TNode equality); - - void delayedSetupPolynomial(TNode polynomial); - void delayedSetupMonomial(const Monomial& mono); + //void delayedSetupEquality(TNode equality); + + //void delayedSetupPolynomial(TNode polynomial); + //void delayedSetupMonomial(const Monomial& mono); /** * Performs a check to see if it is definitely true that setup can be avoided. @@ -271,7 +308,7 @@ private: void internalExplain(TNode n, NodeBuilder<>& explainBuilder); - void asVectors(Polynomial& p, + void asVectors(const Polynomial& p, std::vector& coeffs, std::vector& variables); @@ -293,7 +330,6 @@ private: TimerStat d_presolveTime; IntStat d_initialTableauSize; - //ListStat d_tableauSizeHistory; IntStat d_currSetToSmaller; IntStat d_smallerSetToCurr; TimerStat d_restartTimer; diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index d0340616f..843d29200 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -14,6 +14,7 @@ TESTS = \ arith-int-005.cvc \ arith-int-006.cvc \ arith-int-007.cvc \ + arith-int-008.cvc \ arith-int-009.cvc \ arith-int-010.cvc \ arith-int-011.cvc \ @@ -23,23 +24,92 @@ TESTS = \ arith-int-017.cvc \ arith-int-018.cvc \ arith-int-019.cvc \ - arith-int-020.cvc + arith-int-020.cvc \ + arith-int-021.cvc \ + arith-int-023.cvc \ + arith-int-025.cvc \ + arith-int-026.cvc \ + arith-int-027.cvc \ + arith-int-028.cvc \ + arith-int-029.cvc \ + arith-int-030.cvc \ + arith-int-031.cvc \ + arith-int-032.cvc \ + arith-int-033.cvc \ + arith-int-034.cvc \ + arith-int-035.cvc \ + arith-int-036.cvc \ + arith-int-037.cvc \ + arith-int-038.cvc \ + arith-int-039.cvc \ + arith-int-040.cvc \ + arith-int-043.cvc \ + arith-int-044.cvc \ + arith-int-045.cvc \ + arith-int-046.cvc \ + arith-int-049.cvc \ + arith-int-051.cvc \ + arith-int-052.cvc \ + arith-int-053.cvc \ + arith-int-054.cvc \ + arith-int-055.cvc \ + arith-int-056.cvc \ + arith-int-057.cvc \ + arith-int-058.cvc \ + arith-int-059.cvc \ + arith-int-060.cvc \ + arith-int-061.cvc \ + arith-int-062.cvc \ + arith-int-063.cvc \ + arith-int-064.cvc \ + arith-int-065.cvc \ + arith-int-066.cvc \ + arith-int-067.cvc \ + arith-int-068.cvc \ + arith-int-069.cvc \ + arith-int-070.cvc \ + arith-int-071.cvc \ + arith-int-072.cvc \ + arith-int-073.cvc \ + arith-int-074.cvc \ + arith-int-075.cvc \ + arith-int-076.cvc \ + arith-int-077.cvc \ + arith-int-078.cvc \ + arith-int-079.cvc \ + arith-int-080.cvc \ + arith-int-081.cvc \ + arith-int-083.cvc \ + arith-int-086.cvc \ + arith-int-087.cvc \ + arith-int-088.cvc \ + arith-int-089.cvc \ + arith-int-090.cvc \ + arith-int-091.cvc \ + arith-int-092.cvc \ + arith-int-093.cvc \ + arith-int-094.cvc \ + arith-int-095.cvc \ + arith-int-096.cvc \ + arith-int-098.cvc \ + arith-int-099.cvc \ + arith-int-100.cvc EXTRA_DIST = $(TESTS) \ - arith-int-008.cvc \ arith-int-012.cvc \ arith-int-013.cvc \ arith-int-022.cvc \ + arith-int-024.cvc \ + arith-int-041.cvc \ arith-int-042.cvc \ arith-int-042.min.cvc \ - arith-int-043.cvc \ arith-int-047.cvc \ + arith-int-048.cvc \ arith-int-050.cvc \ arith-int-082.cvc \ arith-int-084.cvc \ - arith-int-097.cvc \ - arith-int-098.cvc \ - arith-int-100.cvc + arith-int-085.cvc \ + arith-int-097.cvc #if CVC4_BUILD_PROFILE_COMPETITION #else -- 2.30.2