diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 481493e13..22e3d0507 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -85,6 +85,8 @@ private: Statistics d_statistics; + context::CDO<bool> d_lemmasAdded; + // Are we in conflict? context::CDO<bool> d_conflict; @@ -97,6 +99,8 @@ private: /** Index of the next literal to propagate */ context::CDO<unsigned> d_literalsToPropagateIndex; + + /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -147,7 +151,9 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); } + void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + + void checkForLemma(TNode node); friend class Bitblaster; friend class BitblastSolver; |