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/smt | |
| 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/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e4ec57bb4..3e82a337c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,6 +83,7 @@ #include "smt_util/boolean_simplification.h" #include "smt_util/nary_builder.h" #include "smt_util/node_visitor.h" +#include "theory/arith/arith_msum.h" #include "theory/arith/pseudoboolean_proc.h" #include "theory/booleans/circuit_propagator.h" #include "theory/bv/bvintropow2.h" @@ -2735,7 +2736,8 @@ Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& v Node ret_lit = ret.getKind()==kind::NOT ? ret[0] : ret; bool ret_pol = ret.getKind()!=kind::NOT; std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( ret_lit, msum ) ){ + if (ArithMSum::getMonomialSumLit(ret_lit, msum)) + { //get common coefficient std::vector< Node > coeffs; for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ |