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