GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/inference_manager.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 Customized inference manager for the theory of strings
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
18
#define CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
19
20
#include <map>
21
#include <vector>
22
23
#include "context/cdhashset.h"
24
#include "context/context.h"
25
#include "expr/node.h"
26
#include "expr/proof_node_manager.h"
27
#include "theory/ext_theory.h"
28
#include "theory/inference_manager_buffered.h"
29
#include "theory/output_channel.h"
30
#include "theory/strings/infer_info.h"
31
#include "theory/strings/infer_proof_cons.h"
32
#include "theory/strings/sequences_stats.h"
33
#include "theory/strings/solver_state.h"
34
#include "theory/strings/term_registry.h"
35
#include "theory/theory_inference_manager.h"
36
#include "theory/uf/equality_engine.h"
37
38
namespace CVC4 {
39
namespace theory {
40
namespace strings {
41
42
/** Inference Manager
43
 *
44
 * The purpose of this class is to process inference steps for strategies
45
 * in the theory of strings.
46
 *
47
 * In particular, inferences are given to this class via calls to functions:
48
 *
49
 * sendInternalInference, sendInference, sendSplit
50
 *
51
 * This class decides how the conclusion of these calls will be processed.
52
 * It primarily has to decide whether the conclusions will be processed:
53
 *
54
 * (1) Internally in the strings solver, via calls to equality engine's
55
 * assertLiteral and assertPredicate commands. We refer to these literals as
56
 * "facts",
57
 * (2) Externally on the output channel of theory of strings as "lemmas",
58
 * (3) External on the output channel as "conflicts" (when a conclusion of an
59
 * inference is false).
60
 *
61
 * It buffers facts and lemmas in vectors d_pending and d_pending_lem
62
 * respectively.
63
 *
64
 * When applicable, facts can be flushed to the equality engine via a call to
65
 * doPendingFacts, and lemmas can be flushed to the output channel via a call
66
 * to doPendingLemmas.
67
 *
68
 * It also manages other kinds of interaction with the output channel of the
69
 * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
70
 * with the extended theory object e.g. markCongruent.
71
 */
72
class InferenceManager : public InferenceManagerBuffered
73
{
74
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
75
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
76
  friend class InferInfo;
77
78
 public:
79
  InferenceManager(Theory& t,
80
                   SolverState& s,
81
                   TermRegistry& tr,
82
                   ExtTheory& e,
83
                   SequencesStatistics& statistics,
84
                   ProofNodeManager* pnm);
85
8994
  ~InferenceManager() {}
86
87
  /**
88
   * Do pending method. This processes all pending facts, lemmas and pending
89
   * phase requests based on the policy of this manager. This means that
90
   * we process the pending facts first and abort if in conflict. Otherwise, we
91
   * process the pending lemmas and then the pending phase requirements.
92
   * Notice that we process the pending lemmas even if there were facts.
93
   */
94
  void doPending();
95
96
  /** send internal inferences
97
   *
98
   * This is called when we have inferred exp => conc, where exp is a set
99
   * of equalities and disequalities that hold in the current equality engine.
100
   * This method adds equalities and disequalities ~( s = t ) via
101
   * sendInference such that both s and t are either constants or terms
102
   * that already occur in the equality engine, and ~( s = t ) is a consequence
103
   * of conc. This function can be seen as a "conservative" version of
104
   * sendInference below in that it does not introduce any new non-constant
105
   * terms to the state.
106
   *
107
   * The argument infer identifies the reason for the inference.
108
   * This is used for debugging and statistics purposes.
109
   *
110
   * Return true if the inference is complete, in the sense that we infer
111
   * inferences that are equivalent to conc. This returns false e.g. if conc
112
   * (or one of its conjuncts if it is a conjunction) was not inferred due
113
   * to the criteria mentioned above.
114
   */
115
  bool sendInternalInference(std::vector<Node>& exp,
116
                             Node conc,
117
                             InferenceId infer);
118
119
  /** send inference
120
   *
121
   * This function should be called when exp => eq. The set exp
122
   * contains literals that are explainable, i.e. those that hold in the
123
   * equality engine of the theory of strings. On the other hand, the set
124
   * noExplain contains nodes that are not explainable by the theory of strings.
125
   * This method may call sendLemma or otherwise add a InferInfo to d_pending,
126
   * indicating a fact should be asserted to the equality engine. Overall, the
127
   * result of this method is one of the following:
128
   *
129
   * [1] (No-op) Do nothing if eq is equivalent to true,
130
   *
131
   * [2] (Infer) Indicate that eq should be added to the equality engine of this
132
   * class with explanation exp, where exp is a set of literals that currently
133
   * hold in the equality engine. We add this to the pending vector d_pending.
134
   *
135
   * [3] (Lemma) Indicate that the lemma
136
   *   ( EXPLAIN(exp \ noExplain) ^ noExplain ) => eq
137
   * should be sent on the output channel of the theory of strings, where
138
   * EXPLAIN returns the explanation of the node in exp in terms of the literals
139
   * asserted to the theory of strings, as computed by the equality engine.
140
   * This is also added to a pending vector, d_pendingLem.
141
   *
142
   * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
143
   * channel of the theory of strings.
144
   *
145
   * Determining which case to apply depends on the form of eq and whether
146
   * noExplain is empty. In particular, lemmas must be used whenever noExplain
147
   * is non-empty, conflicts are used when noExplain is empty and eq is false.
148
   *
149
   * @param exp The explanation of eq.
150
   * @param noExplain The subset of exp that cannot be explained by the
151
   * equality engine. This may impact whether we are processing this call as a
152
   * fact or as a lemma.
153
   * @param eq The conclusion.
154
   * @param infer Identifies the reason for inference, used for
155
   * debugging. This updates the statistics about the number of inferences made
156
   * of each type.
157
   * @param isRev Whether this is the "reverse variant" of the inference, which
158
   * is used as a hint for proof reconstruction.
159
   * @param asLemma If true, then this method will send a lemma instead
160
   * of a fact whenever applicable.
161
   * @return true if the inference was not trivial (e.g. its conclusion did
162
   * not rewrite to true).
163
   */
164
  bool sendInference(const std::vector<Node>& exp,
165
                     const std::vector<Node>& noExplain,
166
                     Node eq,
167
                     InferenceId infer,
168
                     bool isRev = false,
169
                     bool asLemma = false);
170
  /** same as above, but where noExplain is empty */
171
  bool sendInference(const std::vector<Node>& exp,
172
                     Node eq,
173
                     InferenceId infer,
174
                     bool isRev = false,
175
                     bool asLemma = false);
176
177
  /** Send inference
178
   *
179
   * This implements the above methods for the InferInfo object. It is called
180
   * by the methods above.
181
   *
182
   * The inference info ii should have a rewritten conclusion and should not be
183
   * trivial (InferInfo::isTrivial). It is the responsibility of the caller to
184
   * ensure this.
185
   *
186
   * If the flag asLemma is true, then this method will send a lemma instead
187
   * of a fact whenever applicable.
188
   */
189
  void sendInference(InferInfo& ii, bool asLemma = false);
190
  /** Send split
191
   *
192
   * This requests that ( a = b V a != b ) is sent on the output channel as a
193
   * lemma. We additionally request a phase requirement for the equality a=b
194
   * with polarity preq.
195
   *
196
   * The argument infer identifies the reason for inference, used for
197
   * debugging. This updates the statistics about the number of
198
   * inferences made of each type.
199
   *
200
   * This method returns true if the split was non-trivial, and false
201
   * otherwise. A split is trivial if a=b rewrites to a constant.
202
   */
203
  bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true);
204
  /**
205
   * Set that we are incomplete for the current set of assertions (in other
206
   * words, we must answer "unknown" instead of "sat"); this calls the output
207
   * channel's setIncomplete method.
208
   */
209
  void setIncomplete();
210
211
  //----------------------------constructing antecedants
212
  /**
213
   * Adds equality a = b to the vector exp if a and b are distinct terms. It
214
   * must be the case that areEqual( a, b ) holds in this context.
215
   */
216
  void addToExplanation(Node a, Node b, std::vector<Node>& exp) const;
217
  /** Adds lit to the vector exp if it is non-null */
218
  void addToExplanation(Node lit, std::vector<Node>& exp) const;
219
  //----------------------------end constructing antecedants
220
  /**
221
   * Have we processed an inference during this call to check? In particular,
222
   * this returns true if we have a pending fact or lemma, or have encountered
223
   * a conflict.
224
   */
225
  bool hasProcessed() const;
226
227
  // ------------------------------------------------- extended theory
228
  /**
229
   * Mark that terms a and b are congruent in the current context.
230
   * This makes a call to markCongruent in the extended theory object of
231
   * the parent theory if the kind of a (and b) is owned by the extended
232
   * theory.
233
   */
234
  void markCongruent(Node a, Node b);
235
  /**
236
   * Mark that extended function is reduced. If contextDepend is true,
237
   * then this mark is SAT-context dependent, otherwise it is user-context
238
   * dependent (see ExtTheory::markReduced).
239
   */
240
  void markReduced(Node n, bool contextDepend = true);
241
  // ------------------------------------------------- end extended theory
242
243
  /**
244
   * Called when ii is ready to be processed as a conflict. This makes a
245
   * trusted node whose generator is the underlying proof equality engine
246
   * (if it exists), and sends it on the output channel.
247
   */
248
  void processConflict(const InferInfo& ii);
249
250
 private:
251
  /** Called when ii is ready to be processed as a fact */
252
  void processFact(InferInfo& ii, ProofGenerator*& pg);
253
  /** Called when ii is ready to be processed as a lemma */
254
  TrustNode processLemma(InferInfo& ii, LemmaProperty& p);
255
  /** Reference to the solver state of the theory of strings. */
256
  SolverState& d_state;
257
  /** Reference to the term registry of theory of strings */
258
  TermRegistry& d_termReg;
259
  /** the extended theory object for the theory of strings */
260
  ExtTheory& d_extt;
261
  /** Reference to the statistics for the theory of strings/sequences. */
262
  SequencesStatistics& d_statistics;
263
  /** Conversion from inferences to proofs */
264
  std::unique_ptr<InferProofCons> d_ipc;
265
  /** Common constants */
266
  Node d_true;
267
  Node d_false;
268
  Node d_zero;
269
  Node d_one;
270
};
271
272
}  // namespace strings
273
}  // namespace theory
274
}  // namespace CVC4
275
276
#endif