1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Theory of datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H |
19 |
|
#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H |
20 |
|
|
21 |
|
#include <iostream> |
22 |
|
#include <map> |
23 |
|
|
24 |
|
#include "context/cdlist.h" |
25 |
|
#include "expr/attribute.h" |
26 |
|
#include "expr/node_trie.h" |
27 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
28 |
|
#include "theory/datatypes/inference_manager.h" |
29 |
|
#include "theory/datatypes/proof_checker.h" |
30 |
|
#include "theory/datatypes/sygus_extension.h" |
31 |
|
#include "theory/theory.h" |
32 |
|
#include "theory/theory_eq_notify.h" |
33 |
|
#include "theory/theory_state.h" |
34 |
|
#include "theory/uf/equality_engine.h" |
35 |
|
#include "util/hash.h" |
36 |
|
|
37 |
|
namespace cvc5 { |
38 |
|
namespace theory { |
39 |
|
namespace datatypes { |
40 |
|
|
41 |
|
class TheoryDatatypes : public Theory { |
42 |
|
private: |
43 |
|
typedef context::CDList<Node> NodeList; |
44 |
|
/** maps nodes to an index in a vector */ |
45 |
|
typedef context::CDHashMap<Node, size_t> NodeUIntMap; |
46 |
|
typedef context::CDHashMap<Node, bool> BoolMap; |
47 |
|
typedef context::CDHashMap<Node, Node> NodeMap; |
48 |
|
|
49 |
|
private: |
50 |
|
//notification class for equality engine |
51 |
15266 |
class NotifyClass : public TheoryEqNotifyClass |
52 |
|
{ |
53 |
|
TheoryDatatypes& d_dt; |
54 |
|
public: |
55 |
15271 |
NotifyClass(TheoryInferenceManager& im, TheoryDatatypes& dt) |
56 |
15271 |
: TheoryEqNotifyClass(im), d_dt(dt) |
57 |
|
{ |
58 |
15271 |
} |
59 |
443657 |
void eqNotifyNewClass(TNode t) override |
60 |
|
{ |
61 |
443657 |
Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; |
62 |
443657 |
d_dt.eqNotifyNewClass(t); |
63 |
443657 |
} |
64 |
4603818 |
void eqNotifyMerge(TNode t1, TNode t2) override |
65 |
|
{ |
66 |
9207636 |
Debug("dt") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2 << ")" |
67 |
4603818 |
<< std::endl; |
68 |
4603818 |
d_dt.eqNotifyMerge(t1, t2); |
69 |
4603818 |
} |
70 |
|
};/* class TheoryDatatypes::NotifyClass */ |
71 |
|
private: |
72 |
|
/** equivalence class info |
73 |
|
* d_inst is whether the instantiate rule has been applied, |
74 |
|
* d_constructor is a node of kind APPLY_CONSTRUCTOR (if any) in this equivalence class, |
75 |
|
* d_selectors is whether a selector has been applied to this equivalence class. |
76 |
|
*/ |
77 |
|
class EqcInfo |
78 |
|
{ |
79 |
|
public: |
80 |
|
EqcInfo( context::Context* c ); |
81 |
29771 |
~EqcInfo(){} |
82 |
|
//whether we have instantiatied this eqc |
83 |
|
context::CDO< bool > d_inst; |
84 |
|
//constructor equal to this eqc |
85 |
|
context::CDO< Node > d_constructor; |
86 |
|
//all selectors whose argument is this eqc |
87 |
|
context::CDO< bool > d_selectors; |
88 |
|
}; |
89 |
|
/** does eqc of n have a label (do we know its constructor)? */ |
90 |
|
bool hasLabel( EqcInfo* eqc, Node n ); |
91 |
|
/** get the label associated to n */ |
92 |
|
Node getLabel( Node n ); |
93 |
|
/** get the index of the label associated to n */ |
94 |
|
int getLabelIndex( EqcInfo* eqc, Node n ); |
95 |
|
/** does eqc of n have any testers? */ |
96 |
|
bool hasTester( Node n ); |
97 |
|
/** get the possible constructors for n */ |
98 |
|
void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); |
99 |
|
/** skolems for terms */ |
100 |
|
NodeMap d_term_sk; |
101 |
|
Node getTermSkolemFor( Node n ); |
102 |
|
private: |
103 |
|
/** information necessary for equivalence classes */ |
104 |
|
std::map< Node, EqcInfo* > d_eqc_info; |
105 |
|
//---------------------------------labels |
106 |
|
/** labels for each equivalence class |
107 |
|
* |
108 |
|
* For each eqc r, d_labels[r] is testers that hold for this equivalence |
109 |
|
* class, either: |
110 |
|
* a list of equations of the form |
111 |
|
* NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of |
112 |
|
* which are unique testers, n is less than the number of possible |
113 |
|
* constructors for t minus one, |
114 |
|
* or a list of equations of the form |
115 |
|
* NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by |
116 |
|
* is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester. |
117 |
|
* In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r. |
118 |
|
* |
119 |
|
* We store this list in a context-dependent way, using the four data |
120 |
|
* structures below. The three vectors d_labels_data, d_labels_args, and |
121 |
|
* d_labels_tindex store the tester applications, their arguments and the |
122 |
|
* tester index of the application. The map d_labels stores the number of |
123 |
|
* values in these vectors that is valid in the current context (this is an |
124 |
|
* optimization that ensures we don't need to pop data when changing SAT |
125 |
|
* contexts). |
126 |
|
*/ |
127 |
|
NodeUIntMap d_labels; |
128 |
|
/** the tester applications */ |
129 |
|
std::map< Node, std::vector< Node > > d_labels_data; |
130 |
|
/** the argument of each node in d_labels_data */ |
131 |
|
std::map<Node, std::vector<Node> > d_labels_args; |
132 |
|
/** the tester index of each node in d_labels_data */ |
133 |
|
std::map<Node, std::vector<unsigned> > d_labels_tindex; |
134 |
|
//---------------------------------end labels |
135 |
|
/** selector apps for eqch equivalence class */ |
136 |
|
NodeUIntMap d_selector_apps; |
137 |
|
std::map< Node, std::vector< Node > > d_selector_apps_data; |
138 |
|
/** The conflict node */ |
139 |
|
Node d_conflictNode; |
140 |
|
/** |
141 |
|
* SAT-context dependent cache for which terms we have called |
142 |
|
* collectTerms(...) on. |
143 |
|
*/ |
144 |
|
BoolMap d_collectTermsCache; |
145 |
|
/** |
146 |
|
* User-context dependent cache for which terms we have called |
147 |
|
* collectTerms(...) on. |
148 |
|
*/ |
149 |
|
BoolMap d_collectTermsCacheU; |
150 |
|
/** All the function terms that the theory has seen */ |
151 |
|
context::CDList<TNode> d_functionTerms; |
152 |
|
/** counter for forcing assignments (ensures fairness) */ |
153 |
|
unsigned d_dtfCounter; |
154 |
|
/** uninterpreted constant to variable map */ |
155 |
|
std::map< Node, Node > d_uc_to_fresh_var; |
156 |
|
private: |
157 |
|
/** singleton lemmas (for degenerate co-datatype case) */ |
158 |
|
std::map< TypeNode, Node > d_singleton_lemma[2]; |
159 |
|
/** Cache for singleton equalities processed */ |
160 |
|
BoolMap d_singleton_eq; |
161 |
|
private: |
162 |
|
/** assert fact */ |
163 |
|
void assertFact( Node fact, Node exp ); |
164 |
|
|
165 |
|
/** get or make eqc info */ |
166 |
|
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); |
167 |
|
|
168 |
|
/** has eqc info */ |
169 |
3861366 |
bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); } |
170 |
|
|
171 |
|
/** get eqc constructor */ |
172 |
|
TNode getEqcConstructor( TNode r ); |
173 |
|
|
174 |
|
protected: |
175 |
|
void addCarePairs(TNodeTrie* t1, |
176 |
|
TNodeTrie* t2, |
177 |
|
unsigned arity, |
178 |
|
unsigned depth, |
179 |
|
unsigned& n_pairs); |
180 |
|
/** compute care graph */ |
181 |
|
void computeCareGraph() override; |
182 |
|
|
183 |
|
public: |
184 |
|
TheoryDatatypes(Env& env, OutputChannel& out, Valuation valuation); |
185 |
|
~TheoryDatatypes(); |
186 |
|
|
187 |
|
//--------------------------------- initialization |
188 |
|
/** get the official theory rewriter of this theory */ |
189 |
|
TheoryRewriter* getTheoryRewriter() override; |
190 |
|
/** get the proof checker of this theory */ |
191 |
|
ProofRuleChecker* getProofChecker() override; |
192 |
|
/** |
193 |
|
* Returns true if we need an equality engine. If so, we initialize the |
194 |
|
* information regarding how it should be setup. For details, see the |
195 |
|
* documentation in Theory::needsEqualityEngine. |
196 |
|
*/ |
197 |
|
bool needsEqualityEngine(EeSetupInfo& esi) override; |
198 |
|
/** finish initialization */ |
199 |
|
void finishInit() override; |
200 |
|
//--------------------------------- end initialization |
201 |
|
/** propagate */ |
202 |
|
bool propagateLit(TNode literal); |
203 |
|
/** Conflict when merging two constants */ |
204 |
|
void conflict(TNode a, TNode b); |
205 |
|
/** explain */ |
206 |
|
TrustNode explain(TNode literal) override; |
207 |
|
/** called when a new equivalance class is created */ |
208 |
|
void eqNotifyNewClass(TNode t); |
209 |
|
/** called when two equivalance classes have merged */ |
210 |
|
void eqNotifyMerge(TNode t1, TNode t2); |
211 |
|
|
212 |
|
//--------------------------------- standard check |
213 |
|
/** Do we need a check call at last call effort? */ |
214 |
|
bool needsCheckLastEffort() override; |
215 |
|
/** Pre-check, called before the fact queue of the theory is processed. */ |
216 |
|
bool preCheck(Effort level) override; |
217 |
|
/** Post-check, called after the fact queue of the theory is processed. */ |
218 |
|
void postCheck(Effort level) override; |
219 |
|
/** Notify fact */ |
220 |
|
void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; |
221 |
|
//--------------------------------- end standard check |
222 |
|
void preRegisterTerm(TNode n) override; |
223 |
|
TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override; |
224 |
|
EqualityStatus getEqualityStatus(TNode a, TNode b) override; |
225 |
|
std::string identify() const override |
226 |
|
{ |
227 |
|
return std::string("TheoryDatatypes"); |
228 |
|
} |
229 |
|
/** debug print */ |
230 |
|
void printModelDebug( const char* c ); |
231 |
|
/** entailment check */ |
232 |
|
std::pair<bool, Node> entailmentCheck(TNode lit) override; |
233 |
|
|
234 |
|
private: |
235 |
|
/** add tester to equivalence class info */ |
236 |
|
void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg); |
237 |
|
/** add selector to equivalence class info */ |
238 |
|
void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true ); |
239 |
|
/** add constructor */ |
240 |
|
void addConstructor( Node c, EqcInfo* eqc, Node n ); |
241 |
|
/** merge the equivalence class info of t1 and t2 */ |
242 |
|
void merge( Node t1, Node t2 ); |
243 |
|
/** collapse selector, s is of the form sel( n ) where n = c */ |
244 |
|
void collapseSelector( Node s, Node c ); |
245 |
|
/** for checking if cycles exist */ |
246 |
|
void checkCycles(); |
247 |
|
Node searchForCycle(TNode n, |
248 |
|
TNode on, |
249 |
|
std::map<TNode, bool>& visited, |
250 |
|
std::map<TNode, bool>& proc, |
251 |
|
std::vector<Node>& explanation, |
252 |
|
bool firstTime = true); |
253 |
|
/** for checking whether two codatatype terms must be equal */ |
254 |
|
void separateBisimilar(std::vector<Node>& part, |
255 |
|
std::vector<std::vector<Node> >& part_out, |
256 |
|
std::vector<Node>& exp, |
257 |
|
std::map<Node, Node>& cn, |
258 |
|
std::map<Node, std::map<Node, int> >& dni, |
259 |
|
int dniLvl, |
260 |
|
bool mkExp); |
261 |
|
/** build model */ |
262 |
|
Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ); |
263 |
|
/** get singleton lemma */ |
264 |
|
Node getSingletonLemma( TypeNode tn, bool pol ); |
265 |
|
/** collect terms */ |
266 |
|
void collectTerms( Node n ); |
267 |
|
/** get instantiate cons */ |
268 |
|
Node getInstantiateCons(Node n, const DType& dt, int index); |
269 |
|
/** check instantiate, return true if an inference was generated. */ |
270 |
|
bool instantiate(EqcInfo* eqc, Node n); |
271 |
|
|
272 |
|
private: |
273 |
|
//equality queries |
274 |
|
bool hasTerm( TNode a ); |
275 |
|
bool areEqual( TNode a, TNode b ); |
276 |
|
bool areDisequal( TNode a, TNode b ); |
277 |
|
bool areCareDisequal( TNode x, TNode y ); |
278 |
|
TNode getRepresentative( TNode a ); |
279 |
|
|
280 |
|
/** Collect model values in m based on the relevant terms given by termSet */ |
281 |
|
bool collectModelValues(TheoryModel* m, |
282 |
|
const std::set<Node>& termSet) override; |
283 |
|
/** |
284 |
|
* Compute relevant terms. This includes datatypes in non-singleton |
285 |
|
* equivalence classes. |
286 |
|
*/ |
287 |
|
void computeRelevantTerms(std::set<Node>& termSet) override; |
288 |
|
/** Commonly used terms */ |
289 |
|
Node d_true; |
290 |
|
Node d_zero; |
291 |
|
/** sygus symmetry breaking utility */ |
292 |
|
std::unique_ptr<SygusExtension> d_sygusExtension; |
293 |
|
/** The theory rewriter for this theory. */ |
294 |
|
DatatypesRewriter d_rewriter; |
295 |
|
/** A (default) theory state object */ |
296 |
|
TheoryState d_state; |
297 |
|
/** The inference manager */ |
298 |
|
InferenceManager d_im; |
299 |
|
/** The notify class */ |
300 |
|
NotifyClass d_notify; |
301 |
|
/** Proof checker for datatypes */ |
302 |
|
DatatypesProofRuleChecker d_checker; |
303 |
|
};/* class TheoryDatatypes */ |
304 |
|
|
305 |
|
} // namespace datatypes |
306 |
|
} // namespace theory |
307 |
|
} // namespace cvc5 |
308 |
|
|
309 |
|
#endif /* CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H */ |