From 87e0b503340957a62d8302973f676476495f6c72 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 12 Mar 2021 13:06:03 -0600
Subject: (proof-new) Miscellaneous sync to master (#6129)

Towards having proofs working on master.
---
 src/smt/smt_engine.cpp | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'src/smt/smt_engine.cpp')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 94e53a093..3fdf67ed7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1523,6 +1523,19 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
+void SmtEngine::getRelevantInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+  Assert(d_state->getMode() == SmtMode::UNSAT);
+  // generate with new proofs
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
+      pe->getProof(), *d_asserts, *d_definedFunctions);
+  d_ucManager->getRelevantInstantiations(pfn, insts);
+}
+
 std::string SmtEngine::getProof()
 {
   Trace("smt") << "SMT getProof()\n";
@@ -1636,7 +1649,8 @@ void SmtEngine::getInstantiationTermVectors(
   finishInit();
   if (options::proof() && getSmtMode() == SmtMode::UNSAT)
   {
-    // TODO (project #37): minimize instantiations based on proof manager
+    // minimize instantiations based on proof manager
+    getRelevantInstantiationTermVectors(insts);
   }
   else
   {
-- 
cgit v1.2.3