From f1c8b8cda3b99353adbe424e0bf1259147001f3c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Nov 2017 06:33:23 -0600 Subject: [PATCH] Remove remaining references to QuantArith (#1408) --- src/theory/arith/nonlinear_extension.cpp | 38 +-- src/theory/quantifiers/ceg_instantiator.cpp | 4 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 23 +- src/theory/quantifiers/quant_util.cpp | 238 ------------------ src/theory/quantifiers/quant_util.h | 155 ------------ src/theory/quantifiers/trigger.cpp | 8 +- 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 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 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 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 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 NonlinearExtension::checkMonomialInferBounds( std::vectormkNode(GT, lhs, rhs); Node query_mv = computeModelValue(query, 1); if (query_mv == d_true) { @@ -2290,7 +2294,7 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vectorsecond.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 NonlinearExtension::checkMonomialInferBounds( std::vectorsecond.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::iterator itcr = itcc->second.begin(); itcr != itcc->second.end(); ++itcr) { Node rhs = itcr->first; @@ -2512,10 +2516,11 @@ std::vector NonlinearExtension::checkFactoring( const std::set& 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 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 NonlinearExtension::checkFactoring( const std::set& fals Assert( itfo!=factor_to_mono_orig.end() ); for( std::map::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 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::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() ), vts_coeff[t] ); vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); }else if( itv->second.getConst().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& msum ) { - if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ - if( getMonomialSum( lit[0], msum ) ){ - if( lit[1].isConst() && lit[1].getConst().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(); - 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 msum; - if (getMonomialSum(n, msum)) - { - std::map::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& 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& msum); - - /** get monmoial sum literal for literal lit - * - * If this function returns true, it sets msum to a monmoial sum such that - * [msum] 0 is equivalent to lit[0] 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& 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& 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] 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 val) is equivalent to [msum] 0. - * If ret=-1, then (val [veq_c] * v) is equivalent to [msum] 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& msum, Node& veq_c, Node& val, Kind k); - - /** isolate variable v in constraint ([msum] 0) - * - * If this function returns a value ret where ret != 0, then veq - * is set to a literal that is equivalent to ([msum] 0), and: - * If ret=1, then veq is of the form ( v val) if veq_c.isNull(), - * or ([veq_c] * v val) if !veq_c.isNull(). - * If ret=-1, then veq is of the form ( val v) if veq_c.isNull(), - * or (val [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& 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& 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 -- 2.30.2