1 

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

/*! \file lazy_tree_proof_generator.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** 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 lazy tree proof generator class 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H 
18 

#define CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H 
19 


20 

#include <iostream> 
21 


22 

#include "expr/node.h" 
23 

#include "expr/proof_generator.h" 
24 

#include "expr/proof_node_manager.h" 
25 


26 

namespace CVC4 { 
27 

namespace theory { 
28 

namespace detail { 
29 

/** 
30 

* A single node in the proof tree created by the LazyTreeProofGenerator. 
31 

* A node directly represents a ProofNode that is eventually constructed from 
32 

* it. The Nodes of the additional field d_premise are added to d_children as 
33 

* new assumptions via ASSUME. 
34 

*/ 
35 

struct TreeProofNode 
36 

{ 
37 

/** The proof rule */ 
38 

PfRule d_rule = PfRule::UNKNOWN; 
39 

/** Assumptions used as premise for this proof step */ 
40 

std::vector<Node> d_premise; 
41 

/** Arguments for this proof step */ 
42 

std::vector<Node> d_args; 
43 

/** Conclusion of this proof step */ 
44 

Node d_proven; 
45 

/** Children of this proof step */ 
46 

std::vector<TreeProofNode> d_children; 
47 

}; 
48 

} // namespace detail 
49 


50 

/** 
51 

* This class supports the lazy creation of a treeshaped proof. 
52 

* The core idea is that the lazy creation is necessary because proof rules 
53 

* depend on assumptions that are only known after the whole subtree has been 
54 

* finished. 
55 

* 
56 

* We indend to argue about proofs that roughly go as follows: 
57 

*  we assume a set of assumptions 
58 

*  we do a case split 
59 

*  for every case, we derive false, possibly by nested case splits 
60 

* 
61 

* Every case is represented by a SCOPE whose child derives false. When 
62 

* composing the final proof, we explicitly extend the premise of every proof 
63 

* step with the scope (the currently selected case) that this proof step lives 
64 

* in. When doing this, we ignore the outermost scope (which assumes the 
65 

* assertion set) to allow for having conflicts that are only a subset of the 
66 

* assertion set. 
67 

* 
68 

* Consider the example x*x<1 and x>2 and the intended proof 
69 

* (SCOPE 
70 

* (ARITH_NL_CAD_SPLIT 
71 

* (SCOPE 
72 

* (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false) 
73 

* :args [x<=2] 
74 

* ) 
75 

* (SCOPE 
76 

* (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false) 
77 

* :args [x>=1] 
78 

* ) 
79 

* ) 
80 

* :args [ x*x<1, x>2 ] 
81 

* ) 
82 

* We obtain this proof in a way that (in general) gives us the assumptions 
83 

* for the scopes (x<=2, x>=1) only when the scope children have been fully 
84 

* computed. Thus, we store the proof in an intermediate form and add the scope 
85 

* arguments when we learn them. Once we have completed the proof, we can easily 
86 

* transform it into proper ProofNodes. 
87 

* 
88 

* This class is stateful in the sense that the interface (in particular 
89 

* openChild() and closeChild()) navigates the proof tree (and creating it 
90 

* onthefly). Initially, and after reset() has been called, the proof consists 
91 

* of one empty proof node (with proof rule UNKNOWN). It stores the current 
92 

* position in the proof tree internally to make the interface easier to use. 
93 

* 
94 

* THIS MAKES THIS CLASS INHERENTLY NOT THREADSAFE! 
95 

* 
96 

* To construct the above proof, use this class roughly as follows: 
97 

* setCurrent(SCOPE, {}, assertions, false); 
98 

* openChild(); 
99 

* // First nested scope 
100 

* openChild(); 
101 

* setCurrent(SCOPE, {}, {}, false); 
102 

* openChild(); 
103 

* setCurrent(CAD_DIRECT, {x>2}, {}, false); 
104 

* closeChild(); 
105 

* getCurrent().args = {x<=2}; 
106 

* closeChild(); 
107 

* // Second nested scope 
108 

* openChild(); 
109 

* setCurrent(SCOPE, {}, {}, false); 
110 

* openChild(); 
111 

* setCurrent(CAD_DIRECT, {x*x<1}, {}, false); 
112 

* closeChild(); 
113 

* getCurrent().args = {x>=1}; 
114 

* closeChild(); 
115 

* // Finish split 
116 

* setCurrent(CAD_SPLIT, {}, {}, false); 
117 

* closeChild(); 
118 

* closeChild(); 
119 

* 
120 

* To explicitly finish proof construction, we need to call closeChild() one 
121 

* additional time. 
122 

*/ 
123 

