diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
commit | c0324db3ac7e5984c632f46690f58c333b9a42b2 (patch) | |
tree | 7a9a83b7dc1f929d4eb3de06b59ed6ff7b7f43bd /src/theory/bv/bitblast_strategies.cpp | |
parent | 8c4495b18e40a406be35baceaf473878bcc375f1 (diff) |
Merged updated version of the bitvector theory:
* added simplification rewrites
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index dacd6a538..6cbec732c 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -175,7 +175,7 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) { Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) { - Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " + Trace("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } @@ -261,6 +261,19 @@ Node DefaultUgeBB(TNode node, Bitblaster* bb){ Unimplemented(); } +// Node DefaultSltBB(TNode node, Bitblaster* bb){ +// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// // shoudl be rewritten in terms of ult +// Unimplemented(); +// } + +// Node DefaultSleBB(TNode node, Bitblaster* bb){ +// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// // shoudl be rewritten in terms of ule +// Unimplemented(); +// } + + Node DefaultSltBB(TNode node, Bitblaster* bb){ Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; @@ -301,7 +314,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){ /// Term bitblasting strategies void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " + Trace("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } |