Merge branch 'sygusComp2018-2' into replaceSubstitutereplaceSubstitute

1 files changed, 124 insertions, 106 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 4a4cf80ac..478d4cff6 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
@@ -187,7 +187,7 @@ Node ExtendedRewriter::extendedRewrite(Node n)
   if (new_ret.isNull())
   {
     TheoryId tid;
-    if( ret.getKind()==ITE )
+    if (ret.getKind() == ITE)
     {
       tid = Theory::theoryOf(ret.getType());
     }
@@ -195,7 +195,8 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     {
       tid = Theory::theoryOf(ret);
     }
-    Trace("q-ext-rewrite-debug") << "theoryOf( " << ret << " )= " << tid << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "theoryOf( " << ret << " )= " << tid << std::endl;
     if (tid == THEORY_ARITH)
     {
       new_ret = extendedRewriteArith(ret);
@@ -1464,9 +1465,9 @@ bool ExtendedRewriter::inferSubstitution(Node n,
     Node v[2];
     for (unsigned i = 0; i < 2; i++)
     {
-      if( n[i].isConst() )
+      if (n[i].isConst())
       {
-        vars.push_back(n[1-i]);
+        vars.push_back(n[1 - i]);
         subs.push_back(n[i]);
         return true;
       }
@@ -1677,51 +1678,56 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
     }
     debugExtendedRewrite(ret, new_ret, "BV-eq-solve");
   }
-  else if (k == ITE )
+  else if (k == ITE)
   {
-    if( ret[0].getKind()==EQUAL && ret[0][0].getType().isBitVector() )
+    if (ret[0].getKind() == EQUAL && ret[0][0].getType().isBitVector())
     {
-      for( unsigned i=0; i<2; i++ )
+      for (unsigned i = 0; i < 2; i++)
       {
         Node ct = ret[0][i];
-        Node cto = ret[0][1-i];
-        if( ct.isConst() && bv::utils::getSize(ct)==1 )
+        Node cto = ret[0][1 - i];
+        if (ct.isConst() && bv::utils::getSize(ct) == 1)
         {
           // do they differ by exactly one bit?
-          std::vector< Node > rcc;
-          int diff_index = spliceBvConstBit(ret[1],ret[2],rcc);
-          if( diff_index>=0 )
+          std::vector<Node> rcc;
+          int diff_index = spliceBvConstBit(ret[1], ret[2], rcc);
+          if (diff_index >= 0)
           {
-            Node rpl = rcc[diff_index]==ct ? cto : TermUtil::mkNegate(BITVECTOR_NOT,cto);
+            Node rpl = rcc[diff_index] == ct
+                           ? cto
+                           : TermUtil::mkNegate(BITVECTOR_NOT, cto);
             rcc[diff_index] = rpl;
-            new_ret = rcc.size()==1 ? rcc[0] : nm->mkNode( BITVECTOR_CONCAT, rcc );
+            new_ret =
+                rcc.size() == 1 ? rcc[0] : nm->mkNode(BITVECTOR_CONCAT, rcc);
             debugExtendedRewrite(ret, new_ret, "BV 1bit ITE");
           }
         }
-        else if( ct.getKind()==BITVECTOR_EXTRACT )
+        else if (ct.getKind() == BITVECTOR_EXTRACT)
         {
           Node cte = ct[0];
-          if( cte==ret[1] || cte==ret[2] )
+          if (cte == ret[1] || cte == ret[2])
           {
             // get the other branch
-            Node ob = ret[cte==ret[1] ? 2 : 1];
+            Node ob = ret[cte == ret[1] ? 2 : 1];
             // get the extension of the extract
-            std::vector< Node > exs;
+            std::vector<Node> exs;
             exs.push_back(ct);
-            Node ext = extendBv(cte,exs);
-            Assert(ext.getType()==ob.getType());
+            Node ext = extendBv(cte, exs);
+            Assert(ext.getType() == ob.getType());
             // now, splice the other branch
-            std::vector< Node > extc;
-            std::vector< Node > obc;
-            spliceBv(ext,ob,extc,obc);
-            if( obc.size()==2 && ( cto==obc[0] || cto==obc[1] ) )
+            std::vector<Node> extc;
+            std::vector<Node> obc;
+            spliceBv(ext, ob, extc, obc);
+            if (obc.size() == 2 && (cto == obc[0] || cto == obc[1]))
             {
-              unsigned cflip_index = cto==obc[0] ? 1 : 0;
-              if( obc[cflip_index].isConst() && bv::utils::getSize(obc[cflip_index])==1 )
+              unsigned cflip_index = cto == obc[0] ? 1 : 0;
+              if (obc[cflip_index].isConst()
+                  && bv::utils::getSize(obc[cflip_index]) == 1)
               {
-                obc[cflip_index] = TermUtil::mkNegate(BITVECTOR_NOT,obc[cflip_index]);
-                Node new_eq = cte.eqNode( nm->mkNode( BITVECTOR_CONCAT, obc ) );
-                new_ret = nm->mkNode( ITE, new_eq, ret[1], ret[2] );
+                obc[cflip_index] =
+                    TermUtil::mkNegate(BITVECTOR_NOT, obc[cflip_index]);
+                Node new_eq = cte.eqNode(nm->mkNode(BITVECTOR_CONCAT, obc));
+                new_ret = nm->mkNode(ITE, new_eq, ret[1], ret[2]);
                 debugExtendedRewrite(ret, new_ret, "BV 1bit exrem ITE");
               }
             }
@@ -1842,25 +1848,26 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
         }
       }
     }
-    else if( ck==BITVECTOR_CONCAT )
+    else if (ck == BITVECTOR_CONCAT)
     {
       // negating odd numbers flips all but the lsb
       // -concat( t, 1 ) ---> concat( ~t, 1 )
-      Node last_child = ret[0][ret[0].getNumChildren()-1];
-      if( last_child.isConst() )
+      Node last_child = ret[0][ret[0].getNumChildren() - 1];
+      if (last_child.isConst())
       {
-        if( bv::utils::getBit(last_child,0) )
+        if (bv::utils::getBit(last_child, 0))
         {
-          std::vector< Node > children;
-          for( unsigned j=0, size=ret[0].getNumChildren(); j<size-1; j++ )
+          std::vector<Node> children;
+          for (unsigned j = 0, size = ret[0].getNumChildren(); j < size - 1;
+               j++)
           {
-            children.push_back(TermUtil::mkNegate(BITVECTOR_NOT,ret[0][j]));
+            children.push_back(TermUtil::mkNegate(BITVECTOR_NOT, ret[0][j]));
           }
           unsigned csize = bv::utils::getSize(last_child);
-          if( csize>1 )
+          if (csize > 1)
           {
-            Node extract = bv::utils::mkExtract(last_child, csize-1, 1);
-            extract = TermUtil::mkNegate(BITVECTOR_NOT,extract);
+            Node extract = bv::utils::mkExtract(last_child, csize - 1, 1);
+            extract = TermUtil::mkNegate(BITVECTOR_NOT, extract);
             children.push_back(extract);
             children.push_back(bv::utils::mkOnes(1));
           }
@@ -1868,7 +1875,7 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
           {
             children.push_back(last_child);
           }
-          new_ret = nm->mkNode(BITVECTOR_CONCAT,children);
+          new_ret = nm->mkNode(BITVECTOR_CONCAT, children);
           debugExtendedRewrite(ret, new_ret, "NEG-odd");
           return new_ret;
         }
@@ -1876,27 +1883,31 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
       // negating numbers with msb 1-bits flips all but the last
       // -concat( 1...11, t ) ----> concat( 0...0, -concat(1, t) )
       Node first_child = ret[0][0];
-      if( first_child.isConst() )
+      if (first_child.isConst())
       {
         unsigned csize = bv::utils::getSize(first_child);
-        int i = csize-1;
-        while( i>=0 && bv::utils::getBit(first_child,i) )
+        int i = csize - 1;
+        while (i >= 0 && bv::utils::getBit(first_child, i))
         {
           i--;
         }
-        i = i+2;
-        if( i<=static_cast<int>(csize-1) )
+        i = i + 2;
+        if (i <= static_cast<int>(csize - 1))
         {
-          Assert( i>0 );
-          Node extract_flip = bv::utils::mkExtract(first_child, csize-1, i);
-          extract_flip = TermUtil::mkNegate(BITVECTOR_NOT,extract_flip);
-          std::vector< Node > nchildren;
-          nchildren.push_back(bv::utils::mkExtract(first_child, i-1, 0));
-          for( unsigned j=1, size=ret[0].getNumChildren(); j<size; j++ )
+          Assert(i > 0);
+          Node extract_flip = bv::utils::mkExtract(first_child, csize - 1, i);
+          extract_flip = TermUtil::mkNegate(BITVECTOR_NOT, extract_flip);
+          std::vector<Node> nchildren;
+          nchildren.push_back(bv::utils::mkExtract(first_child, i - 1, 0));
+          for (unsigned j = 1, size = ret[0].getNumChildren(); j < size; j++)
           {
-            nchildren.push_back( ret[0][j] );
+            nchildren.push_back(ret[0][j]);
           }
-          new_ret = nm->mkNode(BITVECTOR_CONCAT,extract_flip, nm->mkNode(BITVECTOR_NEG, nm->mkNode(BITVECTOR_CONCAT,nchildren)));
+          new_ret =
+              nm->mkNode(BITVECTOR_CONCAT,
+                         extract_flip,
+                         nm->mkNode(BITVECTOR_NEG,
+                                    nm->mkNode(BITVECTOR_CONCAT, nchildren)));
           debugExtendedRewrite(ret, new_ret, "NEG-msb-1");
           return new_ret;
         }
@@ -3223,134 +3234,141 @@ void ExtendedRewriter::spliceBv(Node a,
   }
 }
 
-
-int ExtendedRewriter::spliceBvConstBit(Node n1,
-            Node n2,
-            std::vector<Node>& nv)
+int ExtendedRewriter::spliceBvConstBit(Node n1, Node n2, std::vector<Node>& nv)
 {
-  if( n1==n2 )
+  if (n1 == n2)
   {
     return -1;
   }
-  Trace("q-ext-rewrite-debug") << "Splice constant bv bit " << n1 << " " << n2 << std::endl;
+  Trace("q-ext-rewrite-debug")
+      << "Splice constant bv bit " << n1 << " " << n2 << std::endl;
   // splice the children
-  std::vector< Node > rc1;
-  std::vector< Node > rc2;
-  spliceBv(n1,n2,rc1,rc2);
-  Assert( rc1.size()==rc2.size() );
+  std::vector<Node> rc1;
+  std::vector<Node> rc2;
+  spliceBv(n1, n2, rc1, rc2);
+  Assert(rc1.size() == rc2.size());
   int diff_index = -1;
-  for( unsigned r=0; r<rc1.size(); r++ )
+  for (unsigned r = 0; r < rc1.size(); r++)
   {
-    if( rc1[r]!=rc2[r] )
+    if (rc1[r] != rc2[r])
     {
-      if( diff_index>=0 )
+      if (diff_index >= 0)
       {
         // differ at more than one index
-        Trace("q-ext-rewrite-debug") << "...more than one diff component." << std::endl;
+        Trace("q-ext-rewrite-debug")
+            << "...more than one diff component." << std::endl;
         return -1;
       }
       diff_index = r;
     }
   }
-  Assert( diff_index>=0 );
-  if( !rc1[diff_index].isConst() || !rc2[diff_index].isConst() )
+  Assert(diff_index >= 0);
+  if (!rc1[diff_index].isConst() || !rc2[diff_index].isConst())
   {
-    Trace("q-ext-rewrite-debug") << "...non-constant diff components." << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "...non-constant diff components." << std::endl;
     return -1;
   }
   // insert prefix
-  if( diff_index>0 )
+  if (diff_index > 0)
   {
-    nv.insert(nv.end(),rc1.begin(),rc1.begin()+diff_index);
+    nv.insert(nv.end(), rc1.begin(), rc1.begin() + diff_index);
   }
-  Assert( rc1[diff_index]!=rc2[diff_index] );
+  Assert(rc1[diff_index] != rc2[diff_index]);
   Node c1 = rc1[diff_index];
   Node c2 = rc2[diff_index];
   // do they differ by exactly one bit?
   int bit_diff_index = -1;
   unsigned csize = bv::utils::getSize(c1);
-  for( unsigned i=0; i<csize; i++ )
+  for (unsigned i = 0; i < csize; i++)
   {
-    if( bv::utils::getBit(c1,i)!=bv::utils::getBit(c2,i) )
+    if (bv::utils::getBit(c1, i) != bv::utils::getBit(c2, i))
     {
-      if( bit_diff_index>=0 )
+      if (bit_diff_index >= 0)
       {
         // differ by more than one bit
         nv.clear();
-        Trace("q-ext-rewrite-debug") << "...more than one bit diff." << std::endl;
+        Trace("q-ext-rewrite-debug")
+            << "...more than one bit diff." << std::endl;
         return -1;
       }
       bit_diff_index = i;
     }
   }
-  if( bit_diff_index>=0 )
+  if (bit_diff_index >= 0)
   {
-    std::vector< Node > split;
-    if( bit_diff_index+1<static_cast<int>(csize) )
+    std::vector<Node> split;
+    if (bit_diff_index + 1 < static_cast<int>(csize))
     {
-      Node extract = bv::utils::mkExtract(c1, csize-1, bit_diff_index+1);
+      Node extract = bv::utils::mkExtract(c1, csize - 1, bit_diff_index + 1);
       nv.push_back(Rewriter::rewrite(extract));
     }
-    Node bit = bv::utils::getBit(c1,bit_diff_index) ? bv::utils::mkOnes(1) : bv::utils::mkZero(1);
+    Node bit = bv::utils::getBit(c1, bit_diff_index) ? bv::utils::mkOnes(1)
+                                                     : bv::utils::mkZero(1);
     diff_index = nv.size();
     nv.push_back(bit);
     // remainder
-    if( bit_diff_index>0 )
+    if (bit_diff_index > 0)
     {
-      Node extract = bv::utils::mkExtract(c1, bit_diff_index-1,0);
+      Node extract = bv::utils::mkExtract(c1, bit_diff_index - 1, 0);
       nv.push_back(Rewriter::rewrite(extract));
     }
     // insert suffix
-    if( diff_index<static_cast<int>(rc1.size()) )
+    if (diff_index < static_cast<int>(rc1.size()))
     {
-      nv.insert(nv.end(),rc1.begin()+diff_index+1,rc1.end());
+      nv.insert(nv.end(), rc1.begin() + diff_index + 1, rc1.end());
     }
     return diff_index;
   }
   return -1;
 }
 
-Node ExtendedRewriter::extendBv(Node n, std::vector< Node >& exs)
+Node ExtendedRewriter::extendBv(Node n, std::vector<Node>& exs)
 {
-  std::map< unsigned, Node > ex_map;
-  for( const Node& e : exs )
+  std::map<unsigned, Node> ex_map;
+  for (const Node& e : exs)
   {
     ex_map[bv::utils::getExtractHigh(e)] = e;
   }
-  return extendBv(n,ex_map);
+  return extendBv(n, ex_map);
 }
 
-Node ExtendedRewriter::extendBv(Node n, std::map< unsigned, Node >& ex_map)
+Node ExtendedRewriter::extendBv(Node n, std::map<unsigned, Node>& ex_map)
 {
   Trace("q-ext-rewrite-debug") << "extendBv " << n << std::endl;
-  std::vector< Node > children;
+  std::vector<Node> children;
   int counter = bv::utils::getSize(n) - 1;
-  for( const std::pair< const unsigned, Node >& ep : ex_map )
+  for (const std::pair<const unsigned, Node>& ep : ex_map)
   {
-    Trace("q-ext-rewrite-debug") << "  process " << ep.first << " : " << ep.second << ", counter=" << counter << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "  process " << ep.first << " : " << ep.second
+        << ", counter=" << counter << std::endl;
     unsigned start = ep.first;
-    Assert( static_cast<int>(start)<=counter );
-    if( static_cast<int>(start)<counter )
+    Assert(static_cast<int>(start) <= counter);
+    if (static_cast<int>(start) < counter)
     {
-      children.push_back( bv::utils::mkExtract(n, counter, start+1) );
+      children.push_back(bv::utils::mkExtract(n, counter, start + 1));
     }
     Node ex = ep.second;
-    children.push_back( ex );
+    children.push_back(ex);
     // update the counter
     unsigned esize = bv::utils::getSize(ex);
-    counter = start-esize;
-    Assert( counter+1>=0 );
+    counter = start - esize;
+    Assert(counter + 1 >= 0);
   }
-  if( counter>=0 )
+  if (counter >= 0)
   {
-    children.push_back( bv::utils::mkExtract(n, counter, 0) );
+    children.push_back(bv::utils::mkExtract(n, counter, 0));
   }
-  Trace("q-ext-rewrite-debug") << "extendBv finish, children = " << children << std::endl;
-  if( children.empty() )
+  Trace("q-ext-rewrite-debug")
+      << "extendBv finish, children = " << children << std::endl;
+  if (children.empty())
   {
     return n;
   }
-  return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( BITVECTOR_CONCAT, children );
+  return children.size() == 1
+             ? children[0]
+             : NodeManager::currentNM()->mkNode(BITVECTOR_CONCAT, children);
 }
 
 void ExtendedRewriter::debugExtendedRewrite(Node n,