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/quantifiers_rewriter.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/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 45c418996..511e8f051 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "options/quantifiers_options.h" +#include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" @@ -942,7 +943,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){ //for arithmetic, solve the (in)equality std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( lit, msum ) ){ + if (ArithMSum::getMonomialSumLit(lit, msum)) + { for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ if( !itm->first.isNull() ){ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); @@ -951,7 +953,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto Assert( pol ); Node veq_c; Node val; - int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); + int ires = + ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){ Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl; vars.push_back( itm->first ); @@ -964,7 +967,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto //store that this literal is upper/lower bound for itm->first Node veq_c; Node val; - int ires = QuantArith::isolate( itm->first, msum, veq_c, val, lit.getKind() ); + int ires = ArithMSum::isolate( + itm->first, msum, veq_c, val, lit.getKind()); if( ires!=0 && veq_c.isNull() ){ bool is_upper = pol!=( ires==1 ); Trace("var-elim-ineq-debug") << lit << " is a " << ( is_upper ? "upper" : "lower" ) << " bound for " << itm->first << std::endl; |