diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-30 15:15:44 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-30 22:15:44 +0000 |
| commit | 839f64ea1f065415268bdb2bfe518ad727ed2a40 (patch) | |
| tree | f8bbaed23e5e15167ddb68f7097d904d6d05aa89 /src/theory/bv/bv_solver.h | |
| parent | df3ffb33b8173f252b7720d27aa0204e8ff3632e (diff) | |
bv: Refactor ppAssert and move to TheoryBV. (#6470)
This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.
Diffstat (limited to 'src/theory/bv/bv_solver.h')
| -rw-r--r-- | src/theory/bv/bv_solver.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 282be6bfc..8ff4318c0 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -86,9 +86,6 @@ class BVSolver virtual std::string identify() const = 0; - virtual Theory::PPAssertStatus ppAssert( - TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0; - virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; virtual void ppStaticLearn(TNode in, NodeBuilder& learned){}; |