Remove mkNode from bv::utils (#1587)

1 files changed, 155 insertions, 101 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c6f2ec74b..fd9ad0c6a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -2,9 +2,9 @@
 /*! \file theory_bv.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Andrew Reynolds, Clark Barrett
+ **   Liana Hadarean, Aina Niemetz, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -252,7 +252,7 @@ void TheoryBV::mkAckermanizationAssertions(std::vector<Node>& assertions) {
           for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
             eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
           }
-          args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs);
+          args_eq = utils::mkAnd(eqs);
         } else {
           AlwaysAssert (args1.getKind() == kind::SELECT &&
                         args1[0] == func);
@@ -363,28 +363,33 @@ void TheoryBV::sendConflict() {
   }
 }
 
-void TheoryBV::checkForLemma(TNode fact) {
-  if (fact.getKind() == kind::EQUAL) {
-    if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
+void TheoryBV::checkForLemma(TNode fact)
+{
+  if (fact.getKind() == kind::EQUAL)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
+    {
       TNode urem = fact[0];
       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, mkZero(getSize(divisor)));
-      Node split = utils::mkNode(
-          kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
+      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+      Node divisor_eq_0 =
+          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = nm->mkNode(
+          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
-    if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
+    if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
+    {
       TNode urem = fact[1];
       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, mkZero(getSize(divisor)));
-      Node split = utils::mkNode(
-          kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
+      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+      Node divisor_eq_0 =
+          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = nm->mkNode(
+          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
   }
@@ -431,7 +436,7 @@ void TheoryBV::check(Effort e)
         d_out->conflict(assertions[0]);
         return;
       }
-      Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
+      Node conflict = utils::mkAnd(assertions);
       d_out->conflict(conflict);
       return;
     }
@@ -505,59 +510,76 @@ void TheoryBV::check(Effort e)
   }
 }
 
-bool TheoryBV::doExtfInferences( std::vector< Node >& terms ) {
+bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
+{
+  NodeManager* nm = NodeManager::currentNM();
   bool sentLemma = false;
-  eq::EqualityEngine * ee = getEqualityEngine();    
-  std::map< Node, Node > op_map;
-  for( unsigned j=0; j<terms.size(); j++ ){
+  eq::EqualityEngine* ee = getEqualityEngine();
+  std::map<Node, Node> op_map;
+  for (unsigned j = 0; j < terms.size(); j++)
+  {
     TNode n = terms[j];
-    Assert (n.getKind() == kind::BITVECTOR_TO_NAT
-            || n.getKind() == kind::INT_TO_BITVECTOR );
-    if( n.getKind()==kind::BITVECTOR_TO_NAT ){
-      //range lemmas
-      if( d_extf_range_infer.find( n )==d_extf_range_infer.end() ){
-        d_extf_range_infer.insert( n );
+    Assert(n.getKind() == kind::BITVECTOR_TO_NAT
+           || n.getKind() == kind::INT_TO_BITVECTOR);
+    if (n.getKind() == kind::BITVECTOR_TO_NAT)
+    {
+      // range lemmas
+      if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
+      {
+        d_extf_range_infer.insert(n);
         unsigned bvs = n[0].getType().getBitVectorSize();
-        Node min = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-        Node max = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) );
-        Node lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, n, min ), NodeManager::currentNM()->mkNode( kind::LT, n, max ) );
-        Trace("bv-extf-lemma") << "BV extf lemma (range) : " << lem << std::endl;
-        d_out->lemma( lem );
+        Node min = nm->mkConst(Rational(0));
+        Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
+        Node lem = nm->mkNode(kind::AND,
+                              nm->mkNode(kind::GEQ, n, min),
+                              nm->mkNode(kind::LT, n, max));
+        Trace("bv-extf-lemma")
+            << "BV extf lemma (range) : " << lem << std::endl;
+        d_out->lemma(lem);
         sentLemma = true;
       }
     }
-    Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n[0] ) : n[0];
+    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
     op_map[r] = n;
   }
-  for( unsigned j=0; j<terms.size(); j++ ){
+  for (unsigned j = 0; j < terms.size(); j++)
+  {
     TNode n = terms[j];
-    Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n ) : n;
-    std::map< Node, Node >::iterator it = op_map.find( r );
-    if( it!=op_map.end() ){
+    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
+    std::map<Node, Node>::iterator it = op_map.find(r);
+    if (it != op_map.end())
+    {
       Node parent = it->second;
-      //Node cterm = parent[0]==n ? parent : NodeManager::currentNM()->mkNode( parent.getOperator(), n );
-      Node cterm = parent[0].eqNode( n );
-      Trace("bv-extf-lemma-debug") << "BV extf collapse based on : " << cterm << std::endl;
-      if( d_extf_collapse_infer.find( cterm )==d_extf_collapse_infer.end() ){
-        d_extf_collapse_infer.insert( cterm );
-      
+      // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
+      // n );
+      Node cterm = parent[0].eqNode(n);
+      Trace("bv-extf-lemma-debug")
+          << "BV extf collapse based on : " << cterm << std::endl;
+      if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
+      {
+        d_extf_collapse_infer.insert(cterm);
+
         Node t = n[0];
-        if( n.getKind()==kind::INT_TO_BITVECTOR ){
-          Assert( t.getType().isInteger() );
-          //congruent modulo 2^( bv width )
+        if (n.getKind() == kind::INT_TO_BITVECTOR)
+        {
+          Assert(t.getType().isInteger());
+          // congruent modulo 2^( bv width )
           unsigned bvs = n.getType().getBitVectorSize();
-          Node coeff = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) );
-          Node k = NodeManager::currentNM()->mkSkolem( "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence" );
-          t = NodeManager::currentNM()->mkNode( kind::PLUS, t, NodeManager::currentNM()->mkNode( kind::MULT, coeff, k ) );
+          Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
+          Node k = nm->mkSkolem(
+              "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
+          t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
         }
-        Node lem = parent.eqNode( t );
-        
-        if( parent[0]!=n ){
-          Assert( ee->areEqual( parent[0], n ) );
-          lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, parent[0].eqNode( n ), lem );
+        Node lem = parent.eqNode(t);
+
+        if (parent[0] != n)
+        {
+          Assert(ee->areEqual(parent[0], n));
+          lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
         }
-        Trace("bv-extf-lemma") << "BV extf lemma (collapse) : " << lem << std::endl;
-        d_out->lemma( lem );
+        Trace("bv-extf-lemma")
+            << "BV extf lemma (collapse) : " << lem << std::endl;
+        d_out->lemma(lem);
         sentLemma = true;
       }
     }
@@ -667,33 +689,44 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
   return false;
 }
 
-int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
+int TheoryBV::getReduction(int effort, Node n, Node& nr)
+{
   Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
-  if( n.getKind()==kind::BITVECTOR_TO_NAT ){
-    //taken from rewrite code
+  NodeManager* const nm = NodeManager::currentNM();
+  if (n.getKind() == kind::BITVECTOR_TO_NAT)
+  {
+    // taken from rewrite code
     const unsigned size = utils::getSize(n[0]);
-    NodeManager* const nm = NodeManager::currentNM();
     const Node z = nm->mkConst(Rational(0));
     const Node bvone = utils::mkOne(1);
     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)), n[0]), bvone);
+    for (unsigned bit = 0; bit < size; ++bit, i *= 2)
+    {
+      Node cond =
+          nm->mkNode(kind::EQUAL,
+                     nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]),
+                     bvone);
       result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
     }
     nr = Node(result);
     return -1;
-  }else if( n.getKind()==kind::INT_TO_BITVECTOR ){
-    //taken from rewrite code
+  }
+  else if (n.getKind() == kind::INT_TO_BITVECTOR)
+  {
+    // taken from rewrite code
     const unsigned size = n.getOperator().getConst<IntToBitVector>().size;
-    NodeManager* const nm = NodeManager::currentNM();
     const Node bvzero = utils::mkZero(1);
     const Node bvone = utils::mkOne(1);
     std::vector<Node> v;
     Integer i = 2;
-    while(v.size() < size) {
-      Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
-      cond = Rewriter::rewrite( cond );
+    while (v.size() < size)
+    {
+      Node cond = nm->mkNode(
+          kind::GEQ,
+          nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))),
+          nm->mkConst(Rational(i, 2)));
+      cond = Rewriter::rewrite(cond);
       v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
       i *= 2;
     }
@@ -704,26 +737,34 @@ int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
   }
   return 0;
 }
-  
-Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  switch(in.getKind()) {
-  case kind::EQUAL:
+
+Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
+                                          SubstitutionMap& outSubstitutions)
+{
+  switch (in.getKind())
+  {
+    case kind::EQUAL:
     {
-      if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
+      if (in[0].isVar() && !in[1].hasSubterm(in[0]))
+      {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
+      if (in[1].isVar() && !in[0].hasSubterm(in[1]))
+      {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
       Node node = Rewriter::rewrite(in);
-      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) ||
-          (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) {
+      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
+          || (node[1].getKind() == kind::BITVECTOR_EXTRACT
+              && node[0].isConst()))
+      {
         Node extract = node[0].isConst() ? node[1] : node[0];
-        if (extract[0].getKind() == kind::VARIABLE) {
+        if (extract[0].getKind() == kind::VARIABLE)
+        {
           Node c = node[0].isConst() ? node[0] : node[1];
 
           unsigned high = utils::getExtractHigh(extract);
@@ -731,18 +772,23 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
           unsigned var_bitwidth = utils::getSize(extract[0]);
           std::vector<Node> children;
 
-          if (low == 0) {
-            Assert (high != var_bitwidth - 1);
+          if (low == 0)
+          {
+            Assert(high != var_bitwidth - 1);
             unsigned skolem_size = var_bitwidth - high - 1;
             Node skolem = utils::mkVar(skolem_size);
             children.push_back(skolem);
             children.push_back(c);
-          } else if (high == var_bitwidth - 1) {
+          }
+          else if (high == var_bitwidth - 1)
+          {
             unsigned skolem_size = low;
             Node skolem = utils::mkVar(skolem_size);
             children.push_back(c);
             children.push_back(skolem);
-          } else {
+          }
+          else
+          {
             unsigned skolem1_size = low;
             unsigned skolem2_size = var_bitwidth - high - 1;
             Node skolem1 = utils::mkVar(skolem1_size);
@@ -751,22 +797,22 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
             children.push_back(c);
             children.push_back(skolem1);
           }
-          Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children);
-          Assert (utils::getSize(concat) == utils::getSize(extract[0]));
+          Node concat = utils::mkConcat(children);
+          Assert(utils::getSize(concat) == utils::getSize(extract[0]));
           outSubstitutions.addSubstitution(extract[0], concat);
           return PP_ASSERT_STATUS_SOLVED;
         }
       }
     }
     break;
-  case kind::BITVECTOR_ULT:
-  case kind::BITVECTOR_SLT:
-  case kind::BITVECTOR_ULE:
-  case kind::BITVECTOR_SLE:
+    case kind::BITVECTOR_ULT:
+    case kind::BITVECTOR_SLT:
+    case kind::BITVECTOR_ULE:
+    case kind::BITVECTOR_SLE:
 
-  default:
-    // TODO other predicates
-    break;
+    default:
+      // TODO other predicates
+      break;
   }
   return PP_ASSERT_STATUS_UNSOLVED;
 }
@@ -795,7 +841,7 @@ Node TheoryBV::ppRewrite(TNode t)
       RewriteRule<ConcatToMult>::run<true>(res[1]);
     Node factor = mult[0];
     Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
-    Node new_eq =utils::mkNode(kind::EQUAL, sum, mult);
+    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
     if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
       res = Rewriter::rewrite(rewr_eq);
@@ -808,17 +854,20 @@ Node TheoryBV::ppRewrite(TNode t)
     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
   }
 
-
   // if(t.getKind() == kind::EQUAL &&
-  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
-  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) {
+  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
+  //    kind::BITVECTOR_PLUS) ||
+  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
+  //     kind::BITVECTOR_PLUS))) {
   //   // if we have an equality between a multiplication and addition
   //   // try to express multiplication in terms of addition
   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
   //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
   //   if (RewriteRule<MultSlice>::applies(mult)) {
   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
-  //     Node new_eq = Rewriter::rewrite(utils::mkNode(kind::EQUAL, new_mult, add));
+  //     Node new_eq =
+  //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
+  //     new_mult, add));
 
   //     // the simplification can cause the formula to blow up
   //     // only apply if formula reduced
@@ -985,7 +1034,8 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
           Node c_eq_0 = c.eqNode(zero);
           Node b_eq_c = b.eqNode(c);
 
-          Node dis = utils::mkNode(kind::OR, b_eq_0, c_eq_0, b_eq_c);
+          Node dis = NodeManager::currentNM()->mkNode(
+              kind::OR, b_eq_0, c_eq_0, b_eq_c);
           Node imp = in.impNode(dis);
           learned << imp;
         }
@@ -1021,15 +1071,19 @@ void TheoryBV::setProofLog( BitVectorProof * bvp ) {
   }
 }
 
-void TheoryBV::setConflict(Node conflict) {
-  if (options::bvAbstraction()) {
+void TheoryBV::setConflict(Node conflict)
+{
+  if (options::bvAbstraction())
+  {
+    NodeManager* const nm = NodeManager::currentNM();
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
 
     std::vector<Node> lemmas;
     lemmas.push_back(new_conflict);
     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
-    for (unsigned i = 0; i < lemmas.size(); ++i) {
-      lemma(utils::mkNode(kind::NOT, lemmas[i]));
+    for (unsigned i = 0; i < lemmas.size(); ++i)
+    {
+      lemma(nm->mkNode(kind::NOT, lemmas[i]));
     }
   }
   d_conflict = true;