projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge branch 'master' of https://github.com/CVC4/CVC4
[cvc5.git] / src / theory / strings / theory_strings.cpp
1 /********************* */
2 /*! \file theory_strings.cpp
3 ** \verbatim
4 ** Original author: Tianyi Liang
5 ** Major contributors: Tianyi Liang, Andrew Reynolds
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2013-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
11 **
12 ** \brief Implementation of the theory of strings.
13 **
14 ** Implementation of the theory of strings.
15 **/
16
17
18 #include "theory/strings/theory_strings.h"
19 #include "theory/valuation.h"
20 #include "expr/kind.h"
21 #include "theory/rewriter.h"
22 #include "expr/command.h"
23 #include "theory/model.h"
24 #include "smt/logic_exception.h"
25 #include "theory/strings/options.h"
26 #include <cmath>
27
28 using namespace std;
29 using namespace CVC4::context;
30
31 namespace CVC4 {
32 namespace theory {
33 namespace strings {
34
35 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
36 : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe),
37 d_notify( *this ),
38 d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
39 d_conflict( c, false ),
40 d_infer(c),
41 d_infer_exp(c),
42 d_nf_pairs(c),
43 d_ind_map1(c),
44 d_ind_map2(c),
45 d_ind_map_exp(c),
46 d_ind_map_lemma(c)
47 {
48 // The kinds we are treating as function application in congruence
49 d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
50 d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
51 d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
52
53 d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
54 d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
55 d_true = NodeManager::currentNM()->mkConst( true );
56 d_false = NodeManager::currentNM()->mkConst( false );
57 }
58
59 TheoryStrings::~TheoryStrings() {
60
61 }
62
63 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
64 d_equalityEngine.setMasterEqualityEngine(eq);
65 }
66
67 void TheoryStrings::addSharedTerm(TNode t) {
68 Debug("strings") << "TheoryStrings::addSharedTerm(): "
69 << t << " " << t.getType().isBoolean() << endl;
70 d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
71 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
72 }
73
74 void TheoryStrings::propagate(Effort e)
75 {
76 // direct propagation now
77 }
78
79 bool TheoryStrings::propagate(TNode literal) {
80 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl;
81 // If already in conflict, no more propagation
82 if (d_conflict) {
83 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
84 return false;
85 }
86 Trace("strings-prop") << "strPropagate " << literal << std::endl;
87 // Propagate out
88 bool ok = d_out->propagate(literal);
89 if (!ok) {
90 d_conflict = true;
91 }
92 return ok;
93 }
94
95 /** explain */
96 void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
97 Debug("strings-explain") << "Explain " << literal << std::endl;
98 bool polarity = literal.getKind() != kind::NOT;
99 TNode atom = polarity ? literal : literal[0];
100 if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
101 d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
102 } else {
103 d_equalityEngine.explainPredicate(atom, polarity, assumptions);
104 }
105 }
106
107 Node TheoryStrings::explain( TNode literal ){
108 std::vector< TNode > assumptions;
109 explain( literal, assumptions );
110 if( assumptions.empty() ){
111 return NodeManager::currentNM()->mkConst( true );
112 }else if( assumptions.size()==1 ){
113 return assumptions[0];
114 }else{
115 return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
116 }
117 }
118
119 /////////////////////////////////////////////////////////////////////////////
120 // MODEL GENERATION
121 /////////////////////////////////////////////////////////////////////////////
122
123
124 void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
125 /*
126 // Generate model
127 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
128 while( !eqcs_i.isFinished() ) {
129 Node eqc = (*eqcs_i);
130 //if eqc.getType is string
131 if (eqc.getType().isString()) {
132 EqcInfo* ei = getOrMakeEqcInfo( eqc );
133 Node cst = ei ? ei->d_const_term : Node::null();
134 if( !cst.isNull() ){
135 //print out
136 Trace("strings-model-debug") << cst << std::endl;
137 }else{
138 //is there a length term?
139 // is there a value for it? if so, assign a constant via enumerator
140 // otherwise: error
141 //otherwise: assign a new unique length, then assign a constant via enumerator
142 }
143 }else{
144 //should be length eqc
145 //if no constant, error
146 }
147
148 ++eqcs_i;
149 }
150 */
151 //TODO: not done
152 }
153
154 /////////////////////////////////////////////////////////////////////////////
155 // MAIN SOLVER
156 /////////////////////////////////////////////////////////////////////////////
157
158 void TheoryStrings::preRegisterTerm(TNode n) {
159 Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
160 //collectTerms( n );
161 switch (n.getKind()) {
162 case kind::EQUAL:
163 d_equalityEngine.addTriggerEquality(n);
164 break;
165 case kind::STRING_IN_REGEXP:
166 d_equalityEngine.addTriggerPredicate(n);
167 break;
168 default:
169 if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
170 Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
171 Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
172 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, zero);
173 Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
174 d_out->lemma(n_len_geq_zero);
175 }
176 if (n.getType().isBoolean()) {
177 // Get triggered for both equal and dis-equal
178 d_equalityEngine.addTriggerPredicate(n);
179 } else {
180 // Function applications/predicates
181 d_equalityEngine.addTerm(n);
182 }
183 break;
184 }
185 }
186
187 void TheoryStrings::dealPositiveWordEquation(TNode n) {
188 Trace("strings-pwe") << "Deal Positive Word Equation: " << n << endl;
189 Node node = n;
190
191 // length left = length right
192 //Node n_left = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]);
193 //Node n_right = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[1]);
194 if(node[0].getKind() == kind::CONST_STRING) {
195 } else if(node[0].getKind() == kind::STRING_CONCAT) {
196 }
197 }
198
199 void TheoryStrings::check(Effort e) {
200 bool polarity;
201 TNode atom;
202
203 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
204 Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
205 while ( !done() && !d_conflict)
206 {
207 // Get all the assertions
208 Assertion assertion = get();
209 TNode fact = assertion.assertion;
210
211 Trace("strings-assertion") << "get assertion: " << fact << endl;
212
213 polarity = fact.getKind() != kind::NOT;
214 atom = polarity ? fact : fact[0];
215 if (atom.getKind() == kind::EQUAL) {
216 //head
217 //if(atom[0].getKind() == kind::CONST_STRING) {
218 //if(atom[1].getKind() == kind::STRING_CONCAT) {
219 //}
220 //}
221 //tail
222 d_equalityEngine.assertEquality(atom, polarity, fact);
223 } else {
224 d_equalityEngine.assertPredicate(atom, polarity, fact);
225 }
226 switch(atom.getKind()) {
227 case kind::EQUAL:
228 if(polarity) {
229 //if(atom[0].isString() && atom[1].isString()) {
230 //dealPositiveWordEquation(atom);
231 //}
232 } else {
233 // TODO: Word Equation negaitive
234 }
235 break;
236 case kind::STRING_IN_REGEXP:
237 // TODO: membership
238 break;
239 default:
240 //possibly error
241 break;
242 }
243 }
244 doPendingFacts();
245
246
247 bool addedLemma = false;
248 if( e == EFFORT_FULL && !d_conflict ) {
249 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
250 while( !eqcs_i.isFinished() ){
251 Node eqc = (*eqcs_i);
252 //if eqc.getType is string
253 if (eqc.getType().isString()) {
254 //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
255 //get the constant for the equivalence class
256 //int c_len = ...;
257 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
258 while( !eqc_i.isFinished() ){
259 Node n = (*eqc_i);
260
261 //if n is concat, and
262 //if n has not instantiatied the concat..length axiom
263 //then, add lemma
264 if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
265 if( d_length_inst.find(n)==d_length_inst.end() ){
266 d_length_inst[n] = true;
267 Trace("strings-debug") << "get n: " << n << endl;
268 Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
269 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
270 eq = Rewriter::rewrite(eq);
271 Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
272 d_out->lemma(eq);
273 Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
274 Node lsum;
275 if( n.getKind() == kind::STRING_CONCAT ){
276 //add lemma
277 std::vector<Node> node_vec;
278 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
279 Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
280 node_vec.push_back(lni);
281 }
282 lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
283 }else{
284 //add lemma
285 lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
286 }
287 Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
288 ceq = Rewriter::rewrite(ceq);
289 Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl;
290 d_out->lemma(ceq);
291 addedLemma = true;
292 }
293 }
294 ++eqc_i;
295 }
296 }
297 ++eqcs_i;
298 }
299 if( !addedLemma ){
300 addedLemma = checkNormalForms();
301 if(!d_conflict && !addedLemma) {
302 addedLemma = checkCardinality();
303 if( !d_conflict && !addedLemma ){
304 addedLemma = checkInductiveEquations();
305 }
306 }
307 }
308 }
309 Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
310 }
311
312 TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) {
313
314 }
315
316 TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) {
317 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc );
318 if( eqc_i==d_eqc_info.end() ){
319 if( doMake ){
320 EqcInfo* ei = new EqcInfo( getSatContext() );
321 d_eqc_info[eqc] = ei;
322 return ei;
323 }else{
324 return NULL;
325 }
326 }else{
327 return (*eqc_i).second;
328 }
329 }
330
331
332 /** Conflict when merging two constants */
333 void TheoryStrings::conflict(TNode a, TNode b){
334 Node conflictNode;
335 if (a.getKind() == kind::CONST_BOOLEAN) {
336 conflictNode = explain( a.iffNode(b) );
337 } else {
338 conflictNode = explain( a.eqNode(b) );
339 }
340 Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
341 d_out->conflict( conflictNode );
342 d_conflict = true;
343 }
344
345 /** called when a new equivalance class is created */
346 void TheoryStrings::eqNotifyNewClass(TNode t){
347 if( t.getKind() == kind::CONST_STRING ){
348 EqcInfo * ei =getOrMakeEqcInfo( t, true );
349 ei->d_const_term = t;
350 }
351 if( t.getKind() == kind::STRING_LENGTH ){
352 Trace("strings-debug") << "New length eqc : " << t << std::endl;
353 Node r = d_equalityEngine.getRepresentative(t[0]);
354 EqcInfo * ei = getOrMakeEqcInfo( r, true );
355 ei->d_length_term = t[0];
356 }
357 }
358
359 /** called when two equivalance classes will merge */
360 void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
361 EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
362 if( e2 ){
363 EqcInfo * e1 = getOrMakeEqcInfo( t1 );
364 //add information from e2 to e1
365 if( !e2->d_const_term.get().isNull() ){
366 e1->d_const_term.set( e2->d_const_term );
367 }
368 if( !e2->d_length_term.get().isNull() ){
369 e1->d_length_term.set( e2->d_length_term );
370 }
371 if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
372 e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
373 }
374 }
375 if( hasTerm( d_zero ) ){
376 Node leqc;
377 if( areEqual(d_zero, t1) ){
378 leqc = t2;
379 }else if( areEqual(d_zero, t2) ){
380 leqc = t1;
381 }
382 if( !leqc.isNull() ){
383 //scan equivalence class to see if we apply
384 eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
385 while( !eqc_i.isFinished() ){
386 Node n = (*eqc_i);
387 if( n.getKind()==kind::STRING_LENGTH ){
388 if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
389 Trace("strings-debug") << "Processing possible inference." << n << std::endl;
390 //apply the rule length(n[0])==0 => n[0] == ""
391 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
392 d_pending.push_back( eq );
393 Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
394 d_pending_exp[eq] = eq_exp;
395 Trace("strings-infer") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
396 d_infer.push_back(eq);
397 d_infer_exp.push_back(eq_exp);
398 }
399 }
400 ++eqc_i;
401 }
402 }
403 }
404 }
405
406 /** called when two equivalance classes have merged */
407 void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) {
408
409 }
410
411 /** called when two equivalance classes are disequal */
412 void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
413
414 }
415
416 void TheoryStrings::computeCareGraph(){
417 Theory::computeCareGraph();
418 }
419
420 void TheoryStrings::doPendingFacts() {
421 int i=0;
422 while( !d_conflict && i<(int)d_pending.size() ){
423 Node fact = d_pending[i];
424 Node exp = d_pending_exp[ fact ];
425 Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
426 bool polarity = fact.getKind() != kind::NOT;
427 TNode atom = polarity ? fact : fact[0];
428 if (atom.getKind() == kind::EQUAL) {
429 d_equalityEngine.assertEquality( atom, polarity, exp );
430 }else{
431 d_equalityEngine.assertPredicate( atom, polarity, exp );
432 }
433 i++;
434 }
435 d_pending.clear();
436 d_pending_exp.clear();
437 }
438
439 void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
440 std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
441 // EqcItr
442 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
443 while( !eqc_i.isFinished() ) {
444 Node n = (*eqc_i);
445 Trace("strings-process") << "Process term " << n << std::endl;
446 if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
447 std::vector<Node> nf_n;
448 std::vector<Node> nf_exp_n;
449 if( n.getKind() == kind::CONST_STRING ){
450 if( n!=d_emptyString ) {
451 nf_n.push_back( n );
452 }
453 } else if( n.getKind() == kind::STRING_CONCAT ) {
454 for( unsigned i=0; i<n.getNumChildren(); i++ ) {
455 Node nr = d_equalityEngine.getRepresentative( n[i] );
456 std::vector< Node > nf_temp;
457 std::vector< Node > nf_exp_temp;
458 Trace("strings-process") << "Normalizing subterm " << n[i] << " = " << nr << std::endl;
459 normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
460 if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
461 return;
462 }
463 if( nf.size()!=1 || nf[0]!=d_emptyString ) {
464 for( unsigned r=0; r<nf_temp.size(); r++ ) {
465 Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
466 }
467 nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
468 }
469 nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
470 if( nr!=n[i] ) {
471 nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
472 }
473 }
474 }
475 normal_forms.push_back(nf_n);
476 normal_forms_exp.push_back(nf_exp_n);
477 normal_form_src.push_back(n);
478 }
479 /* should we add these?
480 else {
481 //var/sk?
482 std::vector<Node> nf_n;
483 std::vector<Node> nf_exp_n;
484 nf_n.push_back(n);
485 normal_forms.push_back(nf_n);
486 normal_forms_exp.push_back(nf_exp_n);
487 normal_form_src.push_back(n);
488 }*/
489 ++eqc_i;
490 }
491
492 // Test the result
493 if( !normal_forms.empty() ) {
494 Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
495 for( unsigned i=0; i<normal_forms.size(); i++ ) {
496 Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
497 for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
498 if(j>0) Trace("strings-solve") << ", ";
499 Trace("strings-solve") << normal_forms[i][j];
500 }
501 Trace("strings-solve") << std::endl;
502 Trace("strings-solve") << " Explanation is : ";
503 if(normal_forms_exp[i].size() == 0) {
504 Trace("strings-solve") << "NONE";
505 } else {
506 for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
507 if(j>0) Trace("strings-solve") << " AND ";
508 Trace("strings-solve") << normal_forms_exp[i][j];
509 }
510 }
511 Trace("strings-solve") << std::endl;
512 }
513 }
514 }
515 //nf_exp is conjunction
516 void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
517 Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
518 if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
519 //nf.push_back( eqc );
520 if( eqc.getKind()==kind::STRING_CONCAT ){
521 for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
522 nf.push_back( eqc[i] );
523 }
524 }else{
525 nf.push_back( eqc );
526 }
527 Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
528 } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){
529 //do nothing
530 Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
531 } else {
532 visited.push_back( eqc );
533 if(d_normal_forms.find(eqc)==d_normal_forms.end() ){
534 //phi => t = s1 * ... * sn
535 // normal form for each non-variable term in this eqc (s1...sn)
536 std::vector< std::vector< Node > > normal_forms;
537 // explanation for each normal form (phi)
538 std::vector< std::vector< Node > > normal_forms_exp;
539 // record terms for each normal form (t)
540 std::vector< Node > normal_form_src;
541 //Get Normal Forms
542 getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
543 if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
544 return;
545 }
546
547 unsigned i = 0;
548 //unify each normal form > 0 with normal_forms[0]
549 for( unsigned j=1; j<normal_forms.size(); j++ ) {
550 std::vector< Node > loop_eqs_x;
551 std::vector< Node > loop_eqs_y;
552 std::vector< Node > loop_eqs_z;
553 std::vector< Node > loop_exps;
554 Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
555 if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
556 Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
557 }else{
558 Trace("strings-solve") << "Not in cache." << std::endl;
559 //the current explanation for why the prefix is equal
560 std::vector< Node > curr_exp;
561 curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
562 curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
563 curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
564 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
565 unsigned index_i = 0;
566 unsigned index_j = 0;
567 bool success;
568 do
569 {
570 success = false;
571 //if we are at the end
572 if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
573 if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
574 //we're done
575 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
576 //add loop equations that we've accumulated
577 for( unsigned r=0; r<loop_eqs_x.size(); r++ ){
578 addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] );
579 }
580 }else{
581 //the remainder must be empty
582 unsigned k = index_i==normal_forms[i].size() ? j : i;
583 unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
584 while(!d_conflict && index_k<normal_forms[k].size()) {
585 //can infer that this string must be empty
586 Node eq_exp;
587 if( curr_exp.empty() ) {
588 eq_exp = NodeManager::currentNM()->mkConst(true);
589 } else if( curr_exp.size() == 1 ) {
590 eq_exp = curr_exp[0];
591 } else {
592 eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
593 }
594 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
595 Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
596 //d_equalityEngine.assertEquality( eq, true, eq_exp );
597 d_pending.push_back( eq );
598 d_pending_exp[eq] = eq_exp;
599 d_infer.push_back(eq);
600 d_infer_exp.push_back(eq_exp);
601 index_k++;
602 }
603 }
604 }else {
605 Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
606 if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
607 Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
608 //terms are equal, continue
609 if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
610 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
611 normal_forms[j][index_j]);
612 Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
613 curr_exp.push_back(eq);
614 }
615 index_j++;
616 index_i++;
617 success = true;
618 }else{
619 EqcInfo * ei = getOrMakeEqcInfo( normal_forms[i][index_i] );
620 Node length_term_i = ei->d_length_term;
621 if( length_term_i.isNull()) {
622 //typically shouldnt be necessary
623 length_term_i = normal_forms[i][index_i];
624 }
625 length_term_i = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_i );
626 EqcInfo * ej = getOrMakeEqcInfo( normal_forms[j][index_j] );
627 Node length_term_j = ej->d_length_term;
628 if( length_term_j.isNull()) {
629 length_term_j = normal_forms[j][index_j];
630 }
631 length_term_j = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_j );
632 //check if length(normal_forms[i][index]) == length(normal_forms[j][index])
633 if( areEqual(length_term_i, length_term_j) ){
634 Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl;
635 //length terms are equal, merge equivalence classes if not already done so
636 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
637 std::vector< Node > temp_exp;
638 temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
639 temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ));
640 Node eq_exp = temp_exp.empty() ? NodeManager::currentNM()->mkConst(true) :
641 temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
642 Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
643 //d_equalityEngine.assertEquality( eq, true, eq_exp );
644 d_pending.push_back( eq );
645 d_pending_exp[eq] = eq_exp;
646 d_infer.push_back(eq);
647 d_infer_exp.push_back(eq_exp);
648 return;
649 }else{
650 Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl;
651 bool sendLemma = false;
652 Node loop_x;
653 Node loop_y;
654 Node loop_z;
655 Node conc;
656 std::vector< Node > antec;
657 std::vector< Node > antec_new_lits;
658 //check for loops
659 Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
660 int has_loop[2] = { -1, -1 };
661 for( unsigned r=0; r<2; r++ ){
662 int index = (r==0 ? index_i : index_j);
663 int other_index = (r==0 ? index_j : index_i );
664 int n_index = (r==0 ? i : j);
665 int other_n_index = (r==0 ? j : i);
666 if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
667 for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
668 if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
669 has_loop[r] = lp;
670 break;
671 }
672 }
673 }
674 }
675 if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
676 int loop_n_index = has_loop[0]!=-1 ? i : j;
677 int other_n_index = has_loop[0]!=-1 ? j : i;
678 int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
679 int index = has_loop[0]!=-1 ? index_i : index_j;
680 int other_index = has_loop[0]!=-1 ? index_j : index_i;
681 Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
682 Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl;
683 //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
684 //check if
685 //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] = y * z
686 // and
687 //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
688 // for some y,z,k
689 int found_size_y = -1;
690 for( int size_y = 0; size_y<(loop_index-index); size_y++ ){
691 int size_z = (loop_index-index)-size_y;
692 bool success = true;
693 //check for z
694 for( int r = 0; r<size_z; r++ ){
695 if( other_index+1+r >= (int)normal_forms[other_n_index].size() ||
696 normal_forms[other_n_index][other_index+1+r]!=normal_forms[loop_n_index][index+size_y+r] ) {
697 success = false;
698 break;
699 }
700 }
701 //check for y
702 if( success ){
703 for( int r=0; r<size_y; r++ ){
704 if( other_index+1+r >= (int)normal_forms[other_n_index].size() ||
705 normal_forms[other_n_index][other_index+1+size_y+r]!=normal_forms[loop_n_index][index+r] ) {
706 success = false;
707 break;
708 }
709 }
710 if( success ){
711 found_size_y = size_y;
712 break;
713 }
714 }
715 }
716 if( found_size_y==-1 ){
717 //need to break
718 Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
719 Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
720
721 sendLemma = true;
722 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
723 //t1 * ... * tn = y * z
724 std::vector< Node > c1c;
725 //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
726 for( int r=index; r<=loop_index-1; r++ ) {
727 c1c.push_back( normal_forms[loop_n_index][r] );
728 }
729 Node conc1 = c1c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c1c ) :
730 c1c.size()==1 ? c1c[0] : d_emptyString;
731 conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
732 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
733 std::vector< Node > c2c;
734 //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
735 for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
736 c2c.push_back( normal_forms[other_n_index][r] );
737 }
738 Node left2 = c2c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c2c ) :
739 c2c.size()==1 ? c2c[0] : d_emptyString;
740 std::vector< Node > c3c;
741 c3c.push_back( sk_z );
742 c3c.push_back( sk_y );
743 //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
744 for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
745 c3c.push_back( normal_forms[loop_n_index][r] );
746 }
747 Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
748 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c3c ) );
749 Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
750 Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
751 Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
752 //Node sk_y_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_y_len, zero);
753 //Node sk_z_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_z_len, zero);
754 conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, sk_y_len_geq_zero, sk_z_len_geq_zero );
755 loop_x = normal_forms[other_n_index][other_index];
756 loop_y = sk_y;
757 loop_z = sk_z;
758 //we will be done
759 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
760 } else {
761 // x = (yz)*y
762 Trace("strings-loop") << "We have that " << normal_forms[loop_n_index][loop_index] << " = (";
763 loop_eqs_x.push_back( normal_forms[loop_n_index][loop_index] );
764 for( unsigned r=0; r<2; r++ ){
765 //print y
766 std::vector< Node > yc;
767 for( int rr = 0; rr<found_size_y; rr++ ){
768 if( rr>0 ) Trace("strings-loop") << ".";
769 Trace("strings-loop") << normal_forms[loop_n_index][index+rr];
770 yc.push_back( normal_forms[loop_n_index][index+rr] );
771 }
772 if( r==0 ){
773 loop_eqs_y.push_back( mkConcat( yc ) );
774 Trace("strings-loop") <<"..";
775 //print z
776 int found_size_z = (loop_index-index)-found_size_y;
777 std::vector< Node > zc;
778 for( int rr = 0; rr<found_size_z; rr++ ){
779 if( rr>0 ) Trace("strings-loop") << ".";
780 Trace("strings-loop") << normal_forms[loop_n_index][index+found_size_y+rr];
781 zc.push_back( normal_forms[loop_n_index][index+found_size_y+rr] );
782 }
783 Trace("strings-loop") << ")*";
784 loop_eqs_z.push_back( mkConcat( zc ) );
785 }
786 }
787 Trace("strings-loop") << std::endl;
788 if( loop_n_index==(int)i ){
789 index_j += (loop_index+1)-index_i;
790 index_i = loop_index+1;
791 }else{
792 index_i += (loop_index+1)-index_j;
793 index_j = loop_index+1;
794 }
795 success = true;
796 std::vector< Node > empty_vec;
797 loop_exps.push_back( mkExplain( antec, empty_vec ) );
798 }
799 }else{
800 Trace("strings-loop") << "No loops detected." << std::endl;
801 if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
802 normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
803 Node const_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[i][index_i] : normal_forms[j][index_j];
804 Node other_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[j][index_j] : normal_forms[i][index_i];
805 if( other_str.getKind() == kind::CONST_STRING ) {
806 unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
807 if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
808 //same prefix
809 //k is the index of the string that is shorter
810 int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
811 int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
812 int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
813 int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
814 Node remainderStr = NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(len_short) );
815 Trace("strings-solve-debug") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
816 normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
817 normal_forms[l][index_l] = normal_forms[k][index_k];
818 success = true;
819 } else {
820 //curr_exp is conflict
821 sendLemma = true;
822 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
823 }
824 } else {
825 Assert( other_str.getKind()!=kind::STRING_CONCAT );
826 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
827 Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
828 NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
829 //split the string
830 Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
831 // |sk| >= 0
832 Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
833 Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
834 //Node sk_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_len, zero);
835
836 Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
837 Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
838 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
839 Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
840 conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
841 Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
842 sendLemma = true;
843 }
844 }else{
845 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
846 Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
847 if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
848 antec.push_back( ldeq );
849 }else{
850 antec_new_lits.push_back(ldeq);
851 }
852 Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
853 Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
854 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
855 Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
856 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
857 conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
858 sendLemma = true;
859 // |sk| > 0
860 Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
861 Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
862 Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, zero);
863 Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
864 //d_out->lemma(sk_gt_zero);
865 d_lemma_cache.push_back( sk_gt_zero );
866 }
867 }
868 Trace("strings-solve-debug2") << "sendLemma/success : " << sendLemma << " " << success << std::endl;
869 if( sendLemma ){
870 Node ant = mkExplain( antec, antec_new_lits );
871 if( conc.isNull() ){
872 d_out->conflict(ant);
873 Trace("strings-conflict") << "Strings conflict : " << ant << std::endl;
874 d_conflict = true;
875 }else{
876 Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
877 Trace("strings-lemma") << "Strings compare lemma : " << lem << std::endl;
878 //d_out->lemma(lem);
879 d_lemma_cache.push_back( lem );
880 }
881 if( !loop_y.isNull() ){
882 addInductiveEquation( loop_x, loop_y, loop_z, ant );
883 }
884 return;
885 }
886 }
887 }
888 }
889 }while(success);
890 }
891 }
892
893 //construct the normal form
894 if( normal_forms.empty() ){
895 Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
896 nf.push_back( eqc );
897 } else {
898 Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
899 //just take the first normal form
900 nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
901 nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
902 if( eqc!=normal_form_src[0] ){
903 nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
904 }
905 Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
906 }
907 //if( visited.empty() ){
908 //TODO : cache?
909 //}
910 d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
911 d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
912 Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl;
913 }else{
914 Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl;
915 nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
916 nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
917 }
918 visited.pop_back();
919 }
920 }
921 bool TheoryStrings::hasTerm( Node a ){
922 return d_equalityEngine.hasTerm( a );
923 }
924
925 bool TheoryStrings::areEqual( Node a, Node b ){
926 if( a==b ){
927 return true;
928 }else if( hasTerm( a ) && hasTerm( b ) ){
929 return d_equalityEngine.areEqual( a, b );
930 }else{
931 return false;
932 }
933 }
934
935 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
936 //Trace("strings-debug") << "add normal form pair. " << n1 << " " << n2 << std::endl;
937 if( !isNormalFormPair( n1, n2 ) ){
938 NodeList* lst;
939 NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
940 if( nf_i == d_nf_pairs.end() ){
941 if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
942 addNormalFormPair( n2, n1 );
943 return;
944 }
945 lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
946 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
947 d_nf_pairs.insertDataFromContextMemory( n1, lst );
948 }else{
949 lst = (*nf_i).second;
950 }
951 lst->push_back( n2 );
952 }
953 }
954 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
955 //TODO: modulo equality?
956 return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
957 }
958 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
959 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
960 NodeList* lst;
961 NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
962 if( nf_i != d_nf_pairs.end() ){
963 lst = (*nf_i).second;
964 for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
965 Node n = *i;
966 if( n==n2 ){
967 return true;
968 }
969 }
970 }
971 return false;
972 }
973
974 void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
975 Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
976
977 NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
978 NodeList* lst1;
979 NodeList* lst2;
980 NodeList* lste;
981 NodeList* lstl;
982 if( itr_x_y == d_ind_map1.end() ) {
983 // add x->y
984 lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
985 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
986 d_ind_map1.insertDataFromContextMemory( x, lst1 );
987 // add x->z
988 lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
989 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
990 d_ind_map2.insertDataFromContextMemory( x, lst2 );
991 // add x->exp
992 lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
993 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
994 d_ind_map_exp.insertDataFromContextMemory( x, lste );
995 // add x->hasLemma false
996 lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
997 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
998 d_ind_map_lemma.insertDataFromContextMemory( x, lstl );
999 } else {
1000 //TODO: x in (yz)*y (exp) vs x in (y1 z1)*y1 (exp1)
1001 lst1 = (*itr_x_y).second;
1002 lst2 = (*d_ind_map2.find(x)).second;
1003 lste = (*d_ind_map_exp.find(x)).second;
1004 lstl = (*d_ind_map_lemma.find(x)).second;
1005 Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl;
1006 Trace("strings-solve-debug") << "... with exp = " << lste << std::endl;
1007 }
1008 lst1->push_back( y );
1009 lst2->push_back( z );
1010 lste->push_back( exp );
1011 }
1012
1013 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
1014 return c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
1015 }
1016
1017 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
1018 std::vector< TNode > antec_exp;
1019 for( unsigned i=0; i<a.size(); i++ ){
1020 Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
1021 //assert
1022 if(a[i].getKind() == kind::EQUAL) {
1023 //assert( hasTerm(a[i][0]) );
1024 //assert( hasTerm(a[i][1]) );
1025 Assert( areEqual(a[i][0], a[i][1]) );
1026 } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
1027 Assert( hasTerm(a[i][0][0]) );
1028 Assert( hasTerm(a[i][0][1]) );
1029 Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
1030 }
1031 explain(a[i], antec_exp);
1032 Trace("strings-solve-debug") << "Done." << std::endl;
1033 }
1034 for( unsigned i=0; i<an.size(); i++ ){
1035 antec_exp.push_back(an[i]);
1036 }
1037 Node ant;
1038 if( antec_exp.empty() ) {
1039 ant = NodeManager::currentNM()->mkConst(true);
1040 } else if( antec_exp.size()==1 ) {
1041 ant = antec_exp[0];
1042 } else {
1043 ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
1044 }
1045 return ant;
1046 }
1047
1048 bool TheoryStrings::checkNormalForms() {
1049 Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
1050 eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
1051 while( !eqcs2_i.isFinished() ){
1052 Node eqc = (*eqcs2_i);
1053 //if (eqc.getType().isString()) {
1054 eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1055 Trace("strings-eqc") << "Eqc( " << eqc << " ) : ";
1056 while( !eqc2_i.isFinished() ) {
1057 Trace("strings-eqc") << (*eqc2_i) << " ";
1058 ++eqc2_i;
1059 }
1060 Trace("strings-eqc") << std::endl;
1061 //}
1062 ++eqcs2_i;
1063 }
1064
1065 bool addedFact = false;
1066 do {
1067 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
1068 d_normal_forms.clear();
1069 d_normal_forms_exp.clear();
1070 std::map< Node, Node > nf_to_eqc;
1071 std::map< Node, Node > eqc_to_exp;
1072 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1073 d_lemma_cache.clear();
1074 while( !eqcs_i.isFinished() ){
1075 Node eqc = (*eqcs_i);
1076 //if eqc.getType is string
1077 if (eqc.getType().isString()) {
1078 Trace("strings-process") << "Verify normal forms are the same for " << eqc << std::endl;
1079 std::vector< Node > visited;
1080 std::vector< Node > nf;
1081 std::vector< Node > nf_exp;
1082 normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
1083 if( d_conflict ){
1084 return true;
1085 }else if ( d_pending.empty() && d_lemma_cache.empty() ){
1086 Node nf_term;
1087 if( nf.size()==0 ){
1088 nf_term = d_emptyString;
1089 }else if( nf.size()==1 ) {
1090 nf_term = nf[0];
1091 } else {
1092 nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
1093 }
1094 nf_term = Rewriter::rewrite( nf_term );
1095 Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
1096 Node nf_term_exp = nf_exp.empty() ? NodeManager::currentNM()->mkConst(true) :
1097 nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
1098 if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){
1099 //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
1100 //two equivalence classes have same normal form, merge
1101 Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] );
1102 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
1103 Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl;
1104 //d_equalityEngine.assertEquality( eq, true, eq_exp );
1105 d_pending.push_back( eq );
1106 d_pending_exp[eq] = eq_exp;
1107 d_infer.push_back(eq);
1108 d_infer_exp.push_back(eq_exp);
1109 }else{
1110 nf_to_eqc[nf_term] = eqc;
1111 eqc_to_exp[eqc] = nf_term_exp;
1112 }
1113 }
1114 Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
1115 }
1116 ++eqcs_i;
1117 }
1118 addedFact = !d_pending.empty();
1119 doPendingFacts();
1120 if( !d_conflict ){
1121 for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
1122 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
1123 d_out->lemma( d_lemma_cache[i] );
1124 }
1125 if( !d_lemma_cache.empty() ){
1126 d_lemma_cache.clear();
1127 return true;
1128 }
1129 }
1130 } while (!d_conflict && addedFact);
1131 return false;
1132 }
1133
1134 bool TheoryStrings::checkCardinality() {
1135 int cardinality = options::stringCharCardinality();
1136 Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
1137
1138 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1139 unsigned leqc_counter = 0;
1140 std::map< Node, unsigned > eqc_to_leqc;
1141 std::map< unsigned, Node > leqc_to_eqc;
1142 std::map< unsigned, std::vector< Node > > eqc_to_strings;
1143 while( !eqcs_i.isFinished() ){
1144 Node eqc = (*eqcs_i);
1145 //if eqc.getType is string
1146 if (eqc.getType().isString()) {
1147 EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
1148 Node lt = ei->d_length_term;
1149 if( !lt.isNull() ){
1150 lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
1151 Node r = d_equalityEngine.getRepresentative( lt );
1152 if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
1153 eqc_to_leqc[r] = leqc_counter;
1154 leqc_to_eqc[leqc_counter] = r;
1155 leqc_counter++;
1156 }
1157 eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
1158 }else{
1159 eqc_to_strings[leqc_counter].push_back( eqc );
1160 leqc_counter++;
1161 }
1162 }
1163 ++eqcs_i;
1164 }
1165 for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
1166 Node lr = leqc_to_eqc[it->first];
1167 Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << it->second.size() << std::endl;
1168 // size > c^k
1169 double k = std::log( it->second.size() ) / log((double) cardinality);
1170 unsigned int int_k = (unsigned int)k;
1171 Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
1172 //double c_k = pow ( (double)cardinality, (double)lr );
1173 if( it->second.size() > 1 ) {
1174 bool allDisequal = true;
1175 for( std::vector< Node >::iterator itr1 = it->second.begin();
1176 itr1 != it->second.end(); ++itr1) {
1177 for( std::vector< Node >::iterator itr2 = itr1 + 1;
1178 itr2 != it->second.end(); ++itr2) {
1179 if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) {
1180 allDisequal = false;
1181 // add split lemma
1182 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, *itr1, *itr2 );
1183 Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
1184 Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
1185 Trace("strings-lemma") << "Strings split lemma : " << lemma_or << std::endl;
1186 d_out->lemma(lemma_or);
1187 return true;
1188 }
1189 }
1190 }
1191 if(allDisequal) {
1192 EqcInfo* ei = getOrMakeEqcInfo( lr, true );
1193 Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ei->d_cardinality_lem_k << std::endl;
1194 if( int_k > ei->d_cardinality_lem_k.get() ){
1195 //add cardinality lemma
1196 Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, it->second );
1197 std::vector< Node > vec_node;
1198 vec_node.push_back( dist );
1199 for( std::vector< Node >::iterator itr1 = it->second.begin();
1200 itr1 != it->second.end(); ++itr1) {
1201 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
1202 if( len!=lr ){
1203 Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len );
1204 vec_node.push_back( len_eq_lr );
1205 }
1206 }
1207 Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
1208 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, it->second[0] );
1209 Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node );
1210 Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
1211 Trace("strings-lemma") << "Strings cardinaliry lemma : " << lemma << std::endl;
1212 d_out->lemma(lemma);
1213 ei->d_cardinality_lem_k.set( k );
1214 return true;
1215 }
1216 }
1217 }
1218 }
1219 return false;
1220 }
1221
1222 bool TheoryStrings::checkInductiveEquations() {
1223 bool hasEq = false;
1224 Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl;
1225 for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
1226 Node x = (*it).first;
1227 NodeList* lst1 = (*it).second;
1228 NodeList* lst2 = (*d_ind_map2.find(x)).second;
1229 NodeList* lste = (*d_ind_map_exp.find(x)).second;
1230 NodeList* lstl = (*d_ind_map_lemma.find(x)).second;
1231 NodeList::const_iterator i1 = lst1->begin();
1232 NodeList::const_iterator i2 = lst2->begin();
1233 NodeList::const_iterator ie = lste->begin();
1234 NodeList::const_iterator il = lstl->begin();
1235 while( i1!=lst1->end() ){
1236 Node y = *i1;
1237 Node z = *i2;
1238 Node exp = *ie;
1239 Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << "..." << z << " )* " << y << std::endl;
1240 if( il==lstl->end() ) {
1241 Trace("strings-ind") << "Add length lemma..." << std::endl;
1242 Node lemma_len;
1243 if( y.getKind()!=kind::STRING_CONCAT || z.getKind()!=kind::STRING_CONCAT ) {
1244 Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
1245 Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
1246 lemma_len = NodeManager::currentNM()->mkNode( kind::GEQ, len_x, len_y );
1247 } else {
1248 // both constants
1249 Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
1250 Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" );
1251 Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
1252 Node len_z = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, z );
1253 Node len_y_plus_len_z = NodeManager::currentNM()->mkNode( kind::PLUS, len_y, len_z );
1254 Node y_p_z_t_a = NodeManager::currentNM()->mkNode( kind::MULT, len_y_plus_len_z, sk );
1255 Node y_p_z_t_a_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, y_p_z_t_a, len_y );
1256 lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, y_p_z_t_a_p_y, len_x );
1257 Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero );
1258 lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero );
1259 }
1260 lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len );
1261 Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl;
1262 d_out->lemma(lemma_len);
1263 lstl->push_back( d_true );
1264 return true;
1265 }
1266
1267 ++i1;
1268 ++i2;
1269 ++ie;
1270 ++il;
1271 hasEq = true;
1272 }
1273 }
1274 if( hasEq ){
1275 d_out->setIncomplete();
1276 }
1277 return false;
1278 }
1279
1280
1281
1282
1283 }/* CVC4::theory::strings namespace */
1284 }/* CVC4::theory namespace */
1285 }/* CVC4 namespace */