Print only instantiations that are in the unsat core when --proof is enabled. Add option to minimize sygus solutions based on unsat core (disabled by default).

1 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 59fa3592d..da8233fc1 100644
--- 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);