#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"
}
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;
}
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
}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] =
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)) {
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());
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;
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) {
{
// 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) {
// 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;
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;
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;
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
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;
#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"
}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 ){
#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"
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
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]);
}
}
}
}
}
- 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") ){
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 ){
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] );
}
}
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 ){
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:
**/
#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"
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() ){
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
projects / cvc5.git / commitdiff