diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-16 14:09:30 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-16 14:09:30 -0600 |
| commit | 6c6f4e23aea405a812b1c6a3dd4d80696eb34741 (patch) | |
| tree | acdb79a293d6f1e9034913dc51f45ad75d892be1 /src/theory/quantifiers/relevant_domain.cpp | |
| parent | 7bd874b098f210b53f5b608bc159d1d90c8794b8 (diff) | |
(Refactor) Arithmetic monomial sum (#1381)
* Add arithmetic monomial sum utility.
* Clang format
* Fix
* Address review.
* Fix missed comment.
* Format
* Fix
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index dcd24b433..e38f76994 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -12,11 +12,12 @@ ** \brief Implementation of relevant domain class **/ -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4; @@ -245,7 +246,8 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No //solve the inequality for one/two variables, if possible if( n[0].getType().isReal() ){ std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( n, msum ) ){ + if (ArithMSum::getMonomialSumLit(n, msum)) + { Node var; Node var2; bool hasNonVar = false; @@ -267,7 +269,8 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No //single variable solve Node veq_c; Node val; - int ires = QuantArith::isolate( var, msum, veq_c, val, n.getKind() ); + int ires = + ArithMSum::isolate(var, msum, veq_c, val, n.getKind()); if( ires!=0 ){ if( veq_c.isNull() ){ r_add = val; @@ -302,10 +305,12 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ - d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, i==0 ? 1 : -1 ) ); + d_rel_dom_lit[hasPol][pol][n].d_val.push_back( + ArithMSum::offset(r_add, i == 0 ? 1 : -1)); } }else if( n.getKind()==GEQ ){ - d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, varLhs ? 1 : -1 ) ); + d_rel_dom_lit[hasPol][pol][n].d_val.push_back( + ArithMSum::offset(r_add, varLhs ? 1 : -1)); } } }else{ |