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