diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-19 03:34:43 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-19 03:34:43 -0800 |
| commit | b4c9b783384fb05a3e71ff535b5f790e79c28a94 (patch) | |
| tree | 4294c32fe33f5bf2e4924264c711579ca0526c51 /src/theory/bv | |
| parent | 8b494ee2e856a0ddb5ea60a1a39340816ba0fc29 (diff) | |
Fix missing-override warning (#2811)
`TLazyBitblaster::setProofLog()` was defined even though the method was
not virtual before PR #2808 and `TBitblaster` was implementing the same
method. After that PR, which made the method virtual, GCC complained
about a missing `override` keyword for `setProofLog()`. However, the
method should have been removed (see
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247299617)).
This commit removes the function definition.
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 8 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 1 |
2 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 2a47c2315..3b44bfddf 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -564,14 +564,6 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp) -{ - THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver); - prop::SatVariable t = d_satSolver->trueVar(); - prop::SatVariable f = d_satSolver->falseVar(); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f)); -} - void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); d_assertedAtoms->deleteSelf(); diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 9af74d8db..8dbf7807d 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -77,7 +77,6 @@ class TLazyBitblaster : public TBitblaster<Node> * constants to equivalence classes that don't already have them */ bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(proof::BitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } |