Support for bv2nat/int2bv in parser and BV rewriter.

10 files changed, 155 insertions, 9 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5aa1e53e4..638c64a69 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1124,6 +1124,11 @@ indexedFunctionName[CVC4::Expr& op]
       { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
     | DIVISIBLE_TOK n=INTEGER_LITERAL
       { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
+    | INT2BV_TOK n=INTEGER_LITERAL
+      { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n)));
+        if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
+        } }
     | badIndexedFunctionName
    )
     RPAREN_TOK
@@ -1234,6 +1239,11 @@ builtinOp[CVC4::Kind& kind]
   | BVSGT_TOK     { $kind = CVC4::kind::BITVECTOR_SGT; }
   | BVSGE_TOK     { $kind = CVC4::kind::BITVECTOR_SGE; }
 
+  | BV2NAT_TOK     { $kind = CVC4::kind::BITVECTOR_TO_NAT;
+                     if(PARSER_STATE->strictModeEnabled()) {
+                       PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
+                     } }
+
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
@@ -1601,6 +1611,8 @@ BVSLT_TOK : 'bvslt';
 BVSLE_TOK : 'bvsle';
 BVSGT_TOK : 'bvsgt';
 BVSGE_TOK : 'bvsge';
+BV2NAT_TOK : 'bv2nat';
+INT2BV_TOK : 'int2bv';
 
 //STRING
 STRCST_TOK : 'str.const';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index db242d101..884502cf2 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -84,6 +84,9 @@ void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_SIGN_EXTEND);
   addOperator(kind::BITVECTOR_ROTATE_LEFT);
   addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+
+  addOperator(kind::INT_TO_BITVECTOR);
+  addOperator(kind::BITVECTOR_TO_NAT);
 }
 
 void Smt2::addStringOperators() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7b25c6fd9..756e521a6 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -304,6 +304,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SLE: out << "bvsle "; break;
   case kind::BITVECTOR_SGT: out << "bvsgt "; break;
   case kind::BITVECTOR_SGE: out << "bvsge "; break;
+  case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
 
   case kind::BITVECTOR_EXTRACT:
   case kind::BITVECTOR_REPEAT:
@@ -311,6 +312,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SIGN_EXTEND:
   case kind::BITVECTOR_ROTATE_LEFT:
   case kind::BITVECTOR_ROTATE_RIGHT:
+  case kind::INT_TO_BITVECTOR:
     printBvParameterizedOp(out, n);
     out << ' ';
     stillNeedToPrintParams = false;
@@ -535,6 +537,10 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
     out << "rotate_right "
         << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
     break;
+  case kind::INT_TO_BITVECTOR:
+    out << "int2bv "
+        << n.getOperator().getConst<IntToBitVector>().size;
+    break;
   default:
     out << n.getKind();
   }
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 052e477ea..aeae1073e 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -120,6 +120,14 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
 
+constant INT_TO_BITVECTOR_OP \
+	::CVC4::IntToBitVector \
+	"::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \
+	"util/bitvector.h" \
+	"operator for the integer conversion to bit-vector"
+parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector"
+operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer"
+
 typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
 
 typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
@@ -166,4 +174,7 @@ typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 
+typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
+typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
+
 endtheory
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index baaf7e133..8426afb59 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -66,6 +66,9 @@ enum RewriteRuleId {
   SremEliminate,
   ZeroExtendEliminate,
   SignExtendEliminate,
+  BVToNatEliminate,
+  IntToBVEliminate,
+
   /// ground term evaluation
   EvalEquals,
   EvalConcat, 
@@ -173,13 +176,15 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case FailEq:              out << "FailEq";              return out;
   case SimplifyEq:          out << "SimplifyEq";          return out;
   case ReflexivityEq:       out << "ReflexivityEq";       return out;
-  case UgtEliminate:            out << "UgtEliminate";            return out;
-  case SgtEliminate:            out << "SgtEliminate";            return out;
-  case UgeEliminate:            out << "UgeEliminate";            return out;
-  case SgeEliminate:            out << "SgeEliminate";            return out;
+  case UgtEliminate:        out << "UgtEliminate";        return out;
+  case SgtEliminate:        out << "SgtEliminate";        return out;
+  case UgeEliminate:        out << "UgeEliminate";        return out;
+  case SgeEliminate:        out << "SgeEliminate";        return out;
   case RepeatEliminate:     out << "RepeatEliminate";     return out;
   case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
   case RotateRightEliminate:out << "RotateRightEliminate";return out;
+  case BVToNatEliminate:    out << "BVToNatEliminate";    return out;
+  case IntToBVEliminate:    out << "IntToBVEliminate";    return out;
   case NandEliminate:       out << "NandEliminate";       return out;
   case NorEliminate :       out << "NorEliminate";        return out;
   case SdivEliminate :      out << "SdivEliminate";       return out;
@@ -214,7 +219,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ExtractBitwise :     out << "ExtractBitwise";      return out;
   case ExtractNot :         out << "ExtractNot";          return out;
   case ExtractArith :       out << "ExtractArith";        return out;
-  case ExtractArith2 :       out << "ExtractArith2";       return out;
+  case ExtractArith2 :      out << "ExtractArith2";       return out;
   case DoubleNeg :          out << "DoubleNeg";           return out;
   case NotConcat :          out << "NotConcat";           return out;
   case NotAnd :             out << "NotAnd";              return out;
@@ -226,7 +231,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case BitwiseNotOr :       out << "BitwiseNotOr";        return out;
   case XorNot :             out << "XorNot";              return out;
   case LtSelf :             out << "LtSelf";              return out;
-  case LteSelf :            out << "LteSelf";              return out;
+  case LteSelf :            out << "LteSelf";             return out;
   case UltZero :            out << "UltZero";             return out;
   case UleZero :            out << "UleZero";             return out;
   case ZeroUle :            out << "ZeroUle";             return out;
@@ -491,7 +496,8 @@ struct AllRewriteRules {
   RewriteRule<BitwiseEq> rule113;
   RewriteRule<UltOne> rule114;
   RewriteRule<SltZero> rule115;
-  
+  RewriteRule<BVToNatEliminate>  rule116;
+  RewriteRule<IntToBVEliminate>  rule117;
 };
 
 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 cf36633fa..b513dbf90 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -231,6 +231,57 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
 }
 
 template<>
