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 | |
parent | 8b4c45340a74a8e2419667d403cd1fde9c7664fd (diff) |
(proof-new) Miscellaneous sync to master (#6129)
Towards having proofs working on master.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/proof_post_processor.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 16 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 13 |
3 files changed, 28 insertions, 3 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index bc701ebc8..ff437e7e6 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -997,7 +997,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp) { - Node tw = SkolemManager::getWitnessForm(t); + Node tw = SkolemManager::getOriginalForm(t); Node eq = t.eqNode(tw); if (t == tw) { 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 { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 94c11be5b..56f3ffbb8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -527,7 +527,12 @@ class CVC4_PUBLIC SmtEngine */ std::vector<Node> getValues(const std::vector<Node>& exprs); - /** Print all instantiations made by the quantifiers module. */ + /** print instantiations + * + * Print all instantiations for all quantified formulas on out, + * returns true if at least one instantiation was printed. The type of output + * (list, num, etc.) is determined by printInstMode. + */ void printInstantiations(std::ostream& out); /** * Print the current proof. This method should be called after an UNSAT @@ -665,6 +670,12 @@ class CVC4_PUBLIC SmtEngine void getInstantiationTermVectors(Node q, std::vector<std::vector<Node>>& tvecs); /** + * As above but only the instantiations that were relevant for the + * refutation. + */ + void getRelevantInstantiationTermVectors( + std::map<Node, std::vector<std::vector<Node>>>& insts); + /** * Get instantiation term vectors, which maps each instantiated quantified * formula to the list of instantiations for that quantified formula. This * list is minimized if proofs are enabled, and this call is immediately |