diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 5 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 336 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 50 |
3 files changed, 249 insertions, 142 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 <vector> #include <stdint.h> #include <limits> @@ -44,6 +45,10 @@ typedef uint32_t ArithVar; typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap; +//Sets of Nodes +typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef context::CDSet<Node, NodeHashFunction> CDNodeSet; + inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst<Rational>(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<SlackAttrID, bool> 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<ArithVar> variables; + vector<Rational> 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<Rational>& coeffs, std::vector<ArithVar>& variables) { +void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& 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<Rational>& 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<Rational>& 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<ArithVar> variables; - vector<Rational> coefficients; +// Polynomial polyLeft = Polynomial::parsePolynomial(left); - asVectors(polyLeft, coefficients, variables); +// vector<ArithVar> variables; +// vector<Rational> 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("<<x<<")"<<std::endl; + Debug("arith") << "setupVariable("<<x<<")"<<std::endl; } ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){ TNode left = getSide<true>(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 << " \\-> " - <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; + << x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; switch(simpKind){ case LEQ: if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { @@ -739,9 +798,9 @@ void TheoryArith::splitDisequalities(){ 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; + 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; @@ -804,11 +863,18 @@ void TheoryArith::propagate(Effort e) { while(d_propManager.hasMorePropagations()){ TNode toProp = d_propManager.getPropagation(); - Node satValue = d_valuation.getSatValue(toProp); - AlwaysAssert(satValue.isNull()); - TNode exp = d_propManager.explain(toProp); - propagated = true; - d_out->propagate(toProp); + TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp; + if(inContextAtom(atom)){ + Node satValue = d_valuation.getSatValue(toProp); + AlwaysAssert(satValue.isNull()); + propagated = true; + d_out->propagate(toProp); + }else{ + //Not clear if this is a good time to do this or not... + Debug("arith::propagate") << "Atom is not in context" << toProp << endl; + #warning "enable remove atom in database" + //d_atomDatabase.removeAtom(atom); + } } if(!propagated){ @@ -1032,7 +1098,7 @@ void TheoryArith::presolve(){ static int callCount = 0; Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; - learner.clear(); + d_learner.clear(); check(FULL_EFFORT); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1ba9a50e0..e8d920084 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -58,8 +58,26 @@ namespace arith { class TheoryArith : public Theory { private: + /** + * The set of atoms that are currently in the context. + * This is exactly the union of preregistered atoms and + * equalities from sharing. + * This is used to reconstruct the rest of arithmetic. + */ + CDNodeSet d_atomsInContext; + bool inContextAtom(TNode atom){ + Assert(isRelationOperator(atom.getKind())); + Assert(Comparison::isNormalAtom(atom)); + return d_atomsInContext.contains(atom); + } + void addToContext(TNode atom){ + Assert(isRelationOperator(atom.getKind())); + Assert(Comparison::isNormalAtom(atom)); + d_atomsInContext.insert(atom); + } + /** Static learner. */ - ArithStaticLearner learner; + ArithStaticLearner d_learner; /** * List of the variables in the system. @@ -67,8 +85,27 @@ private: */ std::vector<Node> 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<Rational>& coeffs, std::vector<ArithVar>& variables); @@ -293,7 +330,6 @@ private: TimerStat d_presolveTime; IntStat d_initialTableauSize; - //ListStat<uint32_t> d_tableauSizeHistory; IntStat d_currSetToSmaller; IntStat d_smallerSetToCurr; TimerStat d_restartTimer; |