Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.

4 files changed, 36 insertions, 13 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 86b0faaf6..74cdee0b7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() {
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
     }
-    //for finite model finding
     if( ! options::instWhenMode.wasSetByUser()){
       //instantiate only on last call
       if( options::eMatching() ){
@@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() {
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
+    if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+      if( !options::preSkolemQuant.wasSetByUser() ){
+        options::preSkolemQuant.set( true );
+      }
+      if( !options::fmfOneInstPerRound.wasSetByUser() ){
+        options::fmfOneInstPerRound.set( true );
+      }
+    }
   }
   
   //implied options...
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index dad173ff5..a428633cc 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas
 # Whether to NNF quantifier bodies
-option nnfQuant --nnf-quant bool :default false
+option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
 
 option clauseSplit --clause-split bool :default false
@@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
 
-option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
 option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
@@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
-option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
  only add one instantiation per quantifier per round for mbqi
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 08fcf319d..e9f85d454 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -29,17 +29,17 @@ namespace quantifiers {
 static const std::string instWhenHelp = "\
 Modes currently supported by the --inst-when option:\n\
 \n\
-full (default)\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+  call.  In other words, interleave instantiation and theory combination.\n\
+\n\
+full\n\
 + Run instantiation round at full effort, before theory combination.\n\
 \n\
 full-delay \n\
 + Run instantiation round at full effort, before theory combination, after\n\
   all other theories have finished.\n\
 \n\
-full-last-call\n\
-+ Alternate running instantiation rounds at full effort and last\n\
-  call.  In other words, interleave instantiation and theory combination.\n\
-\n\
 last-call\n\
 + Run instantiation at last call effort, after theory combination and\n\
   and theories report sat.\n\
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0ed175393..1e6ec3a02 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else{
       std::vector< Node > children;
       Kind k = body[0].getKind();
+      
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
+        k = body[0].getKind()==AND ? OR : AND;
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          children.push_back( computeNNF( body[0][i].notNode() ) );
+          Node nc = computeNNF( body[0][i].notNode() );
+          if( nc.getKind()==k ){
+            for( unsigned j=0; j<nc.getNumChildren(); j++ ){
+              children.push_back( nc[j] );
+            }
+          }else{
+            children.push_back( nc );
+          }
         }
-        k = body[0].getKind()==AND ? OR : AND;
       }else if( body[0].getKind()==IFF ){
         for( int i=0; i<2; i++ ){
           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
@@ -335,10 +343,18 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }else{
     std::vector< Node > children;
     bool childrenChanged = false;
+    bool isAssoc = body.getKind()==AND || body.getKind()==OR;
     for( int i=0; i<(int)body.getNumChildren(); i++ ){
       Node nc = computeNNF( body[i] );
-      children.push_back( nc );
-      childrenChanged = childrenChanged || nc!=body[i];
+      if( isAssoc && nc.getKind()==body.getKind() ){
+        for( unsigned j=0; j<nc.getNumChildren(); j++ ){
+          children.push_back( nc[j] );
+        }
+        childrenChanged = true;
+      }else{
+        children.push_back( nc );
+        childrenChanged = childrenChanged || nc!=body[i];
+      }
     }
     if( childrenChanged ){
       return NodeManager::currentNM()->mkNode( body.getKind(), children );