diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/kinds | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 27 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 18 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 14 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 6 |
7 files changed, 79 insertions, 1 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index b4ecc1d3d..3cbc45cd1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_REDOR 1 "bit-vector redor" +operator BITVECTOR_REDAND 1 "bit-vector redand" + operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" @@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule + + typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 3cc1c323c..768923ee6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -49,6 +49,8 @@ enum RewriteRuleId { UgeEliminate, SgeEliminate, SgtEliminate, + RedorEliminate, + RedandEliminate, SubEliminate, SltEliminate, SleEliminate, @@ -188,6 +190,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case SgtEliminate: out << "SgtEliminate"; return out; case UgeEliminate: out << "UgeEliminate"; return out; case SgeEliminate: out << "SgeEliminate"; return out; + case RedorEliminate: out << "RedorEliminate"; return out; + case RedandEliminate: out << "RedandEliminate"; return out; case RepeatEliminate: out << "RepeatEliminate"; return out; case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; case RotateRightEliminate:out << "RotateRightEliminate";return out; @@ -522,6 +526,8 @@ struct AllRewriteRules { RewriteRule<UltPlusOne> rule119; RewriteRule<ConcatToMult> rule120; RewriteRule<IsPowerOfTwo> rule121; + RewriteRule<RedorEliminate> rule122; + RewriteRule<RedandEliminate> rule123; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 0442c47d9..cd173a6dd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -479,6 +479,33 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) { return utils::mkConcat(extension, node[0]); } +template<> +bool RewriteRule<RedorEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDOR); +} + +template<> +Node RewriteRule<RedorEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) ); + return result.negate(); +} + +template<> +bool RewriteRule<RedandEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDAND); +} + +template<> +Node RewriteRule<RedandEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) ); + return result; +} } } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 86f2c6760..f2adea411 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -553,6 +553,22 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite) return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedorEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedandEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<BVToNatEliminate> @@ -651,6 +667,8 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor; + d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand; d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 42bccb534..3f0fa8194 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -77,6 +77,8 @@ class TheoryBVRewriter { static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false); static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 81a2d9a27..fbb285fe0 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -112,6 +112,20 @@ public: } };/* class BitVectorPredicateTypeRule */ +class BitVectorUnaryPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode type = n[0].getType(check); + if (!type.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + } + return nodeManager->booleanType(); + } +};/* class BitVectorUnaryPredicateTypeRule */ + class BitVectorEagerAtomTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 6ebc9db92..a8b6887e5 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -385,6 +385,8 @@ inline bool isBVPredicate(TNode node) { node.getKind() == kind::BITVECTOR_SGE || node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLE || + node.getKind() == kind::BITVECTOR_REDOR || + node.getKind() == kind::BITVECTOR_REDAND || ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL || node[0].getKind() == kind::BITVECTOR_ULT || node[0].getKind() == kind::BITVECTOR_SLT || @@ -393,7 +395,9 @@ inline bool isBVPredicate(TNode node) { node[0].getKind() == kind::BITVECTOR_SGT || node[0].getKind() == kind::BITVECTOR_SGE || node[0].getKind() == kind::BITVECTOR_ULE || - node[0].getKind() == kind::BITVECTOR_SLE))) + node[0].getKind() == kind::BITVECTOR_SLE || + node[0].getKind() == kind::BITVECTOR_REDOR || + node[0].getKind() == kind::BITVECTOR_REDAND))) { return true; } |