diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/approx_simplex.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 36 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 19 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 10 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 17 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 4 | ||||
-rw-r--r-- | src/theory/arith/constraint.cpp | 26 | ||||
-rw-r--r-- | src/theory/arith/constraint.h | 7 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 2 | ||||
-rw-r--r-- | src/theory/arith/proof_checker.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 19 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 5 |
17 files changed, 93 insertions, 79 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 8e75f6850..caa052065 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -1785,7 +1785,7 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){ // Node explainSet(const set<ConstraintP>& inp){ // Assert(!inp.empty()); -// NodeBuilder<> nb(kind::AND); +// NodeBuilder nb(kind::AND); // set<ConstraintP>::const_iterator iter, end; // for(iter = inp.begin(), end = inp.end(); iter != end; ++iter){ // const ConstraintP c = *iter; diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 4c991dba3..218fdf179 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -35,7 +35,7 @@ namespace theory { namespace arith { Node ArithIteUtils::applyReduceVariablesInItes(Node n){ - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (n.getOperator()); } @@ -239,7 +239,7 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){ } if(n.getNumChildren() > 0){ - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (n.getOperator()); } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 87aba7b45..452200796 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -235,7 +235,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if( num==1 ){ return RewriteResponse(REWRITE_AGAIN, base); }else{ - NodeBuilder<> nb(kind::MULT); + NodeBuilder nb(kind::MULT); for(unsigned i=0; i < num; ++i){ nb << base; } diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 9c764ac7a..ce54133c5 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -57,8 +57,8 @@ ArithStaticLearner::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications); } -void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ - +void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned) +{ vector<TNode> workList; workList.push_back(n); TNodeSet processed; @@ -101,8 +101,10 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ } } - -void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){ +void ArithStaticLearner::process(TNode n, + NodeBuilder& learned, + const TNodeSet& defTrue) +{ Debug("arith::static") << "===================== looking at " << n << endl; switch(n.getKind()){ @@ -136,7 +138,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet } } -void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ +void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned) +{ Assert(n.getKind() == kind::ITE); Assert(n[0].getKind() != EQUAL); Assert(isRelationOperator(n[0].getKind())); @@ -167,8 +170,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ 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; + Node nLeqX = NodeBuilder(LEQ) << n << t; + Node nLeqY = NodeBuilder(LEQ) << n << e; Debug("arith::static") << n << "is a min =>" << nLeqX << nLeqY << endl; learned << nLeqX << nLeqY; ++(d_statistics.d_iteMinMaxApplications); @@ -176,8 +179,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ } 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; + Node nGeqX = NodeBuilder(GEQ) << n << t; + Node nGeqY = NodeBuilder(GEQ) << n << e; Debug("arith::static") << n << "is a max =>" << nGeqX << nGeqY << endl; learned << nGeqX << nGeqY; ++(d_statistics.d_iteMinMaxApplications); @@ -188,7 +191,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ } } -void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ +void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned) +{ Assert(n.getKind() == ITE); Debug("arith::static") << "iteConstant(" << n << ")" << endl; @@ -202,9 +206,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ d_minMap.insert(n, min); Node nGeqMin; if (min.getInfinitesimalPart() == 0) { - nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart()); + nGeqMin = NodeBuilder(kind::GEQ) + << n << mkRationalNode(min.getNoninfinitesimalPart()); } else { - nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart()); + nGeqMin = NodeBuilder(kind::GT) + << n << mkRationalNode(min.getNoninfinitesimalPart()); } learned << nGeqMin; Debug("arith::static") << n << " iteConstant" << nGeqMin << endl; @@ -221,9 +227,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ d_maxMap.insert(n, max); Node nLeqMax; if (max.getInfinitesimalPart() == 0) { - nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart()); + nLeqMax = NodeBuilder(kind::LEQ) + << n << mkRationalNode(max.getNoninfinitesimalPart()); } else { - nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart()); + nLeqMax = NodeBuilder(kind::LT) + << n << mkRationalNode(max.getNoninfinitesimalPart()); } learned << nLeqMax; Debug("arith::static") << n << " iteConstant" << nLeqMax << endl; diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 73810dedd..b96d7a86a 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -45,19 +45,22 @@ private: public: ArithStaticLearner(context::Context* userContext); ~ArithStaticLearner(); - void staticLearning(TNode n, NodeBuilder<>& learned); + void staticLearning(TNode n, NodeBuilder& learned); void addBound(TNode n); -private: - void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue); + private: + void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue); - void iteMinMax(TNode n, NodeBuilder<>& learned); - void iteConstant(TNode n, NodeBuilder<>& learned); + void iteMinMax(TNode n, NodeBuilder& learned); + void iteConstant(TNode n, NodeBuilder& learned); - /** These fields are designed to be accessible to ArithStaticLearner methods. */ - class Statistics { - public: + /** + * These fields are designed to be accessible to ArithStaticLearner methods. + */ + class Statistics + { + public: IntStat d_iteMinMaxApplications; IntStat d_iteConstantApplications; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 852550917..bc35c6941 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -194,17 +194,18 @@ inline Kind negateKind(Kind k){ inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); - NodeBuilder<> orBuilder(kind::OR); + NodeBuilder orBuilder(kind::OR); for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){ TNode child = *i; - Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child); + Node negatedChild = NodeBuilder(kind::NOT) << (child); orBuilder << negatedChild; } return orBuilder; } -inline Node maybeUnaryConvert(NodeBuilder<>& builder){ +inline Node maybeUnaryConvert(NodeBuilder& builder) +{ Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT); Assert(builder.getNumChildren() >= 1); @@ -247,7 +248,8 @@ inline Node getIdentity(Kind k){ } } -inline Node safeConstructNary(NodeBuilder<>& nb) { +inline Node safeConstructNary(NodeBuilder& nb) +{ switch (nb.getNumChildren()) { case 0: return getIdentity(nb.getKind()); diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index ea597468d..43589fdce 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -223,7 +223,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP TNode eq = d_watchedEqualities[s]; ConstraintCP eqC = d_constraintDatabase.getConstraint( s, ConstraintType::Equality, lb->getValue()); - NodeBuilder<> reasonBuilder(Kind::AND); + NodeBuilder reasonBuilder(Kind::AND); auto pfLb = lb->externalExplainByAssertions(reasonBuilder); auto pfUb = ub->externalExplainByAssertions(reasonBuilder); Node reason = safeConstructNary(reasonBuilder); @@ -256,7 +256,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){ //Explain for conflict is correct as these proofs are generated //and stored eagerly //These will be safe for propagation later as well - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); // An open proof of eq from literals now in reason. if (Debug.isOn("arith::cong")) { @@ -284,7 +284,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){ //Explain for conflict is correct as these proofs are generated and stored eagerly //These will be safe for propagation later as well - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); // An open proof of eq from literals now in reason. auto pf = c->externalExplainByAssertions(nb); if (Debug.isOn("arith::cong::notzero")) @@ -456,7 +456,9 @@ void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumpti } } -void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){ +void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, + NodeBuilder& nb) +{ std::set<TNode>::const_iterator it = s.begin(); std::set<TNode>::const_iterator it_end = s.end(); for(; it != it_end; ++it) { @@ -504,7 +506,8 @@ TrustNode ArithCongruenceManager::explain(TNode external) return trn; } -void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){ +void ArithCongruenceManager::explain(TNode external, NodeBuilder& out) +{ Node internal = externalToInternal(external); std::vector<TNode> assumptions; @@ -627,7 +630,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ Node eq = xAsNode.eqNode(asRational); d_keepAlive.push_back(eq); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pf = c->externalExplainByAssertions(nb); Node reason = safeConstructNary(nb); d_keepAlive.push_back(reason); @@ -646,7 +649,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ << ub << std::endl; ArithVar x = lb->getVariable(); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pfLb = lb->externalExplainByAssertions(nb); auto pfUb = ub->externalExplainByAssertions(nb); Node reason = safeConstructNary(nb); diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 055d5ddbb..325f7002b 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -212,7 +212,7 @@ private: void enableSharedTerms(); void dequeueLiterals(); - void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb); + void enqueueIntoNB(const std::set<TNode> all, NodeBuilder& nb); /** * Determine an explaination for `internal`. That is a conjunction of theory @@ -251,7 +251,7 @@ private: */ TrustNode explain(TNode literal); - void explain(TNode lit, NodeBuilder<>& out); + void explain(TNode lit, NodeBuilder& out); void addWatchedPair(ArithVar s, TNode x, TNode y); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index baa9b1ebb..14daca11b 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -481,7 +481,7 @@ bool Constraint::isInternalAssumption() const { TrustNode Constraint::externalExplainByAssertions() const { - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel); Node exp = safeConstructNary(nb); if (d_database->isProofEnabled()) @@ -1078,12 +1078,12 @@ TrustNode Constraint::split() TNode lhs = eqNode[0]; TNode rhs = eqNode[1]; - Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs; - Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; - Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; - Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs; + Node leqNode = NodeBuilder(kind::LEQ) << lhs << rhs; + Node ltNode = NodeBuilder(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder(kind::GT) << lhs << rhs; + Node geqNode = NodeBuilder(kind::GEQ) << lhs << rhs; - Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode; + Node lemma = NodeBuilder(OR) << leqNode << geqNode; TrustNode trustedLemma; if (d_database->isProofEnabled()) @@ -1517,7 +1517,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const Assert(hasProof()); Assert(!isAssumption()); Assert(!isInternalAssumption()); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pfFromAssumptions = externalExplain(nb, d_assertionOrder); Node n = safeConstructNary(nb); if (d_database->isProofEnabled()) @@ -1553,7 +1553,7 @@ TrustNode Constraint::externalExplainConflict() const { Debug("pf::arith::explain") << this << std::endl; Assert(inConflict()); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); auto pf1 = externalExplainByAssertions(nb); auto not2 = getNegation()->getProofLiteral().negate(); auto pf2 = getNegation()->externalExplainByAssertions(nb); @@ -1650,7 +1650,7 @@ void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){ } Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); ConstraintCPVec::const_iterator i, end; for(i = v.begin(), end = v.end(); i != end; ++i){ ConstraintCP v_i = *i; @@ -1660,7 +1660,7 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order) } std::shared_ptr<ProofNode> Constraint::externalExplain( - NodeBuilder<>& nb, AssertionOrder order) const + NodeBuilder& nb, AssertionOrder order) const { if (Debug.isOn("pf::arith::explain")) { @@ -1857,14 +1857,14 @@ std::shared_ptr<ProofNode> Constraint::externalExplain( } Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); a->externalExplainByAssertions(nb); b->externalExplainByAssertions(nb); return nb; } Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); a->externalExplainByAssertions(nb); b->externalExplainByAssertions(nb); c->externalExplainByAssertions(nb); @@ -1982,7 +1982,7 @@ TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const return d_congruenceManager.explain(c->getLiteral()); } -void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const +void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder& nb) const { Assert(c->hasLiteral()); // NOTE: this is not a recommended method since it ignores proofs diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index d00f16c90..33e39a5f0 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -571,8 +571,7 @@ class Constraint { * This is not appropriate for propagation! * Use explainForPropagation() instead. */ - std::shared_ptr<ProofNode> externalExplainByAssertions( - NodeBuilder<>& nb) const + std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const { return externalExplain(nb, AssertionOrderSentinel); } @@ -876,7 +875,7 @@ class Constraint { * This is the minimum fringe of the implication tree * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). */ - std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb, + std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb, AssertionOrder order) const; static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); @@ -1168,7 +1167,7 @@ private: */ TrustNode eeExplain(ConstraintCP c) const; /** Get an explanation for this constraint from the equality engine */ - void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; + void eeExplain(ConstraintCP c, NodeBuilder& nb) const; /** * Returns a constraint with the variable v, the constraint type t, and a value diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 6e069cdf6..3825a3a42 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -198,7 +198,7 @@ Node DioSolver::proveIndex(TrailIndex i){ const Polynomial& proof = d_trail[i].d_proof; Assert(!proof.isConstant()); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for(Polynomial::iterator iter = proof.begin(), end = proof.end(); iter!= end; ++iter){ Monomial m = (*iter); Assert(!m.isConstant()); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 7b9002d82..940812604 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -420,7 +420,7 @@ public: template <class GetNodeIterator> inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) { - NodeBuilder<> nb(k); + NodeBuilder nb(k); while(start != end) { nb << (*start).getNode(); diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 23f141535..248897ced 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -108,8 +108,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder<> leftSum(Kind::PLUS); - NodeBuilder<> rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::PLUS); + NodeBuilder rightSum(Kind::PLUS); for (size_t i = 0; i < children.size(); ++i) { // Adjust strictness @@ -163,8 +163,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder<> leftSum(Kind::PLUS); - NodeBuilder<> rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::PLUS); + NodeBuilder rightSum(Kind::PLUS); for (size_t i = 0; i < children.size(); ++i) { Rational scalar = args[i].getConst<Rational>(); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 834a3d52d..e68ff7d11 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -145,8 +145,8 @@ TrustNode TheoryArith::ppRewriteEq(TNode atom) return TrustNode::null(); } Assert(atom[0].getType().isReal()); - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; + Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; + Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; @@ -167,7 +167,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert( return d_internal->ppAssert(tin, outSubstitutions); } -void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned) +{ d_internal->ppStaticLearn(n, learned); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0c1320b03..99fa9f379 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -122,7 +122,7 @@ class TheoryArith : public Theory { * symbols. */ TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; std::string identify() const override { return std::string("TheoryArith"); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d38dd881b..0a64a4e63 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -239,7 +239,7 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& // Assert(uppos < upconf.getNumChildren()); // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos])); - // NodeBuilder<> nb(kind::AND); + // NodeBuilder nb(kind::AND); // dropPosition(nb, dnconf, dnpos); // dropPosition(nb, upconf, uppos); // return safeConstructNary(nb); @@ -1196,14 +1196,13 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( return Theory::PP_ASSERT_STATUS_UNSOLVED; } -void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder& learned) +{ TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); d_learner.staticLearning(n, learned); } - - ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){ ArithVar bestBasic = ARITHVAR_SENTINEL; uint64_t bestRowLength = std::numeric_limits<uint64_t>::max(); @@ -2206,7 +2205,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){ Debug("arith::toSumNode") << "toSumNode() begin" << endl; - NodeBuilder<> nb(kind::PLUS); + NodeBuilder nb(kind::PLUS); NodeManager* nm = NodeManager::currentNM(); DenseMap<Rational>::const_iterator iter, end; iter = sum.begin(), end = sum.end(); @@ -4677,7 +4676,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b } Node flattenImplication(Node imp){ - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); std::unordered_set<Node, NodeHashFunction> included; Node left = imp[0]; Node right = imp[1]; @@ -4765,7 +4764,7 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // Add the explaination proofs. for (const auto constraint : explain) { - NodeBuilder<> nb; + NodeBuilder nb; conflictPfs.push_back(constraint->externalExplainByAssertions(nb)); } // Collect the farkas coefficients, as nodes. @@ -5270,7 +5269,7 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t Assert(Polynomial::isMember(tp)); tmp.second = DeltaRational(0); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Polynomial p = Polynomial::parsePolynomial(tp); for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) { @@ -5455,7 +5454,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg switch(finalState){ case Inferred: { - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ const Tableau::Entry& e =*ri; ArithVar colVar = e.getColVar(); @@ -5668,7 +5667,7 @@ ArithProofRuleChecker* TheoryArithPrivate::getProofChecker() // switch(finalState){ // case Inferred: // { -// NodeBuilder<> nb(kind::AND); +// NodeBuilder nb(kind::AND); // for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); // !ri.atEnd(); ++ri){ // const Tableau::Entry& e =*ri; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index ca2df4bd8..ba3fdfaf5 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -474,7 +474,7 @@ private: void notifyRestart(); Theory::PPAssertStatus ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions); - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder& learned); std::string identify() const { return std::string("TheoryArith"); } @@ -681,8 +681,7 @@ private: bool isImpliedUpperBound(ArithVar var, Node exp); bool isImpliedLowerBound(ArithVar var, Node exp); - void internalExplain(TNode n, NodeBuilder<>& explainBuilder); - + void internalExplain(TNode n, NodeBuilder& explainBuilder); void asVectors(const Polynomial& p, std::vector<Rational>& coeffs, |