From: Andrew Reynolds Date: Tue, 7 Dec 2021 22:40:40 +0000 (-0600) Subject: Add proof annotation option (#7750) X-Git-Tag: cvc5-1.0.0~710 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0226b383f8f70136843c7c2d21487e10a774f0f0;p=cvc5.git Add proof annotation option (#7750) Adds --proof-annotate which enables a useful stat in which we count the number of times a lemma with a given inference id appears in a final proof. This can be used to determine which lemma schemas are the most useful for showing a problem unsat. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 96de9afeb..de5ef27af 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -151,6 +151,8 @@ libcvc5_add_sources( printer/smt2/smt2_printer.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h + proof/annotation_proof_generator.cpp + proof/annotation_proof_generator.h proof/assumption_proof_generator.cpp proof/assumption_proof_generator.h proof/buffered_proof_generator.cpp @@ -681,6 +683,8 @@ libcvc5_add_sources( theory/incomplete_id.h theory/inference_id.cpp theory/inference_id.h + theory/inference_id_proof_annotator.cpp + theory/inference_id_proof_annotator.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h theory/logic_info.cpp diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 3eb32060e..373e080a1 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -91,6 +91,14 @@ name = "Proof" name = "dsl-rewrite" help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps." +[[option]] + name = "proofAnnotate" + category = "regular" + long = "proof-annotate" + type = "bool" + default = "false" + help = "add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof" + [[option]] name = "proofAletheResPivots" category = "regular" diff --git a/src/proof/annotation_proof_generator.cpp b/src/proof/annotation_proof_generator.cpp new file mode 100644 index 000000000..e9467276b --- /dev/null +++ b/src/proof/annotation_proof_generator.cpp @@ -0,0 +1,87 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of the annotation proof generator class. + */ + +#include "proof/annotation_proof_generator.h" + +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +AnnotationProofGenerator::AnnotationProofGenerator(ProofNodeManager* pnm, + context::Context* c, + std::string name) + : d_pnm(pnm), + d_name(name), + d_exps(c == nullptr ? &d_context : c), + d_proofs(c == nullptr ? &d_context : c) +{ +} + +void AnnotationProofGenerator::setExplanationFor(Node f, + ProofGenerator* pg, + Annotator* a) +{ + Assert(pg != nullptr); + d_exps[f] = std::pair(pg, a); +} + +std::shared_ptr AnnotationProofGenerator::getProofFor(Node f) +{ + // is the proof already cached? + NodeProofNodeMap::iterator it = d_proofs.find(f); + if (it != d_proofs.end()) + { + return (*it).second; + } + // make it into an actual proof now + NodeExpMap::iterator itx = d_exps.find(f); + if (itx == d_exps.end()) + { + return nullptr; + } + // get the proof from the proof generator + std::shared_ptr pf = itx->second.first->getProofFor(f); + if (pf == nullptr) + { + d_proofs[f] = nullptr; + return nullptr; + } + // now anntoate it if an annotator was provided + std::shared_ptr pfa = pf; + if (itx->second.second != nullptr) + { + pfa = itx->second.second->annotate(pf); + } + d_proofs[f] = pfa; + return pfa; +} + +TrustNode AnnotationProofGenerator::transform(const TrustNode& trn, + Annotator* a) +{ + setExplanationFor(trn.getProven(), trn.getGenerator(), a); + return TrustNode::mkReplaceGenTrustNode(trn, this); +} + +bool AnnotationProofGenerator::hasProofFor(Node f) +{ + return d_exps.find(f) != d_exps.end(); +} + +std::string AnnotationProofGenerator::identify() const { return d_name; } + +} // namespace cvc5 diff --git a/src/proof/annotation_proof_generator.h b/src/proof/annotation_proof_generator.h new file mode 100644 index 000000000..fb737dc44 --- /dev/null +++ b/src/proof/annotation_proof_generator.h @@ -0,0 +1,102 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The annotation proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H +#define CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" + +namespace cvc5 { + +class ProofNodeManager; + +/** + * Base class for annotators. An annotator is a utility that implements a + * simple transformation on proofs: `annotate` below. + */ +class Annotator +{ + public: + Annotator() {} + virtual ~Annotator() {} + /** + * Annotate the proof node. This must return a proof node that concludes the + * same thing as p. + */ + virtual std::shared_ptr annotate(std::shared_ptr p) = 0; +}; + +/** + * Annotation proof generator, used to "wrap" proofs of other proof generators + * via the annotate method above. + */ +class AnnotationProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap> + NodeExpMap; + typedef context::CDHashMap> NodeProofNodeMap; + + public: + AnnotationProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "AnnotationProofGenerator"); + ~AnnotationProofGenerator() {} + /** Get the proof for formula f. */ + std::shared_ptr getProofFor(Node f) override; + /** Can we give the proof for formula f? */ + bool hasProofFor(Node f) override; + /** + * Set explanation for fact f, called when pg has a proof for f. + * + * @param f The fact proven by pg, + * @param pg The proof generator that can prove f. + * @param a The annotator that will annotate the proof of f, if necessary. + */ + void setExplanationFor(Node f, ProofGenerator* pg, Annotator* a); + /** + * Transform trust node, will be annotated by the given annotator. + */ + TrustNode transform(const TrustNode& trn, Annotator* a); + /** identify */ + std::string identify() const override; + + protected: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** Name identifier */ + std::string d_name; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** + * A context-dependent map from formulas to a generator + annotation + * pair, which will be used to generate the proof of formulas if asked. + * We use the context provided to this class or otherwise d_context above. + */ + NodeExpMap d_exps; + /** + * A context-dependent map from formulas to the proof nodes we have + * returned in calls to getProofFor. + */ + NodeProofNodeMap d_proofs; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H */ diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp index e8871af34..910af3d90 100644 --- a/src/proof/proof_node_to_sexpr.cpp +++ b/src/proof/proof_node_to_sexpr.cpp @@ -297,6 +297,12 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat( } } break; + case PfRule::ANNOTATION: + if (i == 0) + { + return ArgFormat::INFERENCE_ID; + } + break; default: break; } return ArgFormat::DEFAULT; diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index c82928dc5..9bd714161 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -33,6 +33,7 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; + case PfRule::ANNOTATION: return "ANNOTATION"; case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Trusted rules case PfRule::THEORY_LEMMA: return "THEORY_LEMMA"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index d9e92fa92..eaa92c02c 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -185,6 +185,14 @@ enum class PfRule : uint32_t // where F' and G' are the result of each side of the equation above. Here, // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. MACRO_SR_PRED_TRANSFORM, + // ======== Annotation + // Children: (P1:F) + // Arguments: (a1 ... an) + // ---------------------------------------- + // Conclusion: F + // The terms a1 ... an can be anything used to annotate the proof node, one + // example is where a1 is a theory::InferenceId. + ANNOTATION, //================================================= Processing rules // ======== Remove Term Formulas Axiom // Children: none diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 93b4cae19..484f0dd73 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -34,6 +34,9 @@ ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm) d_instRuleIds( smtStatisticsRegistry().registerHistogram( "finalProof::instRuleId")), + d_annotationRuleIds( + smtStatisticsRegistry().registerHistogram( + "finalProof::annotationRuleId")), d_totalRuleCount( smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")), d_minPedanticLevel( @@ -96,6 +99,33 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, } } } + else if (r == PfRule::ANNOTATION) + { + // we currently assume the annotation is a single inference id + const std::vector& args = pn->getArguments(); + if (args.size() > 0) + { + InferenceId id; + if (getInferenceId(args[0], id)) + { + d_annotationRuleIds << id; + } + } + } + // print for debugging + if (Trace.isOn("final-pf-hole")) + { + // currently only track theory rewrites + if (r == PfRule::THEORY_REWRITE) + { + const std::vector& args = pn->getArguments(); + Node eq = args[0]; + TheoryId tid = THEORY_BUILTIN; + builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid); + Trace("final-pf-hole") << "hole " << r << " " << tid << " : " << eq[0] + << " ---> " << eq[1] << std::endl; + } + } return false; } diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h index 88b8e20ef..a1e6b1f69 100644 --- a/src/smt/proof_final_callback.h +++ b/src/smt/proof_final_callback.h @@ -54,6 +54,11 @@ class ProofFinalCallback : public ProofNodeUpdaterCallback * marked with the given inference id. */ HistogramStat d_instRuleIds; + /** + * Counts number of postprocessed proof nodes of rule ANNOTATION that were + * marked with the given inference id. + */ + HistogramStat d_annotationRuleIds; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 9c05407b7..9d11b9f7d 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -43,6 +43,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); pc->registerChecker(PfRule::THEORY_REWRITE, this); + pc->registerChecker(PfRule::ANNOTATION, this); pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); // trusted rules pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1); @@ -381,6 +382,11 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args[0].getType().isBoolean()); return args[0]; } + else if (id == PfRule::ANNOTATION) + { + Assert(children.size() == 1); + return children[0]; + } // no rule return Node::null(); diff --git a/src/theory/inference_id_proof_annotator.cpp b/src/theory/inference_id_proof_annotator.cpp new file mode 100644 index 000000000..5af98c4bf --- /dev/null +++ b/src/theory/inference_id_proof_annotator.cpp @@ -0,0 +1,55 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The inference id annotator class. + */ + +#include "theory/inference_id_proof_annotator.h" + +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { +namespace theory { + +InferenceIdProofAnnotator::InferenceIdProofAnnotator(ProofNodeManager* pnm, + context::Context* c) + : d_pnm(pnm), d_ids(c), d_list(c) +{ +} +void InferenceIdProofAnnotator::setAnnotation(Node f, InferenceId id) +{ + d_ids[f] = id; +} + +std::shared_ptr InferenceIdProofAnnotator::annotate( + std::shared_ptr p) +{ + Node f = p->getResult(); + NodeInferenceIdMap::iterator it = d_ids.find(f); + if (it != d_ids.end()) + { + std::vector pfArgs; + pfArgs.push_back(mkInferenceIdNode(it->second)); + std::shared_ptr pa = + d_pnm->mkNode(PfRule::ANNOTATION, {p}, pfArgs); + // for now, do a double annotation to make stats accurate + std::shared_ptr paf = + d_pnm->mkNode(PfRule::ANNOTATION, {pa}, {}); + d_list.push_back(paf); + return paf; + } + return p; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/inference_id_proof_annotator.h b/src/theory/inference_id_proof_annotator.h new file mode 100644 index 000000000..8346370f1 --- /dev/null +++ b/src/theory/inference_id_proof_annotator.h @@ -0,0 +1,64 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The inference id annotator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__INFERENCE_ID_PROOF_ANNOTATOR_H +#define CVC5__THEORY__INFERENCE_ID_PROOF_ANNOTATOR_H + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/node.h" +#include "proof/annotation_proof_generator.h" +#include "theory/inference_id.h" + +namespace cvc5 { +namespace theory { + +/** A class that tracks formulas to inference id annotations */ +class InferenceIdProofAnnotator : public Annotator +{ + typedef context::CDHashMap NodeInferenceIdMap; + typedef context::CDList> ProofNodeList; + + public: + InferenceIdProofAnnotator(ProofNodeManager* pnm, context::Context* c); + /** Set annotation, that formula f should be annotated by id */ + void setAnnotation(Node f, InferenceId id); + /** + * Annotate the proof node with the appropriate inference ID. Given proof + * P proving F that was generated as a lemma with inference id `i`, this + * returns (ANNOTATION (ANNOTATION P : args i)). The outer ANNOTATION is + * used since commonly a proof node is "linked" into another, where its + * children and rule are copied into another. Using ANNOTATION (with no + * arguments) ensures the top-most ANNOTATION may be linked/copied + * multiple times; however its child (which counts `i`) will only appear + * once in the final proof. + */ + std::shared_ptr annotate(std::shared_ptr p) override; + + private: + /** The proof node manager of the theory */ + ProofNodeManager* d_pnm; + /** The inference id for each formula */ + NodeInferenceIdMap d_ids; + /** Ensure we keep proof nodes alive */ + ProofNodeList d_list; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__INFERENCE_ID_PROOF_ANNOTATOR_H */ diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 4ed01b618..fda6d0881 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,7 +15,13 @@ #include "theory/theory_inference_manager.h" +#include "options/proof_options.h" +#include "proof/annotation_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine_scope.h" +#include "theory/builtin/proof_checker.h" +#include "theory/inference_id_proof_annotator.h" #include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -56,6 +62,20 @@ TheoryInferenceManager::TheoryInferenceManager(Env& env, // don't add true lemma Node truen = NodeManager::currentNM()->mkConst(true); d_lemmasSent.insert(truen); + + if (isProofEnabled()) + { + context::UserContext* u = userContext(); + ProofNodeManager* pnm = env.getProofNodeManager(); + d_defaultPg.reset( + new EagerProofGenerator(pnm, u, statsName + "EagerProofGenerator")); + if (options().proof.proofAnnotate) + { + d_iipa.reset(new InferenceIdProofAnnotator(pnm, u)); + d_apg.reset(new AnnotationProofGenerator( + pnm, u, statsName + "AnnotationProofGenerator")); + } + } } TheoryInferenceManager::~TheoryInferenceManager() @@ -127,6 +147,11 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) resourceManager()->spendResource(id); Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" << std::endl; + // annotate if the annotation proof generator is active + if (d_apg != nullptr) + { + tconf = annotateId(tconf, id); + } d_out.trustedConflict(tconf); ++d_numConflicts; } @@ -261,7 +286,16 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, // shouldn't send trivially true or false lemmas Assert(!rewrite(tlem.getProven()).isConst()); d_numCurrentLemmas++; - d_out.trustedLemma(tlem, p); + // annotate if the annotation proof generator is active + if (d_apg != nullptr) + { + TrustNode tlema = annotateId(tlem, id); + d_out.trustedLemma(tlema, p); + } + else + { + d_out.trustedLemma(tlem, p); + } return true; } @@ -544,6 +578,24 @@ bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p) return true; } +TrustNode TheoryInferenceManager::annotateId(const TrustNode& trn, + InferenceId id) +{ + Assert(d_iipa != nullptr && d_apg != nullptr); + Node lemma = trn.getProven(); + TrustNode trna = trn; + // ensure we have a proof generator, make trusted theory lemma if not + if (trn.getGenerator() == nullptr) + { + Node tidn = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(d_theory.getId()); + trna = d_defaultPg->mkTrustNode( + lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn}); + } + d_iipa->setAnnotation(lemma, id); + return d_apg->transform(trna, d_iipa.get()); +} + DecisionManager* TheoryInferenceManager::getDecisionManager() { return d_decManager; diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index d7334d0e6..c626bbef9 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -32,12 +32,15 @@ namespace cvc5 { class ProofNodeManager; +class AnnotationProofGenerator; +class EagerProofGenerator; namespace theory { class Theory; class TheoryState; class DecisionManager; +class InferenceIdProofAnnotator; namespace eq { class EqualityEngine; class ProofEqEngine; @@ -426,6 +429,11 @@ class TheoryInferenceManager : protected EnvObj * override this method to take the lemma property into account as needed. */ virtual bool cacheLemma(TNode lem, LemmaProperty p); + /** + * Return the trust node that is equivalent to trn, but its proof (if asked + * for) will be wrapped in (ANNOTATE ... :args id). + */ + TrustNode annotateId(const TrustNode& trn, InferenceId id); /** The theory object */ Theory& d_theory; /** Reference to the state of theory */ @@ -440,6 +448,12 @@ class TheoryInferenceManager : protected EnvObj eq::ProofEqEngine* d_pfee; /** The proof equality engine we allocated */ std::unique_ptr d_pfeeAlloc; + /** Proof generator for trusted THEORY_LEMMA steps */ + std::unique_ptr d_defaultPg; + /** The inference id proof annotator */ + std::unique_ptr d_iipa; + /** The annotation proof generator */ + std::unique_ptr d_apg; /** Whether this manager caches lemmas */ bool d_cacheLemmas; /**