diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-30 06:33:23 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-30 06:33:23 -0600 |
| commit | f1c8b8cda3b99353adbe424e0bf1259147001f3c (patch) | |
| tree | c0b939982d46084e7a0e71c78bb5f1caa4877250 /src/theory/quantifiers/trigger.cpp | |
| parent | 0524281144b562fea63adf10bc3f5d6f75883296 (diff) | |
Remove remaining references to QuantArith (#1408)
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
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 |