diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-12 13:06:03 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-12 13:06:03 -0600 |
| commit | 87e0b503340957a62d8302973f676476495f6c72 (patch) | |
| tree | 4aa48d882d80081fbbc39291f63d4a5afdd8d06a /src/smt/smt_engine.cpp | |
| parent | 8b4c45340a74a8e2419667d403cd1fde9c7664fd (diff) | |
(proof-new) Miscellaneous sync to master (#6129)
Towards having proofs working on master.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 16 |
1 files changed, 15 insertions, 1 deletions
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 { |