From: Tim King Date: Sun, 14 Jun 2015 13:03:15 +0000 (+0200) Subject: Fixes for shared term normalization in replay for constraint construction. X-Git-Tag: cvc5-1.0.0~6275 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=232782d690e1dc333ebc7bec1a9302f086c947b6;p=cvc5.git Fixes for shared term normalization in replay for constraint construction. --- diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 94632e50e..822f0e578 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -34,7 +34,7 @@ namespace arith { /** Given a simplifiedKind this returns the corresponding ConstraintType. */ //ConstraintType constraintTypeOfLiteral(Kind k); -ConstraintType constraintTypeOfComparison(const Comparison& cmp){ +ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){ Kind k = cmp.comparisonKind(); switch(k){ case LT: @@ -989,7 +989,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){ Assert(!hasLiteral(negationNode)); Comparison posCmp = Comparison::parseNormalForm(atomNode); - ConstraintType posType = constraintTypeOfComparison(posCmp); + ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp); Polynomial nvp = posCmp.normalizedVariablePart(); ArithVar v = d_avariables.asArithVar(nvp.getNode()); @@ -1024,7 +1024,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){ }else{ Comparison negCmp = Comparison::parseNormalForm(negationNode); - ConstraintType negType = constraintTypeOfComparison(negCmp); + ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp); DeltaRational negDR = negCmp.normalizedDeltaRational(); ConstraintP negC = new Constraint(v, negType, negDR); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 795798450..0e0b35020 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -93,6 +93,13 @@ #include #include +namespace CVC4 { +namespace theory { +namespace arith { +class Comparison; +} +} +} namespace CVC4 { namespace theory { namespace arith { @@ -448,6 +455,7 @@ private: void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation); + class ConstraintRuleCleanup { public: inline void operator()(ConstraintRule* crp){ @@ -517,6 +525,8 @@ private: public: + static ConstraintType constraintTypeOfComparison(const Comparison& cmp); + inline ConstraintType getType() const { return d_type; } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 616656408..a4825c1c4 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2258,10 +2258,32 @@ std::pair TheoryArithPrivate::replayGetConstraint(const D Node sum = toSumNode(d_partialModel, lhs); if(sum.isNull()){ return make_pair(NullConstraint, added); } - Node norm = Rewriter::rewrite(sum); - DeltaRational dr(rhs); + Debug("approx::constraint") << "replayGetConstraint " << sum + << " " << k + << " " << rhs + << endl; - ConstraintType t = (k == kind::LEQ) ? UpperBound : LowerBound; + Assert( k == kind::LEQ || k == kind::GEQ ); + + Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs)); + Node rewritten = Rewriter::rewrite(comparison); + if(!(Comparison::isNormalAtom(rewritten))){ + return make_pair(NullConstraint, added); + } + + Comparison cmp = Comparison::parseNormalForm(rewritten); + if(cmp.isBoolean()){ return make_pair(NullConstraint, added); } + + Polynomial nvp = cmp.normalizedVariablePart(); + if(nvp.isZero()){ return make_pair(NullConstraint, added); } + + Node norm = nvp.getNode(); + + ConstraintType t = Constraint::constraintTypeOfComparison(cmp); + DeltaRational dr = cmp.normalizedDeltaRational(); + + Debug("approx::constraint") << "rewriting " << rewritten << endl + << " |-> " << norm << " " << t << " " << dr << endl; Assert(!branch || d_partialModel.hasArithVar(norm)); ArithVar v = ARITHVAR_SENTINEL; @@ -2299,6 +2321,8 @@ std::pair TheoryArithPrivate::replayGetConstraint(const D return make_pair(imp, added); } } + + ConstraintP newc = d_constraintDatabase.getConstraint(v, t, dr); d_replayConstraints.push_back(newc); return make_pair(newc, added); @@ -2342,6 +2366,7 @@ std::pair TheoryArithPrivate::replayGetConstraint(const C // } Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ + Debug("arith::toSumNode") << "toSumNode() begin" << endl; NodeBuilder<> nb(kind::PLUS); NodeManager* nm = NodeManager::currentNM(); DenseMap::const_iterator iter, end; @@ -2351,8 +2376,11 @@ Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ if(!vars.hasNode(x)){ return Node::null(); } Node xNode = vars.asNode(x); const Rational& q = sum[x]; - nb << nm->mkNode(kind::MULT, mkRationalNode(q), xNode); + Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode); + Debug("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl; + nb << mult; } + Debug("arith::toSumNode") << "toSumNode() end" << endl; return safeConstructNary(nb); }