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/equality_infer.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/equality_infer.cpp')
-rw-r--r-- | src/theory/quantifiers/equality_infer.cpp | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index 66ca38e8c..a5cbef746 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -15,8 +15,10 @@ **/ #include "theory/quantifiers/equality_infer.h" -#include "theory/quantifiers/quant_util.h" + #include "context/context_mm.h" +#include "theory/rewriter.h" +#include "theory/arith/arith_msum.h" using namespace CVC4; using namespace CVC4::kind; @@ -144,7 +146,8 @@ void EqualityInference::eqNotifyNewClass(TNode t) { //somewhat strange: t may not be in rewritten form Node r = Rewriter::rewrite( t ); std::map< Node, Node > msum; - if( QuantArith::getMonomialSum( r, msum ) ){ + if (ArithMSum::getMonomialSum(r, msum)) + { Trace("eq-infer-debug2") << "...process monomial sum, size = " << msum.size() << std::endl; eqci->d_valid = true; bool changed = false; @@ -185,7 +188,8 @@ void EqualityInference::eqNotifyNewClass(TNode t) { Trace("eq-infer-debug2") << "...pre-rewrite : " << r << std::endl; r = Rewriter::rewrite( r ); msum.clear(); - if( !QuantArith::getMonomialSum( r, msum ) ){ + if (!ArithMSum::getMonomialSum(r, msum)) + { mvalid = false; } } @@ -285,7 +289,8 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { if( tr1!=tr2 ){ Node eq = tr1.eqNode( tr2 ); std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if (ArithMSum::getMonomialSumLit(eq, msum)) + { Node v_solve; //solve for variables with no coefficient if( Trace.isOn("eq-infer-debug2") ){ @@ -315,7 +320,8 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { if( !v_solve.isNull() ){ //solve for v_solve Node veq; - if( QuantArith::isolate( v_solve, msum, veq, kind::EQUAL, true )==1 ){ + if (ArithMSum::isolate(v_solve, msum, veq, kind::EQUAL, true) == 1) + { Node v_value = veq[1]; Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl; Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() ); @@ -375,7 +381,9 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r ); if( itt!=d_eqci.end() && ( itt->second->d_valid || itt->second->d_solved ) ){ std::map< Node, Node > msum2; - if( QuantArith::getMonomialSum( itt->second->d_rep.get(), msum2 ) ){ + if (ArithMSum::getMonomialSum(itt->second->d_rep.get(), + msum2)) + { std::map< Node, Node >::iterator itm = msum2.find( v_solve ); if( itm!=msum2.end() ){ //substitute in solved form @@ -387,7 +395,7 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { itm->second.isNull() ? d_one : itm->second ); } msum2.erase( itm ); - Node rr = QuantArith::mkNode( msum2 ); + Node rr = ArithMSum::mkNode(msum2); rr = Rewriter::rewrite( rr ); Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl; setEqcRep( itt->first, rr, exp, itt->second ); |