Squashed merge of SygusComp 2015 branch.

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; 
     }