Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms.

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 81771c374300b2227eb089808e7c777ca8c90c7f..8958034df0d4ed553351c5c57e0cf6bd752bae39 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -467,12 +467,13 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
   }else{
     //first, try from relevant domain
     RelevantDomain * rd = d_quantEngine->getRelevantDomain();
-    for( unsigned r=0; r<2; r++ ){
-      if( rd || r==1 ){
+    unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+    for( unsigned r=rstart; r<2; r++ ){
+      if( rd || r>0 ){
         if( r==0 ){
           Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
         }else{
-          Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+          Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
         }
         rd->compute();
         unsigned final_max_i = 0;
@@ -550,6 +551,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         }
       }
       if( r==0 ){
+        //complete guess
         if( d_guessed.find( f )==d_guessed.end() ){
           Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
           d_guessed[f] = true;
@@ -561,6 +563,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         }
       }
     }
+    //term enumerator?
   }
   return STATUS_UNKNOWN;
 }

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ce7f01328e743a64ecf42712a3fb46cc11c1a0c9..391abe9eba90bb1791cc6f0e16af49a0a8120df3 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -115,6 +115,8 @@ option eagerInstQuant --eager-inst-quant bool :default false
 
 option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
+option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
+ whether to use relevant domain first for full saturation instantiation strategy
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 1898664944b5862ce20bebd0a16d82819799d279..cc8ae4db04e809a536ff9cac23b6c5ae4ad5b738 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -129,11 +129,12 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
   bool rec = false;
   if( d_processed.find( n )==d_processed.end() ){
     d_processed.insert(n);
-    d_type_map[ n.getType() ].push_back( n );
-    //if this is an atomic trigger, consider adding it
-    //Call the children?
-    if( inst::Trigger::isAtomicTrigger( n ) ){
-      if( !TermDb::hasInstConstAttr(n) ){
+    if( !TermDb::hasInstConstAttr(n) ){
+      Trace("term-db-debug") << "register term : " << n << std::endl;
+      d_type_map[ n.getType() ].push_back( n );
+      //if this is an atomic trigger, consider adding it
+      //Call the children?
+      if( inst::Trigger::isAtomicTrigger( n ) ){
         Trace("term-db") << "register term in db " << n << std::endl;
         Node op = getOperator( n );
         /*
@@ -166,7 +167,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
     d_iclosure_processed.insert( n );
     rec = true;
   }
-  if( rec ){
+  if( rec && n.getKind()!=FORALL ){
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       addTerm( n[i], added, withinQuant, withinInstClosure );
     }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 347aa83c46a02f1b2f99ff5679618016cd0c7126..9f8f0d6cf53d2804fbee73eb340a62775adce10a 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -304,6 +304,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
+      Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
       Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
     if( Trace.isOn("quant-engine-ee") ){
@@ -536,6 +537,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
       for( int i=0; i<(int)d_modules.size(); i++ ){
         d_modules[i]->assertNode( f );
       }
+      addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
     }
   }
 }