From 32cda667fac11b1768ed75d930cb5b0e6933ffe5 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 4 Jun 2015 08:14:30 +0200
Subject: [PATCH] Minor changes to smt comp script for quantified arith.  Add
 option --cbqi-sat whether to disable sat for quantified arith.

---
 contrib/run-script-smtcomp2015                  | 12 ++++++------
 contrib/run-script-smtcomp2015-application      |  4 ++--
 src/theory/quantifiers/instantiation_engine.cpp | 17 ++++++++++++-----
 src/theory/quantifiers/instantiation_engine.h   |  4 +++-
 src/theory/quantifiers/options                  |  2 ++
 5 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
index 3fc8ccec5..9b8a0ba38 100755
--- a/contrib/run-script-smtcomp2015
+++ b/contrib/run-script-smtcomp2015
@@ -67,12 +67,12 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 20 --cbqi --full-saturate-quant
-  trywith 20 --full-saturate-quant
-  trywith 20 --cbqi --cbqi-recurse --full-saturate-quant
-  trywith 60 --qcf-tconstraint --full-saturate-quant
-  trywith 120 --cbqi --cbqi-recurse --full-saturate-quant
-  finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
+  trywith 60 --cbqi --full-saturate-quant
+  trywith 60 --full-saturate-quant
+  trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
+  trywith 180 --qcf-tconstraint --full-saturate-quant
+  trywith 240 --cbqi --cbqi-recurse --full-saturate-quant
+  finishwith --cbqi --cbqi-recurse --pre-skolem-quant --full-saturate-quant
   ;;
 QF_AUFBV)
   trywith 600
diff --git a/contrib/run-script-smtcomp2015-application b/contrib/run-script-smtcomp2015-application
index 69b3f8b37..4219241ef 100755
--- a/contrib/run-script-smtcomp2015-application
+++ b/contrib/run-script-smtcomp2015-application
@@ -33,10 +33,10 @@ QF_LIA)
   runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites
   ;;
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
-  runcvc4 --simplification=none --decision=internal --full-saturate-quant
+  runcvc4 
   ;;
 LIA|LRA|NIA|NRA)
-  runcvc4 --enable-cbqi --full-saturate-quant
+  runcvc4 --cbqi
   ;;
 QF_BV)
   runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
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 
 
-- 
2.30.2