projects / cvc5.git / blob
? search:


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