This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
attribute.cpp
attribute_internals.h
attribute_unique_id.h
+ buffered_proof_generator.cpp
+ buffered_proof_generator.h
emptyset.cpp
emptyset.h
expr_iomanip.cpp
--- /dev/null
+/********************* */
+/*! \file buffered_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Implementation of a proof generator for buffered proof steps
+ **/
+
+#include "expr/buffered_proof_generator.h"
+
+#include "expr/proof.h"
+
+namespace CVC4 {
+
+BufferedProofGenerator::BufferedProofGenerator(context::Context* c,
+ ProofNodeManager* pnm)
+ : ProofGenerator(), d_facts(c), d_pnm(pnm)
+{
+}
+
+bool BufferedProofGenerator::addStep(Node fact,
+ ProofStep ps,
+ CDPOverwrite opolicy)
+{
+ // check duplicates if we are not always overwriting
+ if (opolicy != CDPOverwrite::ALWAYS)
+ {
+ if (d_facts.find(fact) != d_facts.end())
+ {
+ // duplicate
+ return false;
+ }
+ Node symFact = CDProof::getSymmFact(fact);
+ if (!symFact.isNull())
+ {
+ if (d_facts.find(symFact) != d_facts.end())
+ {
+ // duplicate due to symmetry
+ return false;
+ }
+ }
+ }
+ // note that this replaces the value fact is mapped to if there is already one
+ d_facts.insert(fact, std::make_shared<ProofStep>(ps));
+ return true;
+}
+
+std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
+{
+ Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact
+ << std::endl;
+ NodeProofStepMap::iterator it = d_facts.find(fact);
+ if (it == d_facts.end())
+ {
+ Node symFact = CDProof::getSymmFact(fact);
+ if (symFact.isNull())
+ {
+ Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
+ Assert(false);
+ return nullptr;
+ }
+ it = d_facts.find(symFact);
+ if (it == d_facts.end())
+ {
+ Assert(false);
+ Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
+ return nullptr;
+ }
+ }
+ Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
+ CDProof cdp(d_pnm);
+ cdp.addStep(fact, *(*it).second);
+ return cdp.getProofFor(fact);
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file buffered_proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief A proof generator for buffered proof steps
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
+#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "expr/proof_step_buffer.h"
+
+namespace CVC4 {
+
+/**
+ * The proof generator for buffered steps. This class is a context-dependent
+ * mapping from formulas to proof steps. It does not generate ProofNodes until it
+ * is asked to provide a proof for a given fact.
+ */
+class BufferedProofGenerator : public ProofGenerator
+{
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
+ NodeProofStepMap;
+
+ public:
+ BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
+ ~BufferedProofGenerator() {}
+ /** add step
+ * Unless the overwrite policy is ALWAYS it does not replace previously
+ * registered steps (modulo (dis)equality symmetry).
+ */
+ bool addStep(Node fact,
+ ProofStep ps,
+ CDPOverwrite opolicy = CDPOverwrite::NEVER);
+ /** Get proof for. It is robust to (dis)equality symmetry. */
+ std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** identify */
+ std::string identify() const override { return "BufferedProofGenerator"; }
+
+ private:
+ /** maps expected to ProofStep */
+ NodeProofStepMap d_facts;
+ /** the proof node manager */
+ ProofNodeManager* d_pnm;
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
}
-
-ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
- ProofNodeManager* pnm)
- : ProofGenerator(), d_facts(c), d_pnm(pnm)
-{
-}
-
-bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps)
-{
- if (d_facts.find(fact) != d_facts.end())
- {
- // duplicate
- return false;
- }
- Node symFact = CDProof::getSymmFact(fact);
- if (!symFact.isNull())
- {
- if (d_facts.find(symFact) != d_facts.end())
- {
- // duplicate due to symmetry
- return false;
- }
- }
- d_facts.insert(fact, std::make_shared<ProofStep>(ps));
- return true;
-}
-
-std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor(
- Node fact)
-{
- Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
- << std::endl;
- NodeProofStepMap::iterator it = d_facts.find(fact);
- if (it == d_facts.end())
- {
- Node symFact = CDProof::getSymmFact(fact);
- if (symFact.isNull())
- {
- Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
- Assert(false);
- return nullptr;
- }
- it = d_facts.find(symFact);
- if (it == d_facts.end())
- {
- Assert(false);
- Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
- return nullptr;
- }
- }
- Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
- CDProof cdp(d_pnm);
- cdp.addStep(fact, *(*it).second);
- return cdp.getProofFor(fact);
-}
-
} // namespace eq
} // namespace theory
} // namespace CVC4
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
+#include "expr/buffered_proof_generator.h"
#include "expr/lazy_proof.h"
#include "expr/node.h"
#include "expr/proof_node.h"
#include "expr/proof_node_manager.h"
-#include "expr/proof_step_buffer.h"
#include "theory/eager_proof_generator.h"
#include "theory/uf/equality_engine.h"
TrustNode explain(Node conc);
private:
- /**
- * The default proof generator (for simple facts). This class is a context
- * dependent mapping from formulas to proof steps. It does not generate
- * ProofNode until it is asked to provide a proof for a given fact.
- */
- class FactProofGenerator : public ProofGenerator
- {
- typedef context::
- CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
- NodeProofStepMap;
-
- public:
- FactProofGenerator(context::Context* c, ProofNodeManager* pnm);
- ~FactProofGenerator() {}
- /** add step */
- bool addStep(Node fact, ProofStep ps);
- /** Get proof for */
- std::shared_ptr<ProofNode> getProofFor(Node f) override;
- /** identify */
- std::string identify() const override { return "FactProofGenerator"; }
-
- private:
- /** maps expected to ProofStep */
- NodeProofStepMap d_facts;
- /** the proof node manager */
- ProofNodeManager* d_pnm;
- };
/** Assert internal */
bool assertFactInternal(TNode pred, bool polarity, TNode reason);
/** holds */
/** Reference to the equality engine */
eq::EqualityEngine& d_ee;
/** The default proof generator (for simple facts) */
- FactProofGenerator d_factPg;
+ BufferedProofGenerator d_factPg;
/** common nodes */
Node d_true;
Node d_false;
projects / cvc5.git / commitdiff