diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
commit | 1b30b256a0ec40ff431b83296bfe5aa0e099eb2e (patch) | |
tree | 91fb063e9cfcf360d601e21a19996995576ece7d /src/theory/bv | |
parent | 9eaf94708275337a4749b7ef2f44bf1c6746d8fc (diff) |
bitvector rewriting for the core theory and testcases
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/bv/kinds | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 60 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.cpp | 249 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 104 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 53 |
8 files changed, 477 insertions, 7 deletions
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index cab90bbdb..ad858ab53 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -7,6 +7,10 @@ noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ theory_bv.h \ + theory_bv.cpp \ + theory_bv_utils.h \ + theory_bv_rewrite_rules.h \ + theory_bv_rewrite_rules.cpp \ theory_bv_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index f1b926d24..54f861b76 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -12,13 +12,13 @@ constant BITVECTOR_TYPE \ "util/bitvector.h" \ "bit-vector type" -constant BITVECTOR_CONST \ +constant CONST_BITVECTOR \ ::CVC4::BitVector \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ "a fixed-width bit-vector constant" -operator BITVECTOR_CONCAT 2 "bit-vector concatenation" +operator BITVECTOR_CONCAT 2: "bit-vector concatenation" operator BITVECTOR_AND 2 "bitwise and" operator BITVECTOR_OR 2 "bitwise or" operator BITVECTOR_XOR 2 "bitwise xor" diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp new file mode 100644 index 000000000..849740c9a --- /dev/null +++ b/src/theory/bv/theory_bv.cpp @@ -0,0 +1,60 @@ +#include "theory_bv.h" +#include "theory_bv_utils.h" +#include "theory_bv_rewrite_rules.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { + + Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; + + Node result; + + if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */) + result = node; + else { + switch (node.getKind()) { + case kind::BITVECTOR_CONCAT: + result = LinearRewriteStrategy< + // Flatten the top level concatenations + CoreRewriteRules::ConcatFlatten, + // Merge the adjacent extracts on non-constants + CoreRewriteRules::ConcatExtractMerge, + // Merge the adjacent extracts on constants + CoreRewriteRules::ConcatConstantMerge, + // At this point only Extract-Whole could apply, if the result is only one extract + // or at some sub-expression if the result is a concatenation. + ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole> + >::apply(node); + break; + case kind::BITVECTOR_EXTRACT: + result = LinearRewriteStrategy< + // Extract over a constant gives a constant + CoreRewriteRules::ExtractConstant, + // Extract over an extract is simplified to one extract + CoreRewriteRules::ExtractExtract, + // Extract over a concatenation is distributed to the appropriate concatenations + CoreRewriteRules::ExtractConcat, + // At this point only Extract-Whole could apply + CoreRewriteRules::ExtractWhole + >::apply(node); + break; + case kind::EQUAL: + if (node[0] == node[1]) result = mkTrue(); + else result = node; + break; + default: + // TODO: figure out when this is an operator + result = node; + break; + // Unhandled(); + } + } + + Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; + + return RewriteComplete(result); +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 537e7f5fe..ee331af02 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -33,12 +33,12 @@ public: TheoryBV(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out) { } - - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n) { } + void registerTerm(TNode n) { } void check(Effort e) {} void propagate(Effort e) {} - void explain(TNode n, Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { } + RewriteResponse postRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp new file mode 100644 index 000000000..5473768bb --- /dev/null +++ b/src/theory/bv/theory_bv_rewrite_rules.cpp @@ -0,0 +1,249 @@ +#include <vector> +#include "expr/node_builder.h" +#include "theory_bv_rewrite_rules.h" +#include "theory_bv_utils.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +bool CoreRewriteRules::ConcatFlatten::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_CONCAT); +} + +Node CoreRewriteRules::ConcatFlatten::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatFlatten(" << node << ")" << endl; + + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + vector<Node> processing_stack; + processing_stack.push_back(node); + while (!processing_stack.empty()) { + Node current = processing_stack.back(); + processing_stack.pop_back(); + if (current.getKind() == kind::BITVECTOR_CONCAT) { + for (int i = current.getNumChildren() - 1; i >= 0; i--) + processing_stack.push_back(current[i]); + } else { + result << current; + } + } + + Debug("bitvector") << "ConcatFlatten(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ConcatExtractMerge::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_CONCAT); +} + +Node CoreRewriteRules::ConcatExtractMerge::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatExtractMerge(" << node << ")" << endl; + + vector<Node> mergedExtracts; + + Node current = node[0]; + bool mergeStarted = false; + unsigned currentHigh = 0; + unsigned currentLow = 0; + + for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) { + // The next candidate for merging + Node next = node[i]; + // If the current is not an extract we just go to the next + if (current.getKind() != kind::BITVECTOR_EXTRACT) { + mergedExtracts.push_back(current); + current = next; + continue; + } + // If it is an extract and the first one, get the extract parameters + else if (!mergeStarted) { + currentHigh = getExtractHigh(current); + currentLow = getExtractLow(current); + } + + // If the next one can be merged, try to merge + bool merged = false; + if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) { + //x[i : j] @ x[j − 1 : k] -> c x[i : k] + unsigned nextHigh = getExtractHigh(next); + unsigned nextLow = getExtractLow(next); + if(nextHigh + 1 == currentLow) { + currentLow = nextLow; + mergeStarted = true; + merged = true; + } + } + // If we haven't merged anything, add the previous merge and continue with the next + if (!merged) { + if (!mergeStarted) mergedExtracts.push_back(current); + else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow)); + current = next; + mergeStarted = false; + } + } + + // Add the last child + if (!mergeStarted) mergedExtracts.push_back(current); + else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow)); + + // Create the result + Node result = mkConcat(mergedExtracts); + + Debug("bitvector") << "ConcatExtractMerge(" << node << ") =>" << result << endl; + + // Return the result + return result; +} + +bool CoreRewriteRules::ConcatConstantMerge::applies(Node node) { + return node.getKind() == kind::BITVECTOR_CONCAT; +} + +Node CoreRewriteRules::ConcatConstantMerge::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ConcatConstantMerge(" << node << ")" << endl; + + vector<Node> mergedConstants; + for (unsigned i = 0, end = node.getNumChildren(); i < end;) { + if (node[i].getKind() != kind::CONST_BITVECTOR) { + // If not a constant, just add it + mergedConstants.push_back(node[i]); + ++i; + } else { + // Find the longest sequence of constants + unsigned j = i + 1; + while (j < end) { + if (node[j].getKind() != kind::CONST_BITVECTOR) { + break; + } else { + ++ j; + } + } + // Append all the constants + BitVector current = node[i].getConst<BitVector>(); + for (unsigned k = i + 1; k < j; ++ k) { + current = current.concat(node[k].getConst<BitVector>()); + } + // Add the new merged constant + mergedConstants.push_back(mkConst(current)); + i = j + 1; + } + } + + Node result = mkConcat(mergedConstants); + + Debug("bitvector") << "ConcatConstantMerge(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractWhole::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + unsigned length = getSize(node[0]); + unsigned extractHigh = getExtractHigh(node); + if (extractHigh != length - 1) return false; + unsigned extractLow = getExtractLow(node); + if (extractLow != 0) return false; + return true; +} + +Node CoreRewriteRules::ExtractWhole::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractWhole(" << node << ")" << endl; + Debug("bitvector") << "ExtractWhole(" << node << ") => " << node[0] << endl; + + return node[0]; +} + +bool CoreRewriteRules::ExtractConstant::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::CONST_BITVECTOR) return false; + return true; +} + +Node CoreRewriteRules::ExtractConstant::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractConstant(" << node << ")" << endl; + + Node child = node[0]; + BitVector childValue = child.getConst<BitVector>(); + + Node result = mkConst(childValue.extract(getExtractHigh(node), getExtractLow(node))); + + Debug("bitvector") << "ExtractConstant(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractConcat::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false; + return true; +} + +Node CoreRewriteRules::ExtractConcat::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractConcat(" << node << ")" << endl; + + int extract_high = getExtractHigh(node); + int extract_low = getExtractLow(node); + + vector<Node> resultChildren; + + Node concat = node[0]; + for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) { + Node concatChild = concat[i]; + int concatChildSize = getSize(concatChild); + if (extract_low < concatChildSize) { + int extract_start = extract_low < 0 ? 0 : extract_low; + int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1; + resultChildren.push_back(mkExtract(concatChild, extract_end, extract_start)); + } + extract_low -= concatChildSize; + extract_high -= concatChildSize; + } + + std::reverse(resultChildren.begin(), resultChildren.end()); + + Node result = mkConcat(resultChildren); + + Debug("bitvector") << "ExtractConcat(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::ExtractExtract::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; + if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false; + return true; +} + +Node CoreRewriteRules::ExtractExtract::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "ExtractExtract(" << node << ")" << endl; + + // x[i:j][k:l] ~> x[k+j:l+j] + Node child = node[0]; + unsigned k = getExtractHigh(node); + unsigned l = getExtractLow(node); + unsigned j = getExtractLow(child); + + Node result = mkExtract(child[0], k + j, l + j); + + Debug("bitvector") << "ExtractExtract(" << node << ") => " << result << endl; + + return result; + +} diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h new file mode 100644 index 000000000..48696ce33 --- /dev/null +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -0,0 +1,104 @@ +#pragma once + +#include "cvc4_private.h" +#include "theory/theory.h" +#include "context/context.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +struct CoreRewriteRules { + + struct EmptyRule { + static inline Node apply(Node node) { return node; } + static inline bool applies(Node node) { return false; } + }; + + struct ConcatFlatten { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ConcatExtractMerge { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ConcatConstantMerge { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractExtract { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractWhole { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractConcat { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct ExtractConstant { + static Node apply(Node node); + static bool applies(Node node); + }; + +}; + +template<Kind kind, typename Rule> +struct ApplyRuleToChildren { + + static Node apply(Node node) { + if (node.getKind() != kind) { + if (Rule::applies(node)) return Rule::apply(node); + else return node; + } + NodeBuilder<> result(kind); + for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) { + if (Rule::applies(node[i])) result << Rule::apply(node[i]); + else result << node[i]; + } + return result; + } + + static bool applies(Node node) { + if (node.getKind() == kind) return true; + return Rule::applies(node); + } + +}; + + +template < + typename R1, + typename R2, + typename R3 = CoreRewriteRules::EmptyRule, + typename R4 = CoreRewriteRules::EmptyRule, + typename R5 = CoreRewriteRules::EmptyRule, + typename R6 = CoreRewriteRules::EmptyRule, + typename R7 = CoreRewriteRules::EmptyRule + > +struct LinearRewriteStrategy { + static Node apply(Node node) { + Node current = node; + if (R1::applies(current)) current = R1::apply(current); + if (R2::applies(current)) current = R2::apply(current); + if (R3::applies(current)) current = R3::apply(current); + if (R4::applies(current)) current = R4::apply(current); + if (R5::applies(current)) current = R5::apply(current); + if (R6::applies(current)) current = R6::apply(current); + if (R7::applies(current)) current = R7::apply(current); + return current; + } +}; + +} // End namespace bv +} // End namespace theory +} // End namespace CVC4 diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 9bb9e61df..7c4ff495e 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -142,7 +142,7 @@ public: TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); for (; it != it_end; ++ it) { - TypeNode t = n[0].getType(check); + TypeNode t = (*it).getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if we don't check that the arguments // are bit-vectors the result type will be inaccurate diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h new file mode 100644 index 000000000..fa948465d --- /dev/null +++ b/src/theory/bv/theory_bv_utils.h @@ -0,0 +1,53 @@ +#pragma once + +#include <vector> +#include "expr/node_manager.h" + +namespace CVC4 { +namespace theory { +namespace bv { +namespace utils { + +inline unsigned getExtractHigh(TNode node) { + return node.getOperator().getConst<BitVectorExtract>().high; +} + +inline unsigned getExtractLow(TNode node) { + return node.getOperator().getConst<BitVectorExtract>().low; +} + +inline unsigned getSize(TNode node) { + return node.getType().getBitVectorSize(); +} + +inline Node mkTrue() { + return NodeManager::currentNM()->mkConst<bool>(true); +} + +inline Node mkFalse() { + return NodeManager::currentNM()->mkConst<bool>(false); +} + +inline Node mkExtract(TNode node, unsigned high, unsigned low) { + Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low)); + std::vector<Node> children; + children.push_back(node); + return NodeManager::currentNM()->mkNode(extractOp, children); +} + +inline Node mkConcat(std::vector<Node>& children) { + if (children.size() > 1) + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); + else + return children[0]; +} + +inline Node mkConst(const BitVector& value) { + return NodeManager::currentNM()->mkConst<BitVector>(value); +} + + +} +} +} +} |