diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e7e4d464f..27138abfc 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -87,7 +87,10 @@ public: void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + + void setProofLog( BitVectorProof * bvp ); private: @@ -209,11 +212,10 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; } void checkForLemma(TNode node); - friend class LazyBitblaster; friend class TLazyBitblaster; friend class EagerBitblaster; |