Minor changes to smt comp script for quantified arith. Add option --cbqi-sat whether to disable sat for quantified arith.

3 files changed, 17 insertions, 6 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index f530f7b9d..e867aae1e 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -173,6 +173,7 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
 }
 
 void InstantiationEngine::reset_round( Theory::Effort e ) {
+  d_cbqi_set_quant_inactive = false;
   if( options::cbqi() ){
     //set inactive the quantified formulas whose CE literals are asserted false
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
@@ -185,9 +186,11 @@ void InstantiationEngine::reset_round( Theory::Effort e ) {
         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
           Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
           if( !value ){
-            d_quantEngine->getModel()->setQuantifierActive( q, false );
             if( d_quantEngine->getValuation().isDecision( cel ) ){
               Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
+            }else{
+              d_quantEngine->getModel()->setQuantifierActive( q, false );
+              d_cbqi_set_quant_inactive = true;
             }
           }
         }else{
@@ -233,12 +236,16 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 bool InstantiationEngine::checkComplete() {
-  for( unsigned i=0; i<d_quants.size(); i++ ){
-    if( isIncomplete( d_quants[i] ) ){
-      return false;
+  if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){
+    return false;
+  }else{
+    for( unsigned i=0; i<d_quants.size(); i++ ){
+      if( isIncomplete( d_quants[i] ) ){
+        return false;
+      }
     }
+    return true;
   }
-  return true;
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 21056bc05..dc5b976f0 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -87,6 +87,8 @@ private:
   bool doCbqi( Node f );
   /** is the engine incomplete for this quantifier */
   bool isIncomplete( Node f );
+  /** cbqi set inactive */
+  bool d_cbqi_set_quant_inactive;
 private:
   /** do instantiation round */
   bool doInstantiationRound( Theory::Effort effort );
@@ -98,7 +100,7 @@ public:
   /** initialize */
   void finishInit();
 
-  bool needsCheck( Theory::Effort e ); 
+  bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e2d9af74f..fe81df7f8 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -232,6 +232,8 @@ option cbqi2 --cbqi2 bool :read-write :default false
  turns on new implementation of counterexample-based quantifier instantiation
 option recurseCbqi --cbqi-recurse bool :default false
  turns on recursive counterexample-based quantifier instantiation
+option cbqiSat --cbqi-sat bool :read-write :default true
+ answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
  
 ### local theory extensions options