proof/sat_proof_implementation.h
proof/unsat_core.cpp
proof/unsat_core.h
+ prop/bv_sat_solver_notify.h
prop/bvminisat/bvminisat.cpp
prop/bvminisat/bvminisat.h
prop/bvminisat/core/Dimacs.h
prop/minisat/simp/SimpSolver.cc
prop/minisat/simp/SimpSolver.h
prop/minisat/utils/Options.h
+ prop/proof_post_processor.cpp
+ prop/proof_post_processor.h
prop/prop_engine.cpp
prop/prop_engine.h
+ prop/prop_proof_manager.cpp
+ prop/prop_proof_manager.h
prop/registrar.h
prop/sat_solver.h
- prop/sat_solver_factory.cpp
- prop/sat_solver_factory.h
- prop/bv_sat_solver_notify.h
- prop/proof_post_processor.cpp
- prop/proof_post_processor.h
prop/sat_proof_manager.cpp
prop/sat_proof_manager.h
+ prop/sat_solver_factory.cpp
+ prop/sat_solver_factory.h
prop/sat_solver_types.cpp
prop/sat_solver_types.h
prop/theory_proxy.cpp
--- /dev/null
+/********************* */
+/*! \file prop_proof_manager
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** 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 the proof manager for the PropPfManager
+ **/
+
+#include "prop/prop_proof_manager.h"
+
+#include "expr/proof_node_algorithm.h"
+
+namespace CVC4 {
+namespace prop {
+
+PropPfManager::PropPfManager(context::UserContext* userContext,
+ ProofNodeManager* pnm,
+ SatProofManager* satPM,
+ ProofCnfStream* cnfProof)
+ : d_pnm(pnm),
+ d_pfpp(new ProofPostproccess(pnm, cnfProof)),
+ d_satPM(satPM),
+ d_assertions(userContext)
+{
+ // add trivial assumption. This is so that we can check the that the prop
+ // engine's proof is closed, as the SAT solver's refutation proof may use True
+ // as an assumption even when True is not given as an assumption. An example
+ // is when a propagated literal has an empty explanation (i.e., it is a valid
+ // literal), which leads to adding True as its explanation, since for creating
+ // a learned clause we need at least two literals.
+ d_assertions.push_back(NodeManager::currentNM()->mkConst(true));
+}
+
+void PropPfManager::registerAssertion(Node assertion)
+{
+ d_assertions.push_back(assertion);
+}
+
+void PropPfManager::checkProof(context::CDList<Node>* assertions)
+{
+ Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
+ "proof of false is closed\n";
+ std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+ Assert(conflictProof);
+ // connect it with CNF proof
+ d_pfpp->process(conflictProof);
+ // add given assertions d_assertions
+ for (const Node& assertion : *assertions)
+ {
+ d_assertions.push_back(assertion);
+ }
+ std::vector<Node> avec{d_assertions.begin(), d_assertions.end()};
+ pfnEnsureClosedWrt(
+ conflictProof.get(), avec, "sat-proof", "PropPfManager::checkProof");
+}
+
+std::shared_ptr<ProofNode> PropPfManager::getProof()
+{
+ // retrieve the SAT solver's refutation proof
+ Trace("sat-proof")
+ << "PropPfManager::getProof: Getting resolution proof of false\n";
+ std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+ Assert(conflictProof);
+ if (Trace.isOn("sat-proof"))
+ {
+ std::vector<Node> fassumps;
+ expr::getFreeAssumptions(conflictProof.get(), fassumps);
+ Trace("sat-proof")
+ << "PropPfManager::getProof: initial free assumptions are:\n";
+ for (const Node& a : fassumps)
+ {
+ Trace("sat-proof") << "- " << a << "\n";
+ }
+ Trace("sat-proof-debug")
+ << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
+ Trace("sat-proof")
+ << "PropPfManager::getProof: Connecting with CNF proof\n";
+ }
+ // connect it with CNF proof
+ d_pfpp->process(conflictProof);
+ if (Trace.isOn("sat-proof"))
+ {
+ std::vector<Node> fassumps;
+ expr::getFreeAssumptions(conflictProof.get(), fassumps);
+ Trace("sat-proof")
+ << "PropPfManager::getProof: new free assumptions are:\n";
+ for (const Node& a : fassumps)
+ {
+ Trace("sat-proof") << "- " << a << "\n";
+ }
+ Trace("sat-proof") << "PropPfManager::getProof: assertions are:\n";
+ for (const Node& a : d_assertions)
+ {
+ Trace("sat-proof") << "- " << a << "\n";
+ }
+ Trace("sat-proof-debug")
+ << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
+ }
+ return conflictProof;
+}
+
+} // namespace prop
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file prop_proof_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** 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 The proof manager of PropEngine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP_PROOF_MANAGER_H
+#define CVC4__PROP_PROOF_MANAGER_H
+
+#include "context/cdlist.h"
+#include "expr/proof.h"
+#include "expr/proof_node_manager.h"
+#include "prop/proof_post_processor.h"
+#include "prop/sat_proof_manager.h"
+
+namespace CVC4 {
+
+namespace prop {
+
+/**
+ * This class is responsible for managing the proof output of PropEngine, both
+ * building and checking it.
+ *
+ * The expected proof to be built is a refutation proof with preprocessed
+ * assertions as free assumptions.
+ */
+class PropPfManager
+{
+ public:
+ PropPfManager(context::UserContext* userContext,
+ ProofNodeManager* pnm,
+ SatProofManager* satPM,
+ ProofCnfStream* cnfProof);
+
+ /** Saves assertion for later checking whether refutation proof is closed.
+ *
+ * The assertions registered via this interface are preprocessed assertions
+ * from SMT engine as they are asserted to the prop engine.
+ */
+ void registerAssertion(Node assertion);
+ /**
+ * Generates the prop engine proof: a proof of false resulting from the
+ * connection of the refutation proof in d_satPM with the justification for
+ * its assumptions, which are retrieved from the CNF conversion proof, if any.
+ *
+ * The connection is done by running the proof post processor d_pfpp over the
+ * proof of false provided by d_satPM. See ProofPostProcessor for more
+ * details.
+ */
+ std::shared_ptr<ProofNode> getProof();
+
+ /**
+ * Checks that the prop engine proof is closed w.r.t. the given assertions and
+ * previously registered assertions in d_assertions.
+ *
+ * A common use of other assertions on top of the ones already registered on
+ * d_assertions is checking closedness w.r.t. preprocessed *and* input
+ * assertions. This is necessary if a prop engine's proof is modified
+ * externally (which can happen, for example, when connecting the prop
+ * engine's proof with the preprocessing proof) and these changes survive for
+ * a next check-sat call.
+ */
+ void checkProof(context::CDList<Node>* assertions);
+
+ private:
+ /** A node manager */
+ ProofNodeManager* d_pnm;
+ /** The proof post-processor */
+ std::unique_ptr<prop::ProofPostproccess> d_pfpp;
+ /**
+ * The SAT solver's proof manager, which will provide a refutation
+ * proofresolution proof when requested */
+ SatProofManager* d_satPM;
+ /** Assertions corresponding to the leaves of the prop engine's proof.
+ *
+ * These are kept in a context-dependent manner since the prop engine's proof
+ * is also kept in a context-dependent manner.
+ */
+ context::CDList<Node> d_assertions;
+}; /* class PropPfManager */
+
+} // namespace prop
+} // namespace CVC4
+
+#endif /* CVC4__PROP__PROOF_MANAGER_H */
projects / cvc5.git / commitdiff