From: Haniel Barbosa Date: Tue, 29 Sep 2020 19:15:06 +0000 (-0300) Subject: [proof-new] Adds a proof manager for prop engine (#5162) X-Git-Tag: cvc5-1.0.0~2785 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f51491e43e86abb862ea081568b8aa106293d64a;p=cvc5.git [proof-new] Adds a proof manager for prop engine (#5162) Also fixes some weird orderings in src/CMakeLists.txt --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 23d9675b4..30f5f80c1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -139,6 +139,7 @@ libcvc4_add_sources( 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 @@ -185,17 +186,18 @@ libcvc4_add_sources( 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 diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp new file mode 100644 index 000000000..aa58ffa2c --- /dev/null +++ b/src/prop/prop_proof_manager.cpp @@ -0,0 +1,109 @@ +/********************* */ +/*! \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* assertions) +{ + Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution " + "proof of false is closed\n"; + std::shared_ptr 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 avec{d_assertions.begin(), d_assertions.end()}; + pfnEnsureClosedWrt( + conflictProof.get(), avec, "sat-proof", "PropPfManager::checkProof"); +} + +std::shared_ptr PropPfManager::getProof() +{ + // retrieve the SAT solver's refutation proof + Trace("sat-proof") + << "PropPfManager::getProof: Getting resolution proof of false\n"; + std::shared_ptr conflictProof = d_satPM->getProof(); + Assert(conflictProof); + if (Trace.isOn("sat-proof")) + { + std::vector 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 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 diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h new file mode 100644 index 000000000..f3deee5bc --- /dev/null +++ b/src/prop/prop_proof_manager.h @@ -0,0 +1,95 @@ +/********************* */ +/*! \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 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* assertions); + + private: + /** A node manager */ + ProofNodeManager* d_pnm; + /** The proof post-processor */ + std::unique_ptr 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 d_assertions; +}; /* class PropPfManager */ + +} // namespace prop +} // namespace CVC4 + +#endif /* CVC4__PROP__PROOF_MANAGER_H */