Minor updates/fix to --cbqi-recurse

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 5d51381da278dbf21b3a0db5b835f0f6fc7022bb..073a9f297d9e1ba928bdb1d95ba88cde0ea358c1 100755 (executable)
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -2,16 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 70"
 
 file=${bench##*/}
 filename=${file%.*}
 
-echo "Run $bench at $2"
+echo "------- cvc4-fnt $bench at $2..."
 
 # use: trywith [params..]
-# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
-# which case this run script terminates immediately.  Otherwise, this
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
@@ -24,9 +23,14 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench
+}
 
 trywith 30 --finite-model-find --sort-inference --uf-ss-fair
 trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
 trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
-trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round
 echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index eb0478e248e2bdcfad972b5d349cc05a3ae5f7e9..582a14952eb16c9841ca361a3887ab3c73acb358 100755 (executable)
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -2,14 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 85"
 
 file=${bench##*/}
 filename=${file%.*}
 
+echo "------- cvc4-fof $bench at $2..."
+
 # use: trywith [params..]
-# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
-# which case this run script terminates immediately.  Otherwise, this
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
@@ -22,10 +23,16 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+}
 
 trywith 30 --full-saturate-quant
-trywith 10 --decision=internal --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
+trywith 30 --relevant-triggers --full-saturate-quant
 trywith 15 --finite-model-find --decision=justification-stoponly
-trywith $to --quant-cf --full-saturate-quant
+trywith 30 --pre-skolem-quant --full-saturate-quant
+finishwith --quant-cf --full-saturate-quant
 echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff
index 893b6957263b54dabb034d74d1a29378e8af160b..8033bed1fe3d1a6ce37c0465a167b40ab1e0aa68 100755 (executable)
--- a/contrib/run-script-cascj7-tff
+++ b/contrib/run-script-cascj7-tff
@@ -2,11 +2,12 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 170"
 
 file=${bench##*/}
 filename=${file%.*}
 
+echo "------- cvc4-tff $bench at $2..."
+
 # use: trywith [params..]
 # to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
 # which case this run script terminates immediately.  Otherwise, this
@@ -22,11 +23,16 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+}
 
 trywith 15 --cbqi-recurse --full-saturate-quant
 trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant
 trywith 20 --finite-model-find
-trywith 90 --full-saturate-quant
-trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant
+trywith 30 --full-saturate-quant
+trywith 60 --quant-cf --full-saturate-quant
+finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant
 echo "% SZS status" "GaveUp for $filename"

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 3edf97467819941c2a3b3a148593aa746e27e682..e3514d9494dc41308d92df3d17db3d3c59b1a619 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -38,9 +38,13 @@ d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c
 }
 
 void FirstOrderModel::assertQuantifier( Node n ){
-  d_forall_asserts.push_back( n );
-  if( n.getAttribute(AxiomAttribute()) ){
-    d_axiom_asserted = true;
+  if( n.getKind()==FORALL ){
+    d_forall_asserts.push_back( n );
+    if( n.getAttribute(AxiomAttribute()) ){
+      d_axiom_asserted = true;
+    }
+  }else if( n.getKind()==NOT ){
+    Assert( n[0].getKind()==FORALL );
   }
 }
 

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 63df56392899f017661dce94f1ab7122972f6200..5cf5a4c729d00e4bf87276e05f8f5387c0c1d06d 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -679,6 +679,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                 if( d_qe->addInstantiation( f, inst ) ){
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
+                  if( options::fmfOneInstPerRound() ){
+                    break;
+                  }
                 }else{
                   Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
                   //this can happen if evaluation is unknown
@@ -796,6 +799,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         if( d_qe->addInstantiation( f, inst ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
+          if( options::fmfOneInstPerRound() ){
+            break;
+          }
         }else{
           Trace("fmc-exh-debug") << ", failed.";
         }

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 123dc02b611e874228d598979be05ad0a07bb59f..53c6d9e2755b5c17b362a035ab380303077bddf7 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -393,17 +393,15 @@ void InstantiationEngine::debugSat( int reason ){
         }
       }
     }
+    if( options::recurseCbqi() && !options::preSkolemQuant() && d_setIncomplete ){
+      Debug("quantifiers-sat") << "Cannot conclude SAT with nested quantifiers in recursive strategy." << std::endl;
+      //TODO : only when existentials with inst constants
+      d_quantEngine->getOutputChannel().setIncomplete();
+    }
     //}
     Debug("quantifiers-sat") << "return SAT: Cbqi, no quantifier is active. " << std::endl;
-    //static bool setTrust = false;
-    //if( !setTrust ){
-    //  setTrust = true;
-    //  Notice() << "trust-";
-    //}
   }else if( reason==SAT_INST_STRATEGY ){
     Debug("quantifiers-sat") << "return SAT: No strategy chose to add an instantiation." << std::endl;
-    //Notice() << "sat ";
-    //Unimplemented();
   }
 }
 

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a16f46aceeb61501777db009eca1458d8c858466..53163cd5f71e4e68017967951e9b3a235bdf6651 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -266,7 +266,6 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 }
 
 void QuantifiersEngine::assertNode( Node f ){
-  Assert( f.getKind()==FORALL );
   d_model->assertQuantifier( f );
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->assertNode( f );