diff options
| -rw-r--r-- | src/expr/proof_checker.h | 4 | ||||
| -rw-r--r-- | src/expr/term_conversion_proof_generator.h | 9 | ||||
| -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 |
5 files changed, 33 insertions, 11 deletions
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index a14247dce..21ffd63b8 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -148,8 +148,8 @@ class ProofChecker Node checkDebug(PfRule id, const std::vector<Node>& cchildren, const std::vector<Node>& args, - Node expected, - const char* traceTag); + Node expected = Node::null(), + const char* traceTag = ""); /** Indicate that psc is the checker for proof rule id */ void registerChecker(PfRule id, ProofRuleChecker* psc); /** diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 5996cd747..acff2ded1 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -80,12 +80,9 @@ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); * [***] This class traverses the left hand side of a given equality-to-prove * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite * steps to obtain its rewritten form. To do so, it applies any available - * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite - * (post-order traversal). It thus does not require the user of this class to - * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during - * addRewriteStep. In particular, notice that in the above example, we realize - * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then - * ending with f(a)=f(b). + * rewrite step at pre-rewrite (pre-order traversal) and post-rewrite + * (post-order traversal) based on whether the user specified pre-rewrite or a + * post-rewrite during addRewriteStep. * * This class may additionally be used for term-context-sensitive rewrite * systems. An example is the term formula removal pass which rewrites 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 |