diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4acd1b847..8f7e975cd 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -30,6 +30,8 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" #include "theory/valuation.h" using namespace CVC4::context; @@ -363,7 +365,6 @@ void TheoryBV::checkForLemma(TNode fact) { } } - void TheoryBV::check(Effort e) { if (done() && !fullEffort(e)) { @@ -706,6 +707,7 @@ Node TheoryBV::explain(TNode node) { // return the explanation Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; + Debug("bitvector::explain") << "TheoryBV::explain done. \n"; return explanation; } @@ -796,6 +798,16 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector return changed; } +void TheoryBV::setProofLog( BitVectorProof * bvp ) { + if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ + d_eagerSolver->setProofLog( bvp ); + }else{ + for( unsigned i=0; i< d_subtheories.size(); i++ ){ + d_subtheories[i]->setProofLog( bvp ); + } + } +} + void TheoryBV::setConflict(Node conflict) { if (options::bvAbstraction()) { Node new_conflict = d_abstractionModule->simplifyConflict(conflict); |