diff options
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 91c04bc80..dda3b1be4 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -179,20 +179,7 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, std::map< Node, Node > msum; if (QuantArith::getMonomialSumLit( lit, msum )){ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; - for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Trace("bound-int-debug") << " "; - if( !it->second.isNull() ){ - Trace("bound-int-debug") << it->second; - if( !it->first.isNull() ){ - Trace("bound-int-debug") << " * "; - } - } - if( !it->first.isNull() ){ - Trace("bound-int-debug") << it->first; - } - Trace("bound-int-debug") << std::endl; - } - Trace("bound-int-debug") << std::endl; + QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" ); for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){ Node veq; |