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.
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
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
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"
--- /dev/null
+/******************************************************************************
+ * 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<ProofGenerator*, Annotator*>(pg, a);
+}
+
+std::shared_ptr<ProofNode> 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<ProofNode> 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<ProofNode> 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
--- /dev/null
+/******************************************************************************
+ * 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<ProofNode> annotate(std::shared_ptr<ProofNode> 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<Node, std::pair<ProofGenerator*, Annotator*>>
+ NodeExpMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
+
+ public:
+ AnnotationProofGenerator(ProofNodeManager* pnm,
+ context::Context* c = nullptr,
+ std::string name = "AnnotationProofGenerator");
+ ~AnnotationProofGenerator() {}
+ /** Get the proof for formula f. */
+ std::shared_ptr<ProofNode> 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 */
}
}
break;
+ case PfRule::ANNOTATION:
+ if (i == 0)
+ {
+ return ArgFormat::INFERENCE_ID;
+ }
+ break;
default: break;
}
return ArgFormat::DEFAULT;
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";
// 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
d_instRuleIds(
smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
"finalProof::instRuleId")),
+ d_annotationRuleIds(
+ smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
+ "finalProof::annotationRuleId")),
d_totalRuleCount(
smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
d_minPedanticLevel(
}
}
}
+ else if (r == PfRule::ANNOTATION)
+ {
+ // we currently assume the annotation is a single inference id
+ const std::vector<Node>& 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<Node>& 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;
}
* marked with the given inference id.
*/
HistogramStat<theory::InferenceId> d_instRuleIds;
+ /**
+ * Counts number of postprocessed proof nodes of rule ANNOTATION that were
+ * marked with the given inference id.
+ */
+ HistogramStat<theory::InferenceId> d_annotationRuleIds;
/** Total number of postprocessed rule applications */
IntStat d_totalRuleCount;
/** The minimum pedantic level of any rule encountered */
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);
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();
--- /dev/null
+/******************************************************************************
+ * 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<ProofNode> InferenceIdProofAnnotator::annotate(
+ std::shared_ptr<ProofNode> p)
+{
+ Node f = p->getResult();
+ NodeInferenceIdMap::iterator it = d_ids.find(f);
+ if (it != d_ids.end())
+ {
+ std::vector<Node> pfArgs;
+ pfArgs.push_back(mkInferenceIdNode(it->second));
+ std::shared_ptr<ProofNode> pa =
+ d_pnm->mkNode(PfRule::ANNOTATION, {p}, pfArgs);
+ // for now, do a double annotation to make stats accurate
+ std::shared_ptr<ProofNode> paf =
+ d_pnm->mkNode(PfRule::ANNOTATION, {pa}, {});
+ d_list.push_back(paf);
+ return paf;
+ }
+ return p;
+}
+
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * 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<Node, InferenceId> NodeInferenceIdMap;
+ typedef context::CDList<std::shared_ptr<ProofNode>> 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<ProofNode> annotate(std::shared_ptr<ProofNode> 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 */
#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"
// 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()
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;
}
// 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;
}
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;
namespace cvc5 {
class ProofNodeManager;
+class AnnotationProofGenerator;
+class EagerProofGenerator;
namespace theory {
class Theory;
class TheoryState;
class DecisionManager;
+class InferenceIdProofAnnotator;
namespace eq {
class EqualityEngine;
class ProofEqEngine;
* 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 */
eq::ProofEqEngine* d_pfee;
/** The proof equality engine we allocated */
std::unique_ptr<eq::ProofEqEngine> d_pfeeAlloc;
+ /** Proof generator for trusted THEORY_LEMMA steps */
+ std::unique_ptr<EagerProofGenerator> d_defaultPg;
+ /** The inference id proof annotator */
+ std::unique_ptr<InferenceIdProofAnnotator> d_iipa;
+ /** The annotation proof generator */
+ std::unique_ptr<AnnotationProofGenerator> d_apg;
/** Whether this manager caches lemmas */
bool d_cacheLemmas;
/**
projects / cvc5.git / commitdiff