diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
commit | 77ff33bc6be64f338f035bd9d077737f83280944 (patch) | |
tree | 3593a4f931ca107cdcb9b2e6891f7008f6d3be76 /src/theory/bv/theory_bv.h | |
parent | 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 (diff) |
several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e46d052f8..6ef9d18dd 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -42,12 +42,6 @@ namespace bv { /// forward declarations class Bitblaster; -static inline std::string spaces(int level) -{ - std::string indentStr(level, ' '); - return indentStr; -} - class TheoryBV : public Theory { @@ -61,7 +55,9 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; - + + context::CDList<TNode> d_bitblastQueue; + /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; @@ -119,7 +115,7 @@ private: if (value) { return d_bv.storePropagation(predicate, SUB_EQUALITY); } else { - return d_bv.storePropagation(predicate, SUB_EQUALITY); + return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY); } } @@ -134,6 +130,9 @@ private: bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + if (Theory::theoryOf(t1) == THEORY_BOOL) { + return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY); + } return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); } }; @@ -190,6 +189,12 @@ private: friend class Bitblaster; + inline std::string indent() + { + std::string indentStr(getSatContext()->getLevel(), ' '); + return indentStr; + } + public: void propagate(Effort e); |