1 /********************* */
2 /*! \file theory_strings.h
4 ** Top contributors (to current version):
5 ** Tianyi Liang, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
12 ** \brief Theory of strings
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
22 #include "theory/theory.h"
23 #include "theory/uf/equality_engine.h"
24 #include "theory/strings/theory_strings_preprocess.h"
25 #include "theory/strings/regexp_operation.h"
27 #include "context/cdchunk_list.h"
28 #include "context/cdhashset.h"
29 #include "expr/attribute.h"
37 namespace quantifiers
{
44 * Decision procedure for strings.
48 struct StringsProxyVarAttributeId
{};
49 typedef expr::Attribute
< StringsProxyVarAttributeId
, bool > StringsProxyVarAttribute
;
51 class TheoryStrings
: public Theory
{
52 typedef context::CDChunkList
<Node
> NodeList
;
53 typedef context::CDHashMap
<Node
, bool, NodeHashFunction
> NodeBoolMap
;
54 typedef context::CDHashMap
<Node
, int, NodeHashFunction
> NodeIntMap
;
55 typedef context::CDHashMap
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
56 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
59 TheoryStrings(context::Context
* c
, context::UserContext
* u
,
60 OutputChannel
& out
, Valuation valuation
,
61 const LogicInfo
& logicInfo
);
64 void setMasterEqualityEngine(eq::EqualityEngine
* eq
);
66 std::string
identify() const { return std::string("TheoryStrings"); }
69 void propagate(Effort e
);
70 bool propagate(TNode literal
);
71 void explain( TNode literal
, std::vector
<TNode
>& assumptions
);
72 Node
explain( TNode literal
);
75 // NotifyClass for equality engine
76 class NotifyClass
: public eq::EqualityEngineNotify
{
79 NotifyClass(TheoryStrings
& t_str
): d_str(t_str
) {}
80 bool eqNotifyTriggerEquality(TNode equality
, bool value
) {
81 Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false" )<< ")" << std::endl
;
83 return d_str
.propagate(equality
);
85 // We use only literal triggers so taking not is safe
86 return d_str
.propagate(equality
.notNode());
89 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
90 Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
92 return d_str
.propagate(predicate
);
94 return d_str
.propagate(predicate
.notNode());
97 bool eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
98 Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag
<< ", " << t1
<< ", " << t2
<< ")" << std::endl
;
100 return d_str
.propagate(t1
.eqNode(t2
));
102 return d_str
.propagate(t1
.eqNode(t2
).notNode());
105 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
106 Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
107 d_str
.conflict(t1
, t2
);
109 void eqNotifyNewClass(TNode t
) {
110 Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t
<< std::endl
;
111 d_str
.eqNotifyNewClass(t
);
113 void eqNotifyPreMerge(TNode t1
, TNode t2
) {
114 Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1
<< ", " << t2
<< std::endl
;
115 d_str
.eqNotifyPreMerge(t1
, t2
);
117 void eqNotifyPostMerge(TNode t1
, TNode t2
) {
118 Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1
<< ", " << t2
<< std::endl
;
119 d_str
.eqNotifyPostMerge(t1
, t2
);
121 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
122 Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1
<< ", " << t2
<< ", " << reason
<< std::endl
;
123 d_str
.eqNotifyDisequal(t1
, t2
, reason
);
125 };/* class TheoryStrings::NotifyClass */
135 CVC4::Rational RMAXINT
;
136 unsigned d_card_size
;
138 Node
getRepresentative( Node t
);
139 bool hasTerm( Node a
);
140 bool areEqual( Node a
, Node b
);
141 bool areDisequal( Node a
, Node b
);
142 // t is representative, te = t, add lt = te to explanation exp
143 Node
getLengthExp( Node t
, std::vector
< Node
>& exp
, Node te
);
144 Node
getLength( Node t
, std::vector
< Node
>& exp
);
147 /** The notify class */
148 NotifyClass d_notify
;
149 /** Equaltity engine */
150 eq::EqualityEngine d_equalityEngine
;
151 /** Are we in conflict */
152 context::CDO
<bool> d_conflict
;
153 //list of pairs of nodes to merge
154 std::map
< Node
, Node
> d_pending_exp
;
155 std::vector
< Node
> d_pending
;
156 std::vector
< Node
> d_lemma_cache
;
157 std::map
< Node
, bool > d_pending_req_phase
;
158 /** inferences: maintained to ensure ref count for internally introduced nodes */
160 NodeList d_infer_exp
;
162 std::map
< Node
, Node
> d_normal_forms_base
;
163 std::map
< Node
, std::vector
< Node
> > d_normal_forms
;
164 std::map
< Node
, std::vector
< Node
> > d_normal_forms_exp
;
165 std::map
< Node
, std::map
< Node
, std::map
< bool, int > > > d_normal_forms_exp_depend
;
166 //map of pairs of terms that have the same normal form
167 NodeIntMap d_nf_pairs
;
168 std::map
< Node
, std::vector
< Node
> > d_nf_pairs_data
;
169 void addNormalFormPair( Node n1
, Node n2
);
170 bool isNormalFormPair( Node n1
, Node n2
);
171 bool isNormalFormPair2( Node n1
, Node n2
);
173 NodeSet d_loop_antec
;
174 NodeSet d_length_intro_vars
;
176 NodeSet d_pregistered_terms_cache
;
177 NodeSet d_registered_terms_cache
;
179 StringsPreprocess d_preproc
;
180 NodeBoolMap d_preproc_cache
;
181 // extended functions inferences cache
182 NodeSet d_extf_infer_cache
;
183 NodeSet d_extf_infer_cache_u
;
184 std::vector
< Node
> d_empty_vec
;
186 NodeList d_ee_disequalities
;
189 std::map
< Node
, Node
> d_eqc_to_const
;
190 std::map
< Node
, Node
> d_eqc_to_const_base
;
191 std::map
< Node
, Node
> d_eqc_to_const_exp
;
192 Node
getConstantEqc( Node eqc
);
194 std::map
< Node
, Node
> d_eqc_to_len_term
;
195 std::vector
< Node
> d_strings_eqc
;
196 Node d_emptyString_r
;
200 std::map
< TNode
, TermIndex
> d_children
;
201 Node
add( TNode n
, unsigned index
, TheoryStrings
* t
, Node er
, std::vector
< Node
>& c
);
202 void clear(){ d_children
.clear(); }
204 std::map
< Kind
, TermIndex
> d_term_index
;
205 //list of non-congruent concat terms in each eqc
206 std::map
< Node
, std::vector
< Node
> > d_eqc
;
207 std::map
< Node
, std::vector
< Node
> > d_flat_form
;
208 std::map
< Node
, std::vector
< int > > d_flat_form_index
;
210 void debugPrintFlatForms( const char * tc
);
211 void debugPrintNormalForms( const char * tc
);
212 /////////////////////////////////////////////////////////////////////////////
214 /////////////////////////////////////////////////////////////////////////////
216 void collectModelInfo(TheoryModel
* m
, bool fullModel
);
218 /////////////////////////////////////////////////////////////////////////////
220 /////////////////////////////////////////////////////////////////////////////
225 /////////////////////////////////////////////////////////////////////////////
227 /////////////////////////////////////////////////////////////////////////////
229 void addSharedTerm(TNode n
);
230 EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
235 EqcInfo( context::Context
* c
);
237 //constant in this eqc
238 context::CDO
< Node
> d_const_term
;
239 context::CDO
< Node
> d_length_term
;
240 context::CDO
< unsigned > d_cardinality_lem_k
;
241 // 1 = added length lemma
242 context::CDO
< Node
> d_normalized_length
;
244 /** map from representatives to information necessary for equivalence classes */
245 std::map
< Node
, EqcInfo
* > d_eqc_info
;
246 EqcInfo
* getOrMakeEqcInfo( Node eqc
, bool doMake
= true );
247 //maintain which concat terms have the length lemma instantiated
248 NodeNodeMap d_proxy_var
;
249 NodeNodeMap d_proxy_var_to_length
;
250 /** All the function terms that the theory has seen */
251 context::CDList
<TNode
> d_functionsTerms
;
253 //extended string terms, map to whether they are active
254 NodeBoolMap d_ext_func_terms
;
255 //any non-reduced extended functions exist
256 context::CDO
< bool > d_has_extf
;
257 // static information about extf
260 //all variables in this term
261 std::vector
< Node
> d_vars
;
263 // non-static information about extf
268 d_model_active
= true;
270 // list of terms that something (does not) contain and their explanation
271 std::map
< bool, std::vector
< Node
> > d_ctn
;
272 std::map
< bool, std::vector
< Node
> > d_ctn_from
;
276 std::vector
< Node
> d_exp
;
277 //reps -> list of variables
278 std::map
< Node
, std::vector
< Node
> > d_rep_vars
;
279 //false if it is reduced in the model
282 std::map
< Node
, ExtfInfo
> d_extf_info
;
283 std::map
< Node
, ExtfInfoTmp
> d_extf_info_tmp
;
284 //collect extended operator terms
285 void collectExtendedFuncTerms( Node n
, std::map
< Node
, bool >& visited
);
286 void addExtendedFuncTerm( Node n
);
293 std::vector
< Node
> d_ant
;
294 std::vector
< Node
> d_antn
;
295 std::vector
< Node
> d_non_emp_vars
;
298 std::map
< Node
, bool > d_pending_phase
;
299 const char * getId() {
301 case 1:return "S-Split(CST-P)-prop";break;
302 case 2:return "S-Split(VAR)-prop";break;
303 case 3:return "Len-Split(Len)";break;
304 case 4:return "Len-Split(Emp)";break;
305 case 5:return "S-Split(CST-P)-binary";break;
306 case 6:return "S-Split(CST-P)";break;
307 case 7:return "S-Split(VAR)";break;
308 case 8:return "F-Loop";break;
317 void checkConstantEquivalenceClasses( TermIndex
* ti
, std::vector
< Node
>& vecc
);
318 //extended functions evaluation check
319 void checkExtfEval( int effort
= 0 );
320 void checkExtfInference( Node n
, Node nr
, ExtfInfoTmp
& in
, int effort
);
321 void collectVars( Node n
, std::vector
< Node
>& vars
, std::map
< Node
, bool >& visited
);
322 Node
getSymbolicDefinition( Node n
, std::vector
< Node
>& exp
);
323 //check extf reduction
324 void checkExtfReductions( int effort
);
325 void checkExtfReduction( Node atom
, int pol
, int effort
);
327 void checkFlatForms();
328 Node
checkCycles( Node eqc
, std::vector
< Node
>& curr
, std::vector
< Node
>& exp
);
330 void checkNormalForms();
331 void normalizeEquivalenceClass( Node n
);
332 void getNormalForms( Node
&eqc
, std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
333 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
);
334 bool detectLoop(std::vector
< std::vector
< Node
> > &normal_forms
, int i
, int j
, int index
, int &loop_in_i
, int &loop_in_j
);
335 bool processLoop( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
336 int i
, int j
, int loop_n_index
, int other_n_index
,int loop_index
, int index
, InferInfo
& info
);
337 void processNEqc( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
338 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
);
339 void processReverseNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
340 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
341 unsigned i
, unsigned j
, unsigned& index
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
);
342 void processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
343 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
344 unsigned i
, unsigned j
, unsigned& index
, bool isRev
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
);
345 bool processDeq( Node n1
, Node n2
);
346 int processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
);
347 int processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
);
349 void getExplanationVectorForPrefix( std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
350 unsigned i
, int index
, bool isRev
, std::vector
< Node
>& curr_exp
);
351 void getExplanationVectorForPrefixEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
352 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
353 unsigned i
, unsigned j
, int index_i
, int index_j
, bool isRev
, std::vector
< Node
>& curr_exp
);
355 Node
collectConstantStringAt( std::vector
< Node
>& vec
, int& index
, bool isRev
);
357 //check membership constraints
358 Node
mkRegExpAntec(Node atom
, Node ant
);
359 Node
normalizeRegexp(Node r
);
360 bool normalizePosMemberships( std::map
< Node
, std::vector
< Node
> > &memb_with_exps
);
361 bool applyRConsume( CVC4::String
&s
, Node
&r
);
362 Node
applyRSplit( Node s1
, Node s2
, Node r
);
363 bool applyRLen( std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
);
364 bool checkMembershipsWithoutLength( std::map
< Node
, std::vector
< Node
> > &memb_with_exps
,
365 std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
);
366 void checkMemberships();
367 bool checkMemberships2();
368 bool checkPDerivative( Node x
, Node r
, Node atom
, bool &addedLemma
,
369 std::vector
< Node
> &processed
, std::vector
< Node
> &cprocessed
,
370 std::vector
< Node
> &nf_exp
);
372 void checkPosContains( std::vector
< Node
>& posContains
);
373 void checkNegContains( std::vector
< Node
>& negContains
);
374 //lengths normalize check
375 void checkLengthsEqc();
377 void checkCardinality();
380 void addCarePairs( quantifiers::TermArgTrie
* t1
, quantifiers::TermArgTrie
* t2
, unsigned arity
, unsigned depth
);
382 /** preregister term */
383 void preRegisterTerm(TNode n
);
384 /** Expand definition */
385 Node
expandDefinition(LogicRequest
&logicRequest
, Node n
);
386 /** Check at effort e */
387 void check(Effort e
);
388 /** needs check last effort */
389 bool needsCheckLastEffort();
390 /** Conflict when merging two constants */
391 void conflict(TNode a
, TNode b
);
392 /** called when a new equivalence class is created */
393 void eqNotifyNewClass(TNode t
);
394 /** called when two equivalence classes will merge */
395 void eqNotifyPreMerge(TNode t1
, TNode t2
);
396 /** called when two equivalence classes have merged */
397 void eqNotifyPostMerge(TNode t1
, TNode t2
);
398 /** called when two equivalence classes are made disequal */
399 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
400 /** get preprocess */
401 StringsPreprocess
* getPreprocess() { return &d_preproc
; }
403 /** compute care graph */
404 void computeCareGraph();
407 void assertPendingFact(Node atom
, bool polarity
, Node exp
);
408 void doPendingFacts();
409 void doPendingLemmas();
411 void addToExplanation( Node a
, Node b
, std::vector
< Node
>& exp
);
412 void addToExplanation( Node lit
, std::vector
< Node
>& exp
);
415 void registerTerm( Node n
, int effort
);
417 void sendInference( std::vector
< Node
>& exp
, std::vector
< Node
>& exp_n
, Node eq
, const char * c
, bool asLemma
= false );
418 void sendInference( std::vector
< Node
>& exp
, Node eq
, const char * c
, bool asLemma
= false );
419 void sendLemma( Node ant
, Node conc
, const char * c
);
420 void sendInfer( Node eq_exp
, Node eq
, const char * c
);
421 void sendSplit( Node a
, Node b
, const char * c
, bool preq
= true );
422 void sendLengthLemma( Node n
);
424 inline Node
mkConcat( Node n1
, Node n2
);
425 inline Node
mkConcat( Node n1
, Node n2
, Node n3
);
426 inline Node
mkConcat( const std::vector
< Node
>& c
);
427 inline Node
mkLength( Node n
);
440 std::map
< Node
, std::map
< Node
, std::map
< int, Node
> > > d_skolem_cache
;
441 NodeSet d_skolem_cache_ne_reg
;
442 Node
mkSkolemCached( Node a
, Node b
, int id
, const char * c
, int isLenSplit
= 0 );
443 inline Node
mkSkolemS(const char * c
, int isLenSplit
= 0);
444 void registerNonEmptySkolem( Node sk
);
445 //inline Node mkSkolemI(const char * c);
447 Node
mkExplain( std::vector
< Node
>& a
);
448 Node
mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
);
450 Node
mkAnd( std::vector
< Node
>& a
);
451 /** get concat vector */
452 void getConcatVec( Node n
, std::vector
< Node
>& c
);
454 //get equivalence classes
455 void getEquivalenceClasses( std::vector
< Node
>& eqcs
);
457 //separate into collections with equal length
458 void separateByLength( std::vector
< Node
>& n
, std::vector
< std::vector
< Node
> >& col
, std::vector
< Node
>& lts
);
459 void printConcat( std::vector
< Node
>& n
, const char * c
);
461 void inferSubstitutionProxyVars( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::vector
< Node
>& unproc
);
463 // Symbolic Regular Expression
465 // regular expression memberships
466 NodeList d_regexp_memberships
;
467 NodeSet d_regexp_ucached
;
468 NodeSet d_regexp_ccached
;
470 NodeIntMap d_pos_memberships
;
471 std::map
< Node
, std::vector
< Node
> > d_pos_memberships_data
;
472 NodeIntMap d_neg_memberships
;
473 std::map
< Node
, std::vector
< Node
> > d_neg_memberships_data
;
474 unsigned getNumMemberships( Node n
, bool isPos
);
475 Node
getMembership( Node n
, bool isPos
, unsigned i
);
476 // semi normal forms for symbolic expression
477 std::map
< Node
, Node
> d_nf_regexps
;
478 std::map
< Node
, std::vector
< Node
> > d_nf_regexps_exp
;
480 NodeNodeMap d_inter_cache
;
481 NodeIntMap d_inter_index
;
482 // processed memberships
483 NodeSet d_processed_memberships
;
484 // antecedant for why regexp membership must be true
485 NodeNodeMap d_regexp_ant
;
487 //std::map< Node, bool > d_membership_length;
488 // regular expression operations
489 RegExpOpr d_regexp_opr
;
491 CVC4::String
getHeadConst( Node x
);
492 bool deriveRegExp( Node x
, Node r
, Node ant
);
493 void addMembership(Node assertion
);
494 Node
getNormalString(Node x
, std::vector
<Node
> &nf_exp
);
495 Node
getNormalSymRegExp(Node r
, std::vector
<Node
> &nf_exp
);
498 // Finite Model Finding
500 NodeSet d_input_vars
;
501 context::CDO
< Node
> d_input_var_lsum
;
502 context::CDHashMap
< int, Node
> d_cardinality_lits
;
503 context::CDO
< int > d_curr_cardinality
;
505 //for finite model finding
506 Node
getNextDecisionRequest();
508 Node
ppRewrite(TNode atom
);
510 /** statistics class */
515 IntStat d_deq_splits
;
516 IntStat d_loop_lemmas
;
517 IntStat d_new_skolems
;
520 };/* class TheoryStrings::Statistics */
521 Statistics d_statistics
;
522 };/* class TheoryStrings */
524 }/* CVC4::theory::strings namespace */
525 }/* CVC4::theory namespace */
526 }/* CVC4 namespace */
528 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */