From f1c8b8cda3b99353adbe424e0bf1259147001f3c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Nov 2017 06:33:23 -0600 Subject: Remove remaining references to QuantArith (#1408) --- src/theory/quantifiers/trigger.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/trigger.cpp') 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 -- cgit v1.2.3