summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r--src/theory/uf/theory_uf.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 604b1f44c..62ca640aa 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -193,7 +193,7 @@ public:
void preRegisterTerm(TNode term);
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m );
+ void collectModelInfo( TheoryModel* m, bool fullModel );
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
void presolve();
@@ -202,6 +202,7 @@ public:
void computeCareGraph();
void propagate(Effort effort);
+ Node getNextDecisionRequest();
EqualityStatus getEqualityStatus(TNode a, TNode b);
@@ -226,7 +227,6 @@ public:
void registerPpRewrite(TNode op, PpRewrite* callback) {
d_registeredPpRewrites.insert(std::make_pair(op, callback));
}
-
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback