From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Jan 2018 04:16:33 +0000 (-0800)
Subject: Add bv util mkConst(unsigned, Integer&). (#1499)
X-Git-Tag: cvc5-1.0.0~5368
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=707e27e61addafdbcce5e7b6d32a61985f563dfb;p=cvc5.git

Add bv util mkConst(unsigned, Integer&). (#1499)
---

diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index e2e176817..7bfc1c5c5 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -607,7 +607,7 @@ void DefaultShlBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   // check for b < log2(n)
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
-  Node a_size = utils::mkConst(BitVector(size, size));
+  Node a_size = utils::mkConst(size, size);
   Node b_ult_a_size_node =
       Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size));
   // ensure that the inequality is bit-blasted
@@ -656,7 +656,7 @@ void DefaultLshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   // check for b < log2(n)
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
-  Node a_size = utils::mkConst(BitVector(size, size));
+  Node a_size = utils::mkConst(size, size);
   Node b_ult_a_size_node =
       Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size));
   // ensure that the inequality is bit-blasted
@@ -707,7 +707,7 @@ void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   //   check for b < n
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
-  Node a_size = utils::mkConst(BitVector(size, size));
+  Node a_size = utils::mkConst(size, size);
   Node b_ult_a_size_node =
       Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size));
   // ensure that the inequality is bit-blasted
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 9718e9a2f..bb45b771d 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -26,8 +26,8 @@ using namespace CVC4::theory::bv;
 BvToBoolPreprocessor::BvToBoolPreprocessor()
   : d_liftCache()
   , d_boolCache()
-  , d_one(utils::mkConst(BitVector(1, 1u)))
-  , d_zero(utils::mkConst(BitVector(1, 0u)))
+  , d_one(utils::mkOne(1))
+  , d_zero(utils::mkZero(1))
   , d_statistics()
 {}
 
diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp
index cfdab57be..d0e2266a7 100644
--- a/src/theory/bv/bvgauss.cpp
+++ b/src/theory/bv/bvgauss.cpp
@@ -582,8 +582,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem(
           /* Normalize (no negative numbers, hence no subtraction)
            * e.g., x = 4 - 2y  --> x = 4 + 9y (modulo 11) */
           Integer m = iprime - lhs[prow][i];
-          Node bv =
-              nm->mkConst<BitVector>(BitVector(utils::getSize(vvars[i]), m));
+          Node bv = utils::mkConst(utils::getSize(vvars[i]), m);
           Node mult = nm->mkNode(kind::BITVECTOR_MULT, vvars[i], bv);
           stack.push_back(mult);
         }
@@ -602,8 +601,8 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem(
           if (rhs[prow] != 0)
           {
             tmp = nm->mkNode(kind::BITVECTOR_PLUS,
-                             nm->mkConst<BitVector>(BitVector(
-                                 utils::getSize(vvars[pcol]), rhs[prow])),
+                             utils::mkConst(
+                                 utils::getSize(vvars[pcol]), rhs[prow]),
                              tmp);
           }
           Assert(!is_bv_const(tmp));
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index e2bfec893..710e25345 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -216,7 +216,7 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
         bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
     value = value * 2 + bit_int;
   }
-  return utils::mkConst(BitVector(bits.size(), value));
+  return utils::mkConst(bits.size(), value);
 }
 
 bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 7976097e1..831b767e0 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -481,7 +481,7 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
     value = value * 2 + bit_int;
   }
-  return utils::mkConst(BitVector(bits.size(), value));
+  return utils::mkConst(bits.size(), value);
 }
 
 bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index cb214217c..af1dd5331 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -295,7 +295,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
     }
 
     TNode num = node[0], den = node[1];
-    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
+    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
     Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
 				     kind::BITVECTOR_UREM_TOTAL, num, den);
 
