Remove remaining references to QuantArith (#1408)

1 files changed, 0 insertions, 238 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 571c3846a..ccc6e99a8 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -52,244 +52,6 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
 
 quantifiers::TermUtil * QuantifiersModule::getTermUtil() {
   return d_quantEngine->getTermUtil();
-}  
-  
-bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
-  if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
-    c = n[0];
-    v = n[1];
-    return true;
-  }else{
-    return false;
-  }
-}
-bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
-  if( n.isConst() ){
-    if( msum.find(Node::null())==msum.end() ){
-      msum[Node::null()] = n;
-      return true;
-    }
-  }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
-    if( msum.find(n[1])==msum.end() ){
-      msum[n[1]] = n[0];
-      return true;
-    }
-  }else{
-    if( msum.find(n)==msum.end() ){
-      msum[n] = Node::null();
-      return true;
-    }
-  }
-  return false;
-}
-
-bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) {
-  if ( n.getKind()==PLUS ){
-    for( unsigned i=0; i<n.getNumChildren(); i++) {
-      if (!getMonomial( n[i], msum )){
-        return false;
-      }
-    }
-    return true;
-  }else{
-    return getMonomial( n, msum );
-  }
-}
-
-bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
-  if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
-    if( getMonomialSum( lit[0], msum ) ){
-      if( lit[1].isConst() && lit[1].getConst<Rational>().isZero() ){
-        return true;
-      }else{
-        //subtract the other side
-        std::map< Node, Node > msum2;
-        if( getMonomialSum( lit[1], msum2 ) ){
-          for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){
-            std::map< Node, Node >::iterator it2 = msum.find( it->first );
-            if( it2!=msum.end() ){
-              Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second,
-                                                                it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
-              msum[it->first] = Rewriter::rewrite( r );
-            }else{
-              msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second );
-            }
-          }
-          return true;
-        }
-      }
-    }
-  }
-  return false;
-}
-
-Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
-  std::vector< Node > children;
-  for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-    Node m;
-    if( !it->first.isNull() ){
-      if( !it->second.isNull() ){
-        m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
-      }else{
-        m = it->first;
-      }
-    }else{
-      Assert( !it->second.isNull() );
-      m = it->second;
-    }
-    children.push_back(m);
-  }
-  return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
-}
-
-Node QuantArith::mkCoeffTerm( Node coeff, Node t ) {
-  if( coeff.isNull() ){
-    return t;
-  }else{
-    return NodeManager::currentNM()->mkNode( kind::MULT, coeff, t );
-  }
-}
-
-int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
-  std::map< Node, Node >::iterator itv = msum.find( v );
-  if( itv!=msum.end() ){
-    std::vector< Node > children;
-    Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
-    if ( r.sgn()!=0 ){
-      for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-        if( it->first!=v ){
-          Node m;
-          if( !it->first.isNull() ){
-            if ( !it->second.isNull() ){
-              m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
-            }else{
-              m = it->first;
-            }
-          }else{
-            m = it->second;
-          }
-          children.push_back(m);
-        }
-      }
-      val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
-                                (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
-      if( !r.isOne() && !r.isNegativeOne() ){
-        if( v.getType().isInteger() ){
-          veq_c = NodeManager::currentNM()->mkConst( r.abs() );
-        }else{
-          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
-        }
-      }
-      if( r.sgn()==1 ){
-        val = negate(val);
-      }else{
-        val = Rewriter::rewrite( val );
-      }
-      return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1;
-    }
-  }
-  return 0;
-}
-
-int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
-  Node veq_c;
-  Node val;
-  //isolate v in the (in)equality
-  int ires = isolate( v, msum, veq_c, val, k );
-  if( ires!=0 ){
-    Node vc = v;
-    if( !veq_c.isNull() ){
-      if( doCoeff ){
-        vc = NodeManager::currentNM()->mkNode( MULT, veq_c, vc );
-      }else{
-        return 0;
-      }
-    }
-    bool inOrder = ires==1;
-    veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : val, inOrder ? val : vc );
-  }
-  return ires;
-}
-
-Node QuantArith::solveEqualityFor( Node lit, Node v ) {
-  Assert( lit.getKind()==EQUAL );
-  //first look directly at sides
-  TypeNode tn = lit[0].getType();
-  for( unsigned r=0; r<2; r++ ){
-    if( lit[r]==v ){
-      return lit[1-r];
-    }
-  }
-  if( tn.isReal() ){
-    if( quantifiers::TermUtil::containsTerm( lit, v ) ){
-      std::map< Node, Node > msum;
-      if( QuantArith::getMonomialSumLit( lit, msum ) ){
-        Node val, veqc;
-        if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){
-          if( veqc.isNull() ){
-            // in this case, we have an integer equality with a coefficient
-            // on the variable we solved for that could not be eliminated,
-            // hence we fail.
-            return val;
-          }
-        }
-      }
-    }
-  }
-  return Node::null();
-}
-
-bool QuantArith::decompose(Node n, Node v, Node& coeff, Node& rem)
-{
-  std::map<Node, Node> msum;
-  if (getMonomialSum(n, msum))
-  {
-    std::map<Node, Node>::iterator it = msum.find(v);
-    if (it == msum.end())
-    {
-      return false;
-    }
-    else
-    {
-      coeff = it->second;
-      msum.erase(v);
-      rem = mkNode(msum);
-      return true;
-    }
-  }
-  else
-  {
-    return false;
-  }
-}
-
-Node QuantArith::negate( Node t ) {
-  Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
-  tt = Rewriter::rewrite( tt );
-  return tt;
-}
-
-Node QuantArith::offset( Node t, int i ) {
-  Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t );
-  tt = Rewriter::rewrite( tt );
-  return tt;
-}
-
-void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) {
-  for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-    Trace(c) << "  ";
-    if( !it->second.isNull() ){
-      Trace(c) << it->second;
-      if( !it->first.isNull() ){
-        Trace(c) << " * ";
-      }
-    }
-    if( !it->first.isNull() ){
-      Trace(c) << it->first;
-    }
-    Trace(c) << std::endl;
-  }
-  Trace(c) << std::endl;
 }
 
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){