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