@@ -369,10 +369,10 @@ void TheoryBV::checkForLemma(TNode fact) {
       TNode result = fact[1];
       TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
-      Node divisor_eq_0 = mkNode(kind::EQUAL,
-                                 divisor,
-                                 mkConst(BitVector(getSize(divisor), 0u)));
-      Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
+      Node divisor_eq_0 = mkNode(
+          kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = utils::mkNode(
+          kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
@@ -380,10 +380,10 @@ void TheoryBV::checkForLemma(TNode fact) {
       TNode result = fact[0];
       TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
-      Node divisor_eq_0 = mkNode(kind::EQUAL,
-                                 divisor,
-                                 mkConst(BitVector(getSize(divisor), 0u)));
-      Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
+      Node divisor_eq_0 = mkNode(
+          kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = utils::mkNode(
+          kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
   }
@@ -673,7 +673,7 @@ int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
     const unsigned size = utils::getSize(n[0]);
     NodeManager* const nm = NodeManager::currentNM();
     const Node z = nm->mkConst(Rational(0));
-    const Node bvone = nm->mkConst(BitVector(1u, 1u));
+    const Node bvone = utils::mkOne(1);
     NodeBuilder<> result(kind::PLUS);
     Integer i = 1;
     for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
@@ -686,8 +686,8 @@ int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
     //taken from rewrite code
     const unsigned size = n.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));
+    const Node bvzero = utils::mkZero(1);
+    const Node bvone = utils::mkOne(1);
     std::vector<Node> v;
     Integer i = 2;
     while(v.size() < size) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 3ad733f99..07688a8bb 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -979,7 +979,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
   std::vector<Node> children;
   
   if (constant == BitVector(size, (unsigned)0)) {
-    return utils::mkConst(BitVector(size, (unsigned)0)); 
+    return utils::mkZero(size); 
   }
 
   if (constant != utils::mkBitVectorOnes(size)) {
@@ -991,7 +991,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
   for (; it != subterms.end(); ++it) {
     if (it->second.pos > 0 && it->second.neg > 0) {
       // if we have a and ~a 
-      return utils::mkConst(BitVector(size, (unsigned)0)); 
+      return utils::mkZero(size); 
     } else {
       // idempotence 
       if (it->second.neg > 0) {
@@ -1113,7 +1113,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) {
   }
 
   if (children.size() == 0) {
-    return utils::mkConst(BitVector(size, (unsigned)0)); 
+    return utils::mkZero(size); 
   }
   return utils::mkSortedNode(kind::BITVECTOR_OR, children); 
 }
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 f73c4fb0f..4877da1d1 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -95,7 +95,8 @@ Node RewriteRule<SltEliminate>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node[0]);
-  Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
+  Integer val = Integer(1).multiplyByPow2(size - 1);
+  Node pow_two = utils::mkConst(size, val);
   Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
   Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
   
@@ -246,7 +247,7 @@ Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
   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));
+  const Node bvone = utils::mkOne(1);
 
   NodeBuilder<> result(kind::PLUS);
   Integer i = 1;
@@ -273,8 +274,8 @@ Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
 
   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));
+  const Node bvzero = utils::mkZero(1);
+  const Node bvone = utils::mkOne(1);
 
   std::vector<Node> v;
   Integer i = 2;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 9d44d3be5..5956ced7e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -55,7 +55,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) {
   
   if (amount >= Integer(size)) {
     // if we are shifting more than the length of the bitvector return 0
-    return utils::mkConst(BitVector(size, Integer(0)));
+    return utils::mkZero(size);
   }
   
   // make sure we do not lose information casting
@@ -64,7 +64,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) {
   uint32_t uint32_amount = amount.toUnsignedInt();
 
   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
-  Node right = utils::mkConst(BitVector(uint32_amount, Integer(0))); 
+  Node right = utils::mkZero(uint32_amount);
   return utils::mkConcat(left, right); 
 }
 
