1 

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

/*! \file preprocess_proof_generator.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, 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 module for proofs for preprocessing in an SMT engine. 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H 
18 

#define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H 
19 


20 

#include "context/cdhashmap.h" 
21 

#include "expr/lazy_proof.h" 
22 

#include "expr/proof.h" 
23 

#include "expr/proof_set.h" 
24 

#include "expr/proof_generator.h" 
25 

#include "theory/trust_node.h" 
26 


27 

namespace CVC4 { 
28 


29 

class LazyCDProof; 
30 

class ProofNodeManager; 
31 


32 

namespace smt { 
33 


34 

/** 
35 

* This is a proof generator that manages proofs for a set of formulas that 
36 

* may be replaced over time. This set of formulas is implicit; formulas that 
37 

* are not notified as assertions to this class are treated as assumptions. 
38 

* 
39 

* The main use case of this proof generator is for proofs of preprocessing, 
40 

* although it can be used in other scenarios where proofs for an evolving set 
41 

* of formulas is maintained. In the remainder of the description here, we 
42 

* describe its role as a proof generator for proofs of preprocessing. 
43 

* 
44 

* This class has two main interfaces during solving: 
45 

* (1) notifyNewAssert, for assertions that are not part of the input and are 
46 

* added to the assertion pipeline by preprocessing passes, 
47 

* (2) notifyPreprocessed, which is called when a preprocessing pass rewrites 
48 

* an assertion into another. 
49 

* Notice that input assertions do not need to be provided to this class. 
50 

* 
51 

* Its getProofFor method produces a proof for a preprocessed assertion 
52 

* whose free assumptions are intended to be input assertions, which are 
53 

* implictly all assertions that are not notified to this class. 
54 

*/ 
55 

class PreprocessProofGenerator : public ProofGenerator 
56 

{ 
57 

typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction> 
58 

NodeTrustNodeMap; 
59 


60 

public: 
61 

/** 
62 

* @param pnm The proof node manager 
63 

* @param c The context this class depends on 
64 

* @param name The name of this generator (for debugging) 
65 

* @param ra The proof rule to use when no generator is provided for new 
66 

* assertions 
67 

* @param rpp The proof rule to use when no generator is provided for 
68 

* preprocessing steps. 
69 

*/ 
70 

PreprocessProofGenerator(ProofNodeManager* pnm, 
71 

context::Context* c = nullptr, 
72 

std::string name = "PreprocessProofGenerator", 
73 

PfRule ra = PfRule::PREPROCESS_LEMMA, 
74 

PfRule rpp = PfRule::PREPROCESS); 
75 
3848 
~PreprocessProofGenerator() {} 
76 

/** 
77 

* Notify that n is an input (its proof is ASSUME). 
78 

*/ 
79 

void notifyInput(Node n); 
80 

/** 
81 

* Notify that n is a new assertion, where pg can provide a proof of n. 
82 

*/ 
83 

void notifyNewAssert(Node n, ProofGenerator* pg); 
84 

/** Notify a new assertion, trust node version. */ 
85 

void notifyNewTrustedAssert(theory::TrustNode tn); 
86 

/** 
87 

* Notify that n was replaced by np due to preprocessing, where pg can 
88 

* provide a proof of the equality n=np. 
89 

*/ 
90 

void notifyPreprocessed(Node n, Node np, ProofGenerator* pg); 
91 

/** Notify preprocessed, trust node version */ 
92 

void notifyTrustedPreprocessed(theory::TrustNode tnp); 
93 

/** 
94 

* Get proof for f, which returns a proof based on proving an equality based 
95 

* on transitivity of preprocessing steps, and then using the original 
96 

* assertion with EQ_RESOLVE to obtain the proof of the ending assertion f. 
97 

*/ 
98 

std::shared_ptr<ProofNode> getProofFor(Node f) override; 
99 

/** Identify */ 
100 

std::string identify() const override; 
101 

/** Get the proof manager */ 
102 

ProofNodeManager* getManager(); 
103 

/** 
104 

* Allocate a helper proof. This returns a fresh lazy proof object that 
105 

* remains alive in the context. This feature is used to construct 
106 

* helper proofs for preprocessing, e.g. to support the skeleton of proofs 
107 

* that connect AssertionPipeline::conjoin steps. 
108 

*/ 
109 

LazyCDProof* allocateHelperProof(); 
110 


111 

private: 
112 

/** 
113 

* Possibly check pedantic failure for null proof generator provided 
114 

* to this class. 
115 

*/ 
116 

void checkEagerPedantic(PfRule r); 
117 

/** The proof node manager */ 
118 

ProofNodeManager* d_pnm; 
119 

/** A dummy context used by this class if none is provided */ 
120 

context::Context d_context; 
121 

/** The context used here */ 
122 

context::Context* d_ctx; 
123 

/** 
124 

* The trust node that was the source of each node constructed during 
125 

* preprocessing. For each n, d_src[n] is a trust node whose node is n. This 
126 

* can either be: 
127 

* (1) A trust node REWRITE proving (n_src = n) for some n_src, or 
128 

* (2) A trust node LEMMA proving n. 
129 

*/ 
130 

NodeTrustNodeMap d_src; 
131 

/** A contextdependent list of LazyCDProof, allocated for conjoin steps */ 
132 

CDProofSet<LazyCDProof> d_helperProofs; 
133 

/** 
134 

* A cd proof for input assertions, this is an empty proof that intentionally 
135 

* returns (ASSUME f) for all f. 
136 

*/ 
137 

CDProof d_inputPf; 
138 

/** Name for debugging */ 
139 

std::string d_name; 
140 

/** The trust rule for new assertions with no provided proof generator */ 
141 

PfRule d_ra; 
142 

/** The trust rule for rewrites with no provided proof generator */ 
143 

PfRule d_rpp; 
144 

}; 
145 


146 

} // namespace smt 
147 

} // namespace CVC4 
148 


149 

#endif 