Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization for non...

diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
index c46671c081e102014235db7b4cef197229177259..8eb19a24fefec87d90f32f0ae5ad4aadcc8ecbeb 100755 (executable)
--- a/contrib/run-script-smtcomp2015
+++ b/contrib/run-script-smtcomp2015
@@ -54,7 +54,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant
   trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality
   trywith 30 --inst-when=full --full-saturate-quant
-  trywith 30 --fmf-bound-int --macros-quant
+  #trywith 30 --fmf-bound-int --macros-quant   # recently bug fixed
   trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   trywith 30 --decision=justification-stoponly --full-saturate-quant
   # large runs 3min
@@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 60 --cbqi --no-cbqi-sat --full-saturate-quant
+  trywith 180 --cbqi --no-cbqi-sat --full-saturate-quant
   trywith 60 --full-saturate-quant
-  trywith 60 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
   trywith 180 --qcf-tconstraint --full-saturate-quant
-  trywith 240 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
-  finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant
+  finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
   ;;
 QF_AUFBV)
   trywith 600

diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions
index 3292e29fbe3e5c61accbd7579ea8d8634bf6658b..c4f9fc6cc07f2e887a70d9638143f4c1ddb9fa15 100755 (executable)
--- a/contrib/run-script-smtcomp2015-assertions
+++ b/contrib/run-script-smtcomp2015-assertions
@@ -74,10 +74,8 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
 LIA|LRA|NIA|NRA)
   trywith 30 --cbqi --no-cbqi-sat --full-saturate-quant
   trywith 30 --full-saturate-quant
-  trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
   trywith 30 --qcf-tconstraint --full-saturate-quant
-  trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
-  finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant
+  finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant
   ;;
 QF_AUFBV)
   trywith 30

diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental
index 9b8a0ba389d2413adf4f30a76558a7f3a9dde8d5..3480a8e3c6fb7471a8f5346ccbc82b27f3efc9c5 100755 (executable)
--- a/contrib/run-script-smtcomp2015-experimental
+++ b/contrib/run-script-smtcomp2015-experimental
@@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 60 --cbqi --full-saturate-quant
+  trywith 180 --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
+  finishwith --cbqi --cbqi-recurse --full-saturate-quant
   ;;
 QF_AUFBV)
   trywith 600

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9fe3a115de30ca4cf57388c8eef1a46a94b5d9e5..5d5bb93dcaeeb9083b44d9d2bd7bef40550d3265 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1480,7 +1480,13 @@ void SmtEngine::setDefaults() {
       options::conjectureGen.set( false );
     }
   }
-
+  //can't pre-skolemize nested quantifiers without UF theory
+  if( !d_logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant() ){
+    if( !options::preSkolemQuantNested.wasSetByUser() ){
+      options::preSkolemQuantNested.set( false );
+    }
+  } 
+  
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
     if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 0ba8008aaec8134366ff28b6478f6814cfb12270..2fd595a9f1c4624628104b51909e4df63b2f7085 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -372,6 +372,7 @@ Node BoundedIntegers::getNextDecisionRequest() {
       }
     }
   }
+  Trace("bound-int-dec-debug") << "No decision request." << std::endl;
   return Node::null();
 }
 

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 9910431579be7c96b22e7fd2e7f8dccd15231b13..0afdece82dcd7d093bd68804b4bf74ec6ecf8070 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1210,7 +1210,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
     if( polarity ){
-      if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){
+      if( options::preSkolemQuant() && options::preSkolemQuantNested() ){
         vector< Node > children;
         children.push_back( n[0] );
         //add children to current scope

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6a49980166cd43ee2288269b00dcc22d4c196c09..88aea6c752ccbb5db2bf81e7e08f54ab98d77ba1 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -770,6 +770,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   getOutputChannel().safePoint(options::quantifierStep());
 
   Assert( terms.size()==f[0].getNumChildren() );
+  Trace("inst-add-debug") << "For quantified formula " << f << "..." << std::endl;
   Trace("inst-add-debug") << "Add instantiation: ";
   for( unsigned i=0; i<terms.size(); i++ ){
     if( i>0 ) Trace("inst-add-debug") << ", ";

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 5580dc3d711e3ca7dd906230177b4731d2fe03b5..4ab8df72f3792b120c3ab17ceb682b0ac8f97ec0 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -370,7 +370,9 @@ bool RepSetIterator::isFinished(){
 }
 
 Node RepSetIterator::getTerm( int i ){
-  int index = d_index_order[i];
+  Trace("rsi-debug") << "rsi : get term " << i << ", index order = " << d_index_order[i] << std::endl;
+  //int index = d_index_order[i];
+  int index = i;
   if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
     TypeNode tn = d_types[index];
     Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );