From: lianah Date: Sun, 15 Jun 2014 03:06:50 +0000 (-0400) Subject: Evil bitvector preprocessing pass for simplifying powers of two. X-Git-Tag: cvc5-1.0.0~6811 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=782bfe1b122a34f72c0533d9f189045379eb1d58;p=cvc5.git Evil bitvector preprocessing pass for simplifying powers of two. --- diff --git a/src/Makefile.am b/src/Makefile.am index 810e3302a..b1a2032c0 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -217,6 +217,8 @@ libcvc4_la_SOURCES = \ theory/bv/bitblast_mode.h \ theory/bv/bitblast_mode.cpp \ theory/bv/bitblast_utils.h \ + theory/bv/bvintropow2.h \ + theory/bv/bvintropow2.cpp \ theory/idl/idl_model.h \ theory/idl/idl_model.cpp \ theory/idl/idl_assertion.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6b7bf424f..ab805a6c5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -89,6 +89,7 @@ #include "printer/options.h" #include "theory/arith/pseudoboolean_proc.h" +#include "theory/bv/bvintropow2.h" using namespace std; using namespace CVC4; @@ -2926,6 +2927,10 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess); } + if(options::bvIntroducePow2()){ + theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess); + } + dumpAssertions("pre-substitution", d_assertionsToPreprocess); // Apply the substitutions we already have, and normalize 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& 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 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::applies(node)) { + res = RewriteRule::run(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 +#include + +#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& assertionsToPreprocess); + +private: + typedef __gnu_cxx::hash_map 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& assertions, std::vector& 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 TNodeSet; void collectNumerators(TNode term, TNodeSet& seen); + typedef __gnu_cxx::hash_set NodeSet; + NodeSet d_staticLearnCache; + /** * Maps from bit-vector width to divison-by-zero uninterpreted * function symbols.