GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/lazy_tree_proof_generator.h Lines: 0 3 0.0 %
Date: 2021-03-23 Branches: 0 8 0.0 %

Line Exec Source
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) 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.\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 tree-shaped 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
 * on-the-fly). 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 THREAD-SAFE!
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 pretty-print itself using indentation.
216
 */
217
std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
218
219
}  // namespace theory
220
}  // namespace CVC4
221
222
#endif