diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 11 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 5 |
2 files changed, 6 insertions, 10 deletions
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 02570b12c..c49909fe6 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -102,6 +102,11 @@ void CoreSolver::preRegister(TNode node) { } } else { d_equalityEngine.addTerm(node); + // Register with the extended theory, for context-dependent simplification. + // Notice we do this for registered terms but not internally generated + // equivalence classes. The two should roughly cooincide. Since ExtTheory is + // being used as a heuristic, it is good enough to be registered here. + d_extTheory->registerTerm(node); } } @@ -397,10 +402,6 @@ void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_solver.conflict(t1, t2); } -void CoreSolver::NotifyClass::eqNotifyNewClass(TNode t) { - d_solver.eqNotifyNewClass( t ); -} - bool CoreSolver::storePropagation(TNode literal) { return d_bv->storePropagation(literal, SUB_CORE); } @@ -412,8 +413,6 @@ void CoreSolver::conflict(TNode a, TNode b) { d_bv->setConflict(conflict); } -void CoreSolver::eqNotifyNewClass(TNode t) { d_extTheory->registerTerm(t); } - bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) { if (d_useSlicer) return utils::isCoreTerm(term, seen); diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 181d6ec79..ea652e7cd 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -61,7 +61,7 @@ class CoreSolver : public SubtheorySolver { TNode t2, bool value) override; void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; - void eqNotifyNewClass(TNode t) override; + void eqNotifyNewClass(TNode t) override {} void eqNotifyMerge(TNode t1, TNode t2) override {} void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; @@ -79,9 +79,6 @@ class CoreSolver : public SubtheorySolver { /** Store a conflict from merging two constants */ void conflict(TNode a, TNode b); - /** new equivalence class */ - void eqNotifyNewClass(TNode t); - std::unique_ptr<Slicer> d_slicer; context::CDO<bool> d_isComplete; unsigned d_lemmaThreshold; |