diff options
author | lianah <lianahady@gmail.com> | 2014-06-14 23:06:50 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-14 23:06:50 -0400 |
commit | 782bfe1b122a34f72c0533d9f189045379eb1d58 (patch) | |
tree | 099de5435867ce26654b9c0e44195c7fc8ccb0fc /src/theory | |
parent | aeeb951b0fcc33e03feb6a6300808834a96daff5 (diff) |
Evil bitvector preprocessing pass for simplifying powers of two.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bvintropow2.cpp | 64 | ||||
-rw-r--r-- | src/theory/bv/bvintropow2.h | 34 | ||||
-rw-r--r-- | src/theory/bv/options | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 12 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 3 |
5 files changed, 114 insertions, 1 deletions
diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp new file mode 100644 index 000000000..bd092ed12 --- /dev/null +++ b/src/theory/bv/bvintropow2.cpp @@ -0,0 +1,64 @@ +#include "theory/bv/bvintropow2.h" +#include "theory/rewriter.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" + + +namespace CVC4 { +namespace theory { +namespace bv { + +void BVIntroducePow2::pow2Rewrite(std::vector<Node>& assertionsToPreprocess){ + NodeMap cache; + for(size_t i = 0, N= assertionsToPreprocess.size(); i < N; ++i){ + Node curr = assertionsToPreprocess[i]; + Node next = pow2Rewrite(curr, cache); + assertionsToPreprocess[i] = next; + } +} + +Node BVIntroducePow2::pow2Rewrite(Node node, NodeMap& cache){ + NodeMap::const_iterator ci = cache.find(node); + if(ci != cache.end()){ + Node incache = (*ci).second; + + return incache.isNull() ? node : incache; + } + + Node res = Node::null(); + switch(node.getKind()){ + case kind::AND: + { + bool changed = false; + std::vector<Node> children; + for(unsigned i = 0, N = node.getNumChildren(); i < N; ++i){ + Node child = node[i]; + Node found = pow2Rewrite(child, cache); + changed = changed || (child != found); + children.push_back(found); + } + if(changed){ + res = NodeManager::currentNM()->mkNode(kind::AND, children); + } + } + break; + + case kind::EQUAL: + if(node[0].getType().isBitVector()){ + if (RewriteRule<IsPowerOfTwo>::applies(node)) { + res = RewriteRule<IsPowerOfTwo>::run<false>(node); + } + } + break; + default: + break; + } + + cache.insert(std::make_pair(node, res)); + return res.isNull() ? node : res; +} + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h new file mode 100644 index 000000000..3844d03e1 --- /dev/null +++ b/src/theory/bv/bvintropow2.h @@ -0,0 +1,34 @@ + + +#include "cvc4_private.h" +#include "expr/node.h" + +#include <vector> +#include <ext/hash_map> + +#ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H +#define __CVC4__THEORY__BV__BV_INTRO_POW_H + +namespace CVC4 { +namespace theory { +namespace bv { + + +class BVIntroducePow2 { +public: + static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess); + +private: + typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap; + static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache); +}; + + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__BV__BV_INTRO_POW_H */ diff --git a/src/theory/bv/options b/src/theory/bv/options index fc704a71a..b5a4fea93 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -61,5 +61,7 @@ expert-option bvEagerExplanations --bv-eager-explanations bool :default false :r expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false minimize bv conflicts using the QuickXplain algorithm +expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false + introduce bitvector powers of two as a preprocessing pass endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 5be02322d..5ae07466a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -48,6 +48,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories(), d_subtheoryMap(), d_statistics(), + d_staticLearnCache(), d_lemmasAdded(c, false), d_conflict(c, false), d_literalsToPropagate(c), @@ -730,6 +731,11 @@ void TheoryBV::enableCoreTheorySlicer() { void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { + if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){ + return; + } + d_staticLearnCache.insert(in); + if (in.getKind() == kind::EQUAL) { if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL || in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){ @@ -756,7 +762,11 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { } } } - } + }else if(in.getKind() == kind::AND){ + for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){ + ppStaticLearn(in[i], learned); + } + } } bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 27b6b37c4..26ed8c296 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -117,6 +117,9 @@ private: typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; void collectNumerators(TNode term, TNodeSet& seen); + typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + NodeSet d_staticLearnCache; + /** * Maps from bit-vector width to divison-by-zero uninterpreted * function symbols. |