class LazyTreeProofGenerator : public ProofGenerator 
124 

{ 
125 

public: 
126 

friend std::ostream& operator<<(std::ostream& os, 
127 

const LazyTreeProofGenerator& ltpg); 
128 


129 

LazyTreeProofGenerator(ProofNodeManager* pnm, 
130 

const std::string& name = "LazyTreeProofGenerator"); 
131 


132 

std::string identify() const override { return d_name; } 
133 

/** Create a new child and make it the current node */ 
134 

void openChild(); 
135 

/** 
136 

* Finish the current node and return to its parent 
137 

* Checks that the current node has a proof rule different from UNKNOWN. 
138 

* When called on the root node, this finishes the proof construction: we can 
139 

* no longer call getCurrent(), setCurrent() openChild() and closeChild(), but 
140 

* instead can call getProof() now. 
141 

*/ 
142 

void closeChild(); 
143 

/** 
144 

* Return a reference to the current node 
145 

*/ 
146 

detail::TreeProofNode& getCurrent(); 
147 

/** Set the current node / proof step */ 
148 

void setCurrent(PfRule rule, 
149 

const std::vector<Node>& premise, 
150 

std::vector<Node> args, 
151 

Node proven); 
152 

/** Construct the proof as a ProofNode */ 
153 

std::shared_ptr<ProofNode> getProof() const; 
154 

/** Return the constructed proof. Checks that we have proven f */ 
155 

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

/** Checks whether we have proven f */ 
157 

bool hasProofFor(Node f) override; 
158 


159 

/** 
160 

* Removes children from the current node based on the given predicate. 
161 

* It can be used for cases where facts (and their proofs) are eagerly 
162 

* generated and then later pruned, for example to produce smaller conflicts. 
163 

* The predicate is given as a Callable f that is called for every child with 
164 

* the id of the child and the child itself. 
165 

* f should return true if the child should be kept, fals if the child should 
166 

* be removed. 
167 

* @param f a Callable bool(std::size_t, const detail::TreeProofNode&) 
168 

*/ 
169 

template <typename F> 
170 

void pruneChildren(F&& f) 
171 

{ 
172 

auto& children = getCurrent().d_children; 
173 

std::size_t cur = 0; 
174 

std::size_t pos = 0; 
175 

for (std::size_t size = children.size(); cur < size; ++cur) 
176 

{ 
177 

if (f(cur, children[pos])) 
178 

{ 
179 

if (cur != pos) 
180 

{ 
181 

children[pos] = std::move(children[cur]); 
182 

} 
183 

++pos; 
184 

} 
185 

} 
186 

children.resize(pos); 
187 

} 
188 


189 

private: 
190 

/** recursive proof construction used by getProof() */ 
191 

std::shared_ptr<ProofNode> getProof( 
192 

std::vector<std::shared_ptr<ProofNode>>& scope, 
193 

const detail::TreeProofNode& pn) const; 
194 


195 

/** recursive debug printing used by operator<<() */ 
196 

void print(std::ostream& os, 
197 

const std::string& prefix, 
198 

const detail::TreeProofNode& pn) const; 
199 


200 

/** The ProofNodeManager used for constructing ProofNodes */ 
201 

ProofNodeManager* d_pnm; 
202 

/** The trace to the current node */ 
203 

std::vector<detail::TreeProofNode*> d_stack; 
204 

/** The root node of the proof tree */ 
205 

detail::TreeProofNode d_proof; 
206 

/** Caches the result of getProof() */ 
207 

mutable std::shared_ptr<ProofNode> d_cached; 
208 

/** Name of this proof generator */ 
209 

std::string d_name; 
210 

}; 
211 


212 

/** 
213 

* Prints the current state of a LazyTreeProofGenerator. Can also be used on a 
214 

* partially constructed proof. It is intended for debugging only and attempts 
215 

* to prettyprint itself using indentation. 
216 

*/ 
217 

std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); 
218 


219 

} // namespace theory 
220 

} // namespace CVC4 
221 


222 

#endif 