1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The proof manager of PropEngine. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PROP_PROOF_MANAGER_H |
19 |
|
#define CVC5__PROP_PROOF_MANAGER_H |
20 |
|
|
21 |
|
#include "context/cdlist.h" |
22 |
|
#include "expr/proof.h" |
23 |
|
#include "expr/proof_node_manager.h" |
24 |
|
#include "prop/proof_post_processor.h" |
25 |
|
#include "prop/sat_proof_manager.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
namespace prop { |
30 |
|
|
31 |
|
class CDCLTSatSolverInterface; |
32 |
|
|
33 |
|
/** |
34 |
|
* This class is responsible for managing the proof output of PropEngine, both |
35 |
|
* building and checking it. |
36 |
|
* |
37 |
|
* The expected proof to be built is a refutation proof with preprocessed |
38 |
|
* assertions as free assumptions. |
39 |
|
*/ |
40 |
1197 |
class PropPfManager |
41 |
|
{ |
42 |
|
public: |
43 |
|
PropPfManager(context::UserContext* userContext, |
44 |
|
ProofNodeManager* pnm, |
45 |
|
CDCLTSatSolverInterface* satSolver, |
46 |
|
ProofCnfStream* cnfProof); |
47 |
|
|
48 |
|
/** Saves assertion for later checking whether refutation proof is closed. |
49 |
|
* |
50 |
|
* The assertions registered via this interface are preprocessed assertions |
51 |
|
* from SMT engine as they are asserted to the prop engine. |
52 |
|
*/ |
53 |
|
void registerAssertion(Node assertion); |
54 |
|
/** |
55 |
|
* Generates the prop engine proof: a proof of false resulting from the |
56 |
|
* connection of the refutation proof in d_satPM with the justification for |
57 |
|
* its assumptions, which are retrieved from the CNF conversion proof, if any. |
58 |
|
* |
59 |
|
* The connection is done by running the proof post processor d_pfpp over the |
60 |
|
* proof of false provided by d_satPM. See ProofPostProcessor for more |
61 |
|
* details. |
62 |
|
*/ |
63 |
|
std::shared_ptr<ProofNode> getProof(); |
64 |
|
|
65 |
|
/** |
66 |
|
* Checks that the prop engine proof is closed w.r.t. the given assertions and |
67 |
|
* previously registered assertions in d_assertions. |
68 |
|
* |
69 |
|
* A common use of other assertions on top of the ones already registered on |
70 |
|
* d_assertions is checking closedness w.r.t. preprocessed *and* input |
71 |
|
* assertions. This is necessary if a prop engine's proof is modified |
72 |
|
* externally (which can happen, for example, when connecting the prop |
73 |
|
* engine's proof with the preprocessing proof) and these changes survive for |
74 |
|
* a next check-sat call. |
75 |
|
*/ |
76 |
|
void checkProof(context::CDList<Node>* assertions); |
77 |
|
|
78 |
|
private: |
79 |
|
/** A node manager */ |
80 |
|
ProofNodeManager* d_pnm; |
81 |
|
/** The proof post-processor */ |
82 |
|
std::unique_ptr<prop::ProofPostproccess> d_pfpp; |
83 |
|
/** |
84 |
|
* The SAT solver of this prop engine, which should provide a refutation |
85 |
|
* proof when requested */ |
86 |
|
CDCLTSatSolverInterface* d_satSolver; |
87 |
|
/** Assertions corresponding to the leaves of the prop engine's proof. |
88 |
|
* |
89 |
|
* These are kept in a context-dependent manner since the prop engine's proof |
90 |
|
* is also kept in a context-dependent manner. |
91 |
|
*/ |
92 |
|
context::CDList<Node> d_assertions; |
93 |
|
}; /* class PropPfManager */ |
94 |
|
|
95 |
|
} // namespace prop |
96 |
|
} // namespace cvc5 |
97 |
|
|
98 |
|
#endif /* CVC5__PROP__PROOF_MANAGER_H */ |