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