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