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, 18 insertions, 1 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index f73bc7bb2..2dd800592 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -92,7 +92,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
         if( r.isOne() ){
           veq = negate(veq);
         }else{
-          //TODO
+          //TODO : lcd computation
           return false;
         }
       }
@@ -118,6 +118,23 @@ Node QuantArith::offset( Node t, int i ) {
   return tt;
 }
 
+void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) {
+  for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+    Trace(c) << "  ";
+    if( !it->second.isNull() ){
+      Trace(c) << it->second;
+      if( !it->first.isNull() ){
+        Trace(c) << " * ";
+      }
+    }
+    if( !it->first.isNull() ){
+      Trace(c) << it->first;
+    }
+    Trace(c) << std::endl;
+  }
+  Trace(c) << std::endl;
+}
+
 
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f