Remove remaining references to QuantArith (#1408)

6 files changed, 45 insertions, 421 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 77c4e2e40..20f19db9d 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -21,6 +21,7 @@
 
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
+#include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/quantifiers/quant_util.h"
@@ -111,7 +112,7 @@ std::vector<Node> ExpandMultiset(const NodeMultiset& a) {
 }
 
 void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) {
-  Node t = QuantArith::mkCoeffTerm(coeff, x);
+  Node t = ArithMSum::mkCoeffTerm(coeff, x);
   Trace(c) << t << " " << type << " " << rhs;
 }
 
@@ -357,7 +358,8 @@ bool NonLinearExtentionSubstitutionSolver::solve(
         if (!n.isConst()) {
           Trace("nl-subs-debug") << "Look at term : " << n << std::endl;
           std::map<Node, Node> msum;
-          if (QuantArith::getMonomialSum(n, msum)) {
+          if (ArithMSum::getMonomialSum(n, msum))
+          {
             int nconst_count = 0;
             bool evaluatable = true;
             //first, collect sums of equal terms
@@ -402,7 +404,8 @@ bool NonLinearExtentionSubstitutionSolver::solve(
                 }else{
                   //recompute the monomial
                   msum.clear();
-                  if (!QuantArith::getMonomialSum(ns, msum)) {
+                  if (!ArithMSum::getMonomialSum(ns, msum))
+                  {
                     success = false;
                   }else{
                     d_rep_sum_unique_exp[n] =
@@ -562,7 +565,7 @@ bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst(
               d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const,
               d_rep_to_const_exp, d_rep_to_const_base);
           Node eq = (result.term).eqNode(d_rep_to_const[r]);
-          Node v_c = QuantArith::solveEqualityFor(eq, result.variable_term);
+          Node v_c = ArithMSum::solveEqualityFor(eq, result.variable_term);
           if (!v_c.isNull()) {
             Assert(v_c.isConst());
             if (Contains(new_const, result.variable_term)) {
@@ -596,7 +599,7 @@ bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst(
         Node v = result.variable_term;
         Node m_t = result.term;
         Node eq = m_t.eqNode(r_c);
-        Node v_c = QuantArith::solveEqualityFor(eq, v);
+        Node v_c = ArithMSum::solveEqualityFor(eq, v);
         Trace("nl-subs-debug") << "Solved equality " << eq << " for " << v << ", got = " << v_c << std::endl;
         if (!v_c.isNull()) {
           Assert(v_c.isConst());
@@ -837,10 +840,11 @@ void NonlinearExtension::registerConstraint(Node atom) {
     d_constraints.push_back(atom);
     Trace("nl-ext-debug") << "Register constraint : " << atom << std::endl;
     std::map<Node, Node> msum;
-    if (QuantArith::getMonomialSumLit(atom, msum)) {
+    if (ArithMSum::getMonomialSumLit(atom, msum))
+    {
       Trace("nl-ext-debug") << "got monomial sum: " << std::endl;
       if (Trace.isOn("nl-ext-debug")) {
-        QuantArith::debugPrintMonomialSum(msum, "nl-ext-debug");
+        ArithMSum::debugPrintMonomialSum(msum, "nl-ext-debug");
       }
       unsigned max_degree = 0;
       std::vector<Node> all_m;
@@ -867,7 +871,7 @@ void NonlinearExtension::registerConstraint(Node atom) {
       for (unsigned i = 0; i < all_m.size(); i++) {
         Node m = all_m[i];
         Node rhs, coeff;
-        int res = QuantArith::isolate(m, msum, coeff, rhs, atom.getKind());
+        int res = ArithMSum::isolate(m, msum, coeff, rhs, atom.getKind());
         if (res != 0) {
           Kind type = atom.getKind();
           if (res == -1) {
@@ -2272,7 +2276,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
           {
             // we will take the strict inequality in the direction of the
             // model
-            Node lhs = QuantArith::mkCoeffTerm(coeff, x);
+            Node lhs = ArithMSum::mkCoeffTerm(coeff, x);
             Node query = NodeManager::currentNM()->mkNode(GT, lhs, rhs);
             Node query_mv = computeModelValue(query, 1);
             if (query_mv == d_true) {
@@ -2290,7 +2294,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
         // add to status if maximal degree
         d_ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end();
         if (Trace.isOn("nl-ext-bound-debug2")) {
-          Node t = QuantArith::mkCoeffTerm(coeff, x);
+          Node t = ArithMSum::mkCoeffTerm(coeff, x);
           Trace("nl-ext-bound-debug2")
               << "Add Bound: " << t << " " << type << " " << rhs << " by "
               << exp << std::endl;
@@ -2416,7 +2420,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
                  itc->second.begin();
              itcc != itc->second.end(); ++itcc) {
           Node coeff = itcc->first;
-          Node t = QuantArith::mkCoeffTerm(coeff, x);
+          Node t = ArithMSum::mkCoeffTerm(coeff, x);
           for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
                itcr != itcc->second.end(); ++itcr) {
             Node rhs = itcr->first;
@@ -2512,10 +2516,11 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
     Node atom = lit.getKind() == NOT ? lit[0] : lit;
     if( false_asserts.find(lit) != false_asserts.end() || d_skolem_atoms.find(atom)!=d_skolem_atoms.end() ){
       std::map<Node, Node> msum;
-      if (QuantArith::getMonomialSumLit(atom, msum)) {
+      if (ArithMSum::getMonomialSumLit(atom, msum))
+      {
         Trace("nl-ext-factor") << "Factoring for literal " << lit << ", monomial sum is : " << std::endl;
         if (Trace.isOn("nl-ext-factor")) {
-          QuantArith::debugPrintMonomialSum(msum, "nl-ext-factor");
+          ArithMSum::debugPrintMonomialSum(msum, "nl-ext-factor");
         }
         std::map< Node, std::vector< Node > > factor_to_mono;
         std::map< Node, std::vector< Node > > factor_to_mono_orig;
@@ -2563,7 +2568,8 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
             Assert( itfo!=factor_to_mono_orig.end() );
             for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
               if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){
-                poly.push_back( QuantArith::mkCoeffTerm(itm->second, itm->first.isNull() ? d_one : itm->first) );
+                poly.push_back(ArithMSum::mkCoeffTerm(
+                    itm->second, itm->first.isNull() ? d_one : itm->first));
               }
             }
             Node polyn = poly.size() == 1
@@ -2665,14 +2671,14 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
                        itcbc != itcb->second.end(); ++itcbc) {
                     Node coeff_b = itcbc->first;
                     Node rhs_a_res =
-                        QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base);
+                        ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base);
                     for (std::map<Node, Kind>::iterator itcbr =
                              itcbc->second.begin();
                          itcbr != itcbc->second.end(); ++itcbr) {
                       Node rhs_b = itcbr->first;
                       Node rhs_b_res = NodeManager::currentNM()->mkNode(
                           MULT, ita->second, rhs_b);
-                      rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res);
+                      rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
                       rhs_b_res = Rewriter::rewrite(rhs_b_res);
                       if (!hasNewMonomials(rhs_b_res, d_ms)) {
                         Kind type_b = itcbr->second;
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index cf2c51ec1..877db6797 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -17,6 +17,7 @@
 
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
+#include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
@@ -724,7 +725,8 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
     }else if( try_coeff ){
       //must convert to monomial representation
       std::map< Node, Node > msum;
-      if( QuantArith::getMonomialSum( n, msum ) ){
+      if (ArithMSum::getMonomialSum(n, msum))
+      {
         std::map< Node, Node > msum_coeff;
         std::map< Node, Node > msum_term;
         for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 4570d03c3..4d5affd2e 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/trigger.h"
 
+#include "theory/arith/arith_msum.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
@@ -103,10 +104,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
   int ires = 0;
   Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl;
   std::map< Node, Node > msum;
-  if( QuantArith::getMonomialSumLit( atom, msum ) ){
+  if (ArithMSum::getMonomialSumLit(atom, msum))
+  {
     Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl;
     if( Trace.isOn("cegqi-arith-debug") ){
-      QuantArith::debugPrintMonomialSum( msum, "cegqi-arith-debug" );
+      ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug");
     }
     TypeNode pvtn = pv.getType();
     //remove vts symbols from polynomial
@@ -124,13 +126,13 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
           if( itv!=msum.end() ){
             //multiply by the coefficient we will isolate for
             if( itv->second.isNull() ){
-              vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+              vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
             }else{
               if( !pvtn.isInteger() ){
                 vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
                 vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
               }else if( itv->second.getConst<Rational>().sgn()==1 ){
-                vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+                vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
               }
             }
           }
@@ -140,7 +142,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
       }
     }
 
-    ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+    ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
     if( ires!=0 ){
       Node realPart;
       if( Trace.isOn("cegqi-arith-debug") ){
@@ -194,7 +196,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
         Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
         //re-isolate
         Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
-        ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+        ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
         Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
         Trace("cegqi-arith-debug") << "                 real part : " << realPart << std::endl;
         if( ires!=0 ){
@@ -669,13 +671,16 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
   eq = Rewriter::rewrite( eq );
   Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
   std::map< Node, Node > msum;
-  if( QuantArith::getMonomialSumLit( eq, msum ) ){
+  if (ArithMSum::getMonomialSumLit(eq, msum))
+  {
     Node veq;
-    if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){
+    if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) != 0)
+    {
       Node veq_c;
       if( veq[0]!=sf.d_vars[index] ){
         Node veq_v;
-        if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+        if (ArithMSum::getMonomial(veq[0], veq_c, veq_v))
+        {
           Assert( veq_v==sf.d_vars[index] );
         }
       }
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 ){
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index b1bba1842..f3fdfa6f4 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -182,161 +182,6 @@ public:
   virtual bool checkComplete() { return true; }
 };
 
-/** Arithmetic utilities regarding monomial sums.
- *
- * Note the following terminology:
- *
- *   We say Node c is a {monomial constant} (or m-constant) if either:
- *   (a) c is a constant Rational, or
- *   (b) c is null.
- *
- *   We say Node v is a {monomial variable} (or m-variable) if either:
- *   (a) v.getType().isReal() and v is not a constant, or
- *   (b) v is null.
- *
- *   For m-constant or m-variable t, we write [t] to denote 1 if t.isNull() and
- *   t otherwise.
- *
- *   A monomial m is a pair ( mvariable, mconstant ) of the form ( v, c ), which
- *   is interpreted as [c]*[v].
- *
- *   A {monmoial sum} msum is represented by a std::map< Node, Node > having
- *   key-value pairs of the form ( mvariable, mconstant ).
- *   It is interpreted as:
- *   [msum] = sum_{( v, c ) \in msum } [c]*[v]
- *   It is critical that this map is ordered so that operations like adding
- *   two monomial sums can be done efficiently. The ordering itself is not 
- *   important, and currently corresponds to the default ordering on Nodes.
- *
- * The following has utilities involving monmoial sums.
- *
- */
-class QuantArith
-{
-public:
- /** get monomial
-  *
-  * If n = n[0]*n[1] where n[0] is constant and n[1] is not,
-  * this function returns true, sets c to n[0] and v to n[1].
-  */
- static bool getMonomial(Node n, Node& c, Node& v);
-
- /** get monomial
-  *
-  * If this function returns true, it adds the ( m-constant, m-variable )
-  * pair corresponding to the monomial representation of n to the
-  * monomial sum msum.
-  *
-  * This function returns false if the m-variable of n is already
-  * present in n.
-  */
- static bool getMonomial(Node n, std::map<Node, Node>& msum);
-
- /** get monomial sum for real-valued term n
-  *
-  * If this function returns true, it sets msum to a monmoial sum such that
-  *   [msum] is equivalent to n
-  *
-  * This function may return false if n is not a sum of monomials
-  * whose variables are pairwise unique.
-  * If term n is in rewritten form, this function should always return true.
-  */
- static bool getMonomialSum(Node n, std::map<Node, Node>& msum);
-
- /** get monmoial sum literal for literal lit
-  *
-  * If this function returns true, it sets msum to a monmoial sum such that
-  *   [msum] <k> 0  is equivalent to lit[0] <k> lit[1]
-  * where k is the Kind of lit, one of { EQUAL, GEQ }.
-  *
-  * This function may return false if either side of lit is not a sum
-  * of monomials whose variables are pairwise unique on that side.
-  * If literal lit is in rewritten form, this function should always return
-  * true.
-  */
- static bool getMonomialSumLit(Node lit, std::map<Node, Node>& msum);
-
- /** make node for monomial sum
-  *
-  * Make the Node corresponding to the interpretation of msum, [msum], where:
-  *   [msum] = sum_{( v, c ) \in msum } [c]*[v]
-  */
- static Node mkNode(std::map<Node, Node>& msum);
-
- /** make coefficent term
-  *
-  * Input coeff is a m-constant.
-  * Returns the term t if coeff.isNull() or coeff*t otherwise.
-  */
- static Node mkCoeffTerm(Node coeff, Node t);
-
- /** isolate variable v in constraint ([msum] <k> 0)
-  *
-  * If this function returns a value ret where ret != 0, then
-  * veq_c is set to m-constant, and val is set to a term such that:
-  *    If ret=1, then ([veq_c] * v <k> val) is equivalent to [msum] <k> 0.
-  *   If ret=-1, then (val <k> [veq_c] * v) is equivalent to [msum] <k> 0.
-  *   If veq_c is non-null, then it is a positive constant Rational.
-  * The returned value of veq_c is only non-null if v has integer type.
-  *
-  * This function returns 0 indicating a failure if msum does not contain
-  * a (non-zero) monomial having mvariable v.
-  */
- static int isolate(
-     Node v, std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k);
-
- /** isolate variable v in constraint ([msum] <k> 0)
-  *
-  * If this function returns a value ret where ret != 0, then veq
-  * is set to a literal that is equivalent to ([msum] <k> 0), and:
-  *    If ret=1, then veq is of the form ( v <k> val) if veq_c.isNull(),
-  *                   or ([veq_c] * v <k> val) if !veq_c.isNull().
-  *   If ret=-1, then veq is of the form ( val <k> v) if veq_c.isNull(),
-  *                   or (val <k> [veq_c] * v) if !veq_c.isNull().
-  * If doCoeff = false or v does not have Integer type, then veq_c is null.
-  *
-  * This function returns 0 indiciating a failure if msum does not contain
-  * a (non-zero) monomial having variable v, or if veq_c must be non-null
-  * for an integer constraint and doCoeff is false.
-  */
- static int isolate(Node v,
-                    std::map<Node, Node>& msum,
-                    Node& veq,
-                    Kind k,
-                    bool doCoeff = false);
-
- /** solve equality lit for variable
-  *
-  * If return value ret is non-null, then:
-  *    v = ret is equivalent to lit.
-  *
-  * This function may return false if lit does not contain v,
-  * or if lit is an integer equality with a coefficent on v,
-  * e.g. 3*v = 7.
-  */
- static Node solveEqualityFor(Node lit, Node v);
-
- /** decompose real-valued term n
- *
- * If this function returns true, then
- *   ([coeff]*v + rem) is equivalent to n
- * where coeff is non-zero m-constant.
- *
- * This function will return false if n is not a monomial sum containing
- * a monomial with factor v.
- */
- static bool decompose(Node n, Node v, Node& coeff, Node& rem);
-
- /** return the rewritten form of (UMINUS t) */
- static Node negate(Node t);
-
- /** return the rewritten form of (PLUS t (CONST_RATIONAL i)) */
- static Node offset(Node t, int i);
-
- /** debug print for a monmoial sum, prints to Trace(c) */
- static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c);
-};
-
 class QuantPhaseReq
 {
 private:
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index ce306541f..40079933e 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -13,6 +13,8 @@
  **/
 
 #include "theory/quantifiers/trigger.h"
+
+#include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/quantifiers/ho_trigger.h"
 #include "theory/quantifiers/inst_match_generator.h"
@@ -322,7 +324,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
     if( rtr.isNull() && n[0].getType().isReal() ){
       //try to solve relation
       std::map< Node, Node > m;
-      if( QuantArith::getMonomialSumLit(n, m) ){
+      if (ArithMSum::getMonomialSumLit(n, m))
+      {
         for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
           bool trySolve = false;
           if( !it->first.isNull() ){
@@ -335,7 +338,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
           if( trySolve ){
             Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
             Node veq;
-            if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
+            if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
+            {
               rtr = getIsUsableEq( q, veq );
             }
             //either all solves will succeed or all solves will fail