projects / cvc5.git / blob
? search:


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