Print only instantiations that are in the unsat core when --proof is enabled. Add...

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 0a94ad890235748ca3631feff5dbc5ede4415b47..37178510dcf9b3ae86ee1227b29c0c2a86adfe29 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -242,6 +242,8 @@ option cegqiSingleInvPartial --cegqi-si-partial bool :default false
   combined techniques for synthesis conjectures that are partially single invocation 
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSolMinCore --cegqi-si-sol-min-core bool :default false
+  minimize solutions for single invocation conjectures based on unsat core
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index facd7bd2e2411886a87bf10dedc35f25e0375c7d..3f781774de6a6762751ad91527885387153f13bc 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -755,13 +755,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
     bool useUnsatCore = false;
     std::vector< Node > active_lemmas;
-    /*  TODO?
     //minimize based on unsat core, if possible
-    std::vector< Node > active_lemmas;
-    if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){
+    if( options::cegqiSolMinCore() && d_qe->getUnsatCoreLemmas( active_lemmas ) ){
       useUnsatCore = true;
     } 
-    */
     Assert( d_lemmas_produced.size()==d_inst.size() );
     std::vector< unsigned > indices;
     for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 59fa3592dbe975951085039424109fca36c77ef8..da8233fc120f33f42fe18add291ae940adf8cc3a 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1286,10 +1286,11 @@ void QuantifiersEngine::flushLemmas(){
 }
 
 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
-  //TODO: only if unsat core available
+  //only if unsat core available
   bool isUnsatCoreAvailable = false;
-  //if( options::proof() ){
-  //}
+  if( options::proof() ){
+    isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable();
+  }
   if( isUnsatCoreAvailable ){
     Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl;
     ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas);