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