diff options
author | lianah <lianahady@gmail.com> | 2013-04-25 18:43:12 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | 94dc66d4cb4061a80bffe1ec72d2ab98e44dd626 (patch) | |
tree | 0daa9a883d4be5ccf8e863d6305814ef6f12b564 /src/theory/bv/theory_bv.h | |
parent | 7701ac73a62a466eaf4e55c1c2dc238c7110b02f (diff) |
added bvule, bvsle operator elimination rulesl; added bvurem lemma generation
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; |