summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/approx_simplex.cpp2
-rw-r--r--src/theory/arith/arith_ite_utils.cpp4
-rw-r--r--src/theory/arith/arith_rewriter.cpp2
-rw-r--r--src/theory/arith/arith_static_learner.cpp36
-rw-r--r--src/theory/arith/arith_static_learner.h19
-rw-r--r--src/theory/arith/arith_utilities.h10
-rw-r--r--src/theory/arith/congruence_manager.cpp17
-rw-r--r--src/theory/arith/congruence_manager.h4
-rw-r--r--src/theory/arith/constraint.cpp26
-rw-r--r--src/theory/arith/constraint.h7
-rw-r--r--src/theory/arith/dio_solver.cpp2
-rw-r--r--src/theory/arith/normal_form.h2
-rw-r--r--src/theory/arith/proof_checker.cpp8
-rw-r--r--src/theory/arith/theory_arith.cpp7
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arith/theory_arith_private.cpp19
-rw-r--r--src/theory/arith/theory_arith_private.h5
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback