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