projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
adds incremental for strings; clean-up codes
[cvc5.git] / src / theory / strings / theory_strings.cpp
1 /********************* */
2 /*! \file theory_strings.cpp
3 ** \verbatim
4 ** Original author: Tianyi Liang
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
11 **
12 ** \brief Implementation of the theory of strings.
13 **
14 ** Implementation of the theory of strings.
15 **/
16
17
18 #include "theory/strings/theory_strings.h"
19 #include "theory/valuation.h"
20 #include "expr/kind.h"
21 #include "theory/rewriter.h"
22 #include "expr/command.h"
23 #include "theory/theory_model.h"
24 #include "smt/logic_exception.h"
25 #include "theory/strings/options.h"
26 #include "theory/strings/type_enumerator.h"
27 #include <cmath>
28
29 using namespace std;
30 using namespace CVC4::context;
31
32 namespace CVC4 {
33 namespace theory {
34 namespace strings {
35
36 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
37 : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
38 d_notify( *this ),
39 d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
40 d_conflict(c, false),
41 d_infer(c),
42 d_infer_exp(c),
43 d_nf_pairs(c),
44 d_loop_antec(u),
45 d_length_inst(u),
46 d_length_nodes(c),
47 d_str_pos_ctn(c),
48 d_str_neg_ctn(c),
49 d_neg_ctn_eqlen(u),
50 d_neg_ctn_ulen(u),
51 d_pos_ctn_cached(u),
52 d_neg_ctn_cached(u),
53 d_reg_exp_mem(c),
54 d_regexp_ucached(u),
55 d_regexp_ccached(c),
56 d_regexp_ant(c),
57 d_input_vars(u),
58 d_input_var_lsum(u),
59 d_cardinality_lits(u),
60 d_curr_cardinality(c, 0)
61 {
62 // The kinds we are treating as function application in congruence
63 //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
64 d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
65 d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
66 d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
67 d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
68 d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
69 d_equalityEngine.addFunctionKind(kind::STRING_STOI);
70
71 d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
72 d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
73 d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
74 std::vector< Node > nvec;
75 d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
76 d_true = NodeManager::currentNM()->mkConst( true );
77 d_false = NodeManager::currentNM()->mkConst( false );
78
79 //d_opt_regexp_gcd = true;
80 }
81
82 TheoryStrings::~TheoryStrings() {
83
84 }
85
86 Node TheoryStrings::getRepresentative( Node t ) {
87 if( d_equalityEngine.hasTerm( t ) ){
88 return d_equalityEngine.getRepresentative( t );
89 }else{
90 return t;
91 }
92 }
93
94 bool TheoryStrings::hasTerm( Node a ){
95 return d_equalityEngine.hasTerm( a );
96 }
97
98 bool TheoryStrings::areEqual( Node a, Node b ){
99 if( a==b ){
100 return true;
101 }else if( hasTerm( a ) && hasTerm( b ) ){
102 return d_equalityEngine.areEqual( a, b );
103 }else{
104 return false;
105 }
106 }
107
108 bool TheoryStrings::areDisequal( Node a, Node b ){
109 if( a==b ){
110 return false;
111 } else {
112 if( a.getType().isString() ) {
113 for( unsigned i=0; i<2; i++ ) {
114 Node ac = a.getKind()==kind::STRING_CONCAT ? a[i==0 ? 0 : a.getNumChildren()-1] : a;
115 Node bc = b.getKind()==kind::STRING_CONCAT ? b[i==0 ? 0 : b.getNumChildren()-1] : b;
116 if( ac.isConst() && bc.isConst() ){
117 CVC4::String as = ac.getConst<String>();
118 CVC4::String bs = bc.getConst<String>();
119 int slen = as.size() > bs.size() ? bs.size() : as.size();
120 bool flag = i == 1 ? as.rstrncmp(bs, slen): as.strncmp(bs, slen);
121 if(!flag) {
122 return true;
123 }
124 }
125 }
126 }
127 if( hasTerm( a ) && hasTerm( b ) ) {
128 if( d_equalityEngine.areDisequal( a, b, false ) ){
129 return true;
130 }
131 }
132 return false;
133 }
134 }
135
136 Node TheoryStrings::getLengthTerm( Node t ) {
137 EqcInfo * ei = getOrMakeEqcInfo( t, false );
138 Node length_term = ei ? ei->d_length_term : Node::null();
139 if( length_term.isNull()) {
140 //typically shouldnt be necessary
141 length_term = t;
142 }
143 Debug("strings") << "TheoryStrings::getLengthTerm" << t << std::endl;
144 return length_term;
145 }
146
147 Node TheoryStrings::getLength( Node t ) {
148 Node retNode;
149 if(t.isConst()) {
150 retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t );
151 } else {
152 retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
153 }
154 return Rewriter::rewrite( retNode );
155 }
156
157 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
158 d_equalityEngine.setMasterEqualityEngine(eq);
159 }
160
161 void TheoryStrings::addSharedTerm(TNode t) {
162 Debug("strings") << "TheoryStrings::addSharedTerm(): "
163 << t << " " << t.getType().isBoolean() << endl;
164 d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
165 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
166 }
167
168 EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
169 if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
170 if (d_equalityEngine.areEqual(a, b)) {
171 // The terms are implied to be equal
172 return EQUALITY_TRUE;
173 }
174 if (d_equalityEngine.areDisequal(a, b, false)) {
175 // The terms are implied to be dis-equal
176 return EQUALITY_FALSE;
177 }
178 }
179 return EQUALITY_UNKNOWN;
180 }
181
182 void TheoryStrings::propagate(Effort e)
183 {
184 // direct propagation now
185 }
186
187 bool TheoryStrings::propagate(TNode literal) {
188 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl;
189 // If already in conflict, no more propagation
190 if (d_conflict) {
191 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
192 return false;
193 }
194 // Propagate out
195 bool ok = d_out->propagate(literal);
196 if (!ok) {
197 d_conflict = true;
198 }
199 return ok;
200 }
201
202 /** explain */
203 void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
204 Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl;
205 bool polarity = literal.getKind() != kind::NOT;
206 TNode atom = polarity ? literal : literal[0];
207 unsigned ps = assumptions.size();
208 std::vector< TNode > tassumptions;
209 if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
210 d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
211 } else {
212 d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
213 }
214 for( unsigned i=0; i<tassumptions.size(); i++ ){
215 if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
216 assumptions.push_back( tassumptions[i] );
217 }
218 }
219 Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl;
220 for( unsigned i=ps; i<assumptions.size(); i++ ){
221 Debug("strings-explain-debug") << " " << assumptions[i] << std::endl;
222 }
223 }
224
225 Node TheoryStrings::explain( TNode literal ){
226 std::vector< TNode > assumptions;
227 explain( literal, assumptions );
228 if( assumptions.empty() ){
229 return d_true;
230 }else if( assumptions.size()==1 ){
231 return assumptions[0];
232 }else{
233 return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
234 }
235 }
236
237 /////////////////////////////////////////////////////////////////////////////
238 // NOTIFICATIONS
239 /////////////////////////////////////////////////////////////////////////////
240
241
242 void TheoryStrings::presolve() {
243 Trace("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
244 d_opt_fmf = options::stringFMF();
245 }
246
247
248 /////////////////////////////////////////////////////////////////////////////
249 // MODEL GENERATION
250 /////////////////////////////////////////////////////////////////////////////
251
252
253 void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
254 Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
255 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
256 m->assertEqualityEngine( &d_equalityEngine );
257 // Generate model
258 std::vector< Node > nodes;
259 getEquivalenceClasses( nodes );
260 std::map< Node, Node > processed;
261 std::vector< std::vector< Node > > col;
262 std::vector< Node > lts;
263 separateByLength( nodes, col, lts );
264 //step 1 : get all values for known lengths
265 std::vector< Node > lts_values;
266 std::map< unsigned, bool > values_used;
267 for( unsigned i=0; i<col.size(); i++ ){
268 Trace("strings-model") << "Checking length for {";
269 for( unsigned j=0; j<col[i].size(); j++ ){
270 if( j>0 ) Trace("strings-model") << ", ";
271 Trace("strings-model") << col[i][j];
272 }
273 Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
274 if( lts[i].isConst() ){
275 lts_values.push_back( lts[i] );
276 unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
277 values_used[ lvalue ] = true;
278 }else{
279 //get value for lts[i];
280 if( !lts[i].isNull() ){
281 Node v = d_valuation.getModelValue(lts[i]);
282 Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
283 lts_values.push_back( v );
284 unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt();
285 values_used[ lvalue ] = true;
286 }else{
287 //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
288 //Assert( false );
289 lts_values.push_back( Node::null() );
290 }
291 }
292 }
293 ////step 2 : assign arbitrary values for unknown lengths?
294 // confirmed by calculus invariant, see paper
295 //for( unsigned i=0; i<col.size(); i++ ){
296 // if(
297 //}
298 Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
299 //step 3 : assign values to equivalence classes that are pure variables
300 for( unsigned i=0; i<col.size(); i++ ){
301 std::vector< Node > pure_eq;
302 Trace("strings-model") << "The equivalence classes ";
303 for( unsigned j=0; j<col[i].size(); j++ ) {
304 Trace("strings-model") << col[i][j] << " ";
305 //check if col[i][j] has only variables
306 EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
307 Node cst = ei ? ei->d_const_term : Node::null();
308 if( cst.isNull() ){
309 Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
310 if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
311 pure_eq.push_back( col[i][j] );
312 }
313 }else{
314 processed[col[i][j]] = cst;
315 }
316 }
317 Trace("strings-model") << "have length " << lts_values[i] << std::endl;
318
319 //assign a new length if necessary
320 if( !pure_eq.empty() ){
321 if( lts_values[i].isNull() ){
322 unsigned lvalue = 0;
323 while( values_used.find( lvalue )!=values_used.end() ){
324 lvalue++;
325 }
326 Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
327 lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
328 values_used[ lvalue ] = true;
329 }
330 Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
331 for( unsigned j=0; j<pure_eq.size(); j++ ){
332 Trace("strings-model") << pure_eq[j] << " ";
333 }
334 Trace("strings-model") << std::endl;
335
336
337 //use type enumerator
338 StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
339 for( unsigned j=0; j<pure_eq.size(); j++ ){
340 Assert( !sel.isFinished() );
341 Node c = *sel;
342 while( d_equalityEngine.hasTerm( c ) ){
343 ++sel;
344 Assert( !sel.isFinished() );
345 c = *sel;
346 }
347 ++sel;
348 Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
349 processed[pure_eq[j]] = c;
350 m->assertEquality( pure_eq[j], c, true );
351 }
352 }
353 }
354 Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
355 //step 4 : assign constants to all other equivalence classes
356 for( unsigned i=0; i<nodes.size(); i++ ){
357 if( processed.find( nodes[i] )==processed.end() ){
358 Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
359 Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
360 for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
361 if( j>0 ) Trace("strings-model") << " ++ ";
362 Trace("strings-model") << d_normal_forms[nodes[i]][j];
363 Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
364 if( !r.isConst() && processed.find( r )==processed.end() ){
365 Trace("strings-model") << "(UNPROCESSED)";
366 }
367 }
368 Trace("strings-model") << std::endl;
369 std::vector< Node > nc;
370 for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
371 Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
372 Assert( r.isConst() || processed.find( r )!=processed.end() );
373 nc.push_back(r.isConst() ? r : processed[r]);
374 }
375 Node cc = mkConcat( nc );
376 Assert( cc.getKind()==kind::CONST_STRING );
377 Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
378 processed[nodes[i]] = cc;
379 m->assertEquality( nodes[i], cc, true );
380 }
381 }
382 Trace("strings-model") << "String Model : Assigned." << std::endl;
383 //check for negative contains
384 /*
385 Trace("strings-model") << "String Model : Check Neg Contains, size = " << d_str_neg_ctn.size() << std::endl;
386 for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ) {
387 Node x = d_str_neg_ctn[i][0];
388 Node y = d_str_neg_ctn[i][1];
389 Trace("strings-model") << "String Model : Check Neg contains: ~contains(" << x << ", " << y << ")." << std::endl;
390 //Node xv = m->getValue(x);
391 //Node yv = m->getValue(y);
392 //Trace("strings-model") << "String Model : Check Neg contains Value: ~contains(" << xv << ", " << yv << ")." << std::endl;
393 }
394 */
395 Trace("strings-model") << "String Model : Finished." << std::endl;
396 }
397
398 /////////////////////////////////////////////////////////////////////////////
399 // MAIN SOLVER
400 /////////////////////////////////////////////////////////////////////////////
401
402 void TheoryStrings::preRegisterTerm(TNode n) {
403 Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
404 //collectTerms( n );
405 switch (n.getKind()) {
406 case kind::EQUAL:
407 d_equalityEngine.addTriggerEquality(n);
408 break;
409 case kind::STRING_IN_REGEXP:
410 //do not add trigger here
411 //d_equalityEngine.addTriggerPredicate(n);
412 break;
413 case kind::STRING_SUBSTR_TOTAL: {
414 Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
415 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
416 NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
417 Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
418 Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
419 Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
420 Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
421 Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
422 d_statistics.d_new_skolems += 2;
423 Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
424 Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
425 Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
426 Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond,
427 NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
428 n.eqNode(d_emptyString)));
429 Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
430 d_out->lemma(lemma);
431 //d_equalityEngine.addTerm(n);
432 }
433 default: {
434 if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
435 Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
436 Node n_len_eq_z = n.eqNode(d_emptyString); //n_len.eqNode( d_zero );
437 n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
438 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
439 NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
440 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
441 d_out->lemma(n_len_geq_zero);
442 d_out->requirePhase( n_len_eq_z, true );
443 // FMF
444 if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&
445 d_input_vars.insert(n);
446 }
447 }
448 if (n.getType().isBoolean()) {
449 // Get triggered for both equal and dis-equal
450 d_equalityEngine.addTriggerPredicate(n);
451 } else {
452 // Function applications/predicates
453 d_equalityEngine.addTerm(n);
454 }
455 }
456 }
457 }
458
459 void TheoryStrings::check(Effort e) {
460 //Assert( d_pending.empty() );
461
462 bool polarity;
463 TNode atom;
464
465 /*if(getLogicInfo().hasEverything()) {
466 WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n"
467 << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl;
468 }
469 }*/
470
471 if( !done() && !hasTerm( d_emptyString ) ) {
472 preRegisterTerm( d_emptyString );
473 }
474
475 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
476 Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
477 while ( !done() && !d_conflict ) {
478 // Get all the assertions
479 Assertion assertion = get();
480 TNode fact = assertion.assertion;
481
482 Trace("strings-assertion") << "get assertion: " << fact << endl;
483
484 polarity = fact.getKind() != kind::NOT;
485 atom = polarity ? fact : fact[0];
486 //must record string in regular expressions
487 if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
488 d_reg_exp_mem.push_back( assertion );
489 //d_equalityEngine.assertPredicate(atom, polarity, fact);
490 } else if (atom.getKind() == kind::STRING_STRCTN) {
491 if(polarity) {
492 d_str_pos_ctn.push_back( atom );
493 } else {
494 d_str_neg_ctn.push_back( atom );
495 }
496 d_equalityEngine.assertPredicate(atom, polarity, fact);
497 } else if (atom.getKind() == kind::EQUAL) {
498 d_equalityEngine.assertEquality(atom, polarity, fact);
499 } else {
500 d_equalityEngine.assertPredicate(atom, polarity, fact);
501 }
502 }
503 doPendingFacts();
504
505
506 bool addedLemma = false;
507 if( e == EFFORT_FULL && !d_conflict ) {
508 addedLemma = checkSimple();
509 Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
510 if( !addedLemma ) {
511 addedLemma = checkNormalForms();
512 Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
513 if(!d_conflict && !addedLemma) {
514 addedLemma = checkLengthsEqc();
515 Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
516 if(!d_conflict && !addedLemma) {
517 addedLemma = checkContains();
518 Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
519 if( !d_conflict && !addedLemma ) {
520 addedLemma = checkMemberships();
521 Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
522 if( !d_conflict && !addedLemma ) {
523 addedLemma = checkCardinality();
524 Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
525 }
526 }
527 }
528 }
529 }
530 }
531 Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
532 Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
533 Assert( d_pending.empty() );
534 Assert( d_lemma_cache.empty() );
535 }
536
537 TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
538
539 }
540
541 TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) {
542 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc );
543 if( eqc_i==d_eqc_info.end() ){
544 if( doMake ){
545 EqcInfo* ei = new EqcInfo( getSatContext() );
546 d_eqc_info[eqc] = ei;
547 return ei;
548 }else{
549 return NULL;
550 }
551 }else{
552 return (*eqc_i).second;
553 }
554 }
555
556
557 /** Conflict when merging two constants */
558 void TheoryStrings::conflict(TNode a, TNode b){
559 if( !d_conflict ){
560 Trace("strings-conflict-debug") << "Making conflict..." << std::endl;
561 d_conflict = true;
562 Node conflictNode;
563 if (a.getKind() == kind::CONST_BOOLEAN) {
564 conflictNode = explain( a.iffNode(b) );
565 } else {
566 conflictNode = explain( a.eqNode(b) );
567 }
568 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
569 d_out->conflict( conflictNode );
570 }
571 }
572
573 /** called when a new equivalance class is created */
574 void TheoryStrings::eqNotifyNewClass(TNode t){
575 if( t.getKind() == kind::CONST_STRING ){
576 EqcInfo * ei =getOrMakeEqcInfo( t, true );
577 ei->d_const_term = t;
578 }
579 if( t.getKind() == kind::STRING_LENGTH ){
580 Trace("strings-debug") << "New length eqc : " << t << std::endl;
581 Node r = d_equalityEngine.getRepresentative(t[0]);
582 EqcInfo * ei = getOrMakeEqcInfo( r, true );
583 ei->d_length_term = t[0];
584 }
585 }
586
587 /** called when two equivalance classes will merge */
588 void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
589 EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
590 if( e2 ){
591 EqcInfo * e1 = getOrMakeEqcInfo( t1 );
592 //add information from e2 to e1
593 if( !e2->d_const_term.get().isNull() ){
594 e1->d_const_term.set( e2->d_const_term );
595 }
596 if( !e2->d_length_term.get().isNull() ){
597 e1->d_length_term.set( e2->d_length_term );
598 }
599 if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
600 e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
601 }
602 if( !e2->d_normalized_length.get().isNull() ){
603 e1->d_normalized_length.set( e2->d_normalized_length );
604 }
605 }
606 if( hasTerm( d_zero ) ){
607 Node leqc;
608 if( areEqual(d_zero, t1) ){
609 leqc = t2;
610 }else if( areEqual(d_zero, t2) ){
611 leqc = t1;
612 }
613 if( !leqc.isNull() ){
614 //scan equivalence class to see if we apply
615 eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
616 while( !eqc_i.isFinished() ){
617 Node n = (*eqc_i);
618 if( n.getKind()==kind::STRING_LENGTH ){
619 if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
620 //apply the rule length(n[0])==0 => n[0] == ""
621 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
622 d_pending.push_back( eq );
623 Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
624 d_pending_exp[eq] = eq_exp;
625 Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
626 d_infer.push_back(eq);
627 d_infer_exp.push_back(eq_exp);
628 }
629 }
630 ++eqc_i;
631 }
632 }
633 }
634 }
635
636 /** called when two equivalance classes have merged */
637 void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) {
638
639 }
640
641 /** called when two equivalance classes are disequal */
642 void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
643
644 }
645
646 void TheoryStrings::computeCareGraph(){
647 Theory::computeCareGraph();
648 }
649
650 void TheoryStrings::doPendingFacts() {
651 int i=0;
652 while( !d_conflict && i<(int)d_pending.size() ){
653 Node fact = d_pending[i];
654 Node exp = d_pending_exp[ fact ];
655 Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
656 bool polarity = fact.getKind() != kind::NOT;
657 TNode atom = polarity ? fact : fact[0];
658 if (atom.getKind() == kind::EQUAL) {
659 //Assert( d_equalityEngine.hasTerm( atom[0] ) );
660 //Assert( d_equalityEngine.hasTerm( atom[1] ) );
661 for( unsigned j=0; j<2; j++ ){
662 if( !d_equalityEngine.hasTerm( atom[j] ) ){
663 d_equalityEngine.addTerm( atom[j] );
664 }
665 }
666 d_equalityEngine.assertEquality( atom, polarity, exp );
667 }else{
668 d_equalityEngine.assertPredicate( atom, polarity, exp );
669 }
670 i++;
671 }
672 d_pending.clear();
673 d_pending_exp.clear();
674 }
675 void TheoryStrings::doPendingLemmas() {
676 if( !d_conflict && !d_lemma_cache.empty() ){
677 for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
678 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
679 d_out->lemma( d_lemma_cache[i] );
680 }
681 for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
682 Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
683 d_out->requirePhase( it->first, it->second );
684 }
685 }
686 d_lemma_cache.clear();
687 d_pending_req_phase.clear();
688 }
689
690 bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
691 std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
692 Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
693 // EqcItr
694 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
695 while( !eqc_i.isFinished() ) {
696 Node n = (*eqc_i);
697 if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
698 Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
699 std::vector<Node> nf_n;
700 std::vector<Node> nf_exp_n;
701 bool result = true;
702 if( n.getKind() == kind::CONST_STRING ) {
703 if( n!=d_emptyString ) {
704 nf_n.push_back( n );
705 }
706 } else if( n.getKind() == kind::STRING_CONCAT ) {
707 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
708 Node nr = d_equalityEngine.getRepresentative( n[i] );
709 std::vector< Node > nf_temp;
710 std::vector< Node > nf_exp_temp;
711 Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl;
712 bool nresult = false;
713 if( nr==eqc ) {
714 nf_temp.push_back( nr );
715 } else {
716 nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
717 if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
718 return true;
719 }
720 }
721 //successfully computed normal form
722 if( nf.size()!=1 || nf[0]!=d_emptyString ) {
723 for( unsigned r=0; r<nf_temp.size(); r++ ) {
724 if( nresult && nf_temp[r].getKind()==kind::STRING_CONCAT ){
725 Trace("strings-error") << "Strings::Error: From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
726 for( unsigned rr=0; rr<nf_temp.size(); rr++ ) {
727 Trace("strings-error") << nf_temp[rr] << " ";
728 }
729 Trace("strings-error") << std::endl;
730 }
731 Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT );
732 }
733 nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
734 }
735 nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
736 if( nr!=n[i] ) {
737 nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
738 }
739 if( !nresult ) {
740 //Trace("strings-process-debug") << "....Caused already asserted
741 for( unsigned j=i+1; j<n.getNumChildren(); j++ ) {
742 if( !areEqual( n[j], d_emptyString ) ) {
743 nf_n.push_back( n[j] );
744 }
745 }
746 if( nf_n.size()>1 ) {
747 result = false;
748 break;
749 }
750 }
751 }
752 }
753 //if not equal to self
754 //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){
755 if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) {
756 if( nf_n.size()>1 ) {
757 Trace("strings-process-debug") << "Check for cycle lemma for normal form ";
758 printConcat(nf_n,"strings-process-debug");
759 Trace("strings-process-debug") << "..." << std::endl;
760 for( unsigned i=0; i<nf_n.size(); i++ ) {
761 //if a component is equal to whole,
762 if( areEqual( nf_n[i], n ) ){
763 //all others must be empty
764 std::vector< Node > ant;
765 if( nf_n[i]!=n ){
766 ant.push_back( nf_n[i].eqNode( n ) );
767 }
768 ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
769 std::vector< Node > cc;
770 for( unsigned j=0; j<nf_n.size(); j++ ){
771 if( i!=j ){
772 cc.push_back( nf_n[j].eqNode( d_emptyString ) );
773 }
774 }
775 std::vector< Node > empty_vec;
776 Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
777 sendLemma( mkExplain( ant ), conc, "CYCLE" );
778 return true;
779 }
780 }
781 }
782 if( !result ) {
783 Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl;
784 //we have a normal form that will cause a component lemma at a higher level
785 normal_forms.clear();
786 normal_forms_exp.clear();
787 normal_form_src.clear();
788 }
789 normal_forms.push_back(nf_n);
790 normal_forms_exp.push_back(nf_exp_n);
791 normal_form_src.push_back(n);
792 if( !result ){
793 return false;
794 }
795 } else {
796 Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
797 //Assert( areEqual( nf_n[0], eqc ) );
798 if( !areEqual( nn, eqc ) ){
799 std::vector< Node > ant;
800 ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
801 ant.push_back( n.eqNode( eqc ) );
802 Node conc = nn.eqNode( eqc );
803 sendLemma( mkExplain( ant ), conc, "CYCLE-T" );
804 return true;
805 }
806 }
807 //}
808 }
809 ++eqc_i;
810 }
811
812 // Test the result
813 if( !normal_forms.empty() ) {
814 Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
815 for( unsigned i=0; i<normal_forms.size(); i++ ) {
816 Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
817 //mergeCstVec(normal_forms[i]);
818 for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
819 if(j>0) Trace("strings-solve") << ", ";
820 Trace("strings-solve") << normal_forms[i][j];
821 }
822 Trace("strings-solve") << std::endl;
823 Trace("strings-solve") << " Explanation is : ";
824 if(normal_forms_exp[i].size() == 0) {
825 Trace("strings-solve") << "NONE";
826 } else {
827 for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
828 if(j>0) Trace("strings-solve") << " AND ";
829 Trace("strings-solve") << normal_forms_exp[i][j];
830 }
831 }
832 Trace("strings-solve") << std::endl;
833 }
834 }else{
835 //std::vector< Node > nf;
836 //nf.push_back( eqc );
837 //normal_forms.push_back(nf);
838 //std::vector< Node > nf_exp_def;
839 //normal_forms_exp.push_back(nf_exp_def);
840 //normal_form_src.push_back(eqc);
841 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
842 }
843 return true;
844 }
845
846 void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
847 std::vector< Node >::iterator itr = vec_strings.begin();
848 while(itr != vec_strings.end()) {
849 if(itr->isConst()) {
850 std::vector< Node >::iterator itr2 = itr + 1;
851 if(itr2 == vec_strings.end()) {
852 break;
853 } else if(itr2->isConst()) {
854 CVC4::String s1 = itr->getConst<String>();
855 CVC4::String s2 = itr2->getConst<String>();
856 *itr = NodeManager::currentNM()->mkConst(s1.concat(s2));
857 vec_strings.erase(itr2);
858 } else {
859 ++itr;
860 }
861 } else {
862 ++itr;
863 }
864 }
865 }
866
867 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
868 int i, int j, int index_i, int index_j,
869 int &loop_in_i, int &loop_in_j) {
870 int has_loop[2] = { -1, -1 };
871 if( options::stringLB() != 2 ) {
872 for( unsigned r=0; r<2; r++ ) {
873 int index = (r==0 ? index_i : index_j);
874 int other_index = (r==0 ? index_j : index_i );
875 int n_index = (r==0 ? i : j);
876 int other_n_index = (r==0 ? j : i);
877 if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
878 for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
879 if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
880 has_loop[r] = lp;
881 break;
882 }
883 }
884 }
885 }
886 }
887 if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
888 loop_in_i = has_loop[0];
889 loop_in_j = has_loop[1];
890 return true;
891 } else {
892 return false;
893 }
894 }
895 //xs(zy)=t(yz)xr
896 bool TheoryStrings::processLoop(std::vector< Node > &antec,
897 std::vector< std::vector< Node > > &normal_forms,
898 std::vector< Node > &normal_form_src,
899 int i, int j, int loop_n_index, int other_n_index,
900 int loop_index, int index, int other_index) {
901 Node conc;
902 Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
903 Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
904
905 Trace("strings-loop") << " ... T(Y.Z)= ";
906 std::vector< Node > vec_t;
907 for(int lp=index; lp<loop_index; ++lp) {
908 if(lp != index) Trace("strings-loop") << " ++ ";
909 Trace("strings-loop") << normal_forms[loop_n_index][lp];
910 vec_t.push_back( normal_forms[loop_n_index][lp] );
911 }
912 Node t_yz = mkConcat( vec_t );
913 Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
914 Trace("strings-loop") << " ... S(Z.Y)= ";
915 std::vector< Node > vec_s;
916 for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
917 if(lp != other_index+1) Trace("strings-loop") << " ++ ";
918 Trace("strings-loop") << normal_forms[other_n_index][lp];
919 vec_s.push_back( normal_forms[other_n_index][lp] );
920 }
921 Node s_zy = mkConcat( vec_s );
922 Trace("strings-loop") << " (" << s_zy << ")" << std::endl;
923 Trace("strings-loop") << " ... R= ";
924 std::vector< Node > vec_r;
925 for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
926 if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
927 Trace("strings-loop") << normal_forms[loop_n_index][lp];
928 vec_r.push_back( normal_forms[loop_n_index][lp] );
929 }
930 Node r = mkConcat( vec_r );
931 Trace("strings-loop") << " (" << r << ")" << std::endl;
932
933 //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
934 //TODO: can be more general
935 if( s_zy.isConst() && r.isConst() && r != d_emptyString) {
936 int c;
937 bool flag = true;
938 if(s_zy.getConst<String>().tailcmp( r.getConst<String>(), c ) ) {
939 if(c >= 0) {
940 s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, c) );
941 r = d_emptyString;
942 vec_r.clear();
943 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl;
944 flag = false;
945 }
946 }
947 if(flag) {
948 Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl;
949 Node ant = mkExplain( antec );
950 sendLemma( ant, conc, "Conflict" );
951 return true;
952 }
953 }
954
955 //require that x is non-empty
956 if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
957 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
958 sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop-X-E-Split" );
959 } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) {
960 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
961 sendSplit( t_yz, d_emptyString, "Loop-YZ-E-SPlit" );
962 } else {
963 //need to break
964 antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
965 if( t_yz.getKind()!=kind::CONST_STRING ) {
966 antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
967 }
968 Node ant = mkExplain( antec );
969 if(d_loop_antec.find(ant) == d_loop_antec.end()) {
970 d_loop_antec.insert(ant);
971
972 Node str_in_re;
973 if( s_zy == t_yz &&
974 r == d_emptyString &&
975 s_zy.isConst() &&
976 s_zy.getConst<String>().isRepeated()
977 ) {
978 Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
979 Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
980 Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
981 //special case
982 str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
983 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
984 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
985 conc = str_in_re;
986 } else {
987 Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
988 //right
989 Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
990 Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
991 Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
992 d_statistics.d_new_skolems += 3;
993 //t1 * ... * tn = y * z
994 Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
995 // s1 * ... * sk = z * y * r
996 vec_r.insert(vec_r.begin(), sk_y);
997 vec_r.insert(vec_r.begin(), sk_z);
998 Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
999 Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
1000 Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
1001 str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
1002 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
1003 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, restr ) ) );
1004
1005 //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
1006 //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString));
1007
1008 std::vector< Node > vec_conc;
1009 vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3);
1010 vec_conc.push_back(str_in_re);
1011 vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());
1012 conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );//, len_x_gt_len_y
1013 } // normal case
1014
1015 //set its antecedant to ant, to say when it is relevant
1016 d_regexp_ant[str_in_re] = ant;
1017 //unroll the str in re constraint once
1018 // unrollStar( str_in_re );
1019 sendLemma( ant, conc, "LOOP-BREAK" );
1020 ++(d_statistics.d_loop_lemmas);
1021
1022 //we will be done
1023 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
1024 } else {
1025 Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant << " has already added." << std::endl;
1026 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
1027 return false;
1028 }
1029 }
1030 return true;
1031 }
1032 bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms,
1033 std::vector< std::vector< Node > > &normal_forms_exp,
1034 std::vector< Node > &normal_form_src) {
1035 bool flag_lb = false;
1036 std::vector< Node > c_lb_exp;
1037 int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
1038 for(unsigned i=0; i<normal_forms.size()-1; i++) {
1039 //unify each normalform[j] with normal_forms[i]
1040 for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
1041 Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
1042 if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
1043 Trace("strings-solve") << "Strings: Already cached." << std::endl;
1044 } else {
1045 //the current explanation for why the prefix is equal
1046 std::vector< Node > curr_exp;
1047 curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
1048 curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
1049 curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
1050
1051 //process the reverse direction first (check for easy conflicts and inferences)
1052 if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){
1053 return true;
1054 }
1055
1056 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
1057 unsigned index_i = 0;
1058 unsigned index_j = 0;
1059 bool success;
1060 do
1061 {
1062 //simple check
1063 if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
1064 //added a lemma, return
1065 return true;
1066 }
1067
1068 success = false;
1069 //if we are at the end
1070 if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
1071 Assert( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() );
1072 //we're done
1073 //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
1074 } else {
1075 Node length_term_i = getLength( normal_forms[i][index_i] );
1076 Node length_term_j = getLength( normal_forms[j][index_j] );
1077 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
1078 if( !areDisequal(length_term_i, length_term_j) &&
1079 !areEqual(length_term_i, length_term_j) &&
1080 normal_forms[i][index_i].getKind()!=kind::CONST_STRING &&
1081 normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
1082 //length terms are equal, merge equivalence classes if not already done so
1083 Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
1084 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
1085 //try to make the lengths equal via splitting on demand
1086 sendSplit( length_term_i, length_term_j, "Length" );
1087 length_eq = Rewriter::rewrite( length_eq );
1088 d_pending_req_phase[ length_eq ] = true;
1089 return true;
1090 } else {
1091 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
1092 int loop_in_i = -1;
1093 int loop_in_j = -1;
1094 if(detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j)) {
1095 if(!flag_lb) {
1096 c_i = i;
1097 c_j = j;
1098 c_loop_n_index = loop_in_i!=-1 ? i : j;
1099 c_other_n_index = loop_in_i!=-1 ? j : i;
1100 c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
1101 c_index = loop_in_i!=-1 ? index_i : index_j;
1102 c_other_index = loop_in_i!=-1 ? index_j : index_i;
1103
1104 c_lb_exp = curr_exp;
1105
1106 if(options::stringLB() == 0) {
1107 flag_lb = true;
1108 } else {
1109 if(processLoop(c_lb_exp, normal_forms, normal_form_src,
1110 c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
1111 return true;
1112 }
1113 }
1114 }
1115 } else {
1116 Node conc;
1117 std::vector< Node > antec;
1118 Trace("strings-solve-debug") << "No loops detected." << std::endl;
1119 if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
1120 normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
1121 unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
1122 unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
1123 unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
1124 unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
1125 Node const_str = normal_forms[const_k][const_index_k];
1126 Node other_str = normal_forms[nconst_k][nconst_index_k];
1127 Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
1128 Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
1129 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
1130 Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
1131 NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
1132 //split the string
1133 Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
1134 Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
1135 d_pending_req_phase[ eq1 ] = true;
1136 conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
1137 Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
1138
1139 Node ant = mkExplain( antec );
1140 sendLemma( ant, conc, "CST-SPLIT" );
1141 ++(d_statistics.d_eq_splits);
1142 return true;
1143 } else {
1144 std::vector< Node > antec_new_lits;
1145 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
1146
1147 Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
1148 if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
1149 antec.push_back( ldeq );
1150 }else{
1151 antec_new_lits.push_back(ldeq);
1152 }
1153
1154 //x!=e /\ y!=e
1155 for(unsigned xory=0; xory<2; xory++) {
1156 Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j];
1157 Node xgtz = x.eqNode( d_emptyString ).negate();
1158 if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
1159 antec.push_back( xgtz );
1160 } else {
1161 antec_new_lits.push_back( xgtz );
1162 }
1163 }
1164
1165 Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
1166 Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
1167 conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
1168
1169 Node ant = mkExplain( antec, antec_new_lits );
1170 sendLemma( ant, conc, "VAR-SPLIT" );
1171 ++(d_statistics.d_eq_splits);
1172 return true;
1173 }
1174 }
1175 }
1176 }
1177 } while(success);
1178 }
1179 }
1180 if(!flag_lb) {
1181 return false;
1182 }
1183 }
1184 if(flag_lb) {
1185 if(processLoop(c_lb_exp, normal_forms, normal_form_src,
1186 c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
1187 return true;
1188 }
1189 }
1190
1191 return false;
1192 }
1193
1194 bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms,
1195 std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
1196 //reverse normal form of i, j
1197 std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
1198 std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
1199
1200 std::vector< Node > t_curr_exp;
1201 t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
1202 unsigned index_i = 0;
1203 unsigned index_j = 0;
1204 bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
1205
1206 //reverse normal form of i, j
1207 std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
1208 std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
1209
1210 return ret;
1211 }
1212
1213 bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
1214 std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
1215 unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
1216 bool success;
1217 do {
1218 success = false;
1219 //if we are at the end
1220 if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
1221 if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) {
1222 //we're done
1223 } else {
1224 //the remainder must be empty
1225 unsigned k = index_i==normal_forms[i].size() ? j : i;
1226 unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
1227 Node eq_exp = mkAnd( curr_exp );
1228 while(!d_conflict && index_k<normal_forms[k].size()) {
1229 //can infer that this string must be empty
1230 Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
1231 Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
1232 Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
1233 sendInfer( eq_exp, eq, "EQ_Endpoint" );
1234 index_k++;
1235 }
1236 return true;
1237 }
1238 }else{
1239 Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
1240 if(areEqual(normal_forms[i][index_i], normal_forms[j][index_j])) {
1241 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
1242 //terms are equal, continue
1243 if( normal_forms[i][index_i]!=normal_forms[j][index_j] ) {
1244 Node eq = normal_forms[i][index_i].eqNode(normal_forms[j][index_j]);
1245 Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
1246 curr_exp.push_back(eq);
1247 }
1248 index_j++;
1249 index_i++;
1250 success = true;
1251 } else {
1252 Node length_term_i = getLength( normal_forms[i][index_i] );
1253 Node length_term_j = getLength( normal_forms[j][index_j] );
1254 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
1255 if( areEqual(length_term_i, length_term_j) ) {
1256 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
1257 Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
1258 //eq = Rewriter::rewrite( eq );
1259 Node length_eq = length_term_i.eqNode( length_term_j );
1260 std::vector< Node > temp_exp;
1261 temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
1262 temp_exp.push_back(length_eq);
1263 Node eq_exp = temp_exp.empty() ? d_true :
1264 temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
1265 sendInfer( eq_exp, eq, "LengthEq" );
1266 return true;
1267 } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) ||
1268 ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) {
1269 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
1270 Node conc;
1271 std::vector< Node > antec;
1272 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
1273 std::vector< Node > eqn;
1274 for( unsigned r=0; r<2; r++ ) {
1275 int index_k = r==0 ? index_i : index_j;
1276 int k = r==0 ? i : j;
1277 std::vector< Node > eqnc;
1278 for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
1279 if(isRev) {
1280 eqnc.insert(eqnc.begin(), normal_forms[k][index_l] );
1281 } else {
1282 eqnc.push_back( normal_forms[k][index_l] );
1283 }
1284 }
1285 eqn.push_back( mkConcat( eqnc ) );
1286 }
1287 if( !areEqual( eqn[0], eqn[1] ) ) {
1288 conc = eqn[0].eqNode( eqn[1] );
1289 Node ant = mkExplain( antec );
1290 sendLemma( ant, conc, "ENDPOINT" );
1291 return true;
1292 }else{
1293 index_i = normal_forms[i].size();
1294 index_j = normal_forms[j].size();
1295 }
1296 } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
1297 Node const_str = normal_forms[i][index_i];
1298 Node other_str = normal_forms[j][index_j];
1299 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
1300 unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
1301 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);
1302 if( isSameFix ) {
1303 //same prefix/suffix
1304 //k is the index of the string that is shorter
1305 int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
1306 int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
1307 int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
1308 int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
1309 if(isRev) {
1310 int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
1311 Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
1312 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
1313 normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
1314 } else {
1315 Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index_l].getConst<String>().substr(len_short));
1316 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
1317 normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
1318 }
1319 normal_forms[l][index_l] = normal_forms[k][index_k];
1320 index_i++;
1321 index_j++;
1322 success = true;
1323 } else {
1324 Node conc;
1325 std::vector< Node > antec;
1326 //curr_exp is conflict
1327 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
1328 Node ant = mkExplain( antec );
1329 sendLemma( ant, conc, "Const Conflict" );
1330 return true;
1331 }
1332 }
1333 }
1334 }
1335 }while( success );
1336 return false;
1337 }
1338
1339
1340 //nf_exp is conjunction
1341 bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
1342 Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
1343 if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
1344 getConcatVec( eqc, nf );
1345 Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
1346 return false;
1347 } else if( areEqual( eqc, d_emptyString ) ) {
1348 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1349 while( !eqc_i.isFinished() ) {
1350 Node n = (*eqc_i);
1351 if( n.getKind()==kind::STRING_CONCAT ){
1352 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1353 if( !areEqual( n[i], d_emptyString ) ){
1354 sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
1355 }
1356 }
1357 }
1358 ++eqc_i;
1359 }
1360 //do nothing
1361 Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
1362 d_normal_forms_base[eqc] = d_emptyString;
1363 d_normal_forms[eqc].clear();
1364 d_normal_forms_exp[eqc].clear();
1365 return true;
1366 } else {
1367 visited.push_back( eqc );
1368 bool result;
1369 if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
1370 //phi => t = s1 * ... * sn
1371 // normal form for each non-variable term in this eqc (s1...sn)
1372 std::vector< std::vector< Node > > normal_forms;
1373 // explanation for each normal form (phi)
1374 std::vector< std::vector< Node > > normal_forms_exp;
1375 // record terms for each normal form (t)
1376 std::vector< Node > normal_form_src;
1377 //Get Normal Forms
1378 result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
1379 if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
1380 return true;
1381 } else if( result ) {
1382 if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
1383 return true;
1384 }
1385 }
1386
1387 //construct the normal form
1388 if( normal_forms.empty() ){
1389 Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
1390 getConcatVec( eqc, nf );
1391 } else {
1392 Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
1393 //just take the first normal form
1394 nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
1395 nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
1396 if( eqc!=normal_form_src[0] ){
1397 nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
1398 }
1399 Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
1400 }
1401
1402 d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
1403 d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
1404 d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
1405 Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
1406 }else{
1407 Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
1408 nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
1409 nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
1410 result = true;
1411 }
1412 visited.pop_back();
1413 return result;
1414 }
1415 }
1416
1417 //return true for lemma, false if we succeed
1418 bool TheoryStrings::processDeq( Node ni, Node nj ) {
1419 //Assert( areDisequal( ni, nj ) );
1420 if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
1421 std::vector< Node > nfi;
1422 nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
1423 std::vector< Node > nfj;
1424 nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
1425
1426 int revRet = processReverseDeq( nfi, nfj, ni, nj );
1427 if( revRet!=0 ){
1428 return revRet==-1;
1429 }
1430
1431 nfi.clear();
1432 nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
1433 nfj.clear();
1434 nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
1435
1436 unsigned index = 0;
1437 while( index<nfi.size() || index<nfj.size() ){
1438 int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
1439 if( ret!=0 ){
1440 return ret==-1;
1441 }else{
1442 Assert( index<nfi.size() && index<nfj.size() );
1443 Node i = nfi[index];
1444 Node j = nfj[index];
1445 Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl;
1446 if( !areEqual( i, j ) ) {
1447 Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
1448 Node li = getLength( i );
1449 Node lj = getLength( j );
1450 if( areDisequal(li, lj) ){
1451 //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
1452
1453 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
1454 //must add lemma
1455 std::vector< Node > antec;
1456 std::vector< Node > antec_new_lits;
1457 antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
1458 antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
1459 //check disequal
1460 if( areDisequal( ni, nj ) ){
1461 antec.push_back( ni.eqNode( nj ).negate() );
1462 }else{
1463 antec_new_lits.push_back( ni.eqNode( nj ).negate() );
1464 }
1465 antec_new_lits.push_back( li.eqNode( lj ).negate() );
1466 std::vector< Node > conc;
1467 Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
1468 Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
1469 Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
1470 d_statistics.d_new_skolems += 3;
1471 //Node nemp = sk1.eqNode(d_emptyString).negate();
1472 //conc.push_back(nemp);
1473 //nemp = sk2.eqNode(d_emptyString).negate();
1474 //conc.push_back(nemp);
1475 Node nemp = sk3.eqNode(d_emptyString).negate();
1476 conc.push_back(nemp);
1477 Node lsk1 = getLength( sk1 );
1478 conc.push_back( lsk1.eqNode( li ) );
1479 Node lsk2 = getLength( sk2 );
1480 conc.push_back( lsk2.eqNode( lj ) );
1481 conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
1482 j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
1483
1484 sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
1485 ++(d_statistics.d_deq_splits);
1486 return true;
1487 }else if( areEqual( li, lj ) ){
1488 Assert( !areDisequal( i, j ) );
1489 //splitting on demand : try to make them disequal
1490 Node eq = i.eqNode( j );
1491 sendSplit( i, j, "D-EQL-Split" );
1492 eq = Rewriter::rewrite( eq );
1493 d_pending_req_phase[ eq ] = false;
1494 return true;
1495 }else{
1496 //splitting on demand : try to make lengths equal
1497 Node eq = li.eqNode( lj );
1498 sendSplit( li, lj, "D-UNK-Split" );
1499 eq = Rewriter::rewrite( eq );
1500 d_pending_req_phase[ eq ] = true;
1501 return true;
1502 }
1503 }
1504 index++;
1505 }
1506 }
1507 Assert( false );
1508 }
1509 return false;
1510 }
1511
1512 int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ) {
1513 //reverse normal form of i, j
1514 std::reverse( nfi.begin(), nfi.end() );
1515 std::reverse( nfj.begin(), nfj.end() );
1516
1517 unsigned index = 0;
1518 int ret = processSimpleDeq( nfi, nfj, ni, nj, index, true );
1519
1520 //reverse normal form of i, j
1521 std::reverse( nfi.begin(), nfi.end() );
1522 std::reverse( nfj.begin(), nfj.end() );
1523
1524 return ret;
1525 }
1526
1527 int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) {
1528 while( index<nfi.size() || index<nfj.size() ){
1529 if( index>=nfi.size() || index>=nfj.size() ){
1530 std::vector< Node > ant;
1531 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
1532 Node lni = getLength( ni );
1533 Node lnj = getLength( nj );
1534 ant.push_back( lni.eqNode( lnj ) );
1535 ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) );
1536 ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) );
1537 ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
1538 ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
1539 std::vector< Node > cc;
1540 std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
1541 for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
1542 cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
1543 }
1544 Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
1545 conc = Rewriter::rewrite( conc );
1546 sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty");
1547 return -1;
1548 } else {
1549 Node i = nfi[index];
1550 Node j = nfj[index];
1551 Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl;
1552 if( !areEqual( i, j ) ) {
1553 if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
1554 unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
1555 bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
1556 if( isSameFix ) {
1557 //same prefix/suffix
1558 //k is the index of the string that is shorter
1559 Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j;
1560 Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i;
1561 Node remainderStr;
1562 if(isRev) {
1563 int new_len = nl.getConst<String>().size() - len_short;
1564 remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) );
1565 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
1566 } else {
1567 remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
1568 Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
1569 }
1570 if( i.getConst<String>().size() < j.getConst<String>().size() ) {
1571 nfj.insert( nfj.begin() + index + 1, remainderStr );
1572 nfj[index] = nfi[index];
1573 } else {
1574 nfi.insert( nfi.begin() + index + 1, remainderStr );
1575 nfi[index] = nfj[index];
1576 }
1577 } else {
1578 return 1;
1579 }
1580 } else {
1581 Node li = getLength( i );
1582 Node lj = getLength( j );
1583 if( areEqual( li, lj ) && areDisequal( i, j ) ) {
1584 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
1585 //we are done: D-Remove
1586 return 1;
1587 }else{
1588 return 0;
1589 }
1590 }
1591 }
1592 index++;
1593 }
1594 }
1595 return 0;
1596 }
1597
1598 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
1599 if( !isNormalFormPair( n1, n2 ) ){
1600 //Assert( !isNormalFormPair( n1, n2 ) );
1601 NodeList* lst;
1602 NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
1603 if( nf_i == d_nf_pairs.end() ){
1604 if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
1605 addNormalFormPair( n2, n1 );
1606 return;
1607 }
1608 lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
1609 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
1610 d_nf_pairs.insertDataFromContextMemory( n1, lst );
1611 Trace("strings-nf") << "Create cache for " << n1 << std::endl;
1612 }else{
1613 lst = (*nf_i).second;
1614 }
1615 Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
1616 lst->push_back( n2 );
1617 Assert( isNormalFormPair( n1, n2 ) );
1618 }else{
1619 Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
1620 }
1621
1622 }
1623 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
1624 //TODO: modulo equality?
1625 return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
1626 }
1627 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
1628 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
1629 NodeList* lst;
1630 NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
1631 if( nf_i != d_nf_pairs.end() ){
1632 lst = (*nf_i).second;
1633 for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
1634 Node n = *i;
1635 if( n==n2 ){
1636 return true;
1637 }
1638 }
1639 }
1640 return false;
1641 }
1642
1643 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
1644 if( conc.isNull() || conc == d_false ){
1645 d_out->conflict(ant);
1646 Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
1647 d_conflict = true;
1648 }else{
1649 Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
1650 if( ant == d_true ) {
1651 lem = conc;
1652 }
1653 Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
1654 d_lemma_cache.push_back( lem );
1655 }
1656 }
1657
1658 void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
1659 eq = Rewriter::rewrite( eq );
1660 if( eq==d_false ){
1661 sendLemma( eq_exp, eq, c );
1662 }else{
1663 Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
1664 d_pending.push_back( eq );
1665 d_pending_exp[eq] = eq_exp;
1666 d_infer.push_back(eq);
1667 d_infer_exp.push_back(eq_exp);
1668 }
1669 }
1670
1671 void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
1672 Node eq = a.eqNode( b );
1673 eq = Rewriter::rewrite( eq );
1674 Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
1675 Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
1676 Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl;
1677 d_lemma_cache.push_back(lemma_or);
1678 d_pending_req_phase[eq] = preq;
1679 ++(d_statistics.d_splits);
1680 }
1681
1682 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
1683 std::vector< Node > c;
1684 c.push_back( n1 );
1685 c.push_back( n2 );
1686 return mkConcat( c );
1687 }
1688
1689 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
1690 Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
1691 return Rewriter::rewrite( cc );
1692 }
1693
1694 Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
1695 std::vector< Node > an;
1696 return mkExplain( a, an );
1697 }
1698
1699 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
1700 std::vector< TNode > antec_exp;
1701 for( unsigned i=0; i<a.size(); i++ ){
1702 if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ){
1703 bool exp = true;
1704 Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
1705 //assert
1706 if(a[i].getKind() == kind::EQUAL) {
1707 //assert( hasTerm(a[i][0]) );
1708 //assert( hasTerm(a[i][1]) );
1709 Assert( areEqual(a[i][0], a[i][1]) );
1710 if( a[i][0]==a[i][1] ){
1711 exp = false;
1712 }
1713 } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
1714 Assert( hasTerm(a[i][0][0]) );
1715 Assert( hasTerm(a[i][0][1]) );
1716 AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
1717 }
1718 if( exp ){
1719 unsigned ps = antec_exp.size();
1720 explain(a[i], antec_exp);
1721 Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
1722 for( unsigned j=ps; j<antec_exp.size(); j++ ){
1723 Trace("strings-solve-debug") << " " << antec_exp[j] << std::endl;
1724 }
1725 Trace("strings-solve-debug") << std::endl;
1726 }
1727 }
1728 }
1729 for( unsigned i=0; i<an.size(); i++ ){
1730 if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
1731 Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
1732 antec_exp.push_back(an[i]);
1733 }
1734 }
1735 Node ant;
1736 if( antec_exp.empty() ) {
1737 ant = d_true;
1738 } else if( antec_exp.size()==1 ) {
1739 ant = antec_exp[0];
1740 } else {
1741 ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
1742 }
1743 ant = Rewriter::rewrite( ant );
1744 return ant;
1745 }
1746
1747 Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
1748 if( a.empty() ) {
1749 return d_true;
1750 } else if( a.size() == 1 ) {
1751 return a[0];
1752 } else {
1753 return NodeManager::currentNM()->mkNode( kind::AND, a );
1754 }
1755 }
1756
1757 void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
1758 if( n.getKind()==kind::STRING_CONCAT ){
1759 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1760 if( !areEqual( n[i], d_emptyString ) ){
1761 c.push_back( n[i] );
1762 }
1763 }
1764 }else{
1765 c.push_back( n );
1766 }
1767 }
1768
1769 bool TheoryStrings::checkSimple() {
1770 bool addedLemma = false;
1771
1772 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1773 while( !eqcs_i.isFinished() ) {
1774 Node eqc = (*eqcs_i);
1775 //if eqc.getType is string
1776 if (eqc.getType().isString()) {
1777 //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
1778 //get the constant for the equivalence class
1779 //int c_len = ...;
1780 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1781 while( !eqc_i.isFinished() ){
1782 Node n = (*eqc_i);
1783 //if n is concat, and
1784 //if n has not instantiatied the concat..length axiom
1785 //then, add lemma
1786 if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
1787 if( d_length_nodes.find(n)==d_length_nodes.end() ) {
1788 if( d_length_inst.find(n)==d_length_inst.end() ) {
1789 //Node nr = d_equalityEngine.getRepresentative( n );
1790 //if( d_length_nodes.find(nr)==d_length_nodes.end() ) {
1791 d_length_inst.insert(n);
1792 Trace("strings-debug") << "get n: " << n << endl;
1793 Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
1794 d_statistics.d_new_skolems += 1;
1795 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
1796 eq = Rewriter::rewrite(eq);
1797 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
1798 d_out->lemma(eq);
1799 Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
1800 Node lsum;
1801 if( n.getKind() == kind::STRING_CONCAT ) {
1802 //add lemma
1803 std::vector<Node> node_vec;
1804 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
1805 Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
1806 node_vec.push_back(lni);
1807 }
1808 lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
1809 } else if( n.getKind() == kind::CONST_STRING ) {
1810 //add lemma
1811 lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
1812 }
1813 Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
1814 ceq = Rewriter::rewrite(ceq);
1815 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
1816 d_out->lemma(ceq);
1817 addedLemma = true;
1818 //}
1819 }
1820 d_length_nodes[n] = true;
1821 }
1822 }
1823 ++eqc_i;
1824 }
1825 }
1826 ++eqcs_i;
1827 }
1828 return addedLemma;
1829 }
1830
1831 bool TheoryStrings::checkNormalForms() {
1832 Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
1833 eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
1834 for( unsigned t=0; t<2; t++ ){
1835 Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
1836 while( !eqcs2_i.isFinished() ){
1837 Node eqc = (*eqcs2_i);
1838 bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
1839 if (print) {
1840 eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1841 Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
1842 while( !eqc2_i.isFinished() ) {
1843 if( (*eqc2_i)!=eqc ){
1844 Trace("strings-eqc") << (*eqc2_i) << " ";
1845 }
1846 ++eqc2_i;
1847 }
1848 Trace("strings-eqc") << " } " << std::endl;
1849 EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
1850 if( ei ){
1851 Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
1852 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
1853 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
1854 }
1855 }
1856 ++eqcs2_i;
1857 }
1858 Trace("strings-eqc") << std::endl;
1859 }
1860 Trace("strings-eqc") << std::endl;
1861 for( NodeListMap::const_iterator it = d_nf_pairs.begin(); it != d_nf_pairs.end(); ++it ){
1862 NodeList* lst = (*it).second;
1863 NodeList::const_iterator it2 = lst->begin();
1864 Trace("strings-nf") << (*it).first << " has been unified with ";
1865 while( it2!=lst->end() ){
1866 Trace("strings-nf") << (*it2);
1867 ++it2;
1868 }
1869 Trace("strings-nf") << std::endl;
1870 }
1871 Trace("strings-nf") << std::endl;
1872 /*
1873 Trace("strings-nf") << "Current inductive equations : " << std::endl;
1874 for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
1875 Node x = (*it).first;
1876 NodeList* lst1 = (*it).second;
1877 NodeList* lst2 = (*d_ind_map2.find(x)).second;
1878 NodeList::const_iterator i1 = lst1->begin();
1879 NodeList::const_iterator i2 = lst2->begin();
1880 while( i1!=lst1->end() ){
1881 Node y = *i1;
1882 Node z = *i2;
1883 Trace("strings-nf") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " ) * " << y << std::endl;
1884 ++i1;
1885 ++i2;
1886 }
1887 }
1888 */
1889
1890 bool addedFact;
1891 do {
1892 Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
1893 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
1894 d_normal_forms.clear();
1895 d_normal_forms_exp.clear();
1896 std::map< Node, Node > nf_to_eqc;
1897 std::map< Node, Node > eqc_to_exp;
1898 d_lemma_cache.clear();
1899 d_pending_req_phase.clear();
1900 //get equivalence classes
1901 std::vector< Node > eqcs;
1902 getEquivalenceClasses( eqcs );
1903 for( unsigned i=0; i<eqcs.size(); i++ ){
1904 Node eqc = eqcs[i];
1905 Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
1906 std::vector< Node > visited;
1907 std::vector< Node > nf;
1908 std::vector< Node > nf_exp;
1909 normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
1910 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
1911 if( d_conflict ){
1912 doPendingFacts();
1913 doPendingLemmas();
1914 return true;
1915 }else if ( d_pending.empty() && d_lemma_cache.empty() ){
1916 Node nf_term;
1917 if( nf.size()==0 ){
1918 nf_term = d_emptyString;
1919 }else if( nf.size()==1 ) {
1920 nf_term = nf[0];
1921 } else {
1922 nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
1923 }
1924 nf_term = Rewriter::rewrite( nf_term );
1925 Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
1926 Node nf_term_exp = nf_exp.empty() ? d_true :
1927 nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
1928 if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){
1929 //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
1930 //two equivalence classes have same normal form, merge
1931 Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
1932 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
1933 sendInfer( eq_exp, eq, "Normal_Form" );
1934 //d_equalityEngine.assertEquality( eq, true, eq_exp );
1935 }else{
1936 nf_to_eqc[nf_term] = eqc;
1937 eqc_to_exp[eqc] = nf_term_exp;
1938 }
1939 }
1940 Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
1941 }
1942
1943 Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl;
1944 for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
1945 Trace("strings-nf-debug") << " normal_form(" << it->second << ") = " << it->first << std::endl;
1946 }
1947 Trace("strings-nf-debug") << std::endl;
1948 addedFact = !d_pending.empty();
1949 doPendingFacts();
1950 } while ( !d_conflict && d_lemma_cache.empty() && addedFact );
1951
1952 //process disequalities between equivalence classes
1953 checkDeqNF();
1954
1955 Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
1956 //flush pending lemmas
1957 if( !d_lemma_cache.empty() ){
1958 doPendingLemmas();
1959 return true;
1960 }else{
1961 return false;
1962 }
1963 }
1964
1965 void TheoryStrings::checkDeqNF() {
1966 if( !d_conflict && d_lemma_cache.empty() ){
1967 std::vector< Node > eqcs;
1968 getEquivalenceClasses( eqcs );
1969 std::vector< std::vector< Node > > cols;
1970 std::vector< Node > lts;
1971 separateByLength( eqcs, cols, lts );
1972 for( unsigned i=0; i<cols.size(); i++ ){
1973 if( cols[i].size()>1 && d_lemma_cache.empty() ){
1974 Trace("strings-solve") << "- Verify disequalities are processed for ";
1975 printConcat( d_normal_forms[cols[i][0]], "strings-solve" );
1976 Trace("strings-solve") << "..." << std::endl;
1977
1978 //must ensure that normal forms are disequal
1979 for( unsigned j=0; j<cols[i].size(); j++ ){
1980 for( unsigned k=(j+1); k<cols[i].size(); k++ ){
1981 Assert( !d_conflict );
1982 //if( !areDisequal( cols[i][j], cols[i][k] ) ){
1983 // sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
1984 // return;
1985 //}else{
1986 Trace("strings-solve") << "- Compare ";
1987 printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
1988 Trace("strings-solve") << " against ";
1989 printConcat( d_normal_forms[cols[i][k]], "strings-solve" );
1990 Trace("strings-solve") << "..." << std::endl;
1991 if( processDeq( cols[i][j], cols[i][k] ) ){
1992 return;
1993 }
1994 //}
1995 }
1996 }
1997 }
1998 }
1999 }
2000 }
2001
2002 bool TheoryStrings::checkLengthsEqc() {
2003 bool addedLemma = false;
2004 std::vector< Node > nodes;
2005 getEquivalenceClasses( nodes );
2006 for( unsigned i=0; i<nodes.size(); i++ ){
2007 if( d_normal_forms[nodes[i]].size()>1 ) {
2008 Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
2009 //check if there is a length term for this equivalence class
2010 EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false );
2011 Node lt = ei ? ei->d_length_term : Node::null();
2012 if( !lt.isNull() ) {
2013 Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
2014 //now, check if length normalization has occurred
2015 if( ei->d_normalized_length.get().isNull() ) {
2016 //if not, add the lemma
2017 std::vector< Node > ant;
2018 ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
2019 ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
2020 Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
2021 lc = Rewriter::rewrite( lc );
2022 Node eq = llt.eqNode( lc );
2023 ei->d_normalized_length.set( eq );
2024 sendLemma( mkExplain( ant ), eq, "LEN-NORM" );
2025 addedLemma = true;
2026 }
2027 }
2028 }else{
2029 Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
2030 }
2031 }
2032 if( addedLemma ){
2033 doPendingLemmas();
2034 }
2035 return addedLemma;
2036 }
2037
2038 bool TheoryStrings::checkCardinality() {
2039 int cardinality = options::stringCharCardinality();
2040 Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
2041
2042 std::vector< Node > eqcs;
2043 getEquivalenceClasses( eqcs );
2044
2045 std::vector< std::vector< Node > > cols;
2046 std::vector< Node > lts;
2047 separateByLength( eqcs, cols, lts );
2048
2049 for( unsigned i = 0; i<cols.size(); ++i ){
2050 Node lr = lts[i];
2051 Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
2052 if( cols[i].size() > 1 ) {
2053 // size > c^k
2054 double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
2055 unsigned int int_k = (unsigned int) k;
2056 //double c_k = pow ( (double)cardinality, (double)lr );
2057
2058 bool allDisequal = true;
2059 for( std::vector< Node >::iterator itr1 = cols[i].begin();
2060 itr1 != cols[i].end(); ++itr1) {
2061 for( std::vector< Node >::iterator itr2 = itr1 + 1;
2062 itr2 != cols[i].end(); ++itr2) {
2063 if(!areDisequal( *itr1, *itr2 )) {
2064 allDisequal = false;
2065 // add split lemma
2066 sendSplit( *itr1, *itr2, "CARD-SP" );
2067 doPendingLemmas();
2068 return true;
2069 }
2070 }
2071 }
2072 if(allDisequal) {
2073 EqcInfo* ei = getOrMakeEqcInfo( lr, true );
2074 Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
2075 if( int_k+1 > ei->d_cardinality_lem_k.get() ){
2076 Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
2077 //add cardinality lemma
2078 Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
2079 std::vector< Node > vec_node;
2080 vec_node.push_back( dist );
2081 for( std::vector< Node >::iterator itr1 = cols[i].begin();
2082 itr1 != cols[i].end(); ++itr1) {
2083 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
2084 if( len!=lr ){
2085 Node len_eq_lr = len.eqNode(lr);
2086 vec_node.push_back( len_eq_lr );
2087 }
2088 }
2089 Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
2090 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
2091 Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
2092 /*
2093 sendLemma( antc, cons, "Cardinality" );
2094 ei->d_cardinality_lem_k.set( int_k+1 );
2095 if( !d_lemma_cache.empty() ){
2096 doPendingLemmas();
2097 return true;
2098 }
2099 */
2100 Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
2101 lemma = Rewriter::rewrite( lemma );
2102 ei->d_cardinality_lem_k.set( int_k+1 );
2103 if( lemma!=d_true ){
2104 Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl;
2105 d_out->lemma(lemma);
2106 return true;
2107 }
2108 }
2109 }
2110 }
2111 }
2112 return false;
2113 }
2114
2115 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
2116 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
2117 while( !eqcs_i.isFinished() ) {
2118 Node eqc = (*eqcs_i);
2119 //if eqc.getType is string
2120 if (eqc.getType().isString()) {
2121 eqcs.push_back( eqc );
2122 }
2123 ++eqcs_i;
2124 }
2125 }
2126
2127 void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) {
2128 if( n!=d_emptyString ){
2129 if( n.getKind()==kind::STRING_CONCAT ){
2130 for( unsigned i=0; i<n.getNumChildren(); i++ ){
2131 getFinalNormalForm( n[i], nf, exp );
2132 }
2133 }else{
2134 Trace("strings-debug") << "Get final normal form " << n << std::endl;
2135 Assert( d_equalityEngine.hasTerm( n ) );
2136 Node nr = d_equalityEngine.getRepresentative( n );
2137 EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false );
2138 Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null();
2139 if( !nc.isNull() ){
2140 nf.push_back( nc );
2141 if( n!=nc ){
2142 exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) );
2143 }
2144 }else{
2145 Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
2146 if( d_normal_forms[nr][0]==nr ){
2147 Assert( d_normal_forms[nr].size()==1 );
2148 nf.push_back( nr );
2149 if( n!=nr ){
2150 exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) );
2151 }
2152 }else{
2153 for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){
2154 Assert( d_normal_forms[nr][i]!=nr );
2155 getFinalNormalForm( d_normal_forms[nr][i], nf, exp );
2156 }
2157 exp.insert( exp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
2158 }
2159 }
2160 Trace("strings-ind-nf") << "The final normal form of " << n << " is " << nf << std::endl;
2161 }
2162 }
2163 }
2164
2165 void TheoryStrings::separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
2166 std::vector< Node >& lts ) {
2167 unsigned leqc_counter = 0;
2168 std::map< Node, unsigned > eqc_to_leqc;
2169 std::map< unsigned, Node > leqc_to_eqc;
2170 std::map< unsigned, std::vector< Node > > eqc_to_strings;
2171 for( unsigned i=0; i<n.size(); i++ ){
2172 Node eqc = n[i];
2173 Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
2174 EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
2175 Node lt = ei ? ei->d_length_term : Node::null();
2176 if( !lt.isNull() ){
2177 lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
2178 Node r = d_equalityEngine.getRepresentative( lt );
2179 if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
2180 eqc_to_leqc[r] = leqc_counter;
2181 leqc_to_eqc[leqc_counter] = r;
2182 leqc_counter++;
2183 }
2184 eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
2185 }else{
2186 eqc_to_strings[leqc_counter].push_back( eqc );
2187 leqc_counter++;
2188 }
2189 }
2190 for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
2191 std::vector< Node > vec;
2192 vec.insert( vec.end(), it->second.begin(), it->second.end() );
2193 lts.push_back( leqc_to_eqc[it->first] );
2194 cols.push_back( vec );
2195 }
2196 }
2197
2198 void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
2199 for( unsigned i=0; i<n.size(); i++ ){
2200 if( i>0 ) Trace(c) << " ++ ";
2201 Trace(c) << n[i];
2202 }
2203 }
2204
2205
2206 //// Measurements
2207 /*
2208 void TheoryStrings::updateMpl( Node n, int b ) {
2209 if(d_mpl.find(n) == d_mpl.end()) {
2210 //d_curr_cardinality.get();
2211 d_mpl[n] = b;
2212 } else if(b < d_mpl[n]) {
2213 d_mpl[n] = b;
2214 }
2215 }
2216 */
2217
2218 //// Regular Expressions
2219 Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
2220 if(d_regexp_ant.find(atom) == d_regexp_ant.end()) {
2221 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, ant, atom) );
2222 } else {
2223 Node n = d_regexp_ant[atom];
2224 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, ant, n) );
2225 }
2226 }
2227
2228 bool TheoryStrings::checkMemberships() {
2229 bool addedLemma = false;
2230 std::vector< Node > processed;
2231 std::vector< Node > cprocessed;
2232 for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
2233 //check regular expression membership
2234 Node assertion = d_reg_exp_mem[i];
2235 if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end()
2236 && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
2237 Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
2238 Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
2239 bool polarity = assertion.getKind()!=kind::NOT;
2240 bool flag = true;
2241 Node x = atom[0];
2242 Node r = atom[1];
2243 if( polarity ) {
2244 flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed);
2245 } else {
2246 if(! options::stringExp()) {
2247 throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
2248 }
2249 }
2250 if(flag) {
2251 //check if the term is atomic
2252 Node xr = getRepresentative( x );
2253 Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
2254 Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
2255 //TODO
2256 if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
2257 Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
2258 //if so, do simple unrolling
2259 std::vector< Node > nvec;
2260 d_regexp_opr.simplify(atom, nvec, polarity);
2261 Node antec = assertion;
2262 if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
2263 antec = d_regexp_ant[assertion];
2264 for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
2265 if(itr->getKind() == kind::STRING_IN_REGEXP) {
2266 if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
2267 d_regexp_ant[ *itr ] = antec;
2268 }
2269 }
2270 }
2271 }
2272 Node conc = nvec.size()==1 ? nvec[0] :
2273 NodeManager::currentNM()->mkNode(kind::AND, nvec);
2274 conc = Rewriter::rewrite(conc);
2275 sendLemma( antec, conc, "REGEXP" );
2276 addedLemma = true;
2277 processed.push_back( assertion );
2278 //d_regexp_ucached[assertion] = true;
2279 } else {
2280 Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
2281 for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
2282 Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
2283 }
2284 Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
2285 //otherwise, distribute unrolling over parts
2286 Node p1;
2287 Node p2;
2288 if( d_normal_forms[xr].size()>1 ){
2289 p1 = d_normal_forms[xr][0];
2290 std::vector< Node > cc;
2291 cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
2292 p2 = mkConcat( cc );
2293 }
2294
2295 Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
2296 std::vector< Node > antec;
2297 std::vector< Node > antecn;
2298 antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
2299 if( x!=xr ){
2300 antec.push_back( x.eqNode( xr ) );
2301 }
2302 antecn.push_back( assertion );
2303 Node ant = mkExplain( antec, antecn );
2304 Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
2305 Node conc;
2306 if( polarity ){
2307 if( d_normal_forms[xr].size()==0 ){
2308 conc = d_true;
2309 }else if( d_normal_forms[xr].size()==1 ){
2310 Trace("strings-regexp-debug") << "Case 1\n";
2311 conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
2312 }else{
2313 Trace("strings-regexp-debug") << "Case 2\n";
2314 std::vector< Node > conc_c;
2315 Node s11 = NodeManager::currentNM()->mkSkolem( "s11_$$", NodeManager::currentNM()->stringType(), "created for re" );
2316 Node s12 = NodeManager::currentNM()->mkSkolem( "s12_$$", NodeManager::currentNM()->stringType(), "created for re" );
2317 Node s21 = NodeManager::currentNM()->mkSkolem( "s21_$$", NodeManager::currentNM()->stringType(), "created for re" );
2318 Node s22 = NodeManager::currentNM()->mkSkolem( "s22_$$", NodeManager::currentNM()->stringType(), "created for re" );
2319 conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
2320 conc_c.push_back(conc);
2321 conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
2322 conc_c.push_back(conc);
2323 conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
2324 conc_c.push_back(conc);
2325 conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]);
2326 conc_c.push_back(conc);
2327 conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
2328 conc_c.push_back(conc);
2329 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
2330 Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
2331 conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
2332 d_pending_req_phase[eqz] = true;
2333 }
2334 }else{
2335 if( d_normal_forms[xr].size()==0 ){
2336 conc = d_false;
2337 }else if( d_normal_forms[xr].size()==1 ){
2338 Trace("strings-regexp-debug") << "Case 3\n";
2339 conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
2340 }else{
2341 Trace("strings-regexp-debug") << "Case 4\n";
2342 Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
2343 Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
2344 Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
2345 Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
2346 Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
2347 Node g1 = NodeManager::currentNM()->mkNode(kind::AND,
2348 NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
2349 NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
2350 NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
2351 NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
2352 Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
2353 Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
2354 Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
2355 Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
2356 Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
2357 Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate();
2358 Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
2359 conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
2360 conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
2361 conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
2362 conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
2363 }
2364 }
2365 if( conc!=d_true ){
2366 ant = mkRegExpAntec(assertion, ant);
2367 sendLemma(ant, conc, "REGEXP CSTAR");
2368 addedLemma = true;
2369 if( conc==d_false ){
2370 d_regexp_ccached.insert( assertion );
2371 }else{
2372 cprocessed.push_back( assertion );
2373 }
2374 }else{
2375 d_regexp_ccached.insert(assertion);
2376 }
2377 }
2378 }
2379 }
2380 if(d_conflict) {
2381 break;
2382 }
2383 }
2384 if( addedLemma ){
2385 if( !d_conflict ){
2386 for( unsigned i=0; i<processed.size(); i++ ){
2387 d_regexp_ucached.insert(processed[i]);
2388 }
2389 for( unsigned i=0; i<cprocessed.size(); i++ ){
2390 d_regexp_ccached.insert(cprocessed[i]);
2391 }
2392 }
2393 doPendingLemmas();
2394 return true;
2395 }else{
2396 return false;
2397 }
2398 }
2399
2400 bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed) {
2401 /*if(d_opt_regexp_gcd) {
2402 if(d_membership_length.find(atom) == d_membership_length.end()) {
2403 addedLemma = addMembershipLength(atom);
2404 d_membership_length[atom] = true;
2405 } else {
2406 Trace("strings-regexp") << "Membership length is already added." << std::endl;
2407 }
2408 }*/
2409 if(areEqual(x, d_emptyString)) {
2410 int rdel = d_regexp_opr.delta(r);
2411 if(rdel == 1) {
2412 d_regexp_ccached.insert(atom);
2413 } else if(rdel == 2) {
2414 Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
2415 Node conc = Node::null();
2416 sendLemma(antec, conc, "RegExp Delta CONFLICT");
2417 addedLemma = true;
2418 d_regexp_ccached.insert(atom);
2419 return false;
2420 }
2421 } else {
2422 Node xr = getRepresentative( x );
2423 if(x != xr) {
2424 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
2425 Node nn = Rewriter::rewrite( n );
2426 if(nn == d_true) {
2427 d_regexp_ccached.insert(atom);
2428 return false;
2429 } else if(nn == d_false) {
2430 Node antec = mkRegExpAntec(atom, x.eqNode(xr));
2431 Node conc = Node::null();
2432 sendLemma(antec, conc, "RegExp Delta CONFLICT");
2433 addedLemma = true;
2434 d_regexp_ccached.insert(atom);
2435 return false;
2436 }
2437 }
2438 Node sREant = mkRegExpAntec(atom, d_true);
2439 if(splitRegExp( x, r, sREant )) {
2440 addedLemma = true;
2441 processed.push_back( atom );
2442 return false;
2443 }
2444 }
2445 return true;
2446 }
2447
2448 bool TheoryStrings::checkContains() {
2449 bool addedLemma = checkPosContains();
2450 Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
2451 if(!d_conflict && !addedLemma) {
2452 addedLemma = checkNegContains();
2453 Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
2454 }
2455 return addedLemma;
2456 }
2457
2458 bool TheoryStrings::checkPosContains() {
2459 bool addedLemma = false;
2460 for( unsigned i=0; i<d_str_pos_ctn.size(); i++ ) {
2461 if( !d_conflict ){
2462 Node atom = d_str_pos_ctn[i];
2463 Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
2464 Assert( atom.getKind()==kind::STRING_STRCTN );
2465 Node x = atom[0];
2466 Node s = atom[1];
2467 if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
2468 if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) {
2469 Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
2470 Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
2471 d_statistics.d_new_skolems += 2;
2472 Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
2473 sendLemma( atom, eq, "POS-INC" );
2474 addedLemma = true;
2475 d_pos_ctn_cached.insert( atom );
2476 } else {
2477 Trace("strings-ctn") << "... is already rewritten." << std::endl;
2478 }
2479 } else {
2480 Trace("strings-ctn") << "... is satisfied." << std::endl;
2481 }
2482 }
2483 }
2484 if( addedLemma ){
2485 doPendingLemmas();
2486 return true;
2487 } else {
2488 return false;
2489 }
2490 }
2491
2492 bool TheoryStrings::checkNegContains() {
2493 bool addedLemma = false;
2494 for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
2495 if( !d_conflict ){
2496 Node atom = d_str_neg_ctn[i];
2497 Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
2498 if( areEqual( atom[1], d_emptyString ) ) {
2499 Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
2500 Node conc = Node::null();
2501 sendLemma( ant, conc, "NEG-CTN Conflict 1" );
2502 addedLemma = true;
2503 } else if( areEqual( atom[1], atom[0] ) ) {
2504 Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) );
2505 Node conc = Node::null();
2506 sendLemma( ant, conc, "NEG-CTN Conflict 2" );
2507 addedLemma = true;
2508 } else {
2509 if(options::stringExp()) {
2510 Node x = atom[0];
2511 Node s = atom[1];
2512 Node lenx = getLength(x);
2513 Node lens = getLength(s);
2514 if(areEqual(lenx, lens)) {
2515 if(d_neg_ctn_eqlen.find(atom) == d_neg_ctn_eqlen.end()) {
2516 Node eq = lenx.eqNode(lens);
2517 Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
2518 Node xneqs = x.eqNode(s).negate();
2519 d_neg_ctn_eqlen.insert( atom );
2520 sendLemma( antc, xneqs, "NEG-CTN-EQL" );
2521 addedLemma = true;
2522 }
2523 } else if(!areDisequal(lenx, lens)) {
2524 if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
2525 d_neg_ctn_ulen.insert( atom );
2526 sendSplit(lenx, lens, "NEG-CTN-SP");
2527 addedLemma = true;
2528 }
2529 } else {
2530 if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
2531 Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
2532 Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
2533 Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
2534 NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
2535 Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
2536 Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
2537 Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one);
2538
2539 Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
2540
2541 std::vector< Node > vec_nodes;
2542 Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
2543 vec_nodes.push_back(cc);
2544 cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 );
2545 vec_nodes.push_back(cc);
2546
2547 cc = s2.eqNode(s5).negate();
2548 vec_nodes.push_back(cc);
2549
2550 Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) );
2551 Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
2552 conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
2553 conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
2554 conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
2555 conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
2556
2557 d_neg_ctn_cached.insert( atom );
2558 sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
2559 //d_pending_req_phase[xlss] = true;
2560 addedLemma = true;
2561 }
2562 }
2563 } else {
2564 throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
2565 }
2566 }
2567 }
2568 }
2569 if( addedLemma ){
2570 doPendingLemmas();
2571 return true;
2572 } else {
2573 return false;
2574 }
2575 }
2576
2577 CVC4::String TheoryStrings::getHeadConst( Node x ) {
2578 if( x.isConst() ) {
2579 return x.getConst< String >();
2580 } else if( x.getKind() == kind::STRING_CONCAT ) {
2581 if( x[0].isConst() ) {
2582 return x[0].getConst< String >();
2583 } else {
2584 return d_emptyString.getConst< String >();
2585 }
2586 } else {
2587 return d_emptyString.getConst< String >();
2588 }
2589 }
2590
2591 bool TheoryStrings::addMembershipLength(Node atom) {
2592 //Node x = atom[0];
2593 //Node r = atom[1];
2594
2595 /*std::vector< int > co;
2596 co.push_back(0);
2597 for(unsigned int k=0; k<lts.size(); ++k) {
2598 if(lts[k].isConst() && lts[k].getType().isInteger()) {
2599 int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
2600 co[0] += cols[k].size() * len;
2601 } else {
2602 co.push_back( cols[k].size() );
2603 }
2604 }
2605 int g_co = co[0];
2606 for(unsigned k=1; k<co.size(); ++k) {
2607 g_co = gcd(g_co, co[k]);
2608 }*/
2609 return false;
2610 }
2611
2612 bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
2613 // TODO cstr in vre
2614 Assert(x != d_emptyString);
2615 Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
2616 //if(x.isConst()) {
2617 // Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
2618 // Node r = Rewriter::rewrite( n );
2619 // if(n != r) {
2620 // sendLemma(ant, r, "REGEXP REWRITE");
2621 // return true;
2622 // }
2623 //}
2624 CVC4::String s = getHeadConst( x );
2625 if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
2626 Node conc = Node::null();
2627 Node dc = r;
2628 bool flag = true;
2629 for(unsigned i=0; i<s.size(); ++i) {
2630 CVC4::String c = s.substr(i, 1);
2631 dc = d_regexp_opr.derivativeSingle(dc, c);
2632 if(dc == d_emptyRegexp) {
2633 // CONFLICT
2634 flag = false;
2635 break;
2636 }
2637 }
2638 // send lemma
2639 if(flag) {
2640 if(x.isConst()) {
2641 Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
2642 return false;
2643 } else {
2644 Assert( x.getKind() == kind::STRING_CONCAT );
2645 std::vector< Node > vec_nodes;
2646 for(unsigned int i=1; i<x.getNumChildren(); ++i ) {
2647 vec_nodes.push_back( x[i] );
2648 }
2649 Node left = vec_nodes.size() == 1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec_nodes );
2650 left = Rewriter::rewrite( left );
2651 conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
2652
2653 std::vector< Node > sdc;
2654 d_regexp_opr.simplify(conc, sdc, true);
2655 if(sdc.size() == 1) {
2656 conc = sdc[0];
2657 } else {
2658 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
2659 }
2660 }
2661 }
2662 sendLemma(ant, conc, "RegExp-CST-SP");
2663 return true;
2664 } else {
2665 return false;
2666 }
2667 }
2668
2669 //// Finite Model Finding
2670
2671 Node TheoryStrings::getNextDecisionRequest() {
2672 if(d_opt_fmf && !d_conflict) {
2673 Node in_var_lsum = d_input_var_lsum.get();
2674 //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
2675 //initialize the term we will minimize
2676 if( in_var_lsum.isNull() && !d_input_vars.empty() ){
2677 Trace("strings-fmf-debug") << "Input variables: ";
2678 std::vector< Node > ll;
2679 for(NodeSet::const_iterator itr = d_input_vars.begin();
2680 itr != d_input_vars.end(); ++itr) {
2681 Trace("strings-fmf-debug") << " " << (*itr) ;
2682 ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) );
2683 }
2684 Trace("strings-fmf-debug") << std::endl;
2685 in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll );
2686 in_var_lsum = Rewriter::rewrite( in_var_lsum );
2687 d_input_var_lsum.set( in_var_lsum );
2688 }
2689 if( !in_var_lsum.isNull() ){
2690 //Trace("strings-fmf") << "Get next decision request." << std::endl;
2691 //check if we need to decide on something
2692 int decideCard = d_curr_cardinality.get();
2693 if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){
2694 bool value;
2695 Node cnode = d_cardinality_lits[ d_curr_cardinality.get() ];
2696 if( d_valuation.hasSatValue( cnode, value ) ) {
2697 if( !value ){
2698 d_curr_cardinality.set( d_curr_cardinality.get() + 1 );
2699 decideCard = d_curr_cardinality.get();
2700 Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl;
2701 }else{
2702 decideCard = -1;
2703 Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl;
2704 }
2705 }else{
2706 Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl;
2707 }
2708 }
2709 if( decideCard!=-1 ){
2710 if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){
2711 Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) );
2712 lit = Rewriter::rewrite( lit );
2713 d_cardinality_lits[decideCard] = lit;
2714 Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
2715 Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem << ", decideCard = " << decideCard << std::endl;
2716 d_out->lemma( lem );
2717 d_out->requirePhase( lit, true );
2718 }
2719 Node lit = d_cardinality_lits[ decideCard ];
2720 Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit << std::endl;
2721 return lit;
2722 }
2723 }
2724 }
2725
2726 return Node::null();
2727 }
2728
2729 void TheoryStrings::assertNode( Node lit ) {
2730 }
2731
2732 Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ) {
2733 Node sk = NodeManager::currentNM()->mkSkolem( c, lhs.getType(), info );
2734 d_statistics.d_new_skolems += 1;
2735 Node eq = lhs.eqNode( mkConcat( rhs, sk ) );
2736 eq = Rewriter::rewrite( eq );
2737 if( lgtZero ) {
2738 Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
2739 Trace("strings-lemma") << "Strings::Lemma SK-NON-EMPTY: " << sk_gt_zero << std::endl;
2740 d_lemma_cache.push_back( sk_gt_zero );
2741 }
2742 return eq;
2743 }
2744
2745 // Stats
2746 TheoryStrings::Statistics::Statistics():
2747 d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
2748 d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
2749 d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
2750 d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
2751 d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
2752 {
2753 StatisticsRegistry::registerStat(&d_splits);
2754 StatisticsRegistry::registerStat(&d_eq_splits);
2755 StatisticsRegistry::registerStat(&d_deq_splits);
2756 StatisticsRegistry::registerStat(&d_loop_lemmas);
2757 StatisticsRegistry::registerStat(&d_new_skolems);
2758 }
2759
2760 TheoryStrings::Statistics::~Statistics(){
2761 StatisticsRegistry::unregisterStat(&d_splits);
2762 StatisticsRegistry::unregisterStat(&d_eq_splits);
2763 StatisticsRegistry::unregisterStat(&d_deq_splits);
2764 StatisticsRegistry::unregisterStat(&d_loop_lemmas);
2765 StatisticsRegistry::unregisterStat(&d_new_skolems);
2766 }
2767
2768 }/* CVC4::theory::strings namespace */
2769 }/* CVC4::theory namespace */
2770 }/* CVC4 namespace */