summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/theory_uf.cpp4
-rw-r--r--src/theory/uf/theory_uf.h2
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2344adc70..7f5e11a64 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -282,7 +282,7 @@ void TheoryUF::presolve() {
Debug("uf") << "uf: end presolve()" << endl;
}
-void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
+void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
//TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
vector<TNode> workList;
@@ -393,7 +393,7 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
if(Options::current()->ufSymmetryBreaker) {
d_symb.assertFormula(n);
}
-}/* TheoryUF::staticLearning() */
+}/* TheoryUF::ppStaticLearn() */
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
if (d_equalityEngine.areEqual(a, b)) {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2a02208dc..ab391e242 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -109,7 +109,7 @@ public:
void preRegisterTerm(TNode term);
Node explain(TNode n);
- void staticLearning(TNode in, NodeBuilder<>& learned);
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned);
void presolve();
void addSharedTerm(TNode n);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback