diff options
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 1244ae828..37474bfec 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -74,11 +74,11 @@ class SubtheorySolver { virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} - virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0; + virtual bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) = 0; virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; - virtual void addSharedTerm(TNode node) {} bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { Assert(!done()); |