Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.

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;