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