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) 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 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 
8992 
~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 nonconstant 
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] (Noop) 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 nonempty, 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 nontrivial, 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 nonnull */ 
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 SATcontext dependent, otherwise it is usercontext 
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 