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