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