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