@@ -95,7 +95,7 @@ Node RewriteRule<LshrByConst>::apply(TNode node) {
   
   if (amount >= Integer(size)) {
     // if we are shifting more than the length of the bitvector return 0
-    return utils::mkConst(BitVector(size, Integer(0)));
+    return utils::mkZero(size);
   }
   
   // make sure we do not lose information casting
@@ -103,7 +103,7 @@ Node RewriteRule<LshrByConst>::apply(TNode node) {
   
   uint32_t uint32_amount = amount.toUnsignedInt();
   Node right = utils::mkExtract(a, size - 1, uint32_amount);
-  Node left = utils::mkConst(BitVector(uint32_amount, Integer(0))); 
+  Node left = utils::mkZero(uint32_amount);
   return utils::mkConcat(left, right); 
 }
 
@@ -301,7 +301,7 @@ template<> inline
 Node RewriteRule<XorDuplicate>::apply(TNode node) {
   Unreachable();
   Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
-  return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
+  return utils::mkZero(utils::getSize(node));
 }
 
 /**
@@ -404,7 +404,7 @@ template<> inline
 Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
   Unreachable();
   Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
-  return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
+  return utils::mkZero(utils::getSize(node));
 }
 
 /**
@@ -427,8 +427,7 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
   Unreachable();
   Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
   uint32_t size = utils::getSize(node);
-  Integer ones = Integer(1).multiplyByPow2(size) - 1; 
-  return utils::mkConst(BitVector(size, ones)); 
+  return utils::mkOnes(size);
 }
 
 /**
@@ -542,7 +541,7 @@ Node RewriteRule<LteSelf>::apply(TNode node) {
 template<> inline
 bool RewriteRule<ZeroUlt>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+          node[0] == utils::mkZero(utils::getSize(node[0])));
 }
 
 template<> inline
@@ -561,7 +560,7 @@ Node RewriteRule<ZeroUlt>::apply(TNode node) {
 template<> inline
 bool RewriteRule<UltZero>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+          node[1] == utils::mkZero(utils::getSize(node[0])));
 }
 
 template<> inline
@@ -577,13 +576,14 @@ Node RewriteRule<UltZero>::apply(TNode node) {
 template<> inline
 bool RewriteRule<UltOne>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1))));
+          node[1] == utils::mkOne(utils::getSize(node[0])));
 }
 
 template<> inline
 Node RewriteRule<UltOne>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
-  return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u))); 
+  return utils::mkNode(
+      kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0])));
 }
 
 /**
@@ -592,7 +592,7 @@ Node RewriteRule<UltOne>::apply(TNode node) {
 template<> inline
 bool RewriteRule<SltZero>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLT &&
-          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+          node[1] == utils::mkZero(utils::getSize(node[0])));
 }
 
 template<> inline
@@ -600,9 +600,7 @@ Node RewriteRule<SltZero>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node[0]); 
   Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
-  Node one = utils::mkConst(BitVector(1, 1u));
-  
-  return utils::mkNode(kind::EQUAL, most_significant_bit, one); 
+  return utils::mkNode(kind::EQUAL, most_significant_bit, utils::mkOne(1));
 }
 
 
@@ -634,7 +632,7 @@ Node RewriteRule<UltSelf>::apply(TNode node) {
 template<> inline
 bool RewriteRule<UleZero>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+          node[1] == utils::mkZero(utils::getSize(node[0])));
 }
 
 template<> inline
@@ -671,7 +669,7 @@ Node RewriteRule<UleSelf>::apply(TNode node) {
 template<> inline
 bool RewriteRule<ZeroUle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+          node[0] == utils::mkZero(utils::getSize(node[0])));
 }
 
 template<> inline
@@ -692,9 +690,8 @@ bool RewriteRule<UleMax>::applies(TNode node) {
     return false; 
   }
   uint32_t size = utils::getSize(node[0]); 
-  Integer ones = Integer(1).multiplyByPow2(size) -1; 
-  return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[1] == utils::mkConst(BitVector(size, ones)));
+  return (node.getKind() == kind::BITVECTOR_ULE
+          && node[1] == utils::mkOnes(size));
 }
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index a11436c9e..ecd93cd2c 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -217,6 +217,11 @@ inline Node mkConst(unsigned size, unsigned int value) {
   return NodeManager::currentNM()->mkConst<BitVector>(val); 
 }
 
+inline Node mkConst(unsigned size, Integer& value)
+{
+  return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
+}
+
 inline Node mkConst(const BitVector& value) {
   return NodeManager::currentNM()->mkConst<BitVector>(value);
 }
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index ad18f901c..a27d3a64e 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -22,6 +22,7 @@
 #include "expr/kind.h"
 #include "expr/type_node.h"
 #include "theory/type_enumerator.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
 #include "util/integer.h"
 
@@ -45,7 +46,7 @@ public:
     if(d_bits != d_bits.modByPow2(d_size)) {
       throw NoMoreValuesException(getType());
     }
-    return NodeManager::currentNM()->mkConst(BitVector(d_size, d_bits));
+    return utils::mkConst(d_size, d_bits);
   }
 
   BitVectorEnumerator& operator++() throw() {