GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/assertion_pipeline.h Lines: 14 14 100.0 %
Date: 2021-03-22 Branches: 4 4 100.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file assertion_pipeline.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Andrew Reynolds, Morgan Deters
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 AssertionPipeline stores a list of assertions modified by
13
 ** preprocessing passes
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
19
#define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
20
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "theory/trust_node.h"
25
26
namespace CVC4 {
27
28
class ProofGenerator;
29
namespace smt {
30
class PreprocessProofGenerator;
31
}
32
33
namespace preprocessing {
34
35
using IteSkolemMap = std::unordered_map<size_t, Node>;
36
37
/**
38
 * Assertion Pipeline stores a list of assertions modified by preprocessing
39
 * passes. It is assumed that all assertions after d_realAssertionsEnd were
40
 * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
41
 */
42
9605
class AssertionPipeline
43
{
44
 public:
45
  AssertionPipeline();
46
47
567775
  size_t size() const { return d_nodes.size(); }
48
49
1
  void resize(size_t n) { d_nodes.resize(n); }
50
51
  /**
52
   * Clear the list of assertions and assumptions.
53
   */
54
  void clear();
55
56
1546011
  const Node& operator[](size_t i) const { return d_nodes[i]; }
57
58
  /**
59
   * Adds an assertion/assumption to be preprocessed.
60
   *
61
   * @param n The assertion/assumption
62
   * @param isAssumption If true, records that \p n is an assumption. Note that
63
   * all assumptions have to be added contiguously.
64
   * @param isInput If true, n is an input formula (an assumption in the main
65
   * body of the overall proof).
66
   * @param pg The proof generator who can provide a proof of n. The proof
67
   * generator is not required and is ignored if isInput is true.
68
   */
69
  void push_back(Node n,
70
                 bool isAssumption = false,
71
                 bool isInput = false,
72
                 ProofGenerator* pg = nullptr);
73
  /** Same as above, with TrustNode */
74
  void pushBackTrusted(theory::TrustNode trn);
75
76
  /**
77
   * Get the constant reference to the underlying assertions. It is only
78
   * possible to modify these via the replace methods below.
79
   */
80
26552
  const std::vector<Node>& ref() const { return d_nodes; }
81
82
32
  std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
83
60
  std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
84
85
  /*
86
   * Replaces assertion i with node n and records the dependency between the
87
   * original assertion and its replacement.
88
   *
89
   * @param i The position of the assertion to replace.
90
   * @param n The replacement assertion.
91
   * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
92
   * where d_nodes[i] is the assertion at position i prior to this call.
93
   */
94
  void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
95
  /**
96
   * Same as above, with TrustNode trn, which is of kind REWRITE and proves
97
   * d_nodes[i] = n for some n.
98
   */
99
  void replaceTrusted(size_t i, theory::TrustNode trn);
100
101
36112
  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
102
  const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
103
104
11719
  size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
105
106
  /** @return The index of the first assumption */
107
  size_t getAssumptionsStart() const { return d_assumptionsStart; }
108
109
  /** @return The number of assumptions */
110
11323
  size_t getNumAssumptions() const { return d_numAssumptions; }
111
112
11331
  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
113
114
  /**
115
   * Returns true if substitutions must be stored as assertions. This is for
116
   * example the case when we do incremental solving.
117
   */
118
45484
  bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; }
119
120
  /**
121
   * Enables storing substitutions as assertions.
122
   */
123
  void enableStoreSubstsInAsserts();
124
125
  /**
126
   * Disables storing substitutions as assertions.
127
   */
128
  void disableStoreSubstsInAsserts();
129
130
  /**
131
   * Adds a substitution node of the form (= lhs rhs) to the assertions.
132
   * This conjoins n to assertions at a distinguished index given by
133
   * d_substsIndex.
134
   *
135
   * @param n The substitution node
136
   * @param pg The proof generator that can provide a proof of n.
137
   */
138
  void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr);
139
140
  /**
141
   * Conjoin n to the assertion vector at position i. This replaces
142
   * d_nodes[i] with the rewritten form of (AND d_nodes[i] n).
143
   *
144
   * @param i The assertion to replace
145
   * @param n The formula to conjoin at position i
146
   * @param pg The proof generator that can provide a proof of n
147
   */
148
  void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr);
149
150
  /**
151
   * Checks whether the assertion at a given index represents substitutions.
152
   *
153
   * @param i The index in question
154
   */
155
177023
  bool isSubstsIndex(size_t i)
156
  {
157
177023
    return d_storeSubstsInAsserts && i == d_substsIndex;
158
  }
159
  //------------------------------------ for proofs
160
  /** Set proof generator */
161
  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
162
  /** Is proof enabled? */
163
  bool isProofEnabled() const;
164
  //------------------------------------ end for proofs
165
 private:
166
  /** The list of current assertions */
167
  std::vector<Node> d_nodes;
168
169
  /**
170
   * Map from skolem variables to index in d_assertions containing
171
   * corresponding introduced Boolean ite
172
   */
173
  IteSkolemMap d_iteSkolemMap;
174
175
  /** Size of d_nodes when preprocessing starts */
176
  size_t d_realAssertionsEnd;
177
178
  /**
179
   * If true, we store the substitutions as assertions. This is necessary when
180
   * doing incremental solving because we cannot apply them to existing
181
   * assertions while preprocessing new assertions.
182
   */
183
  bool d_storeSubstsInAsserts;
184
185
  /**
186
   * The index of the assertions that holds the substitutions.
187
   *
188
   * TODO(#2473): replace by separate vector of substitution assertions.
189
   */
190
  size_t d_substsIndex;
191
192
  /** Index of the first assumption */
193
  size_t d_assumptionsStart;
194
  /** The number of assumptions */
195
  size_t d_numAssumptions;
196
  /** The proof generator, if one is provided */
197
  smt::PreprocessProofGenerator* d_pppg;
198
}; /* class AssertionPipeline */
199
200
}  // namespace preprocessing
201
}  // namespace CVC4
202
203
#endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */