From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Nov 2016 15:52:52 +0000 (-0600)
Subject: Refactoring related to track instantiation option.
X-Git-Tag: cvc5-1.0.0~5969
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c12cfca2bdd44b6cda5c61a764ae6aee150c384b;p=cvc5.git

Refactoring related to track instantiation option.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 3269b7574..f6b6e2177 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -342,7 +342,7 @@ option quantEqualityEngine --quant-ee bool :default false
  
 ### proof options
 
-option trackInstLemmas --track-inst-lemmas bool :default true
-  when proof is enabled, track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)
+option trackInstLemmas --track-inst-lemmas bool :read-write :default false
+  track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)
  
 endmodule
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5fc96aa6e..f5b769984 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1723,6 +1723,10 @@ void SmtEngine::setDefaults() {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
     options::cbqi.set(false);
   }
+  //track instantiations?
+  if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){
+    options::trackInstLemmas.set( true );
+  }
 
   if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) || 
       ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) {
@@ -5089,6 +5093,8 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   }
   if( d_theoryEngine ){
     d_theoryEngine->printInstantiations( out );
+  }else{
+    Assert( false );
   }
   if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
     out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
@@ -5099,6 +5105,8 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
   SmtScope smts(this);
   if( d_theoryEngine ){
     d_theoryEngine->printSynthSolution( out );
+  }else{
+    Assert( false );
   }
 }
 
@@ -5155,6 +5163,8 @@ void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
     for( unsigned i=0; i<qs_n.size(); i++ ){
       qs.push_back( qs_n[i].toExpr() );
     }
+  }else{
+    Assert( false );
   }
 }
 
@@ -5166,11 +5176,14 @@ void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
     for( unsigned i=0; i<insts_n.size(); i++ ){
       insts.push_back( insts_n[i].toExpr() );
     }
+  }else{
+    Assert( false );
   }
 }
 
 void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
   SmtScope smts(this);
+  Assert(options::trackInstLemmas());
   if( d_theoryEngine ){
     std::vector< std::vector< Node > > tvecs_n;
     d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
@@ -5181,6 +5194,8 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E
       }
       tvecs.push_back( tvec );
     }
+  }else{
+    Assert( false );
   }
 }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 22bfa948f..3168a78e2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -138,8 +138,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_fs = NULL;
   d_rel_dom = NULL;
   d_builder = NULL;
-  
-  d_trackInstLemmas = options::cbqiNestedQE() || ( options::proof() && options::trackInstLemmas() );
 
   d_total_inst_count_debug = 0;
   //allow theory combination to go first, once initially
@@ -1221,7 +1219,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
         }
       }
     }
-    if( d_trackInstLemmas ){
+    if( options::trackInstLemmas() ){
       bool recorded;
       if( options::incrementalSolving() ){
         recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem );
@@ -1409,7 +1407,7 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
 }
 
 void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
-  if( d_trackInstLemmas ){
+  if( options::trackInstLemmas() ){
     if( options::incrementalSolving() ){
       for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
         it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec );
@@ -1433,7 +1431,7 @@ void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems,
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   bool useUnsatCore = false;
   std::vector< Node > active_lemmas;
-  if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){
+  if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
     useUnsatCore = true;
   }
 
@@ -1497,7 +1495,7 @@ void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >&
 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
   bool useUnsatCore = false;
   std::vector< Node > active_lemmas;
-  if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){
+  if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
     useUnsatCore = true;
   }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fc2b27e02..43beec6e3 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -147,9 +147,6 @@ private:
   quantifiers::QuantAntiSkolem * d_anti_skolem;
   /** quantifiers instantiation propagtor */
   quantifiers::InstPropagator * d_inst_prop;
-private:
-  /** whether we are tracking instantiation lemmas */
-  bool d_trackInstLemmas;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,