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