+bool RewriteRule<BVToNatEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_TO_NAT);
+}
+
+template<>
+Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
+
+  const unsigned size = utils::getSize(node[0]);
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node z = nm->mkConst(Rational(0));
+  const Node bvone = nm->mkConst(BitVector(1u, 1u));
+
+  NodeBuilder<> result(kind::PLUS);
+  Integer i = 1;
+  for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
+    Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone);
+    result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
+  }
+
+  return Node(result);
+}
+
+template<>
+bool RewriteRule<IntToBVEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::INT_TO_BITVECTOR);
+}
+
+template<>
+Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
+
+  const unsigned size = node.getOperator().getConst<IntToBitVector>().size;
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node bvzero = nm->mkConst(BitVector(1u, 0u));
+  const Node bvone = nm->mkConst(BitVector(1u, 1u));
+
+  std::vector<Node> v;
+  Integer i = 2;
+  while(v.size() < size) {
+    Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
+    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
+    i *= 2;
+  }
+
+  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  result.append(v.rbegin(), v.rend());
+  return Node(result);
+}
+
+template<>
 bool RewriteRule<NandEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NAND &&
           node.getNumChildren() == 2);
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index f698ec83d..2467ae3f1 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -553,11 +553,27 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite
 RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateLeftEliminate >
-      >::apply(node);
+    >::apply(node);
   
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
+RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<BVToNatEliminate>
+    >::apply(node);
+
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<IntToBVEliminate>
+    >::apply(node);
+
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
 RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
   if (prerewrite) {
     Node resultNode = LinearRewriteStrategy
@@ -640,6 +656,9 @@ 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_TO_NAT ] = RewriteBVToNat;
+  d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
 }
 
 Node TheoryBVRewriter::eliminateBVSDiv(TNode node) {
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 183b5e8d5..def8e24fe 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -78,6 +78,9 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
 
+  static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
+
 public:
 
   static RewriteResponse postRewrite(TNode node);
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index effef49e8..67dae0cfa 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -195,6 +195,29 @@ public:
   }
 };
 
+class BitVectorConversionTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if(n.getKind() == kind::BITVECTOR_TO_NAT) {
+      if(check && !n[0].getType(check).isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+      }
+      return nodeManager->integerType();
+    }
+
+    if(n.getKind() == kind::INT_TO_BITVECTOR) {
+      size_t bvSize = n.getOperator().getConst<IntToBitVector>();
+      if(check && !n[0].getType(check).isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting integer term");
+      }
+      return nodeManager->mkBitVectorType(bvSize);
+    }
+
+    InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+  }
+};
+
 class CardinalityComputer {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2d5d29339..04e23217b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -396,7 +396,7 @@ struct CVC4_PUBLIC BitVectorHashFunction {
 
 /**
  * The structure representing the extraction operation for bit-vectors. The
- * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
+ * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
  * by taking the bits at indices <code>high ... low</code>
  */
 struct CVC4_PUBLIC BitVectorExtract {
@@ -492,6 +492,13 @@ struct CVC4_PUBLIC BitVectorRotateRight {
   operator unsigned () const { return rotateRightAmount; }
 };/* struct BitVectorRotateRight */
 
+struct CVC4_PUBLIC IntToBitVector {
+  unsigned size;
+  IntToBitVector(unsigned size)
+  : size(size) {}
+  operator unsigned () const { return size; }
+};/* struct IntToBitVector */
+
 template <typename T>
 struct CVC4_PUBLIC UnsignedHashFunction {
   inline size_t operator()(const T& x) const {
@@ -514,6 +521,11 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
   return os << "[" << bv.bitIndex << "]";
 }
 
+inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) {
+  return os << "[" << bv.size << "]";
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__BITVECTOR_H */