projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Remove unused code (#1700)
[cvc5.git] / src / theory / strings / theory_strings.cpp
1 /********************* */
2 /*! \file theory_strings.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tianyi Liang, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 Implementation of the theory of strings.
13 **
14 ** Implementation of the theory of strings.
15 **/
16
17 #include "theory/strings/theory_strings.h"
18
19 #include <cmath>
20
21 #include "expr/kind.h"
22 #include "options/strings_options.h"
23 #include "smt/logic_exception.h"
24 #include "smt/smt_statistics_registry.h"
25 #include "smt/command.h"
26 #include "theory/rewriter.h"
27 #include "theory/strings/theory_strings_rewriter.h"
28 #include "theory/strings/type_enumerator.h"
29 #include "theory/theory_model.h"
30 #include "theory/valuation.h"
31 #include "theory/quantifiers/term_database.h"
32
33 using namespace std;
34 using namespace CVC4::context;
35
36 namespace CVC4 {
37 namespace theory {
38 namespace strings {
39
40 std::ostream& operator<<(std::ostream& out, Inference i)
41 {
42 switch (i)
43 {
44 case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
45 case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
46 case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
47 case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
48 case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
49 case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
50 case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
51 case INFER_FLOOP: out << "F-Loop"; break;
52 default: out << "?"; break;
53 }
54 return out;
55 }
56
57 Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) {
58 if( index==n.getNumChildren() ){
59 if( d_data.isNull() ){
60 d_data = n;
61 }
62 return d_data;
63 }else{
64 Assert( index<n.getNumChildren() );
65 TNode nir = t->getRepresentative( n[index] );
66 //if it is empty, and doing CONCAT, ignore
67 if( nir==er && n.getKind()==kind::STRING_CONCAT ){
68 return add( n, index+1, t, er, c );
69 }else{
70 c.push_back( nir );
71 return d_children[nir].add( n, index+1, t, er, c );
72 }
73 }
74 }
75
76
77 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
78 OutputChannel& out, Valuation valuation,
79 const LogicInfo& logicInfo)
80 : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
81 RMAXINT(LONG_MAX),
82 d_notify( *this ),
83 d_equalityEngine(d_notify, c, "theory::strings", true),
84 d_conflict(c, false),
85 d_infer(c),
86 d_infer_exp(c),
87 d_nf_pairs(c),
88 d_pregistered_terms_cache(u),
89 d_registered_terms_cache(u),
90 d_length_lemma_terms_cache(u),
91 d_skolem_ne_reg_cache(u),
92 d_preproc(u),
93 d_preproc_cache(u),
94 d_extf_infer_cache(c),
95 d_extf_infer_cache_u(u),
96 d_ee_disequalities(c),
97 d_congruent(c),
98 d_proxy_var(u),
99 d_proxy_var_to_length(u),
100 d_functionsTerms(c),
101 d_has_extf(c, false ),
102 d_regexp_memberships(c),
103 d_regexp_ucached(u),
104 d_regexp_ccached(c),
105 d_pos_memberships(c),
106 d_neg_memberships(c),
107 d_inter_cache(c),
108 d_inter_index(c),
109 d_processed_memberships(c),
110 d_regexp_ant(c),
111 d_input_vars(u),
112 d_input_var_lsum(u),
113 d_cardinality_lits(u),
114 d_curr_cardinality(c, 0)
115 {
116 setupExtTheory();
117 getExtTheory()->addFunctionKind(kind::STRING_SUBSTR);
118 getExtTheory()->addFunctionKind(kind::STRING_STRIDOF);
119 getExtTheory()->addFunctionKind(kind::STRING_ITOS);
120 getExtTheory()->addFunctionKind(kind::STRING_STOI);
121 getExtTheory()->addFunctionKind(kind::STRING_STRREPL);
122 getExtTheory()->addFunctionKind(kind::STRING_STRCTN);
123 getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
124
125 // The kinds we are treating as function application in congruence
126 d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
127 d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
128 d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
129 if( options::stringLazyPreproc() ){
130 d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
131 d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
132 d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
133 d_equalityEngine.addFunctionKind(kind::STRING_STOI);
134 d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF);
135 d_equalityEngine.addFunctionKind(kind::STRING_STRREPL);
136 }
137
138 d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
139 d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
140 d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
141 std::vector< Node > nvec;
142 d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
143 d_true = NodeManager::currentNM()->mkConst( true );
144 d_false = NodeManager::currentNM()->mkConst( false );
145
146 d_card_size = 128;
147 }
148
149 TheoryStrings::~TheoryStrings() {
150 for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
151 delete it->second;
152 }
153 }
154
155 Node TheoryStrings::getRepresentative( Node t ) {
156 if( d_equalityEngine.hasTerm( t ) ){
157 return d_equalityEngine.getRepresentative( t );
158 }else{
159 return t;
160 }
161 }
162
163 bool TheoryStrings::hasTerm( Node a ){
164 return d_equalityEngine.hasTerm( a );
165 }
166
167 bool TheoryStrings::areEqual( Node a, Node b ){
168 if( a==b ){
169 return true;
170 }else if( hasTerm( a ) && hasTerm( b ) ){
171 return d_equalityEngine.areEqual( a, b );
172 }else{
173 return false;
174 }
175 }
176
177 bool TheoryStrings::areDisequal( Node a, Node b ){
178 if( a==b ){
179 return false;
180 }else{
181 if( hasTerm( a ) && hasTerm( b ) ) {
182 Node ar = d_equalityEngine.getRepresentative( a );
183 Node br = d_equalityEngine.getRepresentative( b );
184 return ( ar!=br && ar.isConst() && br.isConst() ) || d_equalityEngine.areDisequal( ar, br, false );
185 }else{
186 Node ar = getRepresentative( a );
187 Node br = getRepresentative( b );
188 return ar!=br && ar.isConst() && br.isConst();
189 }
190 }
191 }
192
193 bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
194 Assert( d_equalityEngine.hasTerm(x) );
195 Assert( d_equalityEngine.hasTerm(y) );
196 if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
197 TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
198 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
199 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
200 if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
201 return true;
202 }
203 }
204 return false;
205 }
206
207 Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ){
208 Assert( areEqual( t, te ) );
209 Node lt = mkLength( te );
210 if( hasTerm( lt ) ){
211 // use own length if it exists, leads to shorter explanation
212 return lt;
213 }else{
214 EqcInfo * ei = getOrMakeEqcInfo( t, false );
215 Node length_term = ei ? ei->d_length_term : Node::null();
216 if( length_term.isNull() ){
217 //typically shouldnt be necessary
218 length_term = t;
219 }
220 Debug("strings") << "TheoryStrings::getLengthTerm " << t << " is " << length_term << std::endl;
221 addToExplanation( length_term, te, exp );
222 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ) );
223 }
224 }
225
226 Node TheoryStrings::getLength( Node t, std::vector< Node >& exp ) {
227 return getLengthExp( t, exp, t );
228 }
229
230 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
231 d_equalityEngine.setMasterEqualityEngine(eq);
232 }
233
234 void TheoryStrings::addSharedTerm(TNode t) {
235 Debug("strings") << "TheoryStrings::addSharedTerm(): "
236 << t << " " << t.getType().isBoolean() << endl;
237 d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
238 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
239 }
240
241 EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
242 if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
243 if (d_equalityEngine.areEqual(a, b)) {
244 // The terms are implied to be equal
245 return EQUALITY_TRUE;
246 }
247 if (d_equalityEngine.areDisequal(a, b, false)) {
248 // The terms are implied to be dis-equal
249 return EQUALITY_FALSE;
250 }
251 }
252 return EQUALITY_UNKNOWN;
253 }
254
255 void TheoryStrings::propagate(Effort e) {
256 // direct propagation now
257 }
258
259 bool TheoryStrings::propagate(TNode literal) {
260 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl;
261 // If already in conflict, no more propagation
262 if (d_conflict) {
263 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
264 return false;
265 }
266 // Propagate out
267 bool ok = d_out->propagate(literal);
268 if (!ok) {
269 d_conflict = true;
270 }
271 return ok;
272 }
273
274 /** explain */
275 void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
276 Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl;
277 bool polarity = literal.getKind() != kind::NOT;
278 TNode atom = polarity ? literal : literal[0];
279 unsigned ps = assumptions.size();
280 std::vector< TNode > tassumptions;
281 if (atom.getKind() == kind::EQUAL) {
282 if( atom[0]!=atom[1] ){
283 Assert( hasTerm( atom[0] ) );
284 Assert( hasTerm( atom[1] ) );
285 d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
286 }
287 } else {
288 d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
289 }
290 for( unsigned i=0; i<tassumptions.size(); i++ ){
291 if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
292 assumptions.push_back( tassumptions[i] );
293 }
294 }
295 if (Debug.isOn("strings-explain-debug"))
296 {
297 Debug("strings-explain-debug") << "Explanation for " << literal << " was "
298 << std::endl;
299 for (unsigned i = ps; i < assumptions.size(); i++)
300 {
301 Debug("strings-explain-debug") << " " << assumptions[i] << std::endl;
302 }
303 }
304 }
305
306 Node TheoryStrings::explain( TNode literal ){
307 Debug("strings-explain") << "explain called on " << literal << std::endl;
308 std::vector< TNode > assumptions;
309 explain( literal, assumptions );
310 if( assumptions.empty() ){
311 return d_true;
312 }else if( assumptions.size()==1 ){
313 return assumptions[0];
314 }else{
315 return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
316 }
317 }
318
319 bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars,
320 std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
321 Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort << std::endl;
322 for( unsigned i=0; i<vars.size(); i++ ){
323 Node n = vars[i];
324 Trace("strings-subs") << " get subs for " << n << "..." << std::endl;
325 if( effort>=3 ){
326 //model values
327 Node mv = d_valuation.getModel()->getRepresentative( n );
328 Trace("strings-subs") << " model val : " << mv << std::endl;
329 subs.push_back( mv );
330 }else{
331 Node nr = getRepresentative( n );
332 std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
333 if( itc!=d_eqc_to_const.end() ){
334 //constant equivalence classes
335 Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] << " " << d_eqc_to_const_base[nr] << " " << nr << std::endl;
336 subs.push_back( itc->second );
337 if( !d_eqc_to_const_exp[nr].isNull() ){
338 exp[n].push_back( d_eqc_to_const_exp[nr] );
339 }
340 if( !d_eqc_to_const_base[nr].isNull() ){
341 addToExplanation( n, d_eqc_to_const_base[nr], exp[n] );
342 }
343 }else if( effort>=1 && effort<3 && n.getType().isString() ){
344 //normal forms
345 Node ns = getNormalString( d_normal_forms_base[nr], exp[n] );
346 subs.push_back( ns );
347 Trace("strings-subs") << " normal eqc : " << ns << " " << d_normal_forms_base[nr] << " " << nr << std::endl;
348 if( !d_normal_forms_base[nr].isNull() ) {
349 addToExplanation( n, d_normal_forms_base[nr], exp[n] );
350 }
351 }else{
352 //representative?
353 //Trace("strings-subs") << " representative : " << nr << std::endl;
354 //addToExplanation( n, nr, exp[n] );
355 //subs.push_back( nr );
356 subs.push_back( n );
357 }
358 }
359 }
360 return true;
361 }
362
363 int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
364 //determine the effort level to process the extf at
365 // 0 - at assertion time, 1+ - after no other reduction is applicable
366 Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
367 if( d_extf_info_tmp[n].d_model_active ){
368 int r_effort = -1;
369 int pol = d_extf_info_tmp[n].d_pol;
370 if( n.getKind()==kind::STRING_STRCTN ){
371 if( pol==1 ){
372 r_effort = 1;
373 }else if( pol==-1 ){
374 if( effort==2 ){
375 Node x = n[0];
376 Node s = n[1];
377 std::vector< Node > lexp;
378 Node lenx = getLength( x, lexp );
379 Node lens = getLength( s, lexp );
380 if( areEqual( lenx, lens ) ){
381 Trace("strings-extf-debug") << " resolve extf : " << n << " based on equal lengths disequality." << std::endl;
382 //we can reduce to disequality when lengths are equal
383 if( !areDisequal( x, s ) ){
384 lexp.push_back( lenx.eqNode(lens) );
385 lexp.push_back( n.negate() );
386 Node xneqs = x.eqNode(s).negate();
387 sendInference( lexp, xneqs, "NEG-CTN-EQL", true );
388 }
389 return 1;
390 }else if( !areDisequal( lenx, lens ) ){
391 //split on their lenths
392 sendSplit( lenx, lens, "NEG-CTN-SP" );
393 }else{
394 r_effort = 2;
395 }
396 }
397 }
398 }else{
399 if( options::stringLazyPreproc() ){
400 if( n.getKind()==kind::STRING_SUBSTR ){
401 r_effort = 1;
402 }else if( n.getKind()!=kind::STRING_IN_REGEXP ){
403 r_effort = 2;
404 }
405 }
406 }
407 if( effort==r_effort ){
408 Node c_n = pol==-1 ? n.negate() : n;
409 if( d_preproc_cache.find( c_n )==d_preproc_cache.end() ){
410 d_preproc_cache[ c_n ] = true;
411 Trace("strings-process-debug") << "Process reduction for " << n << ", pol = " << pol << std::endl;
412 if( n.getKind()==kind::STRING_STRCTN && pol==1 ){
413 Node x = n[0];
414 Node s = n[1];
415 //positive contains reduces to a equality
416 Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" );
417 Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" );
418 Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
419 std::vector< Node > exp_vec;
420 exp_vec.push_back( n );
421 sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
422 //we've reduced this n
423 Trace("strings-extf-debug") << " resolve extf : " << n << " based on positive contain reduction." << std::endl;
424 return 1;
425 }else{
426 // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
427 // STRING_STRIDOF, STRING_ITOS, STRING_STOI, STRING_STRREPL
428 std::vector< Node > new_nodes;
429 Node res = d_preproc.simplify( n, new_nodes );
430 Assert( res!=n );
431 new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, res, n ) );
432 Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
433 nnlem = Rewriter::rewrite( nnlem );
434 Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
435 Trace("strings-red-lemma") << "...from " << n << std::endl;
436 sendInference( d_empty_vec, nnlem, "Reduction", true );
437 //we've reduced this n
438 Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl;
439 return 1;
440 }
441 }else{
442 return 1;
443 }
444 }
445 }
446 return 0;
447 }
448
449 /////////////////////////////////////////////////////////////////////////////
450 // NOTIFICATIONS
451 /////////////////////////////////////////////////////////////////////////////
452
453
454 void TheoryStrings::presolve() {
455 Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
456
457 if(!options::stdASCII()) {
458 d_card_size = 256;
459 }
460 }
461
462
463 /////////////////////////////////////////////////////////////////////////////
464 // MODEL GENERATION
465 /////////////////////////////////////////////////////////////////////////////
466
467 bool TheoryStrings::collectModelInfo(TheoryModel* m)
468 {
469 Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
470 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
471
472 //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings.
473 // change this if we generalize to sequences.
474 //set<Node> termSet;
475 // Compute terms appearing in assertions and shared terms
476 //computeRelevantTerms(termSet);
477 //m->assertEqualityEngine( &d_equalityEngine, &termSet );
478
479 if (!m->assertEqualityEngine(&d_equalityEngine))
480 {
481 return false;
482 }
483
484 // Generate model
485 std::vector< Node > nodes;
486 getEquivalenceClasses( nodes );
487 std::map< Node, Node > processed;
488 std::vector< std::vector< Node > > col;
489 std::vector< Node > lts;
490 separateByLength( nodes, col, lts );
491 //step 1 : get all values for known lengths
492 std::vector< Node > lts_values;
493 std::map< unsigned, bool > values_used;
494 for( unsigned i=0; i<col.size(); i++ ) {
495 Trace("strings-model") << "Checking length for {";
496 for( unsigned j=0; j<col[i].size(); j++ ) {
497 if( j>0 ) {
498 Trace("strings-model") << ", ";
499 }
500 Trace("strings-model") << col[i][j];
501 }
502 Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
503 if( lts[i].isConst() ) {
504 lts_values.push_back( lts[i] );
505 Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
506 unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
507 values_used[ lvalue ] = true;
508 }else{
509 //get value for lts[i];
510 if( !lts[i].isNull() ){
511 Node v = d_valuation.getModelValue(lts[i]);
512 Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
513 lts_values.push_back( v );
514 Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
515 unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt();
516 values_used[ lvalue ] = true;
517 }else{
518 //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
519 //Assert( false );
520 lts_values.push_back( Node::null() );
521 }
522 }
523 }
524 ////step 2 : assign arbitrary values for unknown lengths?
525 // confirmed by calculus invariant, see paper
526 Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
527 //step 3 : assign values to equivalence classes that are pure variables
528 for( unsigned i=0; i<col.size(); i++ ){
529 std::vector< Node > pure_eq;
530 Trace("strings-model") << "The equivalence classes ";
531 for( unsigned j=0; j<col[i].size(); j++ ) {
532 Trace("strings-model") << col[i][j] << " ";
533 //check if col[i][j] has only variables
534 if( !col[i][j].isConst() ){
535 Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
536 if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
537 pure_eq.push_back( col[i][j] );
538 }
539 }else{
540 processed[col[i][j]] = col[i][j];
541 }
542 }
543 Trace("strings-model") << "have length " << lts_values[i] << std::endl;
544
545 //assign a new length if necessary
546 if( !pure_eq.empty() ){
547 if( lts_values[i].isNull() ){
548 unsigned lvalue = 0;
549 while( values_used.find( lvalue )!=values_used.end() ){
550 lvalue++;
551 }
552 Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
553 lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
554 values_used[ lvalue ] = true;
555 }
556 Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
557 for( unsigned j=0; j<pure_eq.size(); j++ ){
558 Trace("strings-model") << pure_eq[j] << " ";
559 }
560 Trace("strings-model") << std::endl;
561
562
563 //use type enumerator
564 Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
565 StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
566 for( unsigned j=0; j<pure_eq.size(); j++ ){
567 Assert( !sel.isFinished() );
568 Node c = *sel;
569 while( d_equalityEngine.hasTerm( c ) ){
570 ++sel;
571 Assert( !sel.isFinished() );
572 c = *sel;
573 }
574 ++sel;
575 Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
576 processed[pure_eq[j]] = c;
577 if (!m->assertEquality(pure_eq[j], c, true))
578 {
579 return false;
580 }
581 }
582 }
583 }
584 Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
585 //step 4 : assign constants to all other equivalence classes
586 for( unsigned i=0; i<nodes.size(); i++ ){
587 if( processed.find( nodes[i] )==processed.end() ){
588 Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
589 Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
590 for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
591 if( j>0 ) Trace("strings-model") << " ++ ";
592 Trace("strings-model") << d_normal_forms[nodes[i]][j];
593 Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
594 if( !r.isConst() && processed.find( r )==processed.end() ){
595 Trace("strings-model") << "(UNPROCESSED)";
596 }
597 }
598 Trace("strings-model") << std::endl;
599 std::vector< Node > nc;
600 for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
601 Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
602 Assert( r.isConst() || processed.find( r )!=processed.end() );
603 nc.push_back(r.isConst() ? r : processed[r]);
604 }
605 Node cc = mkConcat( nc );
606 Assert( cc.getKind()==kind::CONST_STRING );
607 Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
608 processed[nodes[i]] = cc;
609 if (!m->assertEquality(nodes[i], cc, true))
610 {
611 return false;
612 }
613 }
614 }
615 //Trace("strings-model") << "String Model : Assigned." << std::endl;
616 Trace("strings-model") << "String Model : Finished." << std::endl;
617 return true;
618 }
619
620 /////////////////////////////////////////////////////////////////////////////
621 // MAIN SOLVER
622 /////////////////////////////////////////////////////////////////////////////
623
624
625 void TheoryStrings::preRegisterTerm(TNode n) {
626 if( d_pregistered_terms_cache.find(n) == d_pregistered_terms_cache.end() ) {
627 d_pregistered_terms_cache.insert(n);
628 //check for logic exceptions
629 if( !options::stringExp() ){
630 if( n.getKind()==kind::STRING_STRIDOF ||
631 n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_STOI ||
632 n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
633 std::stringstream ss;
634 ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp";
635 throw LogicException(ss.str());
636 }
637 }
638 switch( n.getKind() ) {
639 case kind::EQUAL: {
640 d_equalityEngine.addTriggerEquality(n);
641 break;
642 }
643 case kind::STRING_IN_REGEXP: {
644 d_out->requirePhase(n, true);
645 d_equalityEngine.addTriggerPredicate(n);
646 d_equalityEngine.addTerm(n[0]);
647 d_equalityEngine.addTerm(n[1]);
648 break;
649 }
650 default: {
651 TypeNode tn = n.getType();
652 if( tn.isString() ) {
653 registerTerm( n, 0 );
654 // FMF
655 if( n.getKind() == kind::VARIABLE && options::stringFMF() ){
656 d_input_vars.insert(n);
657 }
658 d_equalityEngine.addTerm(n);
659 } else if (tn.isBoolean()) {
660 // Get triggered for both equal and dis-equal
661 d_equalityEngine.addTriggerPredicate(n);
662 } else {
663 // Function applications/predicates
664 d_equalityEngine.addTerm(n);
665 if( options::stringExp() ){
666 //collect extended functions here: some may not be asserted to strings (such as those with return type Int),
667 // but we need to record them so they are treated properly
668 getExtTheory()->registerTermRec( n );
669 }
670 }
671 //concat terms do not contribute to theory combination? TODO: verify
672 if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){
673 d_functionsTerms.push_back( n );
674 }
675 }
676 }
677 }
678 }
679
680 Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
681 Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
682 return node;
683 }
684
685
686 void TheoryStrings::check(Effort e) {
687 if (done() && e<EFFORT_FULL) {
688 return;
689 }
690
691 TimerStat::CodeTimer checkTimer(d_checkTime);
692
693 bool polarity;
694 TNode atom;
695
696 if( !done() && !hasTerm( d_emptyString ) ) {
697 preRegisterTerm( d_emptyString );
698 }
699
700 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
701 Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
702 while ( !done() && !d_conflict ) {
703 // Get all the assertions
704 Assertion assertion = get();
705 TNode fact = assertion.assertion;
706
707 Trace("strings-assertion") << "get assertion: " << fact << endl;
708 polarity = fact.getKind() != kind::NOT;
709 atom = polarity ? fact : fact[0];
710
711 //assert pending fact
712 assertPendingFact( atom, polarity, fact );
713 }
714 doPendingFacts();
715
716 if( !d_conflict && ( ( e == EFFORT_FULL && !d_valuation.needCheck() ) || ( e==EFFORT_STANDARD && options::stringEager() ) ) ) {
717 Trace("strings-check") << "Theory of strings full effort check " << std::endl;
718
719 if(Trace.isOn("strings-eqc")) {
720 for( unsigned t=0; t<2; t++ ) {
721 eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
722 Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
723 while( !eqcs2_i.isFinished() ){
724 Node eqc = (*eqcs2_i);
725 bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
726 if (print) {
727 eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
728 Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
729 while( !eqc2_i.isFinished() ) {
730 if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){
731 Trace("strings-eqc") << (*eqc2_i) << " ";
732 }
733 ++eqc2_i;
734 }
735 Trace("strings-eqc") << " } " << std::endl;
736 EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
737 if( ei ){
738 Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
739 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
740 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
741 }
742 }
743 ++eqcs2_i;
744 }
745 Trace("strings-eqc") << std::endl;
746 }
747 Trace("strings-eqc") << std::endl;
748 }
749
750 bool addedLemma = false;
751 bool addedFact;
752 do{
753 Trace("strings-process") << "----check, next round---" << std::endl;
754 checkInit();
755 Trace("strings-process") << "Done check init, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
756 if( !hasProcessed() ){
757 checkExtfEval();
758 Trace("strings-process") << "Done check extended functions eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
759 if( !hasProcessed() ){
760 checkFlatForms();
761 Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
762 if( !hasProcessed() && e==EFFORT_FULL ){
763 checkNormalForms();
764 Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
765 if( !hasProcessed() ){
766 if( options::stringEagerLen() ){
767 checkLengthsEqc();
768 Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
769 }
770 if( !hasProcessed() ){
771 if( options::stringExp() && !options::stringGuessModel() ){
772 checkExtfReductions( 2 );
773 Trace("strings-process") << "Done check extended functions reduction 2, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
774 }
775 if( !hasProcessed() ){
776 checkMemberships();
777 Trace("strings-process") << "Done check memberships, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
778 if( !hasProcessed() ){
779 checkCardinality();
780 Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
781 }
782 }
783 }
784 }
785 }
786 }
787 }
788 //flush the facts
789 addedFact = !d_pending.empty();
790 addedLemma = !d_lemma_cache.empty();
791 doPendingFacts();
792 doPendingLemmas();
793 }while( !d_conflict && !addedLemma && addedFact );
794
795 Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_conflict << std::endl;
796 }else if( e==EFFORT_LAST_CALL ){
797 Assert( !hasProcessed() );
798 Trace("strings-check") << "Theory of strings last call effort check " << std::endl;
799 checkExtfEval( 3 );
800 checkExtfReductions( 2 );
801 doPendingFacts();
802 doPendingLemmas();
803 Trace("strings-process") << "Done check extended functions reduction 2, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
804 }
805 Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
806 Assert( d_pending.empty() );
807 Assert( d_lemma_cache.empty() );
808 }
809
810 bool TheoryStrings::needsCheckLastEffort() {
811 if( options::stringGuessModel() ){
812 return d_has_extf.get();
813 }else{
814 return false;
815 }
816 }
817
818 void TheoryStrings::checkExtfReductions( int effort ) {
819 //standardize this?
820 //std::vector< Node > nred;
821 //getExtTheory()->doReductions( effort, nred, false );
822
823 std::vector< Node > extf = getExtTheory()->getActive();
824 Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl;
825 for( unsigned i=0; i<extf.size(); i++ ){
826 Node n = extf[i];
827 Trace("strings-process") << "Check " << n << ", active in model=" << d_extf_info_tmp[n].d_model_active << std::endl;
828 Node nr;
829 int ret = getReduction( effort, n, nr );
830 Assert( nr.isNull() );
831 if( ret!=0 ){
832 getExtTheory()->markReduced( extf[i] );
833 if( options::stringOpt1() && hasProcessed() ){
834 return;
835 }
836 }
837 }
838 }
839
840 TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
841
842 }
843
844 TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) {
845 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc );
846 if( eqc_i==d_eqc_info.end() ){
847 if( doMake ){
848 EqcInfo* ei = new EqcInfo( getSatContext() );
849 d_eqc_info[eqc] = ei;
850 return ei;
851 }else{
852 return NULL;
853 }
854 }else{
855 return (*eqc_i).second;
856 }
857 }
858
859
860 /** Conflict when merging two constants */
861 void TheoryStrings::conflict(TNode a, TNode b){
862 if( !d_conflict ){
863 Debug("strings-conflict") << "Making conflict..." << std::endl;
864 d_conflict = true;
865 Node conflictNode;
866 conflictNode = explain( a.eqNode(b) );
867 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
868 d_out->conflict( conflictNode );
869 }
870 }
871
872 /** called when a new equivalance class is created */
873 void TheoryStrings::eqNotifyNewClass(TNode t){
874 if( t.getKind() == kind::STRING_LENGTH ){
875 Trace("strings-debug") << "New length eqc : " << t << std::endl;
876 Node r = d_equalityEngine.getRepresentative(t[0]);
877 EqcInfo * ei = getOrMakeEqcInfo( r, true );
878 ei->d_length_term = t[0];
879 //we care about the length of this string
880 registerTerm( t[0], 1 );
881 }else{
882 //getExtTheory()->registerTerm( t );
883 }
884 }
885
886 /** called when two equivalance classes will merge */
887 void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
888 EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
889 if( e2 ){
890 EqcInfo * e1 = getOrMakeEqcInfo( t1 );
891 //add information from e2 to e1
892 if( !e2->d_length_term.get().isNull() ){
893 e1->d_length_term.set( e2->d_length_term );
894 }
895 if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
896 e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
897 }
898 if( !e2->d_normalized_length.get().isNull() ){
899 e1->d_normalized_length.set( e2->d_normalized_length );
900 }
901 }
902 }
903
904 /** called when two equivalance classes have merged */
905 void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) {
906
907 }
908
909 /** called when two equivalance classes are disequal */
910 void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
911 if( t1.getType().isString() ){
912 //store disequalities between strings, may need to check if their lengths are equal/disequal
913 d_ee_disequalities.push_back( t1.eqNode( t2 ) );
914 }
915 }
916
917 void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) {
918 if( depth==arity ){
919 if( t2!=NULL ){
920 Node f1 = t1->getNodeData();
921 Node f2 = t2->getNodeData();
922 if( !d_equalityEngine.areEqual( f1, f2 ) ){
923 Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
924 vector< pair<TNode, TNode> > currentPairs;
925 for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
926 TNode x = f1[k];
927 TNode y = f2[k];
928 Assert( d_equalityEngine.hasTerm(x) );
929 Assert( d_equalityEngine.hasTerm(y) );
930 Assert( !d_equalityEngine.areDisequal( x, y, false ) );
931 Assert( !areCareDisequal( x, y ) );
932 if( !d_equalityEngine.areEqual( x, y ) ){
933 if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
934 TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
935 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
936 currentPairs.push_back(make_pair(x_shared, y_shared));
937 }
938 }
939 }
940 for (unsigned c = 0; c < currentPairs.size(); ++ c) {
941 Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
942 addCarePair(currentPairs[c].first, currentPairs[c].second);
943 }
944 }
945 }
946 }else{
947 if( t2==NULL ){
948 if( depth<(arity-1) ){
949 //add care pairs internal to each child
950 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
951 addCarePairs( &it->second, NULL, arity, depth+1 );
952 }
953 }
954 //add care pairs based on each pair of non-disequal arguments
955 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
956 std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
957 ++it2;
958 for( ; it2 != t1->d_data.end(); ++it2 ){
959 if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
960 if( !areCareDisequal(it->first, it2->first) ){
961 addCarePairs( &it->second, &it2->second, arity, depth+1 );
962 }
963 }
964 }
965 }
966 }else{
967 //add care pairs based on product of indices, non-disequal arguments
968 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
969 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
970 if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
971 if( !areCareDisequal(it->first, it2->first) ){
972 addCarePairs( &it->second, &it2->second, arity, depth+1 );
973 }
974 }
975 }
976 }
977 }
978 }
979 }
980
981 void TheoryStrings::computeCareGraph(){
982 //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
983 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
984 std::map< Node, quantifiers::TermArgTrie > index;
985 std::map< Node, unsigned > arity;
986 unsigned functionTerms = d_functionsTerms.size();
987 for (unsigned i = 0; i < functionTerms; ++ i) {
988 TNode f1 = d_functionsTerms[i];
989 Trace("strings-cg") << "...build for " << f1 << std::endl;
990 Node op = f1.getOperator();
991 std::vector< TNode > reps;
992 bool has_trigger_arg = false;
993 for( unsigned j=0; j<f1.getNumChildren(); j++ ){
994 reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
995 if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_STRINGS ) ){
996 has_trigger_arg = true;
997 }
998 }
999 if( has_trigger_arg ){
1000 index[op].addTerm( f1, reps );
1001 arity[op] = reps.size();
1002 }
1003 }
1004 //for each index
1005 for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
1006 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
1007 addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
1008 }
1009 }
1010
1011 void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
1012 Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
1013 Assert(atom.getKind() != kind::OR, "Infer error: a split.");
1014 if( atom.getKind()==kind::EQUAL ){
1015 Trace("strings-pending-debug") << " Register term" << std::endl;
1016 for( unsigned j=0; j<2; j++ ) {
1017 if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
1018 registerTerm( atom[j], 0 );
1019 }
1020 }
1021 Trace("strings-pending-debug") << " Now assert equality" << std::endl;
1022 d_equalityEngine.assertEquality( atom, polarity, exp );
1023 Trace("strings-pending-debug") << " Finished assert equality" << std::endl;
1024 } else {
1025 d_equalityEngine.assertPredicate( atom, polarity, exp );
1026 //process extf
1027 if( atom.getKind()==kind::STRING_IN_REGEXP ){
1028 if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){
1029 if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){
1030 d_extf_infer_cache_u.insert( atom );
1031 //length of first argument is one
1032 Node conc = d_one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[0] ) );
1033 Node lem = NodeManager::currentNM()->mkNode( kind::OR, atom.negate(), conc );
1034 Trace("strings-lemma") << "Strings::Lemma RE-Range-Len : " << lem << std::endl;
1035 d_out->lemma( lem );
1036 }
1037 }
1038 }
1039 //register the atom here, since it may not create a new equivalence class
1040 //getExtTheory()->registerTerm( atom );
1041 }
1042 Trace("strings-pending-debug") << " Now collect terms" << std::endl;
1043 //collect extended function terms in the atom
1044 getExtTheory()->registerTermRec( atom );
1045 Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
1046 }
1047
1048 void TheoryStrings::doPendingFacts() {
1049 size_t i=0;
1050 while( !d_conflict && i<d_pending.size() ) {
1051 Node fact = d_pending[i];
1052 Node exp = d_pending_exp[ fact ];
1053 if(fact.getKind() == kind::AND) {
1054 for(size_t j=0; j<fact.getNumChildren(); j++) {
1055 bool polarity = fact[j].getKind() != kind::NOT;
1056 TNode atom = polarity ? fact[j] : fact[j][0];
1057 assertPendingFact(atom, polarity, exp);
1058 }
1059 } else {
1060 bool polarity = fact.getKind() != kind::NOT;
1061 TNode atom = polarity ? fact : fact[0];
1062 assertPendingFact(atom, polarity, exp);
1063 }
1064 i++;
1065 }
1066 d_pending.clear();
1067 d_pending_exp.clear();
1068 }
1069
1070 void TheoryStrings::doPendingLemmas() {
1071 if( !d_conflict && !d_lemma_cache.empty() ){
1072 for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
1073 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
1074 d_out->lemma( d_lemma_cache[i] );
1075 }
1076 for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
1077 Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
1078 d_out->requirePhase( it->first, it->second );
1079 }
1080 }
1081 d_lemma_cache.clear();
1082 d_pending_req_phase.clear();
1083 }
1084
1085 bool TheoryStrings::hasProcessed() {
1086 return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
1087 }
1088
1089 void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
1090 if( a!=b ){
1091 Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
1092 Assert( areEqual( a, b ) );
1093 exp.push_back( a.eqNode( b ) );
1094 }
1095 }
1096
1097 void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
1098 if( !lit.isNull() ){
1099 exp.push_back( lit );
1100 }
1101 }
1102
1103 void TheoryStrings::checkInit() {
1104 //build term index
1105 d_eqc_to_const.clear();
1106 d_eqc_to_const_base.clear();
1107 d_eqc_to_const_exp.clear();
1108 d_eqc_to_len_term.clear();
1109 d_term_index.clear();
1110 d_strings_eqc.clear();
1111
1112 std::map< Kind, unsigned > ncongruent;
1113 std::map< Kind, unsigned > congruent;
1114 d_emptyString_r = getRepresentative( d_emptyString );
1115 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1116 while( !eqcs_i.isFinished() ){
1117 Node eqc = (*eqcs_i);
1118 TypeNode tn = eqc.getType();
1119 if( !tn.isRegExp() ){
1120 if( tn.isString() ){
1121 d_strings_eqc.push_back( eqc );
1122 }
1123 Node var;
1124 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1125 while( !eqc_i.isFinished() ) {
1126 Node n = *eqc_i;
1127 if( n.isConst() ){
1128 d_eqc_to_const[eqc] = n;
1129 d_eqc_to_const_base[eqc] = n;
1130 d_eqc_to_const_exp[eqc] = Node::null();
1131 }else if( tn.isInteger() ){
1132 if( n.getKind()==kind::STRING_LENGTH ){
1133 Node nr = getRepresentative( n[0] );
1134 d_eqc_to_len_term[nr] = n[0];
1135 }
1136 }else if( n.getNumChildren()>0 ){
1137 Kind k = n.getKind();
1138 if( k!=kind::EQUAL ){
1139 if( d_congruent.find( n )==d_congruent.end() ){
1140 std::vector< Node > c;
1141 Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c );
1142 if( nc!=n ){
1143 //check if we have inferred a new equality by removal of empty components
1144 if( n.getKind()==kind::STRING_CONCAT && !areEqual( nc, n ) ){
1145 std::vector< Node > exp;
1146 unsigned count[2] = { 0, 0 };
1147 while( count[0]<nc.getNumChildren() || count[1]<n.getNumChildren() ){
1148 //explain empty prefixes
1149 for( unsigned t=0; t<2; t++ ){
1150 Node nn = t==0 ? nc : n;
1151 while( count[t]<nn.getNumChildren() &&
1152 ( nn[count[t]]==d_emptyString || areEqual( nn[count[t]], d_emptyString ) ) ){
1153 if( nn[count[t]]!=d_emptyString ){
1154 exp.push_back( nn[count[t]].eqNode( d_emptyString ) );
1155 }
1156 count[t]++;
1157 }
1158 }
1159 //explain equal components
1160 if( count[0]<nc.getNumChildren() ){
1161 Assert( count[1]<n.getNumChildren() );
1162 if( nc[count[0]]!=n[count[1]] ){
1163 exp.push_back( nc[count[0]].eqNode( n[count[1]] ) );
1164 }
1165 count[0]++;
1166 count[1]++;
1167 }
1168 }
1169 //infer the equality
1170 sendInference( exp, n.eqNode( nc ), "I_Norm" );
1171 }else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){
1172 //mark as congruent : only process if neither has been reduced
1173 getExtTheory()->markCongruent( nc, n );
1174 }
1175 //this node is congruent to another one, we can ignore it
1176 Trace("strings-process-debug") << " congruent term : " << n << std::endl;
1177 d_congruent.insert( n );
1178 congruent[k]++;
1179 }else if( k==kind::STRING_CONCAT && c.size()==1 ){
1180 Trace("strings-process-debug") << " congruent term by singular : " << n << " " << c[0] << std::endl;
1181 //singular case
1182 if( !areEqual( c[0], n ) ){
1183 std::vector< Node > exp;
1184 //explain empty components
1185 bool foundNEmpty = false;
1186 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1187 if( areEqual( n[i], d_emptyString ) ){
1188 if( n[i]!=d_emptyString ){
1189 exp.push_back( n[i].eqNode( d_emptyString ) );
1190 }
1191 }else{
1192 Assert( !foundNEmpty );
1193 if( n[i]!=c[0] ){
1194 exp.push_back( n[i].eqNode( c[0] ) );
1195 }
1196 foundNEmpty = true;
1197 }
1198 }
1199 AlwaysAssert( foundNEmpty );
1200 //infer the equality
1201 sendInference( exp, n.eqNode( c[0] ), "I_Norm_S" );
1202 }
1203 d_congruent.insert( n );
1204 congruent[k]++;
1205 }else{
1206 ncongruent[k]++;
1207 }
1208 }else{
1209 congruent[k]++;
1210 }
1211 }
1212 }else{
1213 if( d_congruent.find( n )==d_congruent.end() ){
1214 if( var.isNull() ){
1215 var = n;
1216 }else{
1217 Trace("strings-process-debug") << " congruent variable : " << n << std::endl;
1218 d_congruent.insert( n );
1219 }
1220 }
1221 }
1222 ++eqc_i;
1223 }
1224 }
1225 ++eqcs_i;
1226 }
1227 if( Trace.isOn("strings-process") ){
1228 for( std::map< Kind, TermIndex >::iterator it = d_term_index.begin(); it != d_term_index.end(); ++it ){
1229 Trace("strings-process") << " Terms[" << it->first << "] = " << ncongruent[it->first] << "/" << (congruent[it->first]+ncongruent[it->first]) << std::endl;
1230 }
1231 }
1232 Trace("strings-process") << "Done check init, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
1233 //now, infer constants for equivalence classes
1234 if( !hasProcessed() ){
1235 //do fixed point
1236 unsigned prevSize;
1237 do{
1238 Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl;
1239 prevSize = d_eqc_to_const.size();
1240 std::vector< Node > vecc;
1241 checkConstantEquivalenceClasses( &d_term_index[kind::STRING_CONCAT], vecc );
1242 }while( !hasProcessed() && d_eqc_to_const.size()>prevSize );
1243 Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
1244 }
1245 }
1246
1247 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
1248 Node n = ti->d_data;
1249 if( !n.isNull() ){
1250 //construct the constant
1251 Node c = mkConcat( vecc );
1252 if( !areEqual( n, c ) ){
1253 Trace("strings-debug") << "Constant eqc : " << c << " for " << n << std::endl;
1254 Trace("strings-debug") << " ";
1255 for( unsigned i=0; i<vecc.size(); i++ ){
1256 Trace("strings-debug") << vecc[i] << " ";
1257 }
1258 Trace("strings-debug") << std::endl;
1259 unsigned count = 0;
1260 unsigned countc = 0;
1261 std::vector< Node > exp;
1262 while( count<n.getNumChildren() ){
1263 while( count<n.getNumChildren() && areEqual( n[count], d_emptyString ) ){
1264 addToExplanation( n[count], d_emptyString, exp );
1265 count++;
1266 }
1267 if( count<n.getNumChildren() ){
1268 Trace("strings-debug") << "...explain " << n[count] << " " << vecc[countc] << std::endl;
1269 if( !areEqual( n[count], vecc[countc] ) ){
1270 Node nrr = getRepresentative( n[count] );
1271 Assert( !d_eqc_to_const_exp[nrr].isNull() );
1272 addToExplanation( n[count], d_eqc_to_const_base[nrr], exp );
1273 exp.push_back( d_eqc_to_const_exp[nrr] );
1274 }else{
1275 addToExplanation( n[count], vecc[countc], exp );
1276 }
1277 countc++;
1278 count++;
1279 }
1280 }
1281 //exp contains an explanation of n==c
1282 Assert( countc==vecc.size() );
1283 if( hasTerm( c ) ){
1284 sendInference( exp, n.eqNode( c ), "I_CONST_MERGE" );
1285 return;
1286 }else if( !hasProcessed() ){
1287 Node nr = getRepresentative( n );
1288 std::map< Node, Node >::iterator it = d_eqc_to_const.find( nr );
1289 if( it==d_eqc_to_const.end() ){
1290 Trace("strings-debug") << "Set eqc const " << n << " to " << c << std::endl;
1291 d_eqc_to_const[nr] = c;
1292 d_eqc_to_const_base[nr] = n;
1293 d_eqc_to_const_exp[nr] = mkAnd( exp );
1294 }else if( c!=it->second ){
1295 //conflict
1296 Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl;
1297 if( d_eqc_to_const_exp[nr].isNull() ){
1298 // n==c ^ n == c' => false
1299 addToExplanation( n, it->second, exp );
1300 }else{
1301 // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
1302 exp.push_back( d_eqc_to_const_exp[nr] );
1303 addToExplanation( n, d_eqc_to_const_base[nr], exp );
1304 }
1305 sendInference( exp, d_false, "I_CONST_CONFLICT" );
1306 return;
1307 }else{
1308 Trace("strings-debug") << "Duplicate constant." << std::endl;
1309 }
1310 }
1311 }
1312 }
1313 for( std::map< TNode, TermIndex >::iterator it = ti->d_children.begin(); it != ti->d_children.end(); ++it ){
1314 std::map< Node, Node >::iterator itc = d_eqc_to_const.find( it->first );
1315 if( itc!=d_eqc_to_const.end() ){
1316 vecc.push_back( itc->second );
1317 checkConstantEquivalenceClasses( &it->second, vecc );
1318 vecc.pop_back();
1319 if( hasProcessed() ){
1320 break;
1321 }
1322 }
1323 }
1324 }
1325
1326 void TheoryStrings::checkExtfEval( int effort ) {
1327 Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
1328 d_extf_info_tmp.clear();
1329 bool has_nreduce = false;
1330 std::vector< Node > terms = getExtTheory()->getActive();
1331 std::vector< Node > sterms;
1332 std::vector< std::vector< Node > > exp;
1333 getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp );
1334 for( unsigned i=0; i<terms.size(); i++ ){
1335 Node n = terms[i];
1336 Node sn = sterms[i];
1337 //setup information about extf
1338 d_extf_info_tmp[n].init();
1339 std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n );
1340 if( n.getType().isBoolean() ){
1341 if( areEqual( n, d_true ) ){
1342 itit->second.d_pol = 1;
1343 }else if( areEqual( n, d_false ) ){
1344 itit->second.d_pol = -1;
1345 }
1346 }
1347 Trace("strings-extf-debug") << "Check extf " << n << " == " << sn << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl;
1348 //do the inference
1349 Node to_reduce;
1350 if( n!=sn ){
1351 itit->second.d_exp.insert( itit->second.d_exp.end(), exp[i].begin(), exp[i].end() );
1352 // inference is rewriting the substituted node
1353 Node nrc = Rewriter::rewrite( sn );
1354 //if rewrites to a constant, then do the inference and mark as reduced
1355 if( nrc.isConst() ){
1356 if( effort<3 ){
1357 getExtTheory()->markReduced( n );
1358 Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl;
1359 std::vector< Node > exps;
1360 // The following optimization gets the "symbolic definition" of
1361 // an extended term. The symbolic definition of a term t is a term
1362 // t' where constants are replaced by their corresponding proxy
1363 // variables.
1364 // For example, if lsym is a proxy variable for "", then
1365 // str.replace( lsym, lsym, lsym ) is the symbolic definition for
1366 // str.replace( "", "", "" ). It is generally better to use symbolic
1367 // definitions when doing cd-rewriting for the purpose of minimizing
1368 // clauses, e.g. we infer the unit equality:
1369 // str.replace( lsym, lsym, lsym ) == ""
1370 // instead of making this inference multiple times:
1371 // x = "" => str.replace( x, x, x ) == ""
1372 // y = "" => str.replace( y, y, y ) == ""
1373 Trace("strings-extf-debug") << " get symbolic definition..." << std::endl;
1374 Node nrs = getSymbolicDefinition( sn, exps );
1375 if( !nrs.isNull() ){
1376 Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl;
1377 Node nrsr = Rewriter::rewrite(nrs);
1378 // ensure the symbolic form is not rewritable
1379 if (nrsr != nrs)
1380 {
1381 // we cannot use the symbolic definition if it rewrites
1382 Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl;
1383 nrs = Node::null();
1384 }
1385 }else{
1386 Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl;
1387 }
1388 Node conc;
1389 if( !nrs.isNull() ){
1390 Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl;
1391 if( !areEqual( nrs, nrc ) ){
1392 //infer symbolic unit
1393 if( n.getType().isBoolean() ){
1394 conc = nrc==d_true ? nrs : nrs.negate();
1395 }else{
1396 conc = nrs.eqNode( nrc );
1397 }
1398 itit->second.d_exp.clear();
1399 }
1400 }else{
1401 if( !areEqual( n, nrc ) ){
1402 if( n.getType().isBoolean() ){
1403 if( areEqual( n, nrc==d_true ? d_false : d_true ) ){
1404 itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n );
1405 conc = d_false;
1406 }else{
1407 conc = nrc==d_true ? n : n.negate();
1408 }
1409 }else{
1410 conc = n.eqNode( nrc );
1411 }
1412 }
1413 }
1414 if( !conc.isNull() ){
1415 Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl;
1416 sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true );
1417 if( d_conflict ){
1418 Trace("strings-extf-debug") << " conflict, return." << std::endl;
1419 return;
1420 }
1421 }
1422 }else{
1423 //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
1424 if( areEqual( n, nrc ) ){
1425 Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl;
1426 itit->second.d_model_active = false;
1427 }
1428 }
1429 //if it reduces to a conjunction, infer each and reduce
1430 }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){
1431 Assert( effort<3 );
1432 getExtTheory()->markReduced( n );
1433 itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n );
1434 Trace("strings-extf-debug") << " decomposable..." << std::endl;
1435 Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl;
1436 for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
1437 sendInference( itit->second.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
1438 }
1439 }else{
1440 to_reduce = nrc;
1441 }
1442 }else{
1443 to_reduce = sterms[i];
1444 }
1445 //if not reduced
1446 if( !to_reduce.isNull() ){
1447 Assert( effort<3 );
1448 if( effort==1 ){
1449 Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl;
1450 }
1451 checkExtfInference( n, to_reduce, itit->second, effort );
1452 if( Trace.isOn("strings-extf-list") ){
1453 Trace("strings-extf-list") << " * " << to_reduce;
1454 if( itit->second.d_pol!=0 ){
1455 Trace("strings-extf-list") << ", pol = " << itit->second.d_pol;
1456 }
1457 if( n!=to_reduce ){
1458 Trace("strings-extf-list") << ", from " << n;
1459 }
1460 Trace("strings-extf-list") << std::endl;
1461 }
1462 if( getExtTheory()->isActive( n ) && itit->second.d_model_active ){
1463 has_nreduce = true;
1464 }
1465 }
1466 }
1467 d_has_extf = has_nreduce;
1468 }
1469
1470 void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){
1471 //make additional inferences that do not contribute to the reduction of n, but may help show a refutation
1472 if( in.d_pol!=0 ){
1473 //add original to explanation
1474 in.d_exp.push_back( in.d_pol==1 ? n : n.negate() );
1475
1476 //d_extf_infer_cache stores whether we have made the inferences associated with a node n,
1477 // this may need to be generalized if multiple inferences apply
1478
1479 if( nr.getKind()==kind::STRING_STRCTN ){
1480 if( ( in.d_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( in.d_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
1481 if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
1482 d_extf_infer_cache.insert( nr );
1483
1484 //one argument does (not) contain each of the components of the other argument
1485 int index = in.d_pol==1 ? 1 : 0;
1486 std::vector< Node > children;
1487 children.push_back( nr[0] );
1488 children.push_back( nr[1] );
1489 //Node exp_n = mkAnd( exp );
1490 for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){
1491 children[index] = nr[index][i];
1492 Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children );
1493 conc = Rewriter::rewrite(in.d_pol == 1 ? conc : conc.negate());
1494 // check if it already (does not) hold
1495 if (hasTerm(conc))
1496 {
1497 if (areEqual(conc, d_false))
1498 {
1499 // should be a conflict
1500 sendInference(in.d_exp, conc, "CTN_Decompose");
1501 }
1502 else if (getExtTheory()->hasFunctionKind(conc.getKind()))
1503 {
1504 // can mark as reduced, since model for n => model for conc
1505 getExtTheory()->markReduced(conc);
1506 }
1507 }
1508 }
1509
1510 }
1511 }else{
1512 //store this (reduced) assertion
1513 //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
1514 bool pol = in.d_pol==1;
1515 if( std::find( d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), d_extf_info_tmp[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info_tmp[nr[0]].d_ctn[pol].end() ){
1516 Trace("strings-extf-debug") << " store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
1517 d_extf_info_tmp[nr[0]].d_ctn[pol].push_back( nr[1] );
1518 d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back( n );
1519 //transitive closure for contains
1520 bool opol = !pol;
1521 for( unsigned i=0; i<d_extf_info_tmp[nr[0]].d_ctn[opol].size(); i++ ){
1522 Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i];
1523 Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] );
1524 conc = Rewriter::rewrite( conc );
1525 bool do_infer = false;
1526 if( conc.getKind()==kind::EQUAL ){
1527 do_infer = !areDisequal( conc[0], conc[1] );
1528 }else{
1529 do_infer = !areEqual( conc, d_false );
1530 }
1531 if( do_infer ){
1532 conc = conc.negate();
1533 std::vector< Node > exp_c;
1534 exp_c.insert( exp_c.end(), in.d_exp.begin(), in.d_exp.end() );
1535 Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i];
1536 Assert( d_extf_info_tmp.find( ofrom )!=d_extf_info_tmp.end() );
1537 exp_c.insert( exp_c.end(), d_extf_info_tmp[ofrom].d_exp.begin(), d_extf_info_tmp[ofrom].d_exp.end() );
1538 sendInference( exp_c, conc, "CTN_Trans" );
1539 }
1540 }
1541 }else{
1542 Trace("strings-extf-debug") << " redundant." << std::endl;
1543 getExtTheory()->markReduced( n );
1544 }
1545 }
1546 }
1547 }
1548 }
1549
1550 void TheoryStrings::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
1551 if( !n.isConst() ){
1552 if( visited.find( n )==visited.end() ){
1553 visited[n] = true;
1554 if( n.getNumChildren()>0 ){
1555 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1556 collectVars( n[i], vars, visited );
1557 }
1558 }else{
1559 //Node nr = getRepresentative( n );
1560 //vars[nr].push_back( n );
1561 vars.push_back( n );
1562 }
1563 }
1564 }
1565 }
1566
1567 Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) {
1568 if( n.getNumChildren()==0 ){
1569 NodeNodeMap::const_iterator it = d_proxy_var.find( n );
1570 if( it==d_proxy_var.end() ){
1571 return Node::null();
1572 }else{
1573 Node eq = n.eqNode( (*it).second );
1574 eq = Rewriter::rewrite( eq );
1575 if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
1576 exp.push_back( eq );
1577 }
1578 return (*it).second;
1579 }
1580 }else{
1581 std::vector< Node > children;
1582 if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
1583 children.push_back( n.getOperator() );
1584 }
1585 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1586 if( n.getKind()==kind::STRING_IN_REGEXP && i==1 ){
1587 children.push_back( n[i] );
1588 }else{
1589 Node ns = getSymbolicDefinition( n[i], exp );
1590 if( ns.isNull() ){
1591 return Node::null();
1592 }else{
1593 children.push_back( ns );
1594 }
1595 }
1596 }
1597 return NodeManager::currentNM()->mkNode( n.getKind(), children );
1598 }
1599 }
1600
1601 Node TheoryStrings::getConstantEqc( Node eqc ) {
1602 std::map< Node, Node >::iterator it = d_eqc_to_const.find( eqc );
1603 if( it!=d_eqc_to_const.end() ){
1604 return it->second;
1605 }else{
1606 return Node::null();
1607 }
1608 }
1609
1610 void TheoryStrings::debugPrintFlatForms( const char * tc ){
1611 for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
1612 Node eqc = d_strings_eqc[k];
1613 if( d_eqc[eqc].size()>1 ){
1614 Trace( tc ) << "EQC [" << eqc << "]" << std::endl;
1615 }else{
1616 Trace( tc ) << "eqc [" << eqc << "]";
1617 }
1618 std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
1619 if( itc!=d_eqc_to_const.end() ){
1620 Trace( tc ) << " C: " << itc->second;
1621 if( d_eqc[eqc].size()>1 ){
1622 Trace( tc ) << std::endl;
1623 }
1624 }
1625 if( d_eqc[eqc].size()>1 ){
1626 for( unsigned i=0; i<d_eqc[eqc].size(); i++ ){
1627 Node n = d_eqc[eqc][i];
1628 Trace( tc ) << " ";
1629 for( unsigned j=0; j<d_flat_form[n].size(); j++ ){
1630 Node fc = d_flat_form[n][j];
1631 itc = d_eqc_to_const.find( fc );
1632 Trace( tc ) << " ";
1633 if( itc!=d_eqc_to_const.end() ){
1634 Trace( tc ) << itc->second;
1635 }else{
1636 Trace( tc ) << fc;
1637 }
1638 }
1639 if( n!=eqc ){
1640 Trace( tc ) << ", from " << n;
1641 }
1642 Trace( tc ) << std::endl;
1643 }
1644 }else{
1645 Trace( tc ) << std::endl;
1646 }
1647 }
1648 Trace( tc ) << std::endl;
1649 }
1650
1651 void TheoryStrings::debugPrintNormalForms( const char * tc ) {
1652 }
1653
1654 struct sortConstLength {
1655 std::map< Node, unsigned > d_const_length;
1656 bool operator() (Node i, Node j) {
1657 std::map< Node, unsigned >::iterator it_i = d_const_length.find( i );
1658 std::map< Node, unsigned >::iterator it_j = d_const_length.find( j );
1659 if( it_i==d_const_length.end() ){
1660 if( it_j==d_const_length.end() ){
1661 return i<j;
1662 }else{
1663 return false;
1664 }
1665 }else{
1666 if( it_j==d_const_length.end() ){
1667 return true;
1668 }else{
1669 return it_i->second<it_j->second;
1670 }
1671 }
1672 }
1673 };
1674
1675
1676 void TheoryStrings::checkFlatForms() {
1677 //first check for cycles, while building ordering of equivalence classes
1678 d_eqc.clear();
1679 d_flat_form.clear();
1680 d_flat_form_index.clear();
1681 Trace("strings-process") << "Check equivalence classes cycles...." << std::endl;
1682 //rebuild strings eqc based on acyclic ordering
1683 std::vector< Node > eqc;
1684 eqc.insert( eqc.end(), d_strings_eqc.begin(), d_strings_eqc.end() );
1685 d_strings_eqc.clear();
1686 if( options::stringBinaryCsp() ){
1687 //sort: process smallest constants first (necessary if doing binary splits)
1688 sortConstLength scl;
1689 for( unsigned i=0; i<eqc.size(); i++ ){
1690 std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc[i] );
1691 if( itc!=d_eqc_to_const.end() ){
1692 scl.d_const_length[eqc[i]] = itc->second.getConst<String>().size();
1693 }
1694 }
1695 std::sort( eqc.begin(), eqc.end(), scl );
1696 }
1697 for( unsigned i=0; i<eqc.size(); i++ ){
1698 std::vector< Node > curr;
1699 std::vector< Node > exp;
1700 checkCycles( eqc[i], curr, exp );
1701 if( hasProcessed() ){
1702 return;
1703 }
1704 }
1705 Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << std::endl;
1706 if( !hasProcessed() ){
1707 //debug print flat forms
1708 if( Trace.isOn("strings-ff") ){
1709 Trace("strings-ff") << "Flat forms : " << std::endl;
1710 debugPrintFlatForms( "strings-ff" );
1711 }
1712
1713 //inferences without recursively expanding flat forms
1714
1715 //(1) approximate equality by containment, infer conflicts
1716 for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
1717 Node eqc = d_strings_eqc[k];
1718 Node c = getConstantEqc( eqc );
1719 if( !c.isNull() ){
1720 //if equivalence class is constant, all component constants in flat forms must be contained in it, in order
1721 std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc );
1722 if( it!=d_eqc.end() ){
1723 for( unsigned i=0; i<it->second.size(); i++ ){
1724 Node n = it->second[i];
1725 int firstc, lastc;
1726 if( !TheoryStringsRewriter::canConstantContainList( c, d_flat_form[n], firstc, lastc ) ){
1727 Trace("strings-ff-debug") << "Flat form for " << n << " cannot be contained in constant " << c << std::endl;
1728 Trace("strings-ff-debug") << " indices = " << firstc << "/" << lastc << std::endl;
1729 //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = f[n] )
1730 std::vector< Node > exp;
1731 Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() );
1732 addToExplanation( n, d_eqc_to_const_base[eqc], exp );
1733 Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() );
1734 if( !d_eqc_to_const_exp[eqc].isNull() ){
1735 exp.push_back( d_eqc_to_const_exp[eqc] );
1736 }
1737 for( int e=firstc; e<=lastc; e++ ){
1738 if( d_flat_form[n][e].isConst() ){
1739 Assert( e>=0 && e<(int)d_flat_form_index[n].size() );
1740 Assert( d_flat_form_index[n][e]>=0 && d_flat_form_index[n][e]<(int)n.getNumChildren() );
1741 addToExplanation( d_flat_form[n][e], n[d_flat_form_index[n][e]], exp );
1742 }
1743 }
1744 Node conc = d_false;
1745 sendInference( exp, conc, "F_NCTN" );
1746 return;
1747 }
1748 }
1749 }
1750 }
1751 }
1752
1753 //(2) scan lists, unification to infer conflicts and equalities
1754 for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
1755 Node eqc = d_strings_eqc[k];
1756 std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc );
1757 if( it!=d_eqc.end() && it->second.size()>1 ){
1758 //iterate over start index
1759 for( unsigned start=0; start<it->second.size()-1; start++ ){
1760 for( unsigned r=0; r<2; r++ ){
1761 unsigned count = 0;
1762 std::vector< Node > inelig;
1763 for( unsigned i=0; i<=start; i++ ){
1764 inelig.push_back( it->second[start] );
1765 }
1766 Node a = it->second[start];
1767 Node b;
1768 do{
1769 std::vector< Node > exp;
1770 //std::vector< Node > exp_n;
1771 Node conc;
1772 int inf_type = -1;
1773 if( count==d_flat_form[a].size() ){
1774 for( unsigned i=start+1; i<it->second.size(); i++ ){
1775 b = it->second[i];
1776 if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
1777 if( count<d_flat_form[b].size() ){
1778 //endpoint
1779 std::vector< Node > conc_c;
1780 for( unsigned j=count; j<d_flat_form[b].size(); j++ ){
1781 conc_c.push_back( b[d_flat_form_index[b][j]].eqNode( d_emptyString ) );
1782 }
1783 Assert( !conc_c.empty() );
1784 conc = mkAnd( conc_c );
1785 inf_type = 2;
1786 Assert( count>0 );
1787 //swap, will enforce is empty past current
1788 a = it->second[i]; b = it->second[start];
1789 count--;
1790 break;
1791 }
1792 inelig.push_back( it->second[i] );
1793 }
1794 }
1795 }else{
1796 Node curr = d_flat_form[a][count];
1797 Node curr_c = getConstantEqc( curr );
1798 Node ac = a[d_flat_form_index[a][count]];
1799 std::vector< Node > lexp;
1800 Node lcurr = getLength( ac, lexp );
1801 for( unsigned i=1; i<it->second.size(); i++ ){
1802 b = it->second[i];
1803 if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
1804 if( count==d_flat_form[b].size() ){
1805 inelig.push_back( b );
1806 //endpoint
1807 std::vector< Node > conc_c;
1808 for( unsigned j=count; j<d_flat_form[a].size(); j++ ){
1809 conc_c.push_back( a[d_flat_form_index[a][j]].eqNode( d_emptyString ) );
1810 }
1811 Assert( !conc_c.empty() );
1812 conc = mkAnd( conc_c );
1813 inf_type = 2;
1814 Assert( count>0 );
1815 count--;
1816 break;
1817 }else{
1818 Node cc = d_flat_form[b][count];
1819 if( cc!=curr ){
1820 Node bc = b[d_flat_form_index[b][count]];
1821 inelig.push_back( b );
1822 Assert( !areEqual( curr, cc ) );
1823 Node cc_c = getConstantEqc( cc );
1824 if( !curr_c.isNull() && !cc_c.isNull() ){
1825 //check for constant conflict
1826 int index;
1827 Node s = TheoryStringsRewriter::splitConstant( cc_c, curr_c, index, r==1 );
1828 if( s.isNull() ){
1829 addToExplanation( ac, d_eqc_to_const_base[curr], exp );
1830 addToExplanation( d_eqc_to_const_exp[curr], exp );
1831 addToExplanation( bc, d_eqc_to_const_base[cc], exp );
1832 addToExplanation( d_eqc_to_const_exp[cc], exp );
1833 conc = d_false;
1834 inf_type = 0;
1835 break;
1836 }
1837 }else if( (d_flat_form[a].size()-1)==count && (d_flat_form[b].size()-1)==count ){
1838 conc = ac.eqNode( bc );
1839 inf_type = 3;
1840 break;
1841 }else{
1842 //if lengths are the same, apply LengthEq
1843 std::vector< Node > lexp2;
1844 Node lcc = getLength( bc, lexp2 );
1845 if( areEqual( lcurr, lcc ) ){
1846 Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
1847 //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
1848 Trace("strings-ff-debug") << "Explanation for " << lcurr << " is ";
1849 for( unsigned j=0; j<lexp.size(); j++ ) { Trace("strings-ff-debug") << lexp[j] << std::endl; }
1850 Trace("strings-ff-debug") << "Explanation for " << lcc << " is ";
1851 for( unsigned j=0; j<lexp2.size(); j++ ) { Trace("strings-ff-debug") << lexp2[j] << std::endl; }
1852 exp.insert( exp.end(), lexp.begin(), lexp.end() );
1853 exp.insert( exp.end(), lexp2.begin(), lexp2.end() );
1854 addToExplanation( lcurr, lcc, exp );
1855 conc = ac.eqNode( bc );
1856 inf_type = 1;
1857 break;
1858 }
1859 }
1860 }
1861 }
1862 }
1863 }
1864 }
1865 if( !conc.isNull() ){
1866 Trace("strings-ff-debug") << "Found inference : " << conc << " based on equality " << a << " == " << b << " " << r << " " << inf_type << std::endl;
1867 addToExplanation( a, b, exp );
1868 //explain why prefixes up to now were the same
1869 for( unsigned j=0; j<count; j++ ){
1870 Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " " << d_flat_form_index[b][j] << std::endl;
1871 addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp );
1872 }
1873 //explain why other components up to now are empty
1874 for( unsigned t=0; t<2; t++ ){
1875 Node c = t==0 ? a : b;
1876 int jj;
1877 if( inf_type==3 || ( t==1 && inf_type==2 ) ){
1878 //explain all the empty components for F_EndpointEq, all for the short end for F_EndpointEmp
1879 jj = r==0 ? c.getNumChildren() : -1;
1880 }else{
1881 jj = t==0 ? d_flat_form_index[a][count] : d_flat_form_index[b][count];
1882 }
1883 if( r==0 ){
1884 for( int j=0; j<jj; j++ ){
1885 if( areEqual( c[j], d_emptyString ) ){
1886 addToExplanation( c[j], d_emptyString, exp );
1887 }
1888 }
1889 }else{
1890 for( int j=(c.getNumChildren()-1); j>jj; --j ){
1891 if( areEqual( c[j], d_emptyString ) ){
1892 addToExplanation( c[j], d_emptyString, exp );
1893 }
1894 }
1895 }
1896 }
1897 //notice that F_EndpointEmp is not typically applied, since strict prefix equality ( a.b = a ) where a,b non-empty
1898 // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) when len(b)!=0.
1899 sendInference( exp, conc, inf_type==0 ? "F_Const" : ( inf_type==1 ? "F_Unify" : ( inf_type==2 ? "F_EndpointEmp" : "F_EndpointEq" ) ) );
1900 if( d_conflict ){
1901 return;
1902 }else{
1903 break;
1904 }
1905 }
1906 count++;
1907 }while( inelig.size()<it->second.size() );
1908
1909 for( unsigned i=0; i<it->second.size(); i++ ){
1910 std::reverse( d_flat_form[it->second[i]].begin(), d_flat_form[it->second[i]].end() );
1911 std::reverse( d_flat_form_index[it->second[i]].begin(), d_flat_form_index[it->second[i]].end() );
1912 }
1913 }
1914 }
1915 }
1916 }
1917 if( !hasProcessed() ){
1918 // simple extended func reduction
1919 Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl;
1920 checkExtfReductions( 1 );
1921 Trace("strings-process") << "Done check extended function reduction" << std::endl;
1922 }
1923 }
1924 }
1925
1926 Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
1927 if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
1928 // a loop
1929 return eqc;
1930 }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){
1931 curr.push_back( eqc );
1932 //look at all terms in this equivalence class
1933 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1934 while( !eqc_i.isFinished() ) {
1935 Node n = (*eqc_i);
1936 if( d_congruent.find( n )==d_congruent.end() ){
1937 if( n.getKind() == kind::STRING_CONCAT ){
1938 Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
1939 if( eqc!=d_emptyString_r ){
1940 d_eqc[eqc].push_back( n );
1941 }
1942 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1943 Node nr = getRepresentative( n[i] );
1944 if( eqc==d_emptyString_r ){
1945 //for empty eqc, ensure all components are empty
1946 if( nr!=d_emptyString_r ){
1947 std::vector< Node > exp;
1948 exp.push_back( n.eqNode( d_emptyString ) );
1949 sendInference( exp, n[i].eqNode( d_emptyString ), "I_CYCLE_E" );
1950 return Node::null();
1951 }
1952 }else{
1953 if( nr!=d_emptyString_r ){
1954 d_flat_form[n].push_back( nr );
1955 d_flat_form_index[n].push_back( i );
1956 }
1957 //for non-empty eqc, recurse and see if we find a loop
1958 Node ncy = checkCycles( nr, curr, exp );
1959 if( !ncy.isNull() ){
1960 Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
1961 addToExplanation( n, eqc, exp );
1962 addToExplanation( nr, n[i], exp );
1963 if( ncy==eqc ){
1964 //can infer all other components must be empty
1965 for( unsigned j=0; j<n.getNumChildren(); j++ ){
1966 //take first non-empty
1967 if( j!=i && !areEqual( n[j], d_emptyString ) ){
1968 sendInference( exp, n[j].eqNode( d_emptyString ), "I_CYCLE" );
1969 return Node::null();
1970 }
1971 }
1972 Trace("strings-error") << "Looping term should be congruent : " << n << " " << eqc << " " << ncy << std::endl;
1973 //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
1974 Assert( false );
1975 }else{
1976 return ncy;
1977 }
1978 }else{
1979 if( hasProcessed() ){
1980 return Node::null();
1981 }
1982 }
1983 }
1984 }
1985 }
1986 }
1987 ++eqc_i;
1988 }
1989 curr.pop_back();
1990 //now we can add it to the list of equivalence classes
1991 d_strings_eqc.push_back( eqc );
1992 }else{
1993 //already processed
1994 }
1995 return Node::null();
1996 }
1997
1998
1999 void TheoryStrings::checkNormalForms(){
2000 if( !options::stringEagerLen() ){
2001 for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
2002 Node eqc = d_strings_eqc[i];
2003 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
2004 while( !eqc_i.isFinished() ) {
2005 Node n = (*eqc_i);
2006 if( d_congruent.find( n )==d_congruent.end() ){
2007 registerTerm( n, 2 );
2008 }
2009 ++eqc_i;
2010 }
2011 }
2012 }
2013 if( !hasProcessed() ){
2014 Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
2015 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
2016 d_normal_forms.clear();
2017 d_normal_forms_exp.clear();
2018 std::map< Node, Node > nf_to_eqc;
2019 std::map< Node, Node > eqc_to_nf;
2020 std::map< Node, Node > eqc_to_exp;
2021 for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
2022 Node eqc = d_strings_eqc[i];
2023 Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
2024 normalizeEquivalenceClass( eqc );
2025 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
2026 if( hasProcessed() ){
2027 return;
2028 }else{
2029 Node nf_term = mkConcat( d_normal_forms[eqc] );
2030 std::map< Node, Node >::iterator itn = nf_to_eqc.find( nf_term );
2031 if( itn!=nf_to_eqc.end() ){
2032 //two equivalence classes have same normal form, merge
2033 std::vector< Node > nf_exp;
2034 nf_exp.push_back( mkAnd( d_normal_forms_exp[eqc] ) );
2035 nf_exp.push_back( eqc_to_exp[itn->second] );
2036 Node eq = d_normal_forms_base[eqc].eqNode( d_normal_forms_base[itn->second] );
2037 sendInference( nf_exp, eq, "Normal_Form" );
2038 } else {
2039 nf_to_eqc[nf_term] = eqc;
2040 eqc_to_nf[eqc] = nf_term;
2041 eqc_to_exp[eqc] = mkAnd( d_normal_forms_exp[eqc] );
2042 }
2043 }
2044 Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
2045 }
2046 if( !hasProcessed() ){
2047 if(Trace.isOn("strings-nf")) {
2048 Trace("strings-nf") << "**** Normal forms are : " << std::endl;
2049 for( std::map< Node, Node >::iterator it = eqc_to_exp.begin(); it != eqc_to_exp.end(); ++it ){
2050 Trace("strings-nf") << " N[" << it->first << "] (base " << d_normal_forms_base[it->first] << ") = " << eqc_to_nf[it->first] << std::endl;
2051 Trace("strings-nf") << " exp: " << it->second << std::endl;
2052 }
2053 Trace("strings-nf") << std::endl;
2054 }
2055 checkExtfEval( 1 );
2056 Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
2057 if( !hasProcessed() ){
2058 if( !options::stringEagerLen() ){
2059 checkLengthsEqc();
2060 if( hasProcessed() ){
2061 return;
2062 }
2063 }
2064 //process disequalities between equivalence classes
2065 checkDeqNF();
2066 Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
2067 }
2068 }
2069 Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
2070 }
2071 }
2072
2073 //compute d_normal_forms_(base,exp,exp_depend)[eqc]
2074 void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
2075 Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
2076 if( areEqual( eqc, d_emptyString ) ) {
2077 #ifdef CVC4_ASSERTIONS
2078 for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){
2079 Node n = d_eqc[eqc][j];
2080 for( unsigned i=0; i<n.getNumChildren(); i++ ){
2081 Assert( areEqual( n[i], d_emptyString ) );
2082 }
2083 }
2084 #endif
2085 //do nothing
2086 Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
2087 d_normal_forms_base[eqc] = d_emptyString;
2088 d_normal_forms[eqc].clear();
2089 d_normal_forms_exp[eqc].clear();
2090 } else {
2091 Assert( d_normal_forms.find(eqc)==d_normal_forms.end() );
2092 //phi => t = s1 * ... * sn
2093 // normal form for each non-variable term in this eqc (s1...sn)
2094 std::vector< std::vector< Node > > normal_forms;
2095 // explanation for each normal form (phi)
2096 std::vector< std::vector< Node > > normal_forms_exp;
2097 // dependency information
2098 std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend;
2099 // record terms for each normal form (t)
2100 std::vector< Node > normal_form_src;
2101 // get normal forms
2102 getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend);
2103 if( hasProcessed() ){
2104 return;
2105 }
2106 // process the normal forms
2107 processNEqc( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend );
2108 if( hasProcessed() ){
2109 return;
2110 }
2111 //debugPrintNormalForms( "strings-solve", eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend );
2112
2113 //construct the normal form
2114 Assert( !normal_forms.empty() );
2115
2116 int nf_index = 0;
2117 std::vector< Node >::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc );
2118 if( itn!=normal_form_src.end() ){
2119 nf_index = itn - normal_form_src.begin();
2120 Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl;
2121 Assert( normal_form_src[nf_index]==eqc );
2122 }else{
2123 //just take the first normal form
2124 Trace("strings-solve-debug2") << "take the first normal form" << std::endl;
2125 }
2126 d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
2127 d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
2128 Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
2129 d_normal_forms_base[eqc] = normal_form_src[nf_index];
2130 //track dependencies
2131 for( unsigned i=0; i<normal_forms_exp[nf_index].size(); i++ ){
2132 Node exp = normal_forms_exp[nf_index][i];
2133 for( unsigned r=0; r<2; r++ ){
2134 d_normal_forms_exp_depend[eqc][exp][r==0] = normal_forms_exp_depend[nf_index][exp][r==0];
2135 }
2136 }
2137 Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << d_normal_forms[eqc].size() << std::endl;
2138 }
2139 }
2140
2141 void trackNfExpDependency( std::vector< Node >& nf_exp_n, std::map< Node, std::map< bool, int > >& nf_exp_depend_n, Node exp, int new_val, int new_rev_val ){
2142 if( std::find( nf_exp_n.begin(), nf_exp_n.end(), exp )==nf_exp_n.end() ){
2143 nf_exp_n.push_back( exp );
2144 }
2145 for( unsigned k=0; k<2; k++ ){
2146 int val = k==0 ? new_val : new_rev_val;
2147 std::map< bool, int >::iterator itned = nf_exp_depend_n[exp].find( k==1 );
2148 if( itned==nf_exp_depend_n[exp].end() ){
2149 Trace("strings-process-debug") << "Deps : set dependency on " << exp << " to " << val << " isRev=" << (k==0) << std::endl;
2150 nf_exp_depend_n[exp][k==1] = val;
2151 }else{
2152 Trace("strings-process-debug") << "Deps : Multiple dependencies on " << exp << " : " << itned->second << " " << val << " isRev=" << (k==0) << std::endl;
2153 //if we already have a dependency (in the case of non-linear string equalities), it is min/max
2154 bool cmp = val > itned->second;
2155 if( cmp==(k==1) ){
2156 nf_exp_depend_n[exp][k==1] = val;
2157 }
2158 }
2159 }
2160 }
2161
2162 void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2163 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
2164 //constant for equivalence class
2165 Node eqc_non_c = eqc;
2166 Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
2167 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
2168 while( !eqc_i.isFinished() ){
2169 Node n = (*eqc_i);
2170 if( d_congruent.find( n )==d_congruent.end() ){
2171 if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ){
2172 Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
2173 std::vector< Node > nf_n;
2174 std::vector< Node > nf_exp_n;
2175 std::map< Node, std::map< bool, int > > nf_exp_depend_n;
2176 if( n.getKind()==kind::CONST_STRING ){
2177 if( n!=d_emptyString ) {
2178 nf_n.push_back( n );
2179 }
2180 }else if( n.getKind()==kind::STRING_CONCAT ){
2181 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
2182 Node nr = d_equalityEngine.getRepresentative( n[i] );
2183 Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl;
2184 Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
2185 unsigned orig_size = nf_n.size();
2186 unsigned add_size = d_normal_forms[nr].size();
2187 //if not the empty string, add to current normal form
2188 if( !d_normal_forms[nr].empty() ){
2189 for( unsigned r=0; r<d_normal_forms[nr].size(); r++ ) {
2190 if( Trace.isOn("strings-error") ) {
2191 if( d_normal_forms[nr][r].getKind()==kind::STRING_CONCAT ){
2192 Trace("strings-error") << "Strings::Error: From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
2193 for( unsigned rr=0; rr<d_normal_forms[nr].size(); rr++ ) {
2194 Trace("strings-error") << d_normal_forms[nr][rr] << " ";
2195 }
2196 Trace("strings-error") << std::endl;
2197 }
2198 }
2199 Assert( d_normal_forms[nr][r].getKind()!=kind::STRING_CONCAT );
2200 }
2201 nf_n.insert( nf_n.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
2202 }
2203
2204 for( unsigned j=0; j<d_normal_forms_exp[nr].size(); j++ ){
2205 Node exp = d_normal_forms_exp[nr][j];
2206 //track depends
2207 trackNfExpDependency( nf_exp_n, nf_exp_depend_n, exp,
2208 orig_size + d_normal_forms_exp_depend[nr][exp][false],
2209 orig_size + ( add_size - d_normal_forms_exp_depend[nr][exp][true] ) );
2210 }
2211 if( d_normal_forms_base[nr]!=n[i] ){
2212 Assert( d_normal_forms_base.find( nr )!=d_normal_forms_base.end() );
2213 Node eq = n[i].eqNode( d_normal_forms_base[nr] );
2214 //track depends : entire current segment is dependent upon base equality
2215 trackNfExpDependency( nf_exp_n, nf_exp_depend_n, eq, orig_size, orig_size + add_size );
2216 }
2217 }
2218 //convert forward indices to reverse indices
2219 int total_size = nf_n.size();
2220 for( std::map< Node, std::map< bool, int > >::iterator it = nf_exp_depend_n.begin(); it != nf_exp_depend_n.end(); ++it ){
2221 it->second[true] = total_size - it->second[true];
2222 Assert( it->second[true]>=0 );
2223 }
2224 }
2225 //if not equal to self
2226 if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
2227 if( nf_n.size()>1 ) {
2228 for( unsigned i=0; i<nf_n.size(); i++ ){
2229 if( Trace.isOn("strings-error") ){
2230 Trace("strings-error") << "Cycle for normal form ";
2231 printConcat(nf_n,"strings-error");
2232 Trace("strings-error") << "..." << nf_n[i] << std::endl;
2233 }
2234 Assert( !areEqual( nf_n[i], n ) );
2235 }
2236 }
2237 normal_forms.push_back(nf_n);
2238 normal_form_src.push_back(n);
2239 normal_forms_exp.push_back(nf_exp_n);
2240 normal_forms_exp_depend.push_back(nf_exp_depend_n);
2241 }else{
2242 //this was redundant: combination of self + empty string(s)
2243 Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
2244 Assert( areEqual( nn, eqc ) );
2245 }
2246 }else{
2247 eqc_non_c = n;
2248 }
2249 }
2250 ++eqc_i;
2251 }
2252
2253 if( normal_forms.empty() ) {
2254 Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
2255 //do not choose a concat here use "eqc_non_c" (in this case they have non-trivial explanation why they normalize to self)
2256 std::vector< Node > eqc_non_c_nf;
2257 getConcatVec( eqc_non_c, eqc_non_c_nf );
2258 normal_forms.push_back( eqc_non_c_nf );
2259 normal_form_src.push_back( eqc_non_c );
2260 normal_forms_exp.push_back( std::vector< Node >() );
2261 normal_forms_exp_depend.push_back( std::map< Node, std::map< bool, int > >() );
2262 }else{
2263 if(Trace.isOn("strings-solve")) {
2264 Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc << " : " << std::endl;
2265 for( unsigned i=0; i<normal_forms.size(); i++ ) {
2266 Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
2267 for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
2268 if(j>0) {
2269 Trace("strings-solve") << ", ";
2270 }
2271 Trace("strings-solve") << normal_forms[i][j];
2272 }
2273 Trace("strings-solve") << std::endl;
2274 Trace("strings-solve") << " Explanation is : ";
2275 if(normal_forms_exp[i].size() == 0) {
2276 Trace("strings-solve") << "NONE";
2277 } else {
2278 for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
2279 if(j>0) {
2280 Trace("strings-solve") << " AND ";
2281 }
2282 Trace("strings-solve") << normal_forms_exp[i][j];
2283 }
2284 Trace("strings-solve") << std::endl;
2285 Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl;
2286 for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
2287 Trace("strings-solve") << " " << normal_forms_exp[i][j] << " -> ";
2288 Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][false] << ",";
2289 Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][true] << std::endl;
2290 }
2291 }
2292 Trace("strings-solve") << std::endl;
2293
2294 }
2295 } else {
2296 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
2297 }
2298
2299 //if equivalence class is constant, approximate as containment, infer conflicts
2300 Node c = getConstantEqc( eqc );
2301 if( !c.isNull() ){
2302 Trace("strings-solve") << "Eqc is constant " << c << std::endl;
2303 for( unsigned i=0; i<normal_forms.size(); i++ ) {
2304 int firstc, lastc;
2305 if( !TheoryStringsRewriter::canConstantContainList( c, normal_forms[i], firstc, lastc ) ){
2306 Node n = normal_form_src[i];
2307 //conflict
2308 Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
2309 //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
2310 std::vector< Node > exp;
2311 Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() );
2312 addToExplanation( n, d_eqc_to_const_base[eqc], exp );
2313 Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() );
2314 if( !d_eqc_to_const_exp[eqc].isNull() ){
2315 exp.push_back( d_eqc_to_const_exp[eqc] );
2316 }
2317 //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
2318 exp.insert( exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
2319 Node conc = d_false;
2320 sendInference( exp, conc, "N_NCTN" );
2321 }
2322 }
2323 }
2324 }
2325 }
2326
2327 void TheoryStrings::getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
2328 unsigned i, int index, bool isRev, std::vector< Node >& curr_exp ) {
2329 if( index==-1 || !options::stringMinPrefixExplain() ){
2330 curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
2331 }else{
2332 for( unsigned k=0; k<normal_forms_exp[i].size(); k++ ){
2333 Node exp = normal_forms_exp[i][k];
2334 int dep = normal_forms_exp_depend[i][exp][isRev];
2335 if( dep<=index ){
2336 curr_exp.push_back( exp );
2337 Trace("strings-explain-prefix-debug") << " include : " << exp << std::endl;
2338 }else{
2339 Trace("strings-explain-prefix-debug") << " exclude : " << exp << std::endl;
2340 }
2341 }
2342 }
2343 }
2344
2345 void TheoryStrings::getExplanationVectorForPrefixEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2346 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
2347 unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp ) {
2348 Trace("strings-explain-prefix") << "Get explanation for prefix " << index_i << ", " << index_j << " of normal forms " << i << " and " << j << ", reverse = " << isRev << std::endl;
2349 for( unsigned r=0; r<2; r++ ){
2350 getExplanationVectorForPrefix( normal_forms_exp, normal_forms_exp_depend, r==0 ? i : j, r==0 ? index_i : index_j, isRev, curr_exp );
2351 }
2352 Trace("strings-explain-prefix") << "Included " << curr_exp.size() << " / " << ( normal_forms_exp[i].size() + normal_forms_exp[j].size() ) << std::endl;
2353 addToExplanation( normal_form_src[i], normal_form_src[j], curr_exp );
2354 }
2355
2356
2357 void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2358 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ){
2359 //the possible inferences
2360 std::vector< InferInfo > pinfer;
2361 // loop over all pairs
2362 for(unsigned i=0; i<normal_forms.size()-1; i++) {
2363 //unify each normalform[j] with normal_forms[i]
2364 for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
2365 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
2366 Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
2367 if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
2368 Trace("strings-solve") << "Strings: Already cached." << std::endl;
2369 }else{
2370 //process the reverse direction first (check for easy conflicts and inferences)
2371 unsigned rindex = 0;
2372 processReverseNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, rindex, 0, pinfer );
2373 if( hasProcessed() ){
2374 return;
2375 }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
2376 break;
2377 }
2378 //AJR: for less aggressive endpoint inference
2379 //rindex = 0;
2380
2381 unsigned index = 0;
2382 processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, rindex, pinfer );
2383 if( hasProcessed() ){
2384 return;
2385 }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
2386 break;
2387 }
2388 }
2389 }
2390 }
2391 if( !pinfer.empty() ){
2392 //now, determine which of the possible inferences we want to add
2393 int use_index = -1;
2394 Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl;
2395 unsigned min_id = 9;
2396 unsigned max_index = 0;
2397 for (unsigned i = 0, size = pinfer.size(); i < size; i++)
2398 {
2399 Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : ";
2400 Trace("strings-solve")
2401 << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl;
2402 if( use_index==-1 || pinfer[i].d_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_index ) ){
2403 min_id = pinfer[i].d_id;
2404 max_index = pinfer[i].d_index;
2405 use_index = i;
2406 }
2407 }
2408 //send the inference
2409 if( !pinfer[use_index].d_nf_pair[0].isNull() ){
2410 Assert( !pinfer[use_index].d_nf_pair[1].isNull() );
2411 addNormalFormPair( pinfer[use_index].d_nf_pair[0], pinfer[use_index].d_nf_pair[1] );
2412 }
2413 std::stringstream ssi;
2414 ssi << pinfer[use_index].d_id;
2415 sendInference(pinfer[use_index].d_ant,
2416 pinfer[use_index].d_antn,
2417 pinfer[use_index].d_conc,
2418 ssi.str().c_str(),
2419 pinfer[use_index].sendAsLemma());
2420 for( std::map< int, std::vector< Node > >::iterator it = pinfer[use_index].d_new_skolem.begin(); it != pinfer[use_index].d_new_skolem.end(); ++it ){
2421 for( unsigned i=0; i<it->second.size(); i++ ){
2422 if( it->first==0 ){
2423 sendLengthLemma( it->second[i] );
2424 }else if( it->first==1 ){
2425 registerNonEmptySkolem( it->second[i] );
2426 }
2427 }
2428 }
2429 }
2430 }
2431
2432 bool TheoryStrings::InferInfo::sendAsLemma() {
2433 return true;
2434 }
2435
2436 void TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2437 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
2438 unsigned i, unsigned j, unsigned& index, unsigned rproc, std::vector< InferInfo >& pinfer ) {
2439 //reverse normal form of i, j
2440 std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
2441 std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
2442
2443 processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, true, rproc, pinfer );
2444
2445 //reverse normal form of i, j
2446 std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
2447 std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
2448 }
2449
2450 //rproc is the # is the size of suffix that is identical
2451 void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2452 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
2453 unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer ) {
2454 Assert( rproc<=normal_forms[i].size() && rproc<=normal_forms[j].size() );
2455 bool success;
2456 do {
2457 success = false;
2458 //if we are at the end
2459 if( index==(normal_forms[i].size()-rproc) || index==(normal_forms[j].size()-rproc) ){
2460 if( index==(normal_forms[i].size()-rproc) && index==(normal_forms[j].size()-rproc) ){
2461 //we're done
2462 }else{
2463 //the remainder must be empty
2464 unsigned k = index==(normal_forms[i].size()-rproc) ? j : i;
2465 unsigned index_k = index;
2466 //Node eq_exp = mkAnd( curr_exp );
2467 std::vector< Node > curr_exp;
2468 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, curr_exp );
2469 while( !d_conflict && index_k<(normal_forms[k].size()-rproc) ){
2470 //can infer that this string must be empty
2471 Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
2472 //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
2473 Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
2474 sendInference( curr_exp, eq, "N_EndpointEmp" );
2475 index_k++;
2476 }
2477 }
2478 }else{
2479 Trace("strings-solve-debug") << "Process " << normal_forms[i][index] << " ... " << normal_forms[j][index] << std::endl;
2480 if( normal_forms[i][index]==normal_forms[j][index] ){
2481 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
2482 index++;
2483 success = true;
2484 }else{
2485 Assert( !areEqual(normal_forms[i][index], normal_forms[j][index]) );
2486 std::vector< Node > temp_exp;
2487 Node length_term_i = getLength( normal_forms[i][index], temp_exp );
2488 Node length_term_j = getLength( normal_forms[j][index], temp_exp );
2489 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
2490 if( areEqual( length_term_i, length_term_j ) ){
2491 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
2492 Node eq = normal_forms[i][index].eqNode( normal_forms[j][index] );
2493 //eq = Rewriter::rewrite( eq );
2494 Node length_eq = length_term_i.eqNode( length_term_j );
2495 //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
2496 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, temp_exp );
2497 temp_exp.push_back(length_eq);
2498 sendInference( temp_exp, eq, "N_Unify" );
2499 return;
2500 }else if( ( normal_forms[i][index].getKind()!=kind::CONST_STRING && index==normal_forms[i].size()-rproc-1 ) ||
2501 ( normal_forms[j][index].getKind()!=kind::CONST_STRING && index==normal_forms[j].size()-rproc-1 ) ){
2502 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
2503 std::vector< Node > antec;
2504 //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
2505 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, antec );
2506 std::vector< Node > eqn;
2507 for( unsigned r=0; r<2; r++ ) {
2508 int index_k = index;
2509 int k = r==0 ? i : j;
2510 std::vector< Node > eqnc;
2511 for( unsigned index_l=index_k; index_l<(normal_forms[k].size()-rproc); index_l++ ) {
2512 if(isRev) {
2513 eqnc.insert(eqnc.begin(), normal_forms[k][index_l] );
2514 } else {
2515 eqnc.push_back( normal_forms[k][index_l] );
2516 }
2517 }
2518 eqn.push_back( mkConcat( eqnc ) );
2519 }
2520 if( !areEqual( eqn[0], eqn[1] ) ){
2521 sendInference( antec, eqn[0].eqNode( eqn[1] ), "N_EndpointEq", true );
2522 return;
2523 }else{
2524 Assert( normal_forms[i].size()==normal_forms[j].size() );
2525 index = normal_forms[i].size()-rproc;
2526 }
2527 }else if( normal_forms[i][index].isConst() && normal_forms[j][index].isConst() ){
2528 Node const_str = normal_forms[i][index];
2529 Node other_str = normal_forms[j][index];
2530 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << " at index " << index << ", isRev = " << isRev << std::endl;
2531 unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
2532 bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
2533 if( isSameFix ) {
2534 //same prefix/suffix
2535 //k is the index of the string that is shorter
2536 int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
2537 int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
2538 //update the nf exp dependencies
2539 //notice this is not critical for soundness: not doing the below incrementing will only lead to overapproximating when antecedants are required in explanations
2540 for( std::map< Node, std::map< bool, int > >::iterator itnd = normal_forms_exp_depend[l].begin(); itnd != normal_forms_exp_depend[l].end(); ++itnd ){
2541 for( std::map< bool, int >::iterator itnd2 = itnd->second.begin(); itnd2 != itnd->second.end(); ++itnd2 ){
2542 //see if this can be incremented: it can if it is not relevant to the current index
2543 Assert( itnd2->second>=0 && itnd2->second<=(int)normal_forms[l].size() );
2544 bool increment = (itnd2->first==isRev) ? itnd2->second>(int)index : ( (int)normal_forms[l].size()-1-itnd2->second )<(int)index;
2545 if( increment ){
2546 normal_forms_exp_depend[l][itnd->first][itnd2->first] = itnd2->second + 1;
2547 }
2548 }
2549 }
2550 if( isRev ){
2551 int new_len = normal_forms[l][index].getConst<String>().size() - len_short;
2552 Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index].getConst<String>().substr(0, new_len) );
2553 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
2554 normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
2555 }else{
2556 Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index].getConst<String>().substr(len_short));
2557 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
2558 normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
2559 }
2560 normal_forms[l][index] = normal_forms[k][index];
2561 index++;
2562 success = true;
2563 }else{
2564 //conflict
2565 std::vector< Node > antec;
2566 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, antec );
2567 sendInference( antec, d_false, "N_Const", true );
2568 return;
2569 }
2570 }else{
2571 //construct the candidate inference "info"
2572 InferInfo info;
2573 info.d_index = index;
2574 //for debugging
2575 info.d_i = i;
2576 info.d_j = j;
2577 info.d_rev = isRev;
2578 bool info_valid = false;
2579 Assert( index<normal_forms[i].size()-rproc && index<normal_forms[j].size()-rproc );
2580 std::vector< Node > lexp;
2581 Node length_term_i = getLength( normal_forms[i][index], lexp );
2582 Node length_term_j = getLength( normal_forms[j][index], lexp );
2583 //split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process)
2584 if( !areDisequal( length_term_i, length_term_j ) && !areEqual( length_term_i, length_term_j ) &&
2585 normal_forms[i][index].getKind()!=kind::CONST_STRING && normal_forms[j][index].getKind()!=kind::CONST_STRING ){ //AJR: remove the latter 2 conditions?
2586 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
2587 //try to make the lengths equal via splitting on demand
2588 Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
2589 length_eq = Rewriter::rewrite( length_eq );
2590 //set info
2591 info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, length_eq, length_eq.negate() );
2592 info.d_pending_phase[ length_eq ] = true;
2593 info.d_id = INFER_LEN_SPLIT;
2594 info_valid = true;
2595 }else{
2596 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
2597 int loop_in_i = -1;
2598 int loop_in_j = -1;
2599 if( detectLoop( normal_forms, i, j, index, loop_in_i, loop_in_j, rproc ) ){
2600 if( !isRev ){ //FIXME
2601 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, info.d_ant );
2602 //set info
2603 if( processLoop( normal_forms, normal_form_src, i, j, loop_in_i!=-1 ? i : j, loop_in_i!=-1 ? j : i, loop_in_i!=-1 ? loop_in_i : loop_in_j, index, info ) ){
2604 info_valid = true;
2605 }
2606 }
2607 }else{
2608 //AJR: length entailment here?
2609 if( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING ){
2610 unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j;
2611 unsigned nconst_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? j : i;
2612 Node other_str = normal_forms[nconst_k][index];
2613 Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
2614 Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
2615 if( !d_equalityEngine.areDisequal( other_str, d_emptyString, true ) ){
2616 Node eq = other_str.eqNode( d_emptyString );
2617 //set info
2618 info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
2619 info.d_id = INFER_LEN_SPLIT_EMP;
2620 info_valid = true;
2621 }else{
2622 if( !isRev ){ //FIXME
2623 Node xnz = other_str.eqNode( d_emptyString ).negate();
2624 unsigned index_nc_k = index+1;
2625 //Node next_const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[nconst_k], index_nc_k, false );
2626 unsigned start_index_nc_k = index+1;
2627 Node next_const_str = TheoryStringsRewriter::getNextConstantAt( normal_forms[nconst_k], start_index_nc_k, index_nc_k, false );
2628 if( !next_const_str.isNull() ) {
2629 unsigned index_c_k = index;
2630 Node const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[const_k], index_c_k, false );
2631 Assert( !const_str.isNull() );
2632 CVC4::String stra = const_str.getConst<String>();
2633 CVC4::String strb = next_const_str.getConst<String>();
2634 //since non-empty, we start with charecter #1
2635 size_t p;
2636 if( isRev ){
2637 CVC4::String stra1 = stra.prefix( stra.size()-1 );
2638 p = stra.size() - stra1.roverlap(strb);
2639 Trace("strings-csp-debug") << "Compute roverlap : " << const_str << " " << next_const_str << std::endl;
2640 size_t p2 = stra1.rfind(strb);
2641 p = p2==std::string::npos ? p : ( p>p2+1? p2+1 : p );
2642 Trace("strings-csp-debug") << "overlap : " << stra1 << " " << strb << " returned " << p << " " << p2 << " " << (p2==std::string::npos) << std::endl;
2643 }else{
2644 CVC4::String stra1 = stra.substr( 1 );
2645 p = stra.size() - stra1.overlap(strb);
2646 Trace("strings-csp-debug") << "Compute overlap : " << const_str << " " << next_const_str << std::endl;
2647 size_t p2 = stra1.find(strb);
2648 p = p2==std::string::npos ? p : ( p>p2+1? p2+1 : p );
2649 Trace("strings-csp-debug") << "overlap : " << stra1 << " " << strb << " returned " << p << " " << p2 << " " << (p2==std::string::npos) << std::endl;
2650 }
2651 if( p>1 ){
2652 if( start_index_nc_k==index+1 ){
2653 info.d_ant.push_back( xnz );
2654 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend,
2655 const_k, nconst_k, index_c_k, index_nc_k, isRev, info.d_ant );
2656 Node prea = p==stra.size() ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( p ) : stra.prefix( p ) );
2657 Node sk = mkSkolemCached( other_str, prea, isRev ? sk_id_c_spt_rev : sk_id_c_spt, "c_spt", -1 );
2658 Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl;
2659 //set info
2660 info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );
2661 info.d_new_skolem[0].push_back( sk );
2662 info.d_id = INFER_SSPLIT_CST_PROP;
2663 info_valid = true;
2664 }
2665 /* FIXME for isRev, speculative
2666 else if( options::stringLenPropCsp() ){
2667 //propagate length constraint
2668 std::vector< Node > cc;
2669 for( unsigned i=index; i<start_index_nc_k; i++ ){
2670 cc.push_back( normal_forms[nconst_k][i] );
2671 }
2672 Node lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( cc ) );
2673 conc = NodeManager::currentNM()->mkNode( kind::GEQ, lt, NodeManager::currentNM()->mkConst( Rational(p) ) );
2674 sendInference( ant, conc, "S-Split(CSP-P)-lprop", true );
2675 }
2676 */
2677 }
2678 }
2679 if( !info_valid ){
2680 info.d_ant.push_back( xnz );
2681 Node const_str = normal_forms[const_k][index];
2682 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, info.d_ant );
2683 CVC4::String stra = const_str.getConst<String>();
2684 if( options::stringBinaryCsp() && stra.size()>3 ){
2685 //split string in half
2686 Node c_firstHalf = NodeManager::currentNM()->mkConst( isRev ? stra.substr( stra.size()/2 ) : stra.substr(0, stra.size()/2 ) );
2687 Node sk = mkSkolemCached( other_str, c_firstHalf , isRev ? sk_id_vc_bin_spt_rev : sk_id_vc_bin_spt, "cb_spt", -1 );
2688 Trace("strings-csp") << "Const Split: " << c_firstHalf << " is removed from " << const_str << " (binary) " << std::endl;
2689 info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, other_str.eqNode( isRev ? mkConcat( sk, c_firstHalf ) : mkConcat( c_firstHalf, sk ) ),
2690 NodeManager::currentNM()->mkNode( kind::AND,
2691 sk.eqNode( d_emptyString ).negate(),
2692 c_firstHalf.eqNode( isRev ? mkConcat( sk, other_str ) : mkConcat( other_str, sk ) ) ) );
2693 info.d_new_skolem[0].push_back( sk );
2694 info.d_id = INFER_SSPLIT_CST_BINARY;
2695 info_valid = true;
2696 }else{
2697 // normal v/c split
2698 Node firstChar = stra.size() == 1 ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( 1 ) : stra.prefix( 1 ) );
2699 Node sk = mkSkolemCached( other_str, firstChar, isRev ? sk_id_vc_spt_rev : sk_id_vc_spt, "c_spt", -1 );
2700 Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl;
2701 info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, firstChar ) : mkConcat(firstChar, sk) );
2702 info.d_new_skolem[0].push_back( sk );
2703 info.d_id = INFER_SSPLIT_CST;
2704 info_valid = true;
2705 }
2706 }
2707 }
2708 }
2709 }else{
2710 int lentTestSuccess = -1;
2711 Node lentTestExp;
2712 if( options::stringCheckEntailLen() ){
2713 //check entailment
2714 for( unsigned e=0; e<2; e++ ){
2715 Node t = e==0 ? normal_forms[i][index] : normal_forms[j][index];
2716 //do not infer constants are larger than variables
2717 if( t.getKind()!=kind::CONST_STRING ){
2718 Node lt1 = e==0 ? length_term_i : length_term_j;
2719 Node lt2 = e==0 ? length_term_j : length_term_i;
2720 Node ent_lit = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, lt1, lt2 ) );
2721 std::pair<bool, Node> et = d_valuation.entailmentCheck( THEORY_OF_TYPE_BASED, ent_lit );
2722 if( et.first ){
2723 Trace("strings-entail") << "Strings entailment : " << ent_lit << " is entailed in the current context." << std::endl;
2724 Trace("strings-entail") << " explanation was : " << et.second << std::endl;
2725 lentTestSuccess = e;
2726 lentTestExp = et.second;
2727 break;
2728 }
2729 }
2730 }
2731 }
2732
2733 getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, info.d_ant );
2734 //x!=e /\ y!=e
2735 for(unsigned xory=0; xory<2; xory++) {
2736 Node x = xory==0 ? normal_forms[i][index] : normal_forms[j][index];
2737 Node xgtz = x.eqNode( d_emptyString ).negate();
2738 if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
2739 info.d_ant.push_back( xgtz );
2740 } else {
2741 info.d_antn.push_back( xgtz );
2742 }
2743 }
2744 Node sk = mkSkolemCached( normal_forms[i][index], normal_forms[j][index], isRev ? sk_id_v_spt_rev : sk_id_v_spt, "v_spt", -1 );
2745 //must add length requirement
2746 info.d_new_skolem[1].push_back( sk );
2747 Node eq1 = normal_forms[i][index].eqNode( isRev ? mkConcat(sk, normal_forms[j][index]) : mkConcat(normal_forms[j][index], sk) );
2748 Node eq2 = normal_forms[j][index].eqNode( isRev ? mkConcat(sk, normal_forms[i][index]) : mkConcat(normal_forms[i][index], sk) );
2749
2750 if( lentTestSuccess!=-1 ){
2751 info.d_antn.push_back( lentTestExp );
2752 info.d_conc = lentTestSuccess==0 ? eq1 : eq2;
2753 info.d_id = INFER_SSPLIT_VAR_PROP;
2754 info_valid = true;
2755 }else{
2756 Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
2757 if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
2758 info.d_ant.push_back( ldeq );
2759 }else{
2760 info.d_antn.push_back(ldeq);
2761 }
2762 //set info
2763 info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
2764 info.d_id = INFER_SSPLIT_VAR;
2765 info_valid = true;
2766 }
2767 }
2768 }
2769 }
2770 if( info_valid ){
2771 pinfer.push_back( info );
2772 Assert( !success );
2773 }
2774 }
2775 }
2776 }
2777 }while( success );
2778 }
2779
2780 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ){
2781 int has_loop[2] = { -1, -1 };
2782 if( options::stringLB() != 2 ) {
2783 for( unsigned r=0; r<2; r++ ) {
2784 int n_index = (r==0 ? i : j);
2785 int other_n_index = (r==0 ? j : i);
2786 if( normal_forms[other_n_index][index].getKind() != kind::CONST_STRING ) {
2787 for( unsigned lp = index+1; lp<normal_forms[n_index].size()-rproc; lp++ ){
2788 if( normal_forms[n_index][lp]==normal_forms[other_n_index][index] ){
2789 has_loop[r] = lp;
2790 break;
2791 }
2792 }
2793 }
2794 }
2795 }
2796 if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
2797 loop_in_i = has_loop[0];
2798 loop_in_j = has_loop[1];
2799 return true;
2800 } else {
2801 Trace("strings-solve-debug") << "No loops detected." << std::endl;
2802 return false;
2803 }
2804 }
2805
2806 //xs(zy)=t(yz)xr
2807 bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
2808 int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, InferInfo& info ){
2809 if( options::stringAbortLoop() ){
2810 Message() << "Looping word equation encountered." << std::endl;
2811 exit( 1 );
2812 }
2813 NodeManager* nm = NodeManager::currentNM();
2814 Node conc;
2815 Trace("strings-loop") << "Detected possible loop for "
2816 << normal_forms[loop_n_index][loop_index] << std::endl;
2817 Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][index]
2818 << std::endl;
2819
2820 Trace("strings-loop") << " ... T(Y.Z)= ";
2821 std::vector<Node>& veci = normal_forms[loop_n_index];
2822 std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index);
2823 Node t_yz = mkConcat(vec_t);
2824 Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
2825 Trace("strings-loop") << " ... S(Z.Y)= ";
2826 std::vector<Node>& vecoi = normal_forms[other_n_index];
2827 std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end());
2828 Node s_zy = mkConcat(vec_s);
2829 Trace("strings-loop") << s_zy << std::endl;
2830 Trace("strings-loop") << " ... R= ";
2831 std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end());
2832 Node r = mkConcat(vec_r);
2833 Trace("strings-loop") << r << std::endl;
2834
2835 if (s_zy.isConst() && r.isConst() && r != d_emptyString)
2836 {
2837 int c;
2838 bool flag = true;
2839 if (s_zy.getConst<String>().tailcmp(r.getConst<String>(), c))
2840 {
2841 if (c >= 0)
2842 {
2843 s_zy = nm->mkConst(s_zy.getConst<String>().substr(0, c));
2844 r = d_emptyString;
2845 vec_r.clear();
2846 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
2847 << ", c=" << c << std::endl;
2848 flag = false;
2849 }
2850 }
2851 if (flag)
2852 {
2853 Trace("strings-loop") << "Strings::Loop: tails are different."
2854 << std::endl;
2855 sendInference(info.d_ant, conc, "Loop Conflict", true);
2856 return false;
2857 }
2858 }
2859
2860 Node split_eq;
2861 for (unsigned r = 0; r < 2; r++)
2862 {
2863 Node t = r == 0 ? normal_forms[loop_n_index][loop_index] : t_yz;
2864 split_eq = t.eqNode(d_emptyString);
2865 Node split_eqr = Rewriter::rewrite(split_eq);
2866 // the equality could rewrite to false
2867 if (!split_eqr.isConst())
2868 {
2869 if (!areDisequal(t, d_emptyString))
2870 {
2871 // try to make t equal to empty to avoid loop
2872 info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
2873 info.d_id = INFER_LEN_SPLIT_EMP;
2874 return true;
2875 }
2876 else
2877 {
2878 info.d_ant.push_back(split_eq.negate());
2879 }
2880 }
2881 else
2882 {
2883 Assert(!split_eqr.getConst<bool>());
2884 }
2885 }
2886
2887 Node ant = mkExplain(info.d_ant);
2888 info.d_ant.clear();
2889 info.d_antn.push_back(ant);
2890
2891 Node str_in_re;
2892 if (s_zy == t_yz && r == d_emptyString && s_zy.isConst()
2893 && s_zy.getConst<String>().isRepeated())
2894 {
2895 Node rep_c = nm->mkConst(s_zy.getConst<String>().substr(0, 1));
2896 Trace("strings-loop") << "Special case (X)="
2897 << normal_forms[other_n_index][index] << " "
2898 << std::endl;
2899 Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
2900 // special case
2901 str_in_re =
2902 nm->mkNode(kind::STRING_IN_REGEXP,
2903 normal_forms[other_n_index][index],
2904 nm->mkNode(kind::REGEXP_STAR,
2905 nm->mkNode(kind::STRING_TO_REGEXP, rep_c)));
2906 conc = str_in_re;
2907 }
2908 else if (t_yz.isConst())
2909 {
2910 Trace("strings-loop") << "Strings::Loop: Const Normal Breaking."
2911 << std::endl;
2912 CVC4::String s = t_yz.getConst<CVC4::String>();
2913 unsigned size = s.size();
2914 std::vector<Node> vconc;
2915 for (unsigned len = 1; len <= size; len++)
2916 {
2917 Node y = nm->mkConst(s.substr(0, len));
2918 Node z = nm->mkConst(s.substr(len, size - len));
2919 Node restr = s_zy;
2920 Node cc;
2921 if (r != d_emptyString)
2922 {
2923 std::vector<Node> v2(vec_r);
2924 v2.insert(v2.begin(), y);
2925 v2.insert(v2.begin(), z);
2926 restr = mkConcat(z, y);
2927 cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(v2)));
2928 }
2929 else
2930 {
2931 cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(z, y)));
2932 }
2933 if (cc == d_false)
2934 {
2935 continue;
2936 }
2937 Node conc2 = nm->mkNode(
2938 kind::STRING_IN_REGEXP,
2939 normal_forms[other_n_index][index],
2940 nm->mkNode(kind::REGEXP_CONCAT,
2941 nm->mkNode(kind::STRING_TO_REGEXP, y),
2942 nm->mkNode(kind::REGEXP_STAR,
2943 nm->mkNode(kind::STRING_TO_REGEXP, restr))));
2944 cc = cc == d_true ? conc2 : nm->mkNode(kind::AND, cc, conc2);
2945 d_regexp_ant[conc2] = ant;
2946 vconc.push_back(cc);
2947 }
2948 conc = vconc.size() == 0 ? Node::null() : vconc.size() == 1
2949 ? vconc[0]
2950 : nm->mkNode(kind::OR, vconc);
2951 }
2952 else
2953 {
2954 Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking."
2955 << std::endl;
2956 // right
2957 Node sk_w = mkSkolemS("w_loop");
2958 Node sk_y = mkSkolemS("y_loop", 1);
2959 Node sk_z = mkSkolemS("z_loop");
2960 // t1 * ... * tn = y * z
2961 Node conc1 = t_yz.eqNode(mkConcat(sk_y, sk_z));
2962 // s1 * ... * sk = z * y * r
2963 vec_r.insert(vec_r.begin(), sk_y);
2964 vec_r.insert(vec_r.begin(), sk_z);
2965 Node conc2 = s_zy.eqNode(mkConcat(vec_r));
2966 Node conc3 =
2967 normal_forms[other_n_index][index].eqNode(mkConcat(sk_y, sk_w));
2968 Node restr = r == d_emptyString ? s_zy : mkConcat(sk_z, sk_y);
2969 str_in_re =
2970 nm->mkNode(kind::STRING_IN_REGEXP,
2971 sk_w,
2972 nm->mkNode(kind::REGEXP_STAR,
2973 nm->mkNode(kind::STRING_TO_REGEXP, restr)));
2974
2975 std::vector<Node> vec_conc;
2976 vec_conc.push_back(conc1);
2977 vec_conc.push_back(conc2);
2978 vec_conc.push_back(conc3);
2979 vec_conc.push_back(str_in_re);
2980 // vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
2981 conc = nm->mkNode(kind::AND, vec_conc);
2982 } // normal case
2983
2984 // set its antecedant to ant, to say when it is relevant
2985 if (!str_in_re.isNull())
2986 {
2987 d_regexp_ant[str_in_re] = ant;
2988 }
2989 // we will be done
2990 if (options::stringProcessLoop())
2991 {
2992 info.d_conc = conc;
2993 info.d_id = INFER_FLOOP;
2994 info.d_nf_pair[0] = normal_form_src[i];
2995 info.d_nf_pair[1] = normal_form_src[j];
2996 return true;
2997 }
2998 d_out->setIncomplete();
2999 return false;
3000 }
3001
3002 //return true for lemma, false if we succeed
3003 void TheoryStrings::processDeq( Node ni, Node nj ) {
3004 //Assert( areDisequal( ni, nj ) );
3005 if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
3006 std::vector< Node > nfi;
3007 nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
3008 std::vector< Node > nfj;
3009 nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
3010
3011 int revRet = processReverseDeq( nfi, nfj, ni, nj );
3012 if( revRet!=0 ){
3013 return;
3014 }
3015
3016 nfi.clear();
3017 nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
3018 nfj.clear();
3019 nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
3020
3021 unsigned index = 0;
3022 while( index<nfi.size() || index<nfj.size() ){
3023 int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
3024 if( ret!=0 ) {
3025 return;
3026 }else{
3027 Assert( index<nfi.size() && index<nfj.size() );
3028 Node i = nfi[index];
3029 Node j = nfj[index];
3030 Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl;
3031 if( !areEqual( i, j ) ){
3032 Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
3033 std::vector< Node > lexp;
3034 Node li = getLength( i, lexp );
3035 Node lj = getLength( j, lexp );
3036 if( areDisequal( li, lj ) ){
3037 if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
3038 //check if empty
3039 Node const_k = i.getKind() == kind::CONST_STRING ? i : j;
3040 Node nconst_k = i.getKind() == kind::CONST_STRING ? j : i;
3041 Node lnck = i.getKind() == kind::CONST_STRING ? lj : li;
3042 if( !d_equalityEngine.areDisequal( nconst_k, d_emptyString, true ) ){
3043 Node eq = nconst_k.eqNode( d_emptyString );
3044 Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
3045 sendInference( d_empty_vec, conc, "D-DISL-Emp-Split" );
3046 return;
3047 }else{
3048 //split on first character
3049 CVC4::String str = const_k.getConst<String>();
3050 Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) );
3051 if( areEqual( lnck, d_one ) ){
3052 if( areDisequal( firstChar, nconst_k ) ){
3053 return;
3054 }else if( !areEqual( firstChar, nconst_k ) ){
3055 //splitting on demand : try to make them disequal
3056 if (sendSplit(
3057 firstChar, nconst_k, "S-Split(DEQL-Const)", false))
3058 {
3059 return;
3060 }
3061 }
3062 }else{
3063 Node sk = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt, "dc_spt", 2 );
3064 Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem" );
3065 Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) );
3066 eq1 = Rewriter::rewrite( eq1 );
3067 Node eq2 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, skr ) );
3068 std::vector< Node > antec;
3069 antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
3070 antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
3071 antec.push_back( nconst_k.eqNode( d_emptyString ).negate() );
3072 sendInference( antec, NodeManager::currentNM()->mkNode( kind::OR,
3073 NodeManager::currentNM()->mkNode( kind::AND, eq1, sk.eqNode( firstChar ).negate() ), eq2 ), "D-DISL-CSplit" );
3074 d_pending_req_phase[ eq1 ] = true;
3075 return;
3076 }
3077 }
3078 }else{
3079 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
3080 //must add lemma
3081 std::vector< Node > antec;
3082 std::vector< Node > antec_new_lits;
3083 antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
3084 antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
3085 //check disequal
3086 if( areDisequal( ni, nj ) ){
3087 antec.push_back( ni.eqNode( nj ).negate() );
3088 }else{
3089 antec_new_lits.push_back( ni.eqNode( nj ).negate() );
3090 }
3091 antec_new_lits.push_back( li.eqNode( lj ).negate() );
3092 std::vector< Node > conc;
3093 Node sk1 = mkSkolemCached( i, j, sk_id_deq_x, "x_dsplit" );
3094 Node sk2 = mkSkolemCached( i, j, sk_id_deq_y, "y_dsplit" );
3095 Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 );
3096 //Node nemp = sk3.eqNode(d_emptyString).negate();
3097 //conc.push_back(nemp);
3098 Node lsk1 = mkLength( sk1 );
3099 conc.push_back( lsk1.eqNode( li ) );
3100 Node lsk2 = mkLength( sk2 );
3101 conc.push_back( lsk2.eqNode( lj ) );
3102 conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
3103 sendInference( antec, antec_new_lits, NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
3104 ++(d_statistics.d_deq_splits);
3105 return;
3106 }
3107 }else if( areEqual( li, lj ) ){
3108 Assert( !areDisequal( i, j ) );
3109 //splitting on demand : try to make them disequal
3110 if (sendSplit(i, j, "S-Split(DEQL)", false))
3111 {
3112 return;
3113 }
3114 }else{
3115 //splitting on demand : try to make lengths equal
3116 if (sendSplit(li, lj, "D-Split"))
3117 {
3118 return;
3119 }
3120 }
3121 }
3122 index++;
3123 }
3124 }
3125 Assert( false );
3126 }
3127 }
3128
3129 int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ) {
3130 //reverse normal form of i, j
3131 std::reverse( nfi.begin(), nfi.end() );
3132 std::reverse( nfj.begin(), nfj.end() );
3133
3134 unsigned index = 0;
3135 int ret = processSimpleDeq( nfi, nfj, ni, nj, index, true );
3136
3137 //reverse normal form of i, j
3138 std::reverse( nfi.begin(), nfi.end() );
3139 std::reverse( nfj.begin(), nfj.end() );
3140
3141 return ret;
3142 }
3143
3144 int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ){
3145 // See if one side is constant, if so, the disequality ni != nj is satisfied
3146 // since ni does not contain nj or vice versa.
3147 // This is only valid when isRev is false, since when isRev=true, the contents
3148 // of normal form vectors nfi and nfj are reversed.
3149 if (!isRev)
3150 {
3151 for (unsigned i = 0; i < 2; i++)
3152 {
3153 Node c = getConstantEqc(i == 0 ? ni : nj);
3154 if (!c.isNull())
3155 {
3156 int findex, lindex;
3157 if (!TheoryStringsRewriter::canConstantContainList(
3158 c, i == 0 ? nfj : nfi, findex, lindex))
3159 {
3160 Trace("strings-solve-debug")
3161 << "Disequality: constant cannot contain list" << std::endl;
3162 return 1;
3163 }
3164 }
3165 }
3166 }
3167 while( index<nfi.size() || index<nfj.size() ) {
3168 if( index>=nfi.size() || index>=nfj.size() ){
3169 Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
3170 std::vector< Node > ant;
3171 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
3172 Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] );
3173 Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] );
3174 ant.push_back( lni.eqNode( lnj ) );
3175 ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
3176 ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
3177 std::vector< Node > cc;
3178 std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
3179 for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
3180 cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
3181 }
3182 Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
3183 conc = Rewriter::rewrite( conc );
3184 sendInference( ant, conc, "Disequality Normalize Empty", true);
3185 return -1;
3186 }else{
3187 Node i = nfi[index];
3188 Node j = nfj[index];
3189 Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl;
3190 if( !areEqual( i, j ) ) {
3191 if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
3192 unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
3193 bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
3194 if( isSameFix ) {
3195 //same prefix/suffix
3196 //k is the index of the string that is shorter
3197 Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j;
3198 Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i;
3199 Node remainderStr;
3200 if( isRev ){
3201 int new_len = nl.getConst<String>().size() - len_short;
3202 remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) );
3203 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
3204 } else {
3205 remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr( len_short ) );
3206 Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
3207 }
3208 if( i.getConst<String>().size() < j.getConst<String>().size() ) {
3209 nfj.insert( nfj.begin() + index + 1, remainderStr );
3210 nfj[index] = nfi[index];
3211 } else {
3212 nfi.insert( nfi.begin() + index + 1, remainderStr );
3213 nfi[index] = nfj[index];
3214 }
3215 }else{
3216 return 1;
3217 }
3218 }else{
3219 std::vector< Node > lexp;
3220 Node li = getLength( i, lexp );
3221 Node lj = getLength( j, lexp );
3222 if( areEqual( li, lj ) && areDisequal( i, j ) ){
3223 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
3224 //we are done: D-Remove
3225 return 1;
3226 }else{
3227 return 0;
3228 }
3229 }
3230 }
3231 index++;
3232 }
3233 }
3234 return 0;
3235 }
3236
3237 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){
3238 if( !isNormalFormPair( n1, n2 ) ){
3239 int index = 0;
3240 NodeIntMap::const_iterator it = d_nf_pairs.find( n1 );
3241 if( it!=d_nf_pairs.end() ){
3242 index = (*it).second;
3243 }
3244 d_nf_pairs[n1] = index + 1;
3245 if( index<(int)d_nf_pairs_data[n1].size() ){
3246 d_nf_pairs_data[n1][index] = n2;
3247 }else{
3248 d_nf_pairs_data[n1].push_back( n2 );
3249 }
3250 Assert( isNormalFormPair( n1, n2 ) );
3251 } else {
3252 Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
3253 }
3254 }
3255
3256 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
3257 //TODO: modulo equality?
3258 return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
3259 }
3260
3261 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
3262 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
3263 NodeIntMap::const_iterator it = d_nf_pairs.find( n1 );
3264 if( it!=d_nf_pairs.end() ){
3265 Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() );
3266 for( int i=0; i<(*it).second; i++ ){
3267 Assert( i<(int)d_nf_pairs_data[n1].size() );
3268 if( d_nf_pairs_data[n1][i]==n2 ){
3269 return true;
3270 }
3271 }
3272 }
3273 return false;
3274 }
3275
3276 void TheoryStrings::registerTerm( Node n, int effort ) {
3277 // 0 : upon preregistration or internal assertion
3278 // 1 : upon occurrence in length term
3279 // 2 : before normal form computation
3280 // 3 : called on normal form terms
3281 bool do_register = false;
3282 if( options::stringEagerLen() ){
3283 do_register = effort==0;
3284 }else{
3285 do_register = effort>0 || n.getKind()!=kind::STRING_CONCAT;
3286 }
3287 if( do_register ){
3288 if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) {
3289 d_registered_terms_cache.insert(n);
3290 Debug("strings-register") << "TheoryStrings::registerTerm() " << n << ", effort = " << effort << std::endl;
3291 if(n.getType().isString()) {
3292 //register length information:
3293 // for variables, split on empty vs positive length
3294 // for concat/const/replace, introduce proxy var and state length relation
3295 Node lsum;
3296 bool processed = false;
3297 if( n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
3298 if( d_length_lemma_terms_cache.find( n )==d_length_lemma_terms_cache.end() ){
3299 Node lsumb = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n );
3300 lsum = Rewriter::rewrite( lsumb );
3301 // can register length term if it does not rewrite
3302 if( lsum==lsumb ){
3303 sendLengthLemma( n );
3304 processed = true;
3305 }
3306 }else{
3307 processed = true;
3308 }
3309 }
3310 if( !processed ){
3311 Node sk = mkSkolemS( "lsym", -1 );
3312 StringsProxyVarAttribute spva;
3313 sk.setAttribute(spva,true);
3314 Node eq = Rewriter::rewrite( sk.eqNode(n) );
3315 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
3316 d_proxy_var[n] = sk;
3317 Trace("strings-assert") << "(assert " << eq << ")" << std::endl;
3318 d_out->lemma(eq);
3319 Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
3320 if( n.getKind()==kind::STRING_CONCAT ){
3321 std::vector<Node> node_vec;
3322 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
3323 if( n[i].getAttribute(StringsProxyVarAttribute()) ){
3324 Assert( d_proxy_var_to_length.find( n[i] )!=d_proxy_var_to_length.end() );
3325 node_vec.push_back( d_proxy_var_to_length[n[i]] );
3326 }else{
3327 Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
3328 node_vec.push_back(lni);
3329 }
3330 }
3331 lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
3332 lsum = Rewriter::rewrite( lsum );
3333 }else if( n.getKind()==kind::CONST_STRING ){
3334 lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
3335 }
3336 Assert( !lsum.isNull() );
3337 d_proxy_var_to_length[sk] = lsum;
3338 Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) );
3339 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
3340 Trace("strings-lemma-debug") << " prerewrite : " << skl.eqNode( lsum ) << std::endl;
3341 Trace("strings-assert") << "(assert " << ceq << ")" << std::endl;
3342 d_out->lemma(ceq);
3343
3344 }
3345 } else {
3346 AlwaysAssert(false, "String Terms only in registerTerm.");
3347 }
3348 }
3349 }
3350 }
3351
3352 void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) {
3353 eq = eq.isNull() ? d_false : Rewriter::rewrite( eq );
3354 if( eq!=d_true ){
3355 if( Trace.isOn("strings-infer-debug") ){
3356 Trace("strings-infer-debug") << "By " << c << ", infer : " << eq << " from: " << std::endl;
3357 for( unsigned i=0; i<exp.size(); i++ ){
3358 Trace("strings-infer-debug") << " " << exp[i] << std::endl;
3359 }
3360 for( unsigned i=0; i<exp_n.size(); i++ ){
3361 Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl;
3362 }
3363 //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
3364 }
3365 //check if we should send a lemma or an inference
3366 if( asLemma || eq==d_false || eq.getKind()==kind::OR || !exp_n.empty() || options::stringInferAsLemmas() ){
3367 Node eq_exp;
3368 if( options::stringRExplainLemmas() ){
3369 eq_exp = mkExplain( exp, exp_n );
3370 }else{
3371 if( exp.empty() ){
3372 eq_exp = mkAnd( exp_n );
3373 }else if( exp_n.empty() ){
3374 eq_exp = mkAnd( exp );
3375 }else{
3376 std::vector< Node > ev;
3377 ev.insert( ev.end(), exp.begin(), exp.end() );
3378 ev.insert( ev.end(), exp_n.begin(), exp_n.end() );
3379 eq_exp = NodeManager::currentNM()->mkNode( kind::AND, ev );
3380 }
3381 }
3382 // if we have unexplained literals, this lemma is not a conflict
3383 if (eq == d_false && !exp_n.empty())
3384 {
3385 eq = eq_exp.negate();
3386 eq_exp = d_true;
3387 }
3388 sendLemma( eq_exp, eq, c );
3389 }else{
3390 sendInfer( mkAnd( exp ), eq, c );
3391 }
3392 }
3393 }
3394
3395 void TheoryStrings::sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma ) {
3396 std::vector< Node > exp_n;
3397 sendInference( exp, exp_n, eq, c, asLemma );
3398 }
3399
3400 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
3401 if( conc.isNull() || conc == d_false ) {
3402 Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
3403 Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
3404 Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
3405 d_out->conflict(ant);
3406 d_conflict = true;
3407 } else {
3408 Node lem;
3409 if( ant == d_true ) {
3410 lem = conc;
3411 }else{
3412 lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
3413 }
3414 Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
3415 Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
3416 d_lemma_cache.push_back( lem );
3417 }
3418 }
3419
3420 void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
3421 if( options::stringInferSym() ){
3422 std::vector< Node > vars;
3423 std::vector< Node > subs;
3424 std::vector< Node > unproc;
3425 inferSubstitutionProxyVars( eq_exp, vars, subs, unproc );
3426 if( unproc.empty() ){
3427 Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
3428 Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
3429 Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl;
3430 for( unsigned i=0; i<vars.size(); i++ ){
3431 Trace("strings-lemma-debug") << " " << vars[i] << " -> " << subs[i] << std::endl;
3432 }
3433 sendLemma( d_true, eqs, c );
3434 return;
3435 }else{
3436 for( unsigned i=0; i<unproc.size(); i++ ){
3437 Trace("strings-lemma-debug") << " non-trivial exp : " << unproc[i] << std::endl;
3438 }
3439 }
3440 }
3441 Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
3442 Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
3443 d_pending.push_back( eq );
3444 d_pending_exp[eq] = eq_exp;
3445 d_infer.push_back( eq );
3446 d_infer_exp.push_back( eq_exp );
3447 }
3448
3449 bool TheoryStrings::sendSplit(Node a, Node b, const char* c, bool preq)
3450 {
3451 Node eq = a.eqNode( b );
3452 eq = Rewriter::rewrite( eq );
3453 if (!eq.isConst())
3454 {
3455 Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
3456 Node lemma_or = NodeManager::currentNM()->mkNode(kind::OR, eq, neq);
3457 Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
3458 << std::endl;
3459 d_lemma_cache.push_back(lemma_or);
3460 d_pending_req_phase[eq] = preq;
3461 ++(d_statistics.d_splits);
3462 return true;
3463 }
3464 return false;
3465 }
3466
3467
3468 void TheoryStrings::sendLengthLemma( Node n ){
3469 Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
3470 if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
3471 Node n_len_eq_z = n_len.eqNode( d_zero );
3472 Node n_len_eq_z_2 = n.eqNode( d_emptyString );
3473 n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
3474 n_len_eq_z_2 = Rewriter::rewrite( n_len_eq_z_2 );
3475 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, n_len_eq_z, n_len_eq_z_2 ),
3476 NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
3477 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
3478 d_out->lemma(n_len_geq_zero);
3479 d_out->requirePhase( n_len_eq_z, true );
3480 d_out->requirePhase( n_len_eq_z_2, true );
3481 }
3482 //AJR: probably a good idea
3483 if( options::stringLenGeqZ() ){
3484 Node n_len_geq = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
3485 n_len_geq = Rewriter::rewrite( n_len_geq );
3486 d_out->lemma( n_len_geq );
3487 }
3488 }
3489
3490 void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ) {
3491 if( n.getKind()==kind::AND ){
3492 for( unsigned i=0; i<n.getNumChildren(); i++ ){
3493 inferSubstitutionProxyVars( n[i], vars, subs, unproc );
3494 }
3495 return;
3496 }else if( n.getKind()==kind::EQUAL ){
3497 Node ns = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
3498 ns = Rewriter::rewrite( ns );
3499 if( ns.getKind()==kind::EQUAL ){
3500 Node s;
3501 Node v;
3502 for( unsigned i=0; i<2; i++ ){
3503 Node ss;
3504 if( ns[i].getAttribute(StringsProxyVarAttribute()) ){
3505 ss = ns[i];
3506 }else if( ns[i].isConst() ){
3507 NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] );
3508 if( it!=d_proxy_var.end() ){
3509 ss = (*it).second;
3510 }
3511 }
3512 if( !ss.isNull() ){
3513 v = ns[1-i];
3514 if( v.getNumChildren()==0 ){
3515 if( s.isNull() ){
3516 s = ss;
3517 }else{
3518 //both sides involved in proxy var
3519 if( ss==s ){
3520 return;
3521 }else{
3522 s = Node::null();
3523 }
3524 }
3525 }
3526 }
3527 }
3528 if( !s.isNull() ){
3529 subs.push_back( s );
3530 vars.push_back( v );
3531 return;
3532 }
3533 }else{
3534 n = ns;
3535 }
3536 }
3537 if( n!=d_true ){
3538 unproc.push_back( n );
3539 }
3540 }
3541
3542
3543 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
3544 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
3545 }
3546
3547 Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) {
3548 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) );
3549 }
3550
3551 Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
3552 return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
3553 }
3554
3555 Node TheoryStrings::mkLength( Node t ) {
3556 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
3557 }
3558
3559 Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit ){
3560 //return mkSkolemS( c, isLenSplit );
3561 std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( id );
3562 if( it==d_skolem_cache[a][b].end() ){
3563 Node sk = mkSkolemS( c, isLenSplit );
3564 d_skolem_cache[a][b][id] = sk;
3565 return sk;
3566 }else{
3567 return it->second;
3568 }
3569 }
3570
3571 //isLenSplit: -1-ignore, 0-no restriction, 1-greater than one, 2-one
3572 Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) {
3573 Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" );
3574 d_length_lemma_terms_cache.insert( n );
3575 ++(d_statistics.d_new_skolems);
3576 if( isLenSplit==0 ){
3577 sendLengthLemma( n );
3578 } else if( isLenSplit == 1 ){
3579 registerNonEmptySkolem( n );
3580 }else if( isLenSplit==2 ){
3581 Node len_one = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ).eqNode( d_one );
3582 Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one << std::endl;
3583 Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
3584 d_out->lemma( len_one );
3585 }
3586 return n;
3587 }
3588
3589 void TheoryStrings::registerNonEmptySkolem( Node n ) {
3590 if( d_skolem_ne_reg_cache.find( n )==d_skolem_ne_reg_cache.end() ){
3591 d_skolem_ne_reg_cache.insert( n );
3592 d_equalityEngine.assertEquality(n.eqNode(d_emptyString), false, d_true);
3593 Node len_n_gt_z = NodeManager::currentNM()->mkNode(kind::GT,
3594 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n), d_zero);
3595 Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z << std::endl;
3596 Trace("strings-assert") << "(assert " << len_n_gt_z << ")" << std::endl;
3597 d_out->lemma(len_n_gt_z);
3598 }
3599 }
3600
3601 Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
3602 std::vector< Node > an;
3603 return mkExplain( a, an );
3604 }
3605
3606 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
3607 std::vector< TNode > antec_exp;
3608 for( unsigned i=0; i<a.size(); i++ ) {
3609 if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
3610 bool exp = true;
3611 Debug("strings-explain") << "Ask for explanation of " << a[i] << std::endl;
3612 //assert
3613 if(a[i].getKind() == kind::EQUAL) {
3614 //Assert( hasTerm(a[i][0]) );
3615 //Assert( hasTerm(a[i][1]) );
3616 Assert( areEqual(a[i][0], a[i][1]) );
3617 if( a[i][0]==a[i][1] ){
3618 exp = false;
3619 }
3620 } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
3621 Assert( hasTerm(a[i][0][0]) );
3622 Assert( hasTerm(a[i][0][1]) );
3623 AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
3624 }else if( a[i].getKind() == kind::AND ){
3625 for( unsigned j=0; j<a[i].getNumChildren(); j++ ){
3626 a.push_back( a[i][j] );
3627 }
3628 exp = false;
3629 }
3630 if( exp ) {
3631 unsigned ps = antec_exp.size();
3632 explain(a[i], antec_exp);
3633 Debug("strings-explain") << "Done, explanation was : " << std::endl;
3634 for( unsigned j=ps; j<antec_exp.size(); j++ ) {
3635 Debug("strings-explain") << " " << antec_exp[j] << std::endl;
3636 }
3637 Debug("strings-explain") << std::endl;
3638 }
3639 }
3640 }
3641 for( unsigned i=0; i<an.size(); i++ ) {
3642 if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
3643 Debug("strings-explain") << "Add to explanation (new literal) " << an[i] << std::endl;
3644 antec_exp.push_back(an[i]);
3645 }
3646 }
3647 Node ant;
3648 if( antec_exp.empty() ) {
3649 ant = d_true;
3650 } else if( antec_exp.size()==1 ) {
3651 ant = antec_exp[0];
3652 } else {
3653 ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
3654 }
3655 //ant = Rewriter::rewrite( ant );
3656 return ant;
3657 }
3658
3659 Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
3660 std::vector< Node > au;
3661 for( unsigned i=0; i<a.size(); i++ ){
3662 if( std::find( au.begin(), au.end(), a[i] )==au.end() ){
3663 au.push_back( a[i] );
3664 }
3665 }
3666 if( au.empty() ) {
3667 return d_true;
3668 } else if( au.size() == 1 ) {
3669 return au[0];
3670 } else {
3671 return NodeManager::currentNM()->mkNode( kind::AND, au );
3672 }
3673 }
3674
3675 void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
3676 if( n.getKind()==kind::STRING_CONCAT ) {
3677 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
3678 if( !areEqual( n[i], d_emptyString ) ) {
3679 c.push_back( n[i] );
3680 }
3681 }
3682 }else{
3683 c.push_back( n );
3684 }
3685 }
3686
3687 void TheoryStrings::checkDeqNF() {
3688 std::vector< std::vector< Node > > cols;
3689 std::vector< Node > lts;
3690 std::map< Node, std::map< Node, bool > > processed;
3691
3692 //for each pair of disequal strings, must determine whether their lengths are equal or disequal
3693 for( NodeList::const_iterator id = d_ee_disequalities.begin(); id != d_ee_disequalities.end(); ++id ) {
3694 Node eq = *id;
3695 Node n[2];
3696 for( unsigned i=0; i<2; i++ ){
3697 n[i] = d_equalityEngine.getRepresentative( eq[i] );
3698 }
3699 if( processed[n[0]].find( n[1] )==processed[n[0]].end() ){
3700 processed[n[0]][n[1]] = true;
3701 Node lt[2];
3702 for( unsigned i=0; i<2; i++ ){
3703 EqcInfo* ei = getOrMakeEqcInfo( n[i], false );
3704 lt[i] = ei ? ei->d_length_term : Node::null();
3705 if( lt[i].isNull() ){
3706 lt[i] = eq[i];
3707 }
3708 lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
3709 }
3710 if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){
3711 sendSplit( lt[0], lt[1], "DEQ-LENGTH-SP" );
3712 }
3713 }
3714 }
3715
3716 if( !hasProcessed() ){
3717 separateByLength( d_strings_eqc, cols, lts );
3718 for( unsigned i=0; i<cols.size(); i++ ){
3719 if( cols[i].size()>1 && d_lemma_cache.empty() ){
3720 Trace("strings-solve") << "- Verify disequalities are processed for " << cols[i][0] << ", normal form : ";
3721 printConcat( d_normal_forms[cols[i][0]], "strings-solve" );
3722 Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl;
3723 //must ensure that normal forms are disequal
3724 for( unsigned j=0; j<cols[i].size(); j++ ){
3725 for( unsigned k=(j+1); k<cols[i].size(); k++ ){
3726 //for strings that are disequal, but have the same length
3727 if( areDisequal( cols[i][j], cols[i][k] ) ){
3728 Assert( !d_conflict );
3729 Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
3730 printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
3731 Trace("strings-solve") << " against " << cols[i][k] << " ";
3732 printConcat( d_normal_forms[cols[i][k]], "strings-solve" );
3733 Trace("strings-solve") << "..." << std::endl;
3734 processDeq( cols[i][j], cols[i][k] );
3735 if( hasProcessed() ){
3736 return;
3737 }
3738 }
3739 }
3740 }
3741 }
3742 }
3743 }
3744 }
3745
3746 void TheoryStrings::checkLengthsEqc() {
3747 if( options::stringLenNorm() ){
3748 for( unsigned i=0; i<d_strings_eqc.size(); i++ ){
3749 //if( d_normal_forms[nodes[i]].size()>1 ) {
3750 Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl;
3751 //check if there is a length term for this equivalence class
3752 EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false );
3753 Node lt = ei ? ei->d_length_term : Node::null();
3754 if( !lt.isNull() ) {
3755 Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
3756 //now, check if length normalization has occurred
3757 if( ei->d_normalized_length.get().isNull() ) {
3758 Node nf = mkConcat( d_normal_forms[d_strings_eqc[i]] );
3759 if( Trace.isOn("strings-process-debug") ){
3760 Trace("strings-process-debug") << " normal form is " << nf << " from base " << d_normal_forms_base[d_strings_eqc[i]] << std::endl;
3761 Trace("strings-process-debug") << " normal form exp is: " << std::endl;
3762 for( unsigned j=0; j<d_normal_forms_exp[d_strings_eqc[i]].size(); j++ ){
3763 Trace("strings-process-debug") << " " << d_normal_forms_exp[d_strings_eqc[i]][j] << std::endl;
3764 }
3765 }
3766
3767 //if not, add the lemma
3768 std::vector< Node > ant;
3769 ant.insert( ant.end(), d_normal_forms_exp[d_strings_eqc[i]].begin(), d_normal_forms_exp[d_strings_eqc[i]].end() );
3770 ant.push_back( d_normal_forms_base[d_strings_eqc[i]].eqNode( lt ) );
3771 Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf );
3772 Node lcr = Rewriter::rewrite( lc );
3773 Trace("strings-process-debug") << "Rewrote length " << lc << " to " << lcr << std::endl;
3774 Node eq = llt.eqNode( lcr );
3775 if( llt!=lcr ){
3776 ei->d_normalized_length.set( eq );
3777 sendInference( ant, eq, "LEN-NORM", true );
3778 }
3779 }
3780 }else{
3781 Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
3782 if( !options::stringEagerLen() ){
3783 Node c = mkConcat( d_normal_forms[d_strings_eqc[i]] );
3784 registerTerm( c, 3 );
3785 /*
3786 if( !c.isConst() ){
3787 NodeNodeMap::const_iterator it = d_proxy_var.find( c );
3788 if( it!=d_proxy_var.end() ){
3789 Node pv = (*it).second;
3790 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
3791 Node pvl = d_proxy_var_to_length[pv];
3792 Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
3793 sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
3794 }
3795 }
3796 */
3797 }
3798 }
3799 //} else {
3800 // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
3801 //}
3802 }
3803 }
3804 }
3805
3806 void TheoryStrings::checkCardinality() {
3807 //int cardinality = options::stringCharCardinality();
3808 //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
3809
3810 //AJR: this will create a partition of eqc, where each collection has length that are pairwise propagated to be equal.
3811 // we do not require disequalities between the lengths of each collection, since we split on disequalities between lengths of string terms that are disequal (DEQ-LENGTH-SP).
3812 // TODO: revisit this?
3813 std::vector< std::vector< Node > > cols;
3814 std::vector< Node > lts;
3815 separateByLength( d_strings_eqc, cols, lts );
3816
3817 for( unsigned i = 0; i<cols.size(); ++i ) {
3818 Node lr = lts[i];
3819 Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
3820 if( cols[i].size() > 1 ) {
3821 // size > c^k
3822 unsigned card_need = 1;
3823 double curr = (double)cols[i].size();
3824 while( curr>d_card_size ){
3825 curr = curr/(double)d_card_size;
3826 card_need++;
3827 }
3828 Trace("strings-card") << "Need length " << card_need << " for this number of strings (where alphabet size is " << d_card_size << ")." << std::endl;
3829 //check if we need to split
3830 bool needsSplit = true;
3831 if( lr.isConst() ){
3832 // if constant, compare
3833 Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) );
3834 cmp = Rewriter::rewrite( cmp );
3835 needsSplit = cmp!=d_true;
3836 }else{
3837 // find the minimimum constant that we are unknown to be disequal from, or otherwise stop if we increment such that cardinality does not apply
3838 unsigned r=0;
3839 bool success = true;
3840 while( r<card_need && success ){
3841 Node rr = NodeManager::currentNM()->mkConst<Rational>( Rational(r) );
3842 if( areDisequal( rr, lr ) ){
3843 r++;
3844 }else{
3845 success = false;
3846 }
3847 }
3848 if( r>0 ){
3849 Trace("strings-card") << "Symbolic length " << lr << " must be at least " << r << " due to constant disequalities." << std::endl;
3850 }
3851 needsSplit = r<card_need;
3852 }
3853
3854 if( needsSplit ){
3855 unsigned int int_k = (unsigned int)card_need;
3856 for( std::vector< Node >::iterator itr1 = cols[i].begin();
3857 itr1 != cols[i].end(); ++itr1) {
3858 for( std::vector< Node >::iterator itr2 = itr1 + 1;
3859 itr2 != cols[i].end(); ++itr2) {
3860 if(!areDisequal( *itr1, *itr2 )) {
3861 // add split lemma
3862 if (sendSplit(*itr1, *itr2, "CARD-SP"))
3863 {
3864 return;
3865 }
3866 }
3867 }
3868 }
3869 EqcInfo* ei = getOrMakeEqcInfo( lr, true );
3870 Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
3871 if( int_k+1 > ei->d_cardinality_lem_k.get() ){
3872 Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
3873 //add cardinality lemma
3874 Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
3875 std::vector< Node > vec_node;
3876 vec_node.push_back( dist );
3877 for( std::vector< Node >::iterator itr1 = cols[i].begin();
3878 itr1 != cols[i].end(); ++itr1) {
3879 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
3880 if( len!=lr ) {
3881 Node len_eq_lr = len.eqNode(lr);
3882 vec_node.push_back( len_eq_lr );
3883 }
3884 }
3885 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
3886 Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
3887 cons = Rewriter::rewrite( cons );
3888 ei->d_cardinality_lem_k.set( int_k+1 );
3889 if( cons!=d_true ){
3890 sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true );
3891 return;
3892 }
3893 }
3894 }
3895 }
3896 }
3897 }
3898
3899 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
3900 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
3901 while( !eqcs_i.isFinished() ) {
3902 Node eqc = (*eqcs_i);
3903 //if eqc.getType is string
3904 if (eqc.getType().isString()) {
3905 eqcs.push_back( eqc );
3906 }
3907 ++eqcs_i;
3908 }
3909 }
3910
3911 void TheoryStrings::separateByLength(std::vector< Node >& n,
3912 std::vector< std::vector< Node > >& cols,
3913 std::vector< Node >& lts ) {
3914 unsigned leqc_counter = 0;
3915 std::map< Node, unsigned > eqc_to_leqc;
3916 std::map< unsigned, Node > leqc_to_eqc;
3917 std::map< unsigned, std::vector< Node > > eqc_to_strings;
3918 for( unsigned i=0; i<n.size(); i++ ) {
3919 Node eqc = n[i];
3920 Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
3921 EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
3922 Node lt = ei ? ei->d_length_term : Node::null();
3923 if( !lt.isNull() ){
3924 lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
3925 Node r = d_equalityEngine.getRepresentative( lt );
3926 if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
3927 eqc_to_leqc[r] = leqc_counter;
3928 leqc_to_eqc[leqc_counter] = r;
3929 leqc_counter++;
3930 }
3931 eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
3932 }else{
3933 eqc_to_strings[leqc_counter].push_back( eqc );
3934 leqc_counter++;
3935 }
3936 }
3937 for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
3938 cols.push_back( std::vector< Node >() );
3939 cols.back().insert( cols.back().end(), it->second.begin(), it->second.end() );
3940 lts.push_back( leqc_to_eqc[it->first] );
3941 }
3942 }
3943
3944 void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
3945 for( unsigned i=0; i<n.size(); i++ ){
3946 if( i>0 ) Trace(c) << " ++ ";
3947 Trace(c) << n[i];
3948 }
3949 }
3950
3951
3952
3953 //// Finite Model Finding
3954
3955 Node TheoryStrings::getNextDecisionRequest( unsigned& priority ) {
3956 if( options::stringFMF() && !d_conflict ){
3957 Node in_var_lsum = d_input_var_lsum.get();
3958 //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
3959 //initialize the term we will minimize
3960 if( in_var_lsum.isNull() && !d_input_vars.empty() ){
3961 Trace("strings-fmf-debug") << "Input variables: ";
3962 std::vector< Node > ll;
3963 for(NodeSet::key_iterator itr = d_input_vars.key_begin();
3964 itr != d_input_vars.key_end(); ++itr) {
3965 Trace("strings-fmf-debug") << " " << (*itr) ;
3966 ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) );
3967 }
3968 Trace("strings-fmf-debug") << std::endl;
3969 in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll );
3970 in_var_lsum = Rewriter::rewrite( in_var_lsum );
3971 d_input_var_lsum.set( in_var_lsum );
3972 }
3973 if( !in_var_lsum.isNull() ){
3974 //Trace("strings-fmf") << "Get next decision request." << std::endl;
3975 //check if we need to decide on something
3976 int decideCard = d_curr_cardinality.get();
3977 if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){
3978 bool value;
3979 Node cnode = d_cardinality_lits[ d_curr_cardinality.get() ];
3980 if( d_valuation.hasSatValue( cnode, value ) ) {
3981 if( !value ){
3982 d_curr_cardinality.set( d_curr_cardinality.get() + 1 );
3983 decideCard = d_curr_cardinality.get();
3984 Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl;
3985 }else{
3986 decideCard = -1;
3987 Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl;
3988 }
3989 }else{
3990 Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl;
3991 }
3992 }
3993 if( decideCard!=-1 ){
3994 if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){
3995 Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) );
3996 lit = Rewriter::rewrite( lit );
3997 d_cardinality_lits[decideCard] = lit;
3998 Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
3999 Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem << ", decideCard = " << decideCard << std::endl;
4000 d_out->lemma( lem );
4001 d_out->requirePhase( lit, true );
4002 }
4003 Node lit = d_cardinality_lits[ decideCard ];
4004 Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit << std::endl;
4005 priority = 1;
4006 return lit;
4007 }
4008 }
4009 }
4010 return Node::null();
4011 }
4012
4013 Node TheoryStrings::ppRewrite(TNode atom) {
4014 Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
4015 if( !options::stringLazyPreproc() ){
4016 //eager preprocess here
4017 std::vector< Node > new_nodes;
4018 Node ret = d_preproc.processAssertion( atom, new_nodes );
4019 if( ret!=atom ){
4020 Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl;
4021 for( unsigned i=0; i<new_nodes.size(); i++ ){
4022 Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl;
4023 d_out->lemma( new_nodes[i] );
4024 }
4025 return ret;
4026 }else{
4027 Assert( new_nodes.empty() );
4028 }
4029 }
4030 return atom;
4031 }
4032
4033 // Stats
4034 TheoryStrings::Statistics::Statistics():
4035 d_splits("theory::strings::NumOfSplitOnDemands", 0),
4036 d_eq_splits("theory::strings::NumOfEqSplits", 0),
4037 d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
4038 d_loop_lemmas("theory::strings::NumOfLoops", 0),
4039 d_new_skolems("theory::strings::NumOfNewSkolems", 0)
4040 {
4041 smtStatisticsRegistry()->registerStat(&d_splits);
4042 smtStatisticsRegistry()->registerStat(&d_eq_splits);
4043 smtStatisticsRegistry()->registerStat(&d_deq_splits);
4044 smtStatisticsRegistry()->registerStat(&d_loop_lemmas);
4045 smtStatisticsRegistry()->registerStat(&d_new_skolems);
4046 }
4047
4048 TheoryStrings::Statistics::~Statistics(){
4049 smtStatisticsRegistry()->unregisterStat(&d_splits);
4050 smtStatisticsRegistry()->unregisterStat(&d_eq_splits);
4051 smtStatisticsRegistry()->unregisterStat(&d_deq_splits);
4052 smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas);
4053 smtStatisticsRegistry()->unregisterStat(&d_new_skolems);
4054 }
4055
4056
4057
4058
4059
4060
4061
4062
4063
4064
4065
4066
4067
4068
4069
4070
4071
4072
4073
4074
4075 //// Regular Expressions
4076
4077
4078 unsigned TheoryStrings::getNumMemberships( Node n, bool isPos ) {
4079 if( isPos ){
4080 NodeIntMap::const_iterator it = d_pos_memberships.find( n );
4081 if( it!=d_pos_memberships.end() ){
4082 return (*it).second;
4083 }
4084 }else{
4085 NodeIntMap::const_iterator it = d_neg_memberships.find( n );
4086 if( it!=d_neg_memberships.end() ){
4087 return (*it).second;
4088 }
4089 }
4090 return 0;
4091 }
4092
4093 Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) {
4094 return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i];
4095 }
4096
4097 Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
4098 if(d_regexp_ant.find(atom) == d_regexp_ant.end()) {
4099 return NodeManager::currentNM()->mkNode(kind::AND, ant, atom);
4100 } else {
4101 Node n = d_regexp_ant[atom];
4102 return NodeManager::currentNM()->mkNode(kind::AND, ant, n);
4103 }
4104 }
4105
4106 bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
4107 Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
4108 Assert( d_regexp_opr.checkConstRegExp(r) );
4109
4110 if( !s.isEmptyString() ) {
4111 Node dc = r;
4112
4113 for(unsigned i=0; i<s.size(); ++i) {
4114 CVC4::String c = s.substr(i, 1);
4115 Node dc2;
4116 int rt = d_regexp_opr.derivativeS(dc, c, dc2);
4117 dc = dc2;
4118 if(rt == 0) {
4119 Unreachable();
4120 } else if(rt == 2) {
4121 return false;
4122 }
4123 }
4124 r = dc;
4125 }
4126
4127 return true;
4128 }
4129
4130 Node TheoryStrings::applyRSplit(Node s1, Node s2, Node r) {
4131 Assert(d_regexp_opr.checkConstRegExp(r));
4132
4133 std::vector< std::pair< Node, Node > > vec_can;
4134 d_regexp_opr.splitRegExp(r, vec_can);
4135 //TODO: lazy cache or eager?
4136 std::vector< Node > vec_or;
4137
4138 for(unsigned int i=0; i<vec_can.size(); i++) {
4139 Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
4140 Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
4141 Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
4142 vec_or.push_back( c );
4143 }
4144 Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
4145 return conc;
4146 }
4147
4148 bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) {
4149 if(XinR_with_exps.size() > 0) {
4150 //TODO: get vector, var, store.
4151 return true;
4152 } else {
4153 return false;
4154 }
4155 }
4156
4157 void TheoryStrings::checkMemberships() {
4158 //add the memberships
4159 std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
4160 for (unsigned i = 0; i < mems.size(); i++) {
4161 Node n = mems[i];
4162 Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
4163 if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){
4164 bool pol = d_extf_info_tmp[n].d_pol==1;
4165 Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl;
4166 addMembership( pol ? n : n.negate() );
4167 }else{
4168 Trace("strings-process-debug") << " irrelevant (non-asserted) membership : " << n << std::endl;
4169 }
4170 }
4171
4172 bool addedLemma = false;
4173 bool changed = false;
4174 std::vector< Node > processed;
4175 std::vector< Node > cprocessed;
4176
4177 Trace("regexp-debug") << "Checking Memberships ... " << std::endl;
4178 //if(options::stringEIT()) {
4179 //TODO: Opt for normal forms
4180 for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){
4181 bool spflag = false;
4182 Node x = (*itr_xr).first;
4183 Trace("regexp-debug") << "Checking Memberships for " << x << std::endl;
4184 if(d_inter_index.find(x) == d_inter_index.end()) {
4185 d_inter_index[x] = 0;
4186 }
4187 int cur_inter_idx = d_inter_index[x];
4188 unsigned n_pmem = (*itr_xr).second;
4189 Assert( getNumMemberships( x, true )==n_pmem );
4190 if( cur_inter_idx != (int)n_pmem ) {
4191 if( n_pmem == 1) {
4192 d_inter_cache[x] = getMembership( x, true, 0 );
4193 d_inter_index[x] = 1;
4194 Trace("regexp-debug") << "... only one choice " << std::endl;
4195 } else if(n_pmem > 1) {
4196 Node r;
4197 if(d_inter_cache.find(x) != d_inter_cache.end()) {
4198 r = d_inter_cache[x];
4199 }
4200 if(r.isNull()) {
4201 r = getMembership( x, true, 0 );
4202 cur_inter_idx = 1;
4203 }
4204
4205 unsigned k_start = cur_inter_idx;
4206 Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << n_pmem << std::endl;
4207 for(unsigned k = k_start; k<n_pmem; k++) {
4208 Node r2 = getMembership( x, true, k );
4209 r = d_regexp_opr.intersect(r, r2, spflag);
4210 if(spflag) {
4211 break;
4212 } else if(r == d_emptyRegexp) {
4213 std::vector< Node > vec_nodes;
4214 for( unsigned kk=0; kk<=k; kk++ ){
4215 Node rr = getMembership( x, true, kk );
4216 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, rr);
4217 vec_nodes.push_back( n );
4218 }
4219 Node conc;
4220 sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
4221 addedLemma = true;
4222 break;
4223 }
4224 if(d_conflict) {
4225 break;
4226 }
4227 }
4228 //updates
4229 if(!d_conflict && !spflag) {
4230 d_inter_cache[x] = r;
4231 d_inter_index[x] = (int)n_pmem;
4232 }
4233 }
4234 }
4235 }
4236 //}
4237
4238 Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma << std::endl;
4239 if(!addedLemma) {
4240 for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
4241 //check regular expression membership
4242 Node assertion = d_regexp_memberships[i];
4243 Trace("regexp-debug") << "Check : " << assertion << " " << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()) << " " << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end()) << std::endl;
4244 if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end()
4245 && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
4246 Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
4247 Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
4248 bool polarity = assertion.getKind()!=kind::NOT;
4249 bool flag = true;
4250 Node x = atom[0];
4251 Node r = atom[1];
4252 std::vector< Node > rnfexp;
4253
4254 //if(options::stringOpt1()) {
4255 if(true){
4256 if(!x.isConst()) {
4257 x = getNormalString( x, rnfexp);
4258 changed = true;
4259 }
4260 if(!d_regexp_opr.checkConstRegExp(r)) {
4261 r = getNormalSymRegExp(r, rnfexp);
4262 changed = true;
4263 }
4264 Trace("strings-regexp-nf") << "Term " << atom << " is normalized to " << x << " IN " << r << std::endl;
4265 if(changed) {
4266 Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r) );
4267 if(!polarity) {
4268 tmp = tmp.negate();
4269 }
4270 if(tmp == d_true) {
4271 d_regexp_ccached.insert(assertion);
4272 continue;
4273 } else if(tmp == d_false) {
4274 Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
4275 Node conc = Node::null();
4276 sendLemma(antec, conc, "REGEXP NF Conflict");
4277 addedLemma = true;
4278 break;
4279 }
4280 }
4281 }
4282
4283 if( polarity ) {
4284 flag = checkPDerivative(x, r, atom, addedLemma, rnfexp);
4285 if(options::stringOpt2() && flag) {
4286 if(d_regexp_opr.checkConstRegExp(r) && x.getKind()==kind::STRING_CONCAT) {
4287 std::vector< std::pair< Node, Node > > vec_can;
4288 d_regexp_opr.splitRegExp(r, vec_can);
4289 //TODO: lazy cache or eager?
4290 std::vector< Node > vec_or;
4291 std::vector< Node > vec_s2;
4292 for(unsigned int s2i=1; s2i<x.getNumChildren(); s2i++) {
4293 vec_s2.push_back(x[s2i]);
4294 }
4295 Node s1 = x[0];
4296 Node s2 = mkConcat(vec_s2);
4297 for(unsigned int i=0; i<vec_can.size(); i++) {
4298 Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
4299 Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
4300 Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
4301 vec_or.push_back( c );
4302 }
4303 Node conc = vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
4304 //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
4305 Node antec = mkRegExpAntec(atom, mkExplain(rnfexp));
4306 if(conc == d_true) {
4307 if(changed) {
4308 cprocessed.push_back( assertion );
4309 } else {
4310 processed.push_back( assertion );
4311 }
4312 } else {
4313 sendLemma(antec, conc, "RegExp-CST-SP");
4314 }
4315 addedLemma = true;
4316 flag = false;
4317 }
4318 }
4319 } else {
4320 if(! options::stringExp()) {
4321 throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
4322 }
4323 }
4324 if(flag) {
4325 //check if the term is atomic
4326 Node xr = getRepresentative( x );
4327 //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
4328 //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
4329 Trace("strings-regexp")
4330 << "Unroll/simplify membership of atomic term " << xr
4331 << std::endl;
4332 // if so, do simple unrolling
4333 std::vector<Node> nvec;
4334
4335 if (nvec.empty())
4336 {
4337 d_regexp_opr.simplify(atom, nvec, polarity);
4338 }
4339 Node antec = assertion;
4340 if (d_regexp_ant.find(assertion) != d_regexp_ant.end())
4341 {
4342 antec = d_regexp_ant[assertion];
4343 for (std::vector<Node>::const_iterator itr = nvec.begin();
4344 itr < nvec.end();
4345 itr++)
4346 {
4347 if (itr->getKind() == kind::STRING_IN_REGEXP)
4348 {
4349 if (d_regexp_ant.find(*itr) == d_regexp_ant.end())
4350 {
4351 d_regexp_ant[*itr] = antec;
4352 }
4353 }
4354 }
4355 }
4356 antec = NodeManager::currentNM()->mkNode(
4357 kind::AND, antec, mkExplain(rnfexp));
4358 Node conc = nvec.size() == 1
4359 ? nvec[0]
4360 : NodeManager::currentNM()->mkNode(kind::AND, nvec);
4361 conc = Rewriter::rewrite(conc);
4362 sendLemma(antec, conc, "REGEXP_Unfold");
4363 addedLemma = true;
4364 if (changed)
4365 {
4366 cprocessed.push_back(assertion);
4367 }
4368 else
4369 {
4370 processed.push_back(assertion);
4371 }
4372 // d_regexp_ucached[assertion] = true;
4373 }
4374 }
4375 if(d_conflict) {
4376 break;
4377 }
4378 }
4379 }
4380 if( addedLemma ) {
4381 if( !d_conflict ){
4382 for( unsigned i=0; i<processed.size(); i++ ) {
4383 Trace("strings-regexp") << "...add " << processed[i] << " to u-cache." << std::endl;
4384 d_regexp_ucached.insert(processed[i]);
4385 }
4386 for( unsigned i=0; i<cprocessed.size(); i++ ) {
4387 Trace("strings-regexp") << "...add " << cprocessed[i] << " to c-cache." << std::endl;
4388 d_regexp_ccached.insert(cprocessed[i]);
4389 }
4390 }
4391 }
4392 }
4393
4394 bool TheoryStrings::checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp ) {
4395
4396 Node antnf = mkExplain(nf_exp);
4397
4398 if(areEqual(x, d_emptyString)) {
4399 Node exp;
4400 switch(d_regexp_opr.delta(r, exp)) {
4401 case 0: {
4402 Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
4403 antec = NodeManager::currentNM()->mkNode(kind::AND, antec, antnf);
4404 sendLemma(antec, exp, "RegExp Delta");
4405 addedLemma = true;
4406 d_regexp_ccached.insert(atom);
4407 return false;
4408 }
4409 case 1: {
4410 d_regexp_ccached.insert(atom);
4411 break;
4412 }
4413 case 2: {
4414 Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
4415 antec = NodeManager::currentNM()->mkNode(kind::AND, antec, antnf);
4416 Node conc = Node::null();
4417 sendLemma(antec, conc, "RegExp Delta CONFLICT");
4418 addedLemma = true;
4419 d_regexp_ccached.insert(atom);
4420 return false;
4421 }
4422 default:
4423 //Impossible
4424 break;
4425 }
4426 } else {
4427 /*Node xr = getRepresentative( x );
4428 if(x != xr) {
4429 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
4430 Node nn = Rewriter::rewrite( n );
4431 if(nn == d_true) {
4432 d_regexp_ccached.insert(atom);
4433 return false;
4434 } else if(nn == d_false) {
4435 Node antec = mkRegExpAntec(atom, x.eqNode(xr));
4436 Node conc = Node::null();
4437 sendLemma(antec, conc, "RegExp Delta CONFLICT");
4438 addedLemma = true;
4439 d_regexp_ccached.insert(atom);
4440 return false;
4441 }
4442 }*/
4443 Node sREant = mkRegExpAntec(atom, d_true);
4444 sREant = NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf);
4445 if(deriveRegExp( x, r, sREant )) {
4446 addedLemma = true;
4447 d_regexp_ccached.insert(atom);
4448 return false;
4449 }
4450 }
4451 return true;
4452 }
4453
4454 CVC4::String TheoryStrings::getHeadConst( Node x ) {
4455 if( x.isConst() ) {
4456 return x.getConst< String >();
4457 } else if( x.getKind() == kind::STRING_CONCAT ) {
4458 if( x[0].isConst() ) {
4459 return x[0].getConst< String >();
4460 } else {
4461 return d_emptyString.getConst< String >();
4462 }
4463 } else {
4464 return d_emptyString.getConst< String >();
4465 }
4466 }
4467
4468 bool TheoryStrings::deriveRegExp( Node x, Node r, Node ant ) {
4469 // TODO cstr in vre
4470 Assert(x != d_emptyString);
4471 Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x << ", r= " << r << std::endl;
4472 //if(x.isConst()) {
4473 // Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
4474 // Node r = Rewriter::rewrite( n );
4475 // if(n != r) {
4476 // sendLemma(ant, r, "REGEXP REWRITE");
4477 // return true;
4478 // }
4479 //}
4480 CVC4::String s = getHeadConst( x );
4481 if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
4482 Node conc = Node::null();
4483 Node dc = r;
4484 bool flag = true;
4485 for(unsigned i=0; i<s.size(); ++i) {
4486 CVC4::String c = s.substr(i, 1);
4487 Node dc2;
4488 int rt = d_regexp_opr.derivativeS(dc, c, dc2);
4489 dc = dc2;
4490 if(rt == 0) {
4491 //TODO
4492 } else if(rt == 2) {
4493 // CONFLICT
4494 flag = false;
4495 break;
4496 }
4497 }
4498 // send lemma
4499 if(flag) {
4500 if(x.isConst()) {
4501 Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
4502 return false;
4503 } else {
4504 Assert( x.getKind() == kind::STRING_CONCAT );
4505 std::vector< Node > vec_nodes;
4506 for(unsigned int i=1; i<x.getNumChildren(); ++i ) {
4507 vec_nodes.push_back( x[i] );
4508 }
4509 Node left = mkConcat( vec_nodes );
4510 left = Rewriter::rewrite( left );
4511 conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
4512
4513 /*std::vector< Node > sdc;
4514 d_regexp_opr.simplify(conc, sdc, true);
4515 if(sdc.size() == 1) {
4516 conc = sdc[0];
4517 } else {
4518 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
4519 }*/
4520 }
4521 }
4522 sendLemma(ant, conc, "RegExp-Derive");
4523 return true;
4524 } else {
4525 return false;
4526 }
4527 }
4528
4529 void TheoryStrings::addMembership(Node assertion) {
4530 bool polarity = assertion.getKind() != kind::NOT;
4531 TNode atom = polarity ? assertion : assertion[0];
4532 Node x = atom[0];
4533 Node r = atom[1];
4534 if(polarity) {
4535 int index = 0;
4536 NodeIntMap::const_iterator it = d_pos_memberships.find( x );
4537 if( it!=d_nf_pairs.end() ){
4538 index = (*it).second;
4539 for( int k=0; k<index; k++ ){
4540 if( k<(int)d_pos_memberships_data[x].size() ){
4541 if( d_pos_memberships_data[x][k]==r ){
4542 return;
4543 }
4544 }else{
4545 break;
4546 }
4547 }
4548 }
4549 d_pos_memberships[x] = index + 1;
4550 if( index<(int)d_pos_memberships_data[x].size() ){
4551 d_pos_memberships_data[x][index] = r;
4552 }else{
4553 d_pos_memberships_data[x].push_back( r );
4554 }
4555 } else if(!options::stringIgnNegMembership()) {
4556 /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
4557 int rt;
4558 Node r2 = d_regexp_opr.complement(r, rt);
4559 Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
4560 }*/
4561 int index = 0;
4562 NodeIntMap::const_iterator it = d_neg_memberships.find( x );
4563 if( it!=d_nf_pairs.end() ){
4564 index = (*it).second;
4565 for( int k=0; k<index; k++ ){
4566 if( k<(int)d_neg_memberships_data[x].size() ){
4567 if( d_neg_memberships_data[x][k]==r ){
4568 return;
4569 }
4570 }else{
4571 break;
4572 }
4573 }
4574 }
4575 d_neg_memberships[x] = index + 1;
4576 if( index<(int)d_neg_memberships_data[x].size() ){
4577 d_neg_memberships_data[x][index] = r;
4578 }else{
4579 d_neg_memberships_data[x].push_back( r );
4580 }
4581 }
4582 // old
4583 if(polarity || !options::stringIgnNegMembership()) {
4584 d_regexp_memberships.push_back( assertion );
4585 }
4586 }
4587
4588 Node TheoryStrings::getNormalString( Node x, std::vector< Node >& nf_exp ){
4589 if( !x.isConst() ){
4590 Node xr = getRepresentative( x );
4591 if( d_normal_forms.find( xr ) != d_normal_forms.end() ){
4592 Node ret = mkConcat( d_normal_forms[xr] );
4593 nf_exp.insert( nf_exp.end(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
4594 addToExplanation( x, d_normal_forms_base[xr], nf_exp );
4595 Trace("strings-debug") << "Term: " << x << " has a normal form " << ret << std::endl;
4596 return ret;
4597 } else {
4598 if(x.getKind() == kind::STRING_CONCAT) {
4599 std::vector< Node > vec_nodes;
4600 for(unsigned i=0; i<x.getNumChildren(); i++) {
4601 Node nc = getNormalString( x[i], nf_exp );
4602 vec_nodes.push_back( nc );
4603 }
4604 return mkConcat( vec_nodes );
4605 }
4606 }
4607 }
4608 return x;
4609 }
4610
4611 Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
4612 Node ret = r;
4613 switch( r.getKind() ) {
4614 case kind::REGEXP_EMPTY:
4615 case kind::REGEXP_SIGMA:
4616 break;
4617 case kind::STRING_TO_REGEXP: {
4618 if(!r[0].isConst()) {
4619 Node tmp = getNormalString( r[0], nf_exp );
4620 if(tmp != r[0]) {
4621 ret = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, tmp);
4622 }
4623 }
4624 break;
4625 }
4626 case kind::REGEXP_CONCAT: {
4627 std::vector< Node > vec_nodes;
4628 for(unsigned i=0; i<r.getNumChildren(); ++i) {
4629 vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
4630 }
4631 ret = mkConcat(vec_nodes);
4632 break;
4633 }
4634 case kind::REGEXP_UNION: {
4635 std::vector< Node > vec_nodes;
4636 for(unsigned i=0; i<r.getNumChildren(); ++i) {
4637 vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
4638 }
4639 ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
4640 break;
4641 }
4642 case kind::REGEXP_INTER: {
4643 std::vector< Node > vec_nodes;
4644 for(unsigned i=0; i<r.getNumChildren(); ++i) {
4645 vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
4646 }
4647 ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, vec_nodes) );
4648 break;
4649 }
4650 case kind::REGEXP_STAR: {
4651 ret = getNormalSymRegExp( r[0], nf_exp );
4652 ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, ret) );
4653 break;
4654 }
4655 //case kind::REGEXP_PLUS:
4656 //case kind::REGEXP_OPT:
4657 //case kind::REGEXP_RANGE:
4658 default: {
4659 Trace("strings-error") << "Unsupported term: " << r << " in normalization SymRegExp." << std::endl;
4660 Assert( false );
4661 //return Node::null();
4662 }
4663 }
4664 return ret;
4665 }
4666
4667 }/* CVC4::theory::strings namespace */
4668 }/* CVC4::theory namespace */
4669 }/* CVC4 namespace */