diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 7 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 3 |
5 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8f006d8ff..5fbbd3700 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1841,7 +1841,7 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge Node EqualityEngine::evaluateTerm(TNode node) { Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl; - NodeBuilder<> builder; + NodeBuilder builder; builder << node.getKind(); if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << node.getOperator(); diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 558838bd8..0586da6a0 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -525,7 +525,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Debug("ufsymm") << "UFSYMM p == " << p << endl; if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; - NodeBuilder<> disj(kind::OR); + NodeBuilder disj(kind::OR); NodeManager* nm = NodeManager::currentNM(); for (const Node& nn : cts) { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index b4ea3640d..e38a1f67b 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -65,7 +65,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; - NodeBuilder<> d_assertions; + NodeBuilder d_assertions; std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e8ce7660a..9cb37a26d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -108,7 +108,7 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { return conjunctions[0]; } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); std::set<TNode>::const_iterator it = all.begin(); std::set<TNode>::const_iterator it_end = all.end(); while (it != it_end) { @@ -343,7 +343,8 @@ void TheoryUF::presolve() { Debug("uf") << "uf: end presolve()" << endl; } -void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned) +{ //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); vector<TNode> workList; @@ -462,7 +463,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { if(options::ufSymmetryBreaker()) { d_symb.assertFormula(n); } -}/* TheoryUF::ppStaticLearn() */ +} /* TheoryUF::ppStaticLearn() */ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index bae2a2544..cc53094b7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -146,8 +146,7 @@ private: void preRegisterTerm(TNode term) override; TrustNode explain(TNode n) override; - - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; void presolve() override; void computeCareGraph() override; |