1 

/********************* */ 
2 

/*! \file prop_proof_manager.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Haniel Barbosa, Gereon Kremer 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The proof manager of PropEngine 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__PROP_PROOF_MANAGER_H 
18 

#define CVC4__PROP_PROOF_MANAGER_H 
19 


20 

#include "context/cdlist.h" 
21 

#include "expr/proof.h" 
22 

#include "expr/proof_node_manager.h" 
23 

#include "prop/proof_post_processor.h" 
24 

#include "prop/sat_proof_manager.h" 
25 


26 

namespace CVC4 { 
27 


28 

namespace prop { 
29 


30 

class CDCLTSatSolverInterface; 
31 


32 

/** 
33 

* This class is responsible for managing the proof output of PropEngine, both 
34 

* building and checking it. 
35 

* 
36 

* The expected proof to be built is a refutation proof with preprocessed 
37 

* assertions as free assumptions. 
38 

*/ 
39 
966 
class PropPfManager 
40 

{ 
41 

public: 
42 

PropPfManager(context::UserContext* userContext, 
43 

ProofNodeManager* pnm, 
44 

CDCLTSatSolverInterface* satSolver, 
45 

ProofCnfStream* cnfProof); 
46 


47 

/** Saves assertion for later checking whether refutation proof is closed. 
48 

* 
49 

* The assertions registered via this interface are preprocessed assertions 
50 

* from SMT engine as they are asserted to the prop engine. 
51 

*/ 
52 

void registerAssertion(Node assertion); 
53 

/** 
54 

* Generates the prop engine proof: a proof of false resulting from the 
55 

* connection of the refutation proof in d_satPM with the justification for 
56 

* its assumptions, which are retrieved from the CNF conversion proof, if any. 
57 

* 
58 

* The connection is done by running the proof post processor d_pfpp over the 
59 

* proof of false provided by d_satPM. See ProofPostProcessor for more 
60 

* details. 
61 

*/ 
62 

std::shared_ptr<ProofNode> getProof(); 
63 


64 

/** 
65 

* Checks that the prop engine proof is closed w.r.t. the given assertions and 
66 

* previously registered assertions in d_assertions. 
67 

* 
68 

* A common use of other assertions on top of the ones already registered on 
69 

* d_assertions is checking closedness w.r.t. preprocessed *and* input 
70 

* assertions. This is necessary if a prop engine's proof is modified 
71 

* externally (which can happen, for example, when connecting the prop 
72 

* engine's proof with the preprocessing proof) and these changes survive for 
73 

* a next checksat call. 
74 

*/ 
75 

void checkProof(context::CDList<Node>* assertions); 
76 


77 

private: 
78 

/** A node manager */ 
79 

ProofNodeManager* d_pnm; 
80 

/** The proof postprocessor */ 
81 

std::unique_ptr<prop::ProofPostproccess> d_pfpp; 
82 

/** 
83 

* The SAT solver of this prop engine, which should provide a refutation 
84 

* proof when requested */ 
85 

CDCLTSatSolverInterface* d_satSolver; 
86 

/** Assertions corresponding to the leaves of the prop engine's proof. 
87 

* 
88 

* These are kept in a contextdependent manner since the prop engine's proof 
89 

* is also kept in a contextdependent manner. 
90 

*/ 
91 

context::CDList<Node> d_assertions; 
92 

}; /* class PropPfManager */ 
93 


94 

} // namespace prop 
95 

} // namespace CVC4 
96 


97 

#endif /* CVC4__PROP__PROOF_MANAGER_H */ 