1 /********************* */
2 /*! \file theory_strings.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tianyi Liang, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
12 ** \brief Implementation of the theory of strings.
14 ** Implementation of the theory of strings.
17 #include "theory/strings/theory_strings.h"
21 #include "expr/kind.h"
22 #include "options/strings_options.h"
23 #include "smt/logic_exception.h"
24 #include "smt/smt_statistics_registry.h"
25 #include "smt/command.h"
26 #include "theory/rewriter.h"
27 #include "theory/strings/theory_strings_rewriter.h"
28 #include "theory/strings/type_enumerator.h"
29 #include "theory/theory_model.h"
30 #include "theory/valuation.h"
31 #include "theory/quantifiers/term_database.h"
34 using namespace CVC4::context
;
40 Node
TheoryStrings::TermIndex::add( Node n
, unsigned index
, TheoryStrings
* t
, Node er
, std::vector
< Node
>& c
) {
41 if( index
==n
.getNumChildren() ){
42 if( d_data
.isNull() ){
47 Assert( index
<n
.getNumChildren() );
48 Node nir
= t
->getRepresentative( n
[index
] );
49 //if it is empty, and doing CONCAT, ignore
50 if( nir
==er
&& n
.getKind()==kind::STRING_CONCAT
){
51 return add( n
, index
+1, t
, er
, c
);
54 return d_children
[nir
].add( n
, index
+1, t
, er
, c
);
60 TheoryStrings::TheoryStrings(context::Context
* c
, context::UserContext
* u
,
61 OutputChannel
& out
, Valuation valuation
,
62 const LogicInfo
& logicInfo
)
63 : Theory(THEORY_STRINGS
, c
, u
, out
, valuation
, logicInfo
),
66 d_equalityEngine(d_notify
, c
, "theory::strings::TheoryStrings", true),
72 d_length_intro_vars(u
),
73 d_pregistered_terms_cache(u
),
74 d_registered_terms_cache(u
),
77 d_extf_infer_cache(c
),
78 d_ee_disequalities(c
),
81 d_proxy_var_to_length(u
),
87 d_regexp_memberships(c
),
94 d_processed_memberships(c
),
98 d_cardinality_lits(u
),
99 d_curr_cardinality(c
, 0)
101 // The kinds we are treating as function application in congruence
102 d_equalityEngine
.addFunctionKind(kind::STRING_IN_REGEXP
);
103 d_equalityEngine
.addFunctionKind(kind::STRING_LENGTH
);
104 d_equalityEngine
.addFunctionKind(kind::STRING_CONCAT
);
105 d_equalityEngine
.addFunctionKind(kind::STRING_STRCTN
);
106 d_equalityEngine
.addFunctionKind(kind::STRING_SUBSTR
);
107 d_equalityEngine
.addFunctionKind(kind::STRING_ITOS
);
108 d_equalityEngine
.addFunctionKind(kind::STRING_STOI
);
109 if( options::stringLazyPreproc() ){
110 d_equalityEngine
.addFunctionKind(kind::STRING_U16TOS
);
111 d_equalityEngine
.addFunctionKind(kind::STRING_STOU16
);
112 d_equalityEngine
.addFunctionKind(kind::STRING_U32TOS
);
113 d_equalityEngine
.addFunctionKind(kind::STRING_STOU32
);
114 d_equalityEngine
.addFunctionKind(kind::STRING_STRIDOF
);
115 d_equalityEngine
.addFunctionKind(kind::STRING_STRREPL
);
118 d_zero
= NodeManager::currentNM()->mkConst( Rational( 0 ) );
119 d_one
= NodeManager::currentNM()->mkConst( Rational( 1 ) );
120 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
121 std::vector
< Node
> nvec
;
122 d_emptyRegexp
= NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY
, nvec
);
123 d_true
= NodeManager::currentNM()->mkConst( true );
124 d_false
= NodeManager::currentNM()->mkConst( false );
129 TheoryStrings::~TheoryStrings() {
133 Node
TheoryStrings::getRepresentative( Node t
) {
134 if( d_equalityEngine
.hasTerm( t
) ){
135 return d_equalityEngine
.getRepresentative( t
);
141 bool TheoryStrings::hasTerm( Node a
){
142 return d_equalityEngine
.hasTerm( a
);
145 bool TheoryStrings::areEqual( Node a
, Node b
){
148 }else if( hasTerm( a
) && hasTerm( b
) ){
149 return d_equalityEngine
.areEqual( a
, b
);
155 bool TheoryStrings::areDisequal( Node a
, Node b
){
159 if( a
.getType().isString() ) {
160 for( unsigned i
=0; i
<2; i
++ ) {
161 Node ac
= a
.getKind()==kind::STRING_CONCAT
? a
[i
==0 ? 0 : a
.getNumChildren()-1] : a
;
162 Node bc
= b
.getKind()==kind::STRING_CONCAT
? b
[i
==0 ? 0 : b
.getNumChildren()-1] : b
;
163 if( ac
.isConst() && bc
.isConst() ){
164 CVC4::String as
= ac
.getConst
<String
>();
165 CVC4::String bs
= bc
.getConst
<String
>();
166 int slen
= as
.size() > bs
.size() ? bs
.size() : as
.size();
167 bool flag
= i
== 1 ? as
.rstrncmp(bs
, slen
): as
.strncmp(bs
, slen
);
174 if( hasTerm( a
) && hasTerm( b
) ) {
175 if( d_equalityEngine
.areDisequal( a
, b
, false ) ){
183 Node
TheoryStrings::getLengthExp( Node t
, std::vector
< Node
>& exp
, Node te
){
184 Assert( areEqual( t
, te
) );
185 Node lt
= mkLength( te
);
187 // use own length if it exists, leads to shorter explanation
190 EqcInfo
* ei
= getOrMakeEqcInfo( t
, false );
191 Node length_term
= ei
? ei
->d_length_term
: Node::null();
192 if( length_term
.isNull() ){
193 //typically shouldnt be necessary
196 Debug("strings") << "TheoryStrings::getLengthTerm " << t
<< " is " << length_term
<< std::endl
;
197 addToExplanation( length_term
, te
, exp
);
198 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, length_term
) );
202 Node
TheoryStrings::getLength( Node t
, std::vector
< Node
>& exp
) {
203 return getLengthExp( t
, exp
, t
);
206 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
207 d_equalityEngine
.setMasterEqualityEngine(eq
);
210 void TheoryStrings::addSharedTerm(TNode t
) {
211 Debug("strings") << "TheoryStrings::addSharedTerm(): "
212 << t
<< " " << t
.getType().isBoolean() << endl
;
213 d_equalityEngine
.addTriggerTerm(t
, THEORY_STRINGS
);
214 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl
;
217 EqualityStatus
TheoryStrings::getEqualityStatus(TNode a
, TNode b
) {
218 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
219 if (d_equalityEngine
.areEqual(a
, b
)) {
220 // The terms are implied to be equal
221 return EQUALITY_TRUE
;
223 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
224 // The terms are implied to be dis-equal
225 return EQUALITY_FALSE
;
228 return EQUALITY_UNKNOWN
;
231 void TheoryStrings::propagate(Effort e
) {
232 // direct propagation now
235 bool TheoryStrings::propagate(TNode literal
) {
236 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< ")" << std::endl
;
237 // If already in conflict, no more propagation
239 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< "): already in conflict" << std::endl
;
243 bool ok
= d_out
->propagate(literal
);
251 void TheoryStrings::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
252 Debug("strings-explain") << "Explain " << literal
<< " " << d_conflict
<< std::endl
;
253 bool polarity
= literal
.getKind() != kind::NOT
;
254 TNode atom
= polarity
? literal
: literal
[0];
255 unsigned ps
= assumptions
.size();
256 std::vector
< TNode
> tassumptions
;
257 if (atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
258 if( atom
[0]!=atom
[1] ){
259 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, tassumptions
);
262 d_equalityEngine
.explainPredicate(atom
, polarity
, tassumptions
);
264 for( unsigned i
=0; i
<tassumptions
.size(); i
++ ){
265 if( std::find( assumptions
.begin(), assumptions
.end(), tassumptions
[i
] )==assumptions
.end() ){
266 assumptions
.push_back( tassumptions
[i
] );
269 Debug("strings-explain-debug") << "Explanation for " << literal
<< " was " << std::endl
;
270 for( unsigned i
=ps
; i
<assumptions
.size(); i
++ ){
271 Debug("strings-explain-debug") << " " << assumptions
[i
] << std::endl
;
275 Node
TheoryStrings::explain( TNode literal
){
276 std::vector
< TNode
> assumptions
;
277 explain( literal
, assumptions
);
278 if( assumptions
.empty() ){
280 }else if( assumptions
.size()==1 ){
281 return assumptions
[0];
283 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
287 /////////////////////////////////////////////////////////////////////////////
289 /////////////////////////////////////////////////////////////////////////////
292 void TheoryStrings::presolve() {
293 Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl
;
295 if(!options::stdASCII()) {
301 /////////////////////////////////////////////////////////////////////////////
303 /////////////////////////////////////////////////////////////////////////////
306 void TheoryStrings::collectModelInfo( TheoryModel
* m
, bool fullModel
) {
307 Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel
<< std::endl
;
308 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl
;
309 m
->assertEqualityEngine( &d_equalityEngine
);
311 std::vector
< Node
> nodes
;
312 getEquivalenceClasses( nodes
);
313 std::map
< Node
, Node
> processed
;
314 std::vector
< std::vector
< Node
> > col
;
315 std::vector
< Node
> lts
;
316 separateByLength( nodes
, col
, lts
);
317 //step 1 : get all values for known lengths
318 std::vector
< Node
> lts_values
;
319 std::map
< unsigned, bool > values_used
;
320 for( unsigned i
=0; i
<col
.size(); i
++ ) {
321 Trace("strings-model") << "Checking length for {";
322 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
324 Trace("strings-model") << ", ";
326 Trace("strings-model") << col
[i
][j
];
328 Trace("strings-model") << " } (length is " << lts
[i
] << ")" << std::endl
;
329 if( lts
[i
].isConst() ) {
330 lts_values
.push_back( lts
[i
] );
331 Assert(lts
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
332 unsigned lvalue
= lts
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt();
333 values_used
[ lvalue
] = true;
335 //get value for lts[i];
336 if( !lts
[i
].isNull() ){
337 Node v
= d_valuation
.getModelValue(lts
[i
]);
338 Trace("strings-model") << "Model value for " << lts
[i
] << " is " << v
<< std::endl
;
339 lts_values
.push_back( v
);
340 Assert(v
.getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
341 unsigned lvalue
= v
.getConst
<Rational
>().getNumerator().toUnsignedInt();
342 values_used
[ lvalue
] = true;
344 //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
346 lts_values
.push_back( Node::null() );
350 ////step 2 : assign arbitrary values for unknown lengths?
351 // confirmed by calculus invariant, see paper
352 Trace("strings-model") << "Assign to equivalence classes..." << std::endl
;
353 //step 3 : assign values to equivalence classes that are pure variables
354 for( unsigned i
=0; i
<col
.size(); i
++ ){
355 std::vector
< Node
> pure_eq
;
356 Trace("strings-model") << "The equivalence classes ";
357 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
358 Trace("strings-model") << col
[i
][j
] << " ";
359 //check if col[i][j] has only variables
360 EqcInfo
* ei
= getOrMakeEqcInfo( col
[i
][j
], false );
361 Node cst
= ei
? ei
->d_const_term
: Node::null();
363 Assert( d_normal_forms
.find( col
[i
][j
] )!=d_normal_forms
.end() );
364 if( d_normal_forms
[col
[i
][j
]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
365 pure_eq
.push_back( col
[i
][j
] );
368 processed
[col
[i
][j
]] = cst
;
371 Trace("strings-model") << "have length " << lts_values
[i
] << std::endl
;
373 //assign a new length if necessary
374 if( !pure_eq
.empty() ){
375 if( lts_values
[i
].isNull() ){
377 while( values_used
.find( lvalue
)!=values_used
.end() ){
380 Trace("strings-model") << "*** Decide to make length of " << lvalue
<< std::endl
;
381 lts_values
[i
] = NodeManager::currentNM()->mkConst( Rational( lvalue
) );
382 values_used
[ lvalue
] = true;
384 Trace("strings-model") << "Need to assign values of length " << lts_values
[i
] << " to equivalence classes ";
385 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
386 Trace("strings-model") << pure_eq
[j
] << " ";
388 Trace("strings-model") << std::endl
;
391 //use type enumerator
392 Assert(lts_values
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
393 StringEnumeratorLength
sel(lts_values
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt());
394 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
395 Assert( !sel
.isFinished() );
397 while( d_equalityEngine
.hasTerm( c
) ){
399 Assert( !sel
.isFinished() );
403 Trace("strings-model") << "*** Assigned constant " << c
<< " for " << pure_eq
[j
] << std::endl
;
404 processed
[pure_eq
[j
]] = c
;
405 m
->assertEquality( pure_eq
[j
], c
, true );
409 Trace("strings-model") << "String Model : Pure Assigned." << std::endl
;
410 //step 4 : assign constants to all other equivalence classes
411 for( unsigned i
=0; i
<nodes
.size(); i
++ ){
412 if( processed
.find( nodes
[i
] )==processed
.end() ){
413 Assert( d_normal_forms
.find( nodes
[i
] )!=d_normal_forms
.end() );
414 Trace("strings-model") << "Construct model for " << nodes
[i
] << " based on normal form ";
415 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
416 if( j
>0 ) Trace("strings-model") << " ++ ";
417 Trace("strings-model") << d_normal_forms
[nodes
[i
]][j
];
418 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
419 if( !r
.isConst() && processed
.find( r
)==processed
.end() ){
420 Trace("strings-model") << "(UNPROCESSED)";
423 Trace("strings-model") << std::endl
;
424 std::vector
< Node
> nc
;
425 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
426 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
427 Assert( r
.isConst() || processed
.find( r
)!=processed
.end() );
428 nc
.push_back(r
.isConst() ? r
: processed
[r
]);
430 Node cc
= mkConcat( nc
);
431 Assert( cc
.getKind()==kind::CONST_STRING
);
432 Trace("strings-model") << "*** Determined constant " << cc
<< " for " << nodes
[i
] << std::endl
;
433 processed
[nodes
[i
]] = cc
;
434 m
->assertEquality( nodes
[i
], cc
, true );
437 //Trace("strings-model") << "String Model : Assigned." << std::endl;
438 Trace("strings-model") << "String Model : Finished." << std::endl
;
441 /////////////////////////////////////////////////////////////////////////////
443 /////////////////////////////////////////////////////////////////////////////
446 void TheoryStrings::preRegisterTerm(TNode n
) {
447 if( d_pregistered_terms_cache
.find(n
) == d_pregistered_terms_cache
.end() ) {
448 d_pregistered_terms_cache
.insert(n
);
449 //check for logic exceptions
450 if( !options::stringExp() ){
451 if( n
.getKind()==kind::STRING_STRIDOF
||
452 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
453 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
454 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
455 std::stringstream ss
;
456 ss
<< "Term of kind " << n
.getKind() << " not supported in default mode, try --strings-exp";
457 throw LogicException(ss
.str());
460 switch( n
.getKind() ) {
462 d_equalityEngine
.addTriggerEquality(n
);
465 case kind::STRING_IN_REGEXP
: {
466 d_out
->requirePhase(n
, true);
467 d_equalityEngine
.addTriggerPredicate(n
);
468 d_equalityEngine
.addTerm(n
[0]);
469 d_equalityEngine
.addTerm(n
[1]);
473 TypeNode tn
= n
.getType();
474 if( tn
.isString() ) {
475 registerTerm( n
, 0 );
477 if( n
.getKind() == kind::VARIABLE
&& options::stringFMF() ){
478 d_input_vars
.insert(n
);
480 d_equalityEngine
.addTerm(n
);
481 } else if (tn
.isBoolean()) {
482 // Get triggered for both equal and dis-equal
483 d_equalityEngine
.addTriggerPredicate(n
);
485 // Function applications/predicates
486 d_equalityEngine
.addTerm(n
);
487 if( options::stringExp() ){
488 //collect extended functions here: some may not be asserted to strings (such as those with return type Int),
489 // but we need to record them so they are treated properly
490 std::map
< Node
, bool > visited
;
491 collectExtendedFuncTerms( n
, visited
);
494 //concat terms do not contribute to theory combination? TODO: verify
495 if( n
.hasOperator() && kindToTheoryId( n
.getKind() )==THEORY_STRINGS
&& n
.getKind()!=kind::STRING_CONCAT
){
496 d_functionsTerms
.push_back( n
);
503 Node
TheoryStrings::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
504 Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node
<< std::endl
;
509 void TheoryStrings::check(Effort e
) {
510 if (done() && !fullEffort(e
)) {
514 TimerStat::CodeTimer
checkTimer(d_checkTime
);
519 /*if(getLogicInfo().hasEverything()) {
520 WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n"
521 << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl;
525 if( !done() && !hasTerm( d_emptyString
) ) {
526 preRegisterTerm( d_emptyString
);
529 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
530 Trace("strings-check") << "Theory of strings, check : " << e
<< std::endl
;
531 while ( !done() && !d_conflict
) {
532 // Get all the assertions
533 Assertion assertion
= get();
534 TNode fact
= assertion
.assertion
;
536 Trace("strings-assertion") << "get assertion: " << fact
<< endl
;
537 polarity
= fact
.getKind() != kind::NOT
;
538 atom
= polarity
? fact
: fact
[0];
540 //run preprocess on memberships
541 if( options::stringLazyPreproc() ){
542 checkReduction( atom
, polarity
? 1 : -1, 0 );
545 //assert pending fact
546 assertPendingFact( atom
, polarity
, fact
);
550 if( !d_conflict
&& ( ( e
== EFFORT_FULL
&& !d_valuation
.needCheck() ) || ( e
==EFFORT_STANDARD
&& options::stringEager() ) ) ) {
551 Trace("strings-check") << "Theory of strings full effort check " << std::endl
;
553 if(Trace
.isOn("strings-eqc")) {
554 for( unsigned t
=0; t
<2; t
++ ) {
555 eq::EqClassesIterator eqcs2_i
= eq::EqClassesIterator( &d_equalityEngine
);
556 Trace("strings-eqc") << (t
==0 ? "STRINGS:" : "OTHER:") << std::endl
;
557 while( !eqcs2_i
.isFinished() ){
558 Node eqc
= (*eqcs2_i
);
559 bool print
= (t
==0 && eqc
.getType().isString() ) || (t
==1 && !eqc
.getType().isString() );
561 eq::EqClassIterator eqc2_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
562 Trace("strings-eqc") << "Eqc( " << eqc
<< " ) : { ";
563 while( !eqc2_i
.isFinished() ) {
564 if( (*eqc2_i
)!=eqc
&& (*eqc2_i
).getKind()!=kind::EQUAL
){
565 Trace("strings-eqc") << (*eqc2_i
) << " ";
569 Trace("strings-eqc") << " } " << std::endl
;
570 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
572 Trace("strings-eqc-debug") << "* Length term : " << ei
->d_length_term
.get() << std::endl
;
573 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei
->d_cardinality_lem_k
.get() << std::endl
;
574 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei
->d_normalized_length
.get() << std::endl
;
579 Trace("strings-eqc") << std::endl
;
581 Trace("strings-eqc") << std::endl
;
584 bool addedLemma
= false;
587 Trace("strings-process") << "----check, next round---" << std::endl
;
589 Trace("strings-process") << "Done check init, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
590 if( !hasProcessed() ){
591 checkExtendedFuncsEval();
592 Trace("strings-process") << "Done check extended functions eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
593 if( !hasProcessed() ){
595 Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
596 if( !hasProcessed() && e
==EFFORT_FULL
){
598 Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
599 if( !hasProcessed() ){
600 if( options::stringEagerLen() ){
602 Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
604 if( !hasProcessed() ){
605 checkExtendedFuncs();
606 Trace("strings-process") << "Done check extended functions, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
607 if( !hasProcessed() ){
609 Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
617 addedFact
= !d_pending
.empty();
618 addedLemma
= !d_lemma_cache
.empty();
621 }while( !d_conflict
&& !addedLemma
&& addedFact
);
623 Trace("strings-check") << "Theory of strings done full effort check " << addedLemma
<< " " << d_conflict
<< std::endl
;
625 Trace("strings-check") << "Theory of strings, done check : " << e
<< std::endl
;
626 Assert( d_pending
.empty() );
627 Assert( d_lemma_cache
.empty() );
630 void TheoryStrings::checkExtfReduction( int effort
) {
631 Trace("strings-process-debug") << "Checking preprocess at effort " << effort
<< ", #to process=" << d_ext_func_terms
.size() << "..." << std::endl
;
632 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
633 Trace("strings-process-debug2") << (*it
).first
<< ", active=" << !(*it
).second
<< std::endl
;
635 Node n
= (*it
).first
;
636 checkReduction( n
, d_extf_pol
[n
], effort
);
637 if( hasProcessed() ){
644 void TheoryStrings::checkReduction( Node atom
, int pol
, int effort
) {
645 //determine the effort level to process the extf at
646 // 0 - at assertion time, 1+ - after no other reduction is applicable
648 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
649 if( pol
==1 && atom
[1].getKind()==kind::REGEXP_RANGE
){
652 }else if( atom
.getKind()==kind::STRING_STRCTN
){
657 if( options::stringLazyPreproc() ){
658 if( atom
.getKind()==kind::STRING_SUBSTR
){
659 r_effort
= options::stringLazyPreproc2() ? 1 : 0;
661 r_effort
= options::stringLazyPreproc2() ? 2 : 0;
665 if( effort
==r_effort
){
666 if( d_preproc_cache
.find( atom
)==d_preproc_cache
.end() ){
667 d_preproc_cache
[ atom
] = true;
668 Trace("strings-process-debug") << "Process reduction for " << atom
<< std::endl
;
669 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
670 if( atom
[1].getKind()==kind::REGEXP_RANGE
){
671 Node eq
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, atom
[0]));
672 std::vector
< Node
> exp_vec
;
673 exp_vec
.push_back( atom
);
674 sendInference( d_empty_vec
, exp_vec
, eq
, "RE-Range-Len", true );
676 }else if( atom
.getKind()==kind::STRING_STRCTN
){
679 //would have already reduced by now
680 Assert( !areEqual( s
, d_emptyString
) && !areEqual( s
, x
) );
681 Node sk1
= mkSkolemCached( x
, s
, sk_id_ctn_pre
, "sc1" );
682 Node sk2
= mkSkolemCached( x
, s
, sk_id_ctn_post
, "sc2" );
683 Node eq
= Rewriter::rewrite( x
.eqNode( mkConcat( sk1
, s
, sk2
) ) );
684 std::vector
< Node
> exp_vec
;
685 exp_vec
.push_back( atom
);
686 sendInference( d_empty_vec
, exp_vec
, eq
, "POS-CTN", true );
688 // for STRING_SUBSTR,
689 // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
690 std::vector
< Node
> new_nodes
;
691 Node res
= d_preproc
.decompose( atom
, new_nodes
);
693 if( !new_nodes
.empty() ){
694 Node nnlem
= new_nodes
.size()==1 ? new_nodes
[0] : NodeManager::currentNM()->mkNode( kind::AND
, new_nodes
);
695 nnlem
= Rewriter::rewrite( nnlem
);
696 Trace("strings-red-lemma") << "Reduction_" << effort
<< " lemma : " << nnlem
<< std::endl
;
697 Trace("strings-red-lemma") << "...from " << atom
<< std::endl
;
698 sendInference( d_empty_vec
, nnlem
, "Reduction", true );
705 TheoryStrings::EqcInfo::EqcInfo( context::Context
* c
) : d_const_term(c
), d_length_term(c
), d_cardinality_lem_k(c
), d_normalized_length(c
) {
709 TheoryStrings::EqcInfo
* TheoryStrings::getOrMakeEqcInfo( Node eqc
, bool doMake
) {
710 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( eqc
);
711 if( eqc_i
==d_eqc_info
.end() ){
713 EqcInfo
* ei
= new EqcInfo( getSatContext() );
714 d_eqc_info
[eqc
] = ei
;
720 return (*eqc_i
).second
;
725 /** Conflict when merging two constants */
726 void TheoryStrings::conflict(TNode a
, TNode b
){
728 Debug("strings-conflict") << "Making conflict..." << std::endl
;
731 if (a
.getKind() == kind::CONST_BOOLEAN
) {
732 conflictNode
= explain( a
.iffNode(b
) );
734 conflictNode
= explain( a
.eqNode(b
) );
736 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode
<< std::endl
;
737 d_out
->conflict( conflictNode
);
741 /** called when a new equivalance class is created */
742 void TheoryStrings::eqNotifyNewClass(TNode t
){
743 if( t
.getKind() == kind::CONST_STRING
){
744 EqcInfo
* ei
=getOrMakeEqcInfo( t
, true );
745 ei
->d_const_term
= t
;
747 if( t
.getKind() == kind::STRING_LENGTH
){
748 Trace("strings-debug") << "New length eqc : " << t
<< std::endl
;
749 Node r
= d_equalityEngine
.getRepresentative(t
[0]);
750 EqcInfo
* ei
= getOrMakeEqcInfo( r
, true );
751 ei
->d_length_term
= t
[0];
752 //we care about the length of this string
753 registerTerm( t
[0], 1 );
757 /** called when two equivalance classes will merge */
758 void TheoryStrings::eqNotifyPreMerge(TNode t1
, TNode t2
){
759 EqcInfo
* e2
= getOrMakeEqcInfo(t2
, false);
761 EqcInfo
* e1
= getOrMakeEqcInfo( t1
);
762 //add information from e2 to e1
763 if( !e2
->d_const_term
.get().isNull() ){
764 e1
->d_const_term
.set( e2
->d_const_term
);
766 if( !e2
->d_length_term
.get().isNull() ){
767 e1
->d_length_term
.set( e2
->d_length_term
);
769 if( e2
->d_cardinality_lem_k
.get()>e1
->d_cardinality_lem_k
.get() ) {
770 e1
->d_cardinality_lem_k
.set( e2
->d_cardinality_lem_k
);
772 if( !e2
->d_normalized_length
.get().isNull() ){
773 e1
->d_normalized_length
.set( e2
->d_normalized_length
);
778 /** called when two equivalance classes have merged */
779 void TheoryStrings::eqNotifyPostMerge(TNode t1
, TNode t2
) {
783 /** called when two equivalance classes are disequal */
784 void TheoryStrings::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
785 if( t1
.getType().isString() ){
786 //store disequalities between strings, may need to check if their lengths are equal/disequal
787 d_ee_disequalities
.push_back( t1
.eqNode( t2
) );
791 void TheoryStrings::addCarePairs( quantifiers::TermArgTrie
* t1
, quantifiers::TermArgTrie
* t2
, unsigned arity
, unsigned depth
) {
794 Node f1
= t1
->getNodeData();
795 Node f2
= t2
->getNodeData();
796 if( !d_equalityEngine
.areEqual( f1
, f2
) ){
797 Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1
<< " and " << f2
<< std::endl
;
798 vector
< pair
<TNode
, TNode
> > currentPairs
;
799 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++ k
) {
802 Assert( d_equalityEngine
.hasTerm(x
) );
803 Assert( d_equalityEngine
.hasTerm(y
) );
804 Assert( !d_equalityEngine
.areDisequal( x
, y
, false ) );
805 if( !d_equalityEngine
.areEqual( x
, y
) ){
806 if( d_equalityEngine
.isTriggerTerm(x
, THEORY_STRINGS
) && d_equalityEngine
.isTriggerTerm(y
, THEORY_STRINGS
) ){
807 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_STRINGS
);
808 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_STRINGS
);
809 EqualityStatus eqStatus
= d_valuation
.getEqualityStatus(x_shared
, y_shared
);
810 if( eqStatus
==EQUALITY_FALSE_AND_PROPAGATED
|| eqStatus
==EQUALITY_FALSE
|| eqStatus
==EQUALITY_FALSE_IN_MODEL
){
811 //an argument is disequal, we are done
814 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
819 for (unsigned c
= 0; c
< currentPairs
.size(); ++ c
) {
820 Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs
[c
].first
<< " " << currentPairs
[c
].second
<< std::endl
;
821 Trace("ajr-temp") << currentPairs
[c
].first
<< ", " << currentPairs
[c
].second
<< std::endl
;
822 addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
828 if( depth
<(arity
-1) ){
829 //add care pairs internal to each child
830 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
831 addCarePairs( &it
->second
, NULL
, arity
, depth
+1 );
834 //add care pairs based on each pair of non-disequal arguments
835 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
836 std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it2
= it
;
838 for( ; it2
!= t1
->d_data
.end(); ++it2
){
839 if( !d_equalityEngine
.areDisequal(it
->first
, it2
->first
, false) ){
840 addCarePairs( &it
->second
, &it2
->second
, arity
, depth
+1 );
845 //add care pairs based on product of indices, non-disequal arguments
846 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
847 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it2
= t2
->d_data
.begin(); it2
!= t2
->d_data
.end(); ++it2
){
848 if( !d_equalityEngine
.areDisequal(it
->first
, it2
->first
, false) ){
849 addCarePairs( &it
->second
, &it2
->second
, arity
, depth
+1 );
857 void TheoryStrings::computeCareGraph(){
858 //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
859 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl
;
860 std::map
< Node
, quantifiers::TermArgTrie
> index
;
861 std::map
< Node
, unsigned > arity
;
862 unsigned functionTerms
= d_functionsTerms
.size();
863 for (unsigned i
= 0; i
< functionTerms
; ++ i
) {
864 TNode f1
= d_functionsTerms
[i
];
865 Trace("strings-cg") << "...build for " << f1
<< std::endl
;
866 Node op
= f1
.getOperator();
867 std::vector
< TNode
> reps
;
868 bool has_trigger_arg
= false;
869 for( unsigned j
=0; j
<f1
.getNumChildren(); j
++ ){
870 reps
.push_back( d_equalityEngine
.getRepresentative( f1
[j
] ) );
871 if( d_equalityEngine
.isTriggerTerm( f1
[j
], THEORY_STRINGS
) ){
872 has_trigger_arg
= true;
875 if( has_trigger_arg
){
876 index
[op
].addTerm( f1
, reps
);
877 arity
[op
] = reps
.size();
881 for( std::map
< Node
, quantifiers::TermArgTrie
>::iterator itii
= index
.begin(); itii
!= index
.end(); ++itii
){
882 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii
->first
<< "..." << std::endl
;
883 addCarePairs( &itii
->second
, NULL
, arity
[ itii
->first
], 0 );
887 void TheoryStrings::assertPendingFact(Node atom
, bool polarity
, Node exp
) {
888 Trace("strings-pending") << "Assert pending fact : " << atom
<< " " << polarity
<< " from " << exp
<< std::endl
;
889 Assert(atom
.getKind() != kind::OR
, "Infer error: a split.");
890 if( atom
.getKind()==kind::EQUAL
){
891 Trace("strings-pending-debug") << " Register term" << std::endl
;
892 for( unsigned j
=0; j
<2; j
++ ) {
893 if( !d_equalityEngine
.hasTerm( atom
[j
] ) && atom
[j
].getType().isString() ) {
894 registerTerm( atom
[j
], 0 );
897 Trace("strings-pending-debug") << " Now assert equality" << std::endl
;
898 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
899 Trace("strings-pending-debug") << " Finished assert equality" << std::endl
;
901 if( atom
.getKind()==kind::STRING_IN_REGEXP
) {
902 if( d_ext_func_terms
.find( atom
)==d_ext_func_terms
.end() ){
903 Trace("strings-extf-debug") << "Found extended function (membership) : " << atom
<< std::endl
;
904 d_ext_func_terms
[atom
] = true;
907 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
909 Trace("strings-pending-debug") << " Now collect terms" << std::endl
;
910 //collect extended function terms in the atom
911 std::map
< Node
, bool > visited
;
912 collectExtendedFuncTerms( atom
, visited
);
913 Trace("strings-pending-debug") << " Finished collect terms" << std::endl
;
916 void TheoryStrings::doPendingFacts() {
918 while( !d_conflict
&& i
<d_pending
.size() ) {
919 Node fact
= d_pending
[i
];
920 Node exp
= d_pending_exp
[ fact
];
921 if(fact
.getKind() == kind::AND
) {
922 for(size_t j
=0; j
<fact
.getNumChildren(); j
++) {
923 bool polarity
= fact
[j
].getKind() != kind::NOT
;
924 TNode atom
= polarity
? fact
[j
] : fact
[j
][0];
925 assertPendingFact(atom
, polarity
, exp
);
928 bool polarity
= fact
.getKind() != kind::NOT
;
929 TNode atom
= polarity
? fact
: fact
[0];
930 assertPendingFact(atom
, polarity
, exp
);
935 d_pending_exp
.clear();
938 void TheoryStrings::doPendingLemmas() {
939 if( !d_conflict
&& !d_lemma_cache
.empty() ){
940 for( unsigned i
=0; i
<d_lemma_cache
.size(); i
++ ){
941 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache
[i
] << std::endl
;
942 d_out
->lemma( d_lemma_cache
[i
] );
944 for( std::map
< Node
, bool >::iterator it
= d_pending_req_phase
.begin(); it
!= d_pending_req_phase
.end(); ++it
){
945 Trace("strings-pending") << "Require phase : " << it
->first
<< ", polarity = " << it
->second
<< std::endl
;
946 d_out
->requirePhase( it
->first
, it
->second
);
949 d_lemma_cache
.clear();
950 d_pending_req_phase
.clear();
953 bool TheoryStrings::hasProcessed() {
954 return d_conflict
|| !d_lemma_cache
.empty() || !d_pending
.empty();
957 void TheoryStrings::addToExplanation( Node a
, Node b
, std::vector
< Node
>& exp
) {
959 Debug("strings-explain") << "Add to explanation : " << a
<< " == " << b
<< std::endl
;
960 Assert( areEqual( a
, b
) );
961 exp
.push_back( a
.eqNode( b
) );
965 void TheoryStrings::addToExplanation( Node lit
, std::vector
< Node
>& exp
) {
967 exp
.push_back( lit
);
971 void TheoryStrings::checkInit() {
973 d_eqc_to_const
.clear();
974 d_eqc_to_const_base
.clear();
975 d_eqc_to_const_exp
.clear();
976 d_eqc_to_len_term
.clear();
977 d_term_index
.clear();
978 d_strings_eqc
.clear();
980 std::map
< Kind
, unsigned > ncongruent
;
981 std::map
< Kind
, unsigned > congruent
;
982 d_emptyString_r
= getRepresentative( d_emptyString
);
983 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
984 while( !eqcs_i
.isFinished() ){
985 Node eqc
= (*eqcs_i
);
986 TypeNode tn
= eqc
.getType();
987 if( !tn
.isRegExp() ){
989 d_strings_eqc
.push_back( eqc
);
992 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
993 while( !eqc_i
.isFinished() ) {
995 if( tn
.isInteger() ){
996 if( n
.getKind()==kind::STRING_LENGTH
){
997 Node nr
= getRepresentative( n
[0] );
998 d_eqc_to_len_term
[nr
] = n
[0];
1000 }else if( n
.isConst() ){
1001 d_eqc_to_const
[eqc
] = n
;
1002 d_eqc_to_const_base
[eqc
] = n
;
1003 d_eqc_to_const_exp
[eqc
] = Node::null();
1004 }else if( n
.getNumChildren()>0 ){
1005 Kind k
= n
.getKind();
1006 if( k
!=kind::EQUAL
){
1007 if( d_congruent
.find( n
)==d_congruent
.end() ){
1008 std::vector
< Node
> c
;
1009 Node nc
= d_term_index
[k
].add( n
, 0, this, d_emptyString_r
, c
);
1011 //check if we have inferred a new equality by removal of empty components
1012 if( n
.getKind()==kind::STRING_CONCAT
&& !areEqual( nc
, n
) ){
1013 std::vector
< Node
> exp
;
1014 unsigned count
[2] = { 0, 0 };
1015 while( count
[0]<nc
.getNumChildren() || count
[1]<n
.getNumChildren() ){
1016 //explain empty prefixes
1017 for( unsigned t
=0; t
<2; t
++ ){
1018 Node nn
= t
==0 ? nc
: n
;
1019 while( count
[t
]<nn
.getNumChildren() &&
1020 ( nn
[count
[t
]]==d_emptyString
|| areEqual( nn
[count
[t
]], d_emptyString
) ) ){
1021 if( nn
[count
[t
]]!=d_emptyString
){
1022 exp
.push_back( nn
[count
[t
]].eqNode( d_emptyString
) );
1027 //explain equal components
1028 if( count
[0]<nc
.getNumChildren() ){
1029 Assert( count
[1]<n
.getNumChildren() );
1030 if( nc
[count
[0]]!=n
[count
[1]] ){
1031 exp
.push_back( nc
[count
[0]].eqNode( n
[count
[1]] ) );
1037 //infer the equality
1038 sendInference( exp
, n
.eqNode( nc
), "I_Norm" );
1040 //update the extf map : only process if neither has been reduced
1041 NodeBoolMap::const_iterator it
= d_ext_func_terms
.find( n
);
1042 if( it
!=d_ext_func_terms
.end() ){
1043 if( d_ext_func_terms
.find( nc
)==d_ext_func_terms
.end() ){
1044 d_ext_func_terms
[nc
] = (*it
).second
;
1046 d_ext_func_terms
[nc
] = d_ext_func_terms
[nc
] && (*it
).second
;
1048 d_ext_func_terms
[n
] = false;
1051 //this node is congruent to another one, we can ignore it
1052 Trace("strings-process-debug") << " congruent term : " << n
<< std::endl
;
1053 d_congruent
.insert( n
);
1055 }else if( k
==kind::STRING_CONCAT
&& c
.size()==1 ){
1056 Trace("strings-process-debug") << " congruent term by singular : " << n
<< " " << c
[0] << std::endl
;
1058 if( !areEqual( c
[0], n
) ){
1059 std::vector
< Node
> exp
;
1060 //explain empty components
1061 bool foundNEmpty
= false;
1062 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1063 if( areEqual( n
[i
], d_emptyString
) ){
1064 if( n
[i
]!=d_emptyString
){
1065 exp
.push_back( n
[i
].eqNode( d_emptyString
) );
1068 Assert( !foundNEmpty
);
1070 exp
.push_back( n
[i
].eqNode( c
[0] ) );
1075 AlwaysAssert( foundNEmpty
);
1076 //infer the equality
1077 sendInference( exp
, n
.eqNode( c
[0] ), "I_Norm_S" );
1079 d_congruent
.insert( n
);
1089 if( d_congruent
.find( n
)==d_congruent
.end() ){
1093 Trace("strings-process-debug") << " congruent variable : " << n
<< std::endl
;
1094 d_congruent
.insert( n
);
1103 if( Trace
.isOn("strings-process") ){
1104 for( std::map
< Kind
, TermIndex
>::iterator it
= d_term_index
.begin(); it
!= d_term_index
.end(); ++it
){
1105 Trace("strings-process") << " Terms[" << it
->first
<< "] = " << ncongruent
[it
->first
] << "/" << (congruent
[it
->first
]+ncongruent
[it
->first
]) << std::endl
;
1108 Trace("strings-process") << "Done check init, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1109 //now, infer constants for equivalence classes
1110 if( !hasProcessed() ){
1114 Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl
;
1115 prevSize
= d_eqc_to_const
.size();
1116 std::vector
< Node
> vecc
;
1117 checkConstantEquivalenceClasses( &d_term_index
[kind::STRING_CONCAT
], vecc
);
1118 }while( !hasProcessed() && d_eqc_to_const
.size()>prevSize
);
1119 Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1123 void TheoryStrings::checkExtendedFuncsEval( int effort
) {
1124 Trace("strings-extf-list") << "Active extended functions, effort=" << effort
<< " : " << std::endl
;
1126 d_extf_vars
.clear();
1130 d_extf_info
.clear();
1131 Trace("strings-extf-debug") << "Checking " << d_ext_func_terms
.size() << " extended functions." << std::endl
;
1132 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
1134 Node n
= (*it
).first
;
1136 if( n
.getType().isBoolean() ){
1137 if( areEqual( n
, d_true
) ){
1139 }else if( areEqual( n
, d_false
) ){
1143 Trace("strings-extf-debug") << "Check extf " << n
<< ", pol = " << d_extf_pol
[n
] << "..." << std::endl
;
1145 std::map
< Node
, bool > visited
;
1146 collectVars( n
, d_extf_vars
[n
], visited
);
1148 //build up a best current substitution for the variables in the term, exp is explanation for substitution
1149 std::vector
< Node
> var
;
1150 std::vector
< Node
> sub
;
1151 for( std::map
< Node
, std::vector
< Node
> >::iterator itv
= d_extf_vars
[n
].begin(); itv
!= d_extf_vars
[n
].end(); ++itv
){
1152 Node nr
= itv
->first
;
1153 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( nr
);
1157 if( itc
!=d_eqc_to_const
.end() ){
1158 b
= d_eqc_to_const_base
[nr
];
1160 e
= d_eqc_to_const_exp
[nr
];
1161 }else if( effort
>0 ){
1162 b
= d_normal_forms_base
[nr
];
1163 std::vector
< Node
> expt
;
1164 s
= getNormalString( b
, expt
);
1169 for( unsigned i
=0; i
<itv
->second
.size(); i
++ ){
1170 if( itv
->second
[i
]!=s
){
1171 var
.push_back( itv
->second
[i
] );
1173 addToExplanation( itv
->second
[i
], b
, d_extf_exp
[n
] );
1174 Trace("strings-extf-debug") << " " << itv
->second
[i
] << " --> " << s
<< std::endl
;
1179 addToExplanation( e
, d_extf_exp
[n
] );
1185 Node nr
= n
.substitute( var
.begin(), var
.end(), sub
.begin(), sub
.end() );
1186 Node nrc
= Rewriter::rewrite( nr
);
1187 if( nrc
.isConst() ){
1189 d_ext_func_terms
[n
] = false;
1190 Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl
;
1191 std::vector
< Node
> exps
;
1192 Trace("strings-extf-debug") << " get symbolic definition..." << std::endl
;
1193 Node nrs
= getSymbolicDefinition( nr
, exps
);
1194 if( !nrs
.isNull() ){
1195 Trace("strings-extf-debug") << " rewrite " << nrs
<< "..." << std::endl
;
1196 nrs
= Rewriter::rewrite( nrs
);
1197 //ensure the symbolic form is non-trivial
1198 if( nrs
.isConst() ){
1199 Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl
;
1203 Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl
;
1206 if( !nrs
.isNull() ){
1207 Trace("strings-extf-debug") << " symbolic def : " << nrs
<< std::endl
;
1208 if( !areEqual( nrs
, nrc
) ){
1209 //infer symbolic unit
1210 if( n
.getType().isBoolean() ){
1211 conc
= nrc
==d_true
? nrs
: nrs
.negate();
1213 conc
= nrs
.eqNode( nrc
);
1215 d_extf_exp
[n
].clear();
1218 if( !areEqual( n
, nrc
) ){
1219 if( n
.getType().isBoolean() ){
1220 if( areEqual( n
, nrc
==d_true
? d_false
: d_true
) ){
1221 d_extf_exp
[n
].push_back( nrc
==d_true
? n
.negate() : n
);
1224 conc
= nrc
==d_true
? n
: n
.negate();
1227 conc
= n
.eqNode( nrc
);
1231 if( !conc
.isNull() ){
1232 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< std::endl
;
1233 sendInference( d_extf_exp
[n
], conc
, effort
==0 ? "EXTF" : "EXTF-N", true );
1235 Trace("strings-extf-debug") << " conflict, return." << std::endl
;
1239 }else if( ( nrc
.getKind()==kind::OR
&& d_extf_pol
[n
]==-1 ) || ( nrc
.getKind()==kind::AND
&& d_extf_pol
[n
]==1 ) ){
1240 //infer the consequence of each
1241 d_ext_func_terms
[n
] = false;
1242 d_extf_exp
[n
].push_back( d_extf_pol
[n
]==-1 ? n
.negate() : n
);
1243 Trace("strings-extf-debug") << " decomposable..." << std::endl
;
1244 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< ", pol = " << d_extf_pol
[n
] << std::endl
;
1245 for( unsigned i
=0; i
<nrc
.getNumChildren(); i
++ ){
1246 sendInference( d_extf_exp
[n
], d_extf_pol
[n
]==-1 ? nrc
[i
].negate() : nrc
[i
], effort
==0 ? "EXTF_d" : "EXTF_d-N" );
1254 if( !to_reduce
.isNull() ){
1256 Trace("strings-extf") << " cannot rewrite extf : " << to_reduce
<< std::endl
;
1258 checkExtfInference( n
, to_reduce
, effort
);
1259 if( Trace
.isOn("strings-extf-list") ){
1260 Trace("strings-extf-list") << " * " << to_reduce
;
1261 if( d_extf_pol
[n
]!=0 ){
1262 Trace("strings-extf-list") << ", pol = " << d_extf_pol
[n
];
1265 Trace("strings-extf-list") << ", from " << n
;
1267 Trace("strings-extf-list") << std::endl
;
1271 Trace("strings-extf-debug") << " already reduced " << (*it
).first
<< std::endl
;
1276 void TheoryStrings::checkExtfInference( Node n
, Node nr
, int effort
){
1277 int n_pol
= d_extf_pol
[n
];
1279 //add original to explanation
1280 d_extf_exp
[n
].push_back( n_pol
==1 ? n
: n
.negate() );
1281 if( nr
.getKind()==kind::STRING_STRCTN
){
1282 if( ( n_pol
==1 && nr
[1].getKind()==kind::STRING_CONCAT
) || ( n_pol
==-1 && nr
[0].getKind()==kind::STRING_CONCAT
) ){
1283 if( d_extf_infer_cache
.find( nr
)==d_extf_infer_cache
.end() ){
1284 d_extf_infer_cache
.insert( nr
);
1285 //one argument does (not) contain each of the components of the other argument
1286 int index
= n_pol
==1 ? 1 : 0;
1287 std::vector
< Node
> children
;
1288 children
.push_back( nr
[0] );
1289 children
.push_back( nr
[1] );
1290 //Node exp_n = mkAnd( d_extf_exp[n] );
1291 for( unsigned i
=0; i
<nr
[index
].getNumChildren(); i
++ ){
1292 children
[index
] = nr
[index
][i
];
1293 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, children
);
1294 //can mark as reduced, since model for n => model for conc
1295 d_ext_func_terms
[conc
] = false;
1296 sendInference( d_extf_exp
[n
], n_pol
==1 ? conc
: conc
.negate(), "CTN_Decompose" );
1300 //store this (reduced) assertion
1301 //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
1302 bool pol
= n_pol
==1;
1303 if( std::find( d_extf_info
[nr
[0]].d_ctn
[pol
].begin(), d_extf_info
[nr
[0]].d_ctn
[pol
].end(), nr
[1] )==d_extf_info
[nr
[0]].d_ctn
[pol
].end() ){
1304 Trace("strings-extf-debug") << " store contains info : " << nr
[0] << " " << pol
<< " " << nr
[1] << std::endl
;
1305 d_extf_info
[nr
[0]].d_ctn
[pol
].push_back( nr
[1] );
1306 d_extf_info
[nr
[0]].d_ctn_from
[pol
].push_back( n
);
1307 //transitive closure for contains
1309 for( unsigned i
=0; i
<d_extf_info
[nr
[0]].d_ctn
[opol
].size(); i
++ ){
1310 Node onr
= d_extf_info
[nr
[0]].d_ctn
[opol
][i
];
1311 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, pol
? nr
[1] : onr
, pol
? onr
: nr
[1] );
1312 conc
= Rewriter::rewrite( conc
);
1313 bool do_infer
= false;
1314 if( conc
.getKind()==kind::EQUAL
){
1315 do_infer
= !areDisequal( conc
[0], conc
[1] );
1317 do_infer
= !areEqual( conc
, d_false
);
1320 conc
= conc
.negate();
1321 std::vector
< Node
> exp
;
1322 exp
.insert( exp
.end(), d_extf_exp
[n
].begin(), d_extf_exp
[n
].end() );
1323 Node ofrom
= d_extf_info
[nr
[0]].d_ctn_from
[opol
][i
];
1324 Assert( d_extf_exp
.find( ofrom
)!=d_extf_exp
.end() );
1325 exp
.insert( exp
.end(), d_extf_exp
[ofrom
].begin(), d_extf_exp
[ofrom
].end() );
1326 sendInference( exp
, conc
, "CTN_Trans" );
1330 Trace("strings-extf-debug") << " redundant." << std::endl
;
1331 d_ext_func_terms
[n
] = false;
1338 void TheoryStrings::collectVars( Node n
, std::map
< Node
, std::vector
< Node
> >& vars
, std::map
< Node
, bool >& visited
) {
1340 if( visited
.find( n
)==visited
.end() ){
1342 if( n
.getNumChildren()>0 ){
1343 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1344 collectVars( n
[i
], vars
, visited
);
1347 Node nr
= getRepresentative( n
);
1348 vars
[nr
].push_back( n
);
1354 Node
TheoryStrings::getSymbolicDefinition( Node n
, std::vector
< Node
>& exp
) {
1355 if( n
.getNumChildren()==0 ){
1356 NodeNodeMap::const_iterator it
= d_proxy_var
.find( n
);
1357 if( it
==d_proxy_var
.end() ){
1358 return Node::null();
1360 Node eq
= n
.eqNode( (*it
).second
);
1361 eq
= Rewriter::rewrite( eq
);
1362 if( std::find( exp
.begin(), exp
.end(), eq
)==exp
.end() ){
1363 exp
.push_back( eq
);
1365 return (*it
).second
;
1368 std::vector
< Node
> children
;
1369 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1370 children
.push_back( n
.getOperator() );
1372 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1373 if( n
.getKind()==kind::STRING_IN_REGEXP
&& i
==1 ){
1374 children
.push_back( n
[i
] );
1376 Node ns
= getSymbolicDefinition( n
[i
], exp
);
1378 return Node::null();
1380 children
.push_back( ns
);
1384 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1389 void TheoryStrings::debugPrintFlatForms( const char * tc
){
1390 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1391 Node eqc
= d_strings_eqc
[k
];
1392 if( d_eqc
[eqc
].size()>1 ){
1393 Trace( tc
) << "EQC [" << eqc
<< "]" << std::endl
;
1395 Trace( tc
) << "eqc [" << eqc
<< "]";
1397 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
1398 if( itc
!=d_eqc_to_const
.end() ){
1399 Trace( tc
) << " C: " << itc
->second
;
1400 if( d_eqc
[eqc
].size()>1 ){
1401 Trace( tc
) << std::endl
;
1404 if( d_eqc
[eqc
].size()>1 ){
1405 for( unsigned i
=0; i
<d_eqc
[eqc
].size(); i
++ ){
1406 Node n
= d_eqc
[eqc
][i
];
1408 for( unsigned j
=0; j
<d_flat_form
[n
].size(); j
++ ){
1409 Node fc
= d_flat_form
[n
][j
];
1410 itc
= d_eqc_to_const
.find( fc
);
1412 if( itc
!=d_eqc_to_const
.end() ){
1413 Trace( tc
) << itc
->second
;
1419 Trace( tc
) << ", from " << n
;
1421 Trace( tc
) << std::endl
;
1424 Trace( tc
) << std::endl
;
1427 Trace( tc
) << std::endl
;
1430 void TheoryStrings::checkFlatForms() {
1431 //first check for cycles, while building ordering of equivalence classes
1433 d_flat_form
.clear();
1434 d_flat_form_index
.clear();
1435 Trace("strings-process") << "Check equivalence classes cycles...." << std::endl
;
1436 //rebuild strings eqc based on acyclic ordering
1437 std::vector
< Node
> eqc
;
1438 eqc
.insert( eqc
.end(), d_strings_eqc
.begin(), d_strings_eqc
.end() );
1439 d_strings_eqc
.clear();
1440 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
1441 std::vector
< Node
> curr
;
1442 std::vector
< Node
> exp
;
1443 checkCycles( eqc
[i
], curr
, exp
);
1444 if( hasProcessed() ){
1448 Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << std::endl
;
1449 if( !hasProcessed() ){
1450 //debug print flat forms
1451 if( Trace
.isOn("strings-ff") ){
1452 Trace("strings-ff") << "Flat forms : " << std::endl
;
1453 debugPrintFlatForms( "strings-ff" );
1455 //inferences without recursively expanding flat forms
1456 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1457 Node eqc
= d_strings_eqc
[k
];
1459 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
1460 if( itc
!=d_eqc_to_const
.end() ){
1461 c
= itc
->second
; //use?
1463 std::map
< Node
, std::vector
< Node
> >::iterator it
= d_eqc
.find( eqc
);
1464 if( it
!=d_eqc
.end() && it
->second
.size()>1 ){
1465 //iterate over start index
1466 for( unsigned start
=0; start
<it
->second
.size()-1; start
++ ){
1467 for( unsigned r
=0; r
<2; r
++ ){
1469 std::vector
< Node
> inelig
;
1470 for( unsigned i
=0; i
<=start
; i
++ ){
1471 inelig
.push_back( it
->second
[start
] );
1473 Node a
= it
->second
[start
];
1476 std::vector
< Node
> exp
;
1477 //std::vector< Node > exp_n;
1480 if( count
==d_flat_form
[a
].size() ){
1481 for( unsigned i
=start
+1; i
<it
->second
.size(); i
++ ){
1483 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
1484 if( count
<d_flat_form
[b
].size() ){
1486 std::vector
< Node
> conc_c
;
1487 for( unsigned j
=count
; j
<d_flat_form
[b
].size(); j
++ ){
1488 conc_c
.push_back( b
[d_flat_form_index
[b
][j
]].eqNode( d_emptyString
) );
1490 Assert( !conc_c
.empty() );
1491 conc
= mkAnd( conc_c
);
1494 //swap, will enforce is empty past current
1495 a
= it
->second
[i
]; b
= it
->second
[start
];
1499 inelig
.push_back( it
->second
[i
] );
1503 Node curr
= d_flat_form
[a
][count
];
1504 Node curr_c
= d_eqc_to_const
[curr
];
1505 Node ac
= a
[d_flat_form_index
[a
][count
]];
1506 std::vector
< Node
> lexp
;
1507 Node lcurr
= getLength( ac
, lexp
);
1508 for( unsigned i
=1; i
<it
->second
.size(); i
++ ){
1510 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
1511 if( count
==d_flat_form
[b
].size() ){
1512 inelig
.push_back( b
);
1514 std::vector
< Node
> conc_c
;
1515 for( unsigned j
=count
; j
<d_flat_form
[a
].size(); j
++ ){
1516 conc_c
.push_back( a
[d_flat_form_index
[a
][j
]].eqNode( d_emptyString
) );
1518 Assert( !conc_c
.empty() );
1519 conc
= mkAnd( conc_c
);
1525 Node cc
= d_flat_form
[b
][count
];
1527 Node bc
= b
[d_flat_form_index
[b
][count
]];
1528 inelig
.push_back( b
);
1529 Assert( !areEqual( curr
, cc
) );
1530 Node cc_c
= d_eqc_to_const
[cc
];
1531 if( !curr_c
.isNull() && !cc_c
.isNull() ){
1532 //check for constant conflict
1534 Node s
= TheoryStringsRewriter::splitConstant( cc_c
, curr_c
, index
, r
==1 );
1536 addToExplanation( ac
, d_eqc_to_const_base
[curr
], exp
);
1537 addToExplanation( d_eqc_to_const_exp
[curr
], exp
);
1538 addToExplanation( bc
, d_eqc_to_const_base
[cc
], exp
);
1539 addToExplanation( d_eqc_to_const_exp
[cc
], exp
);
1544 }else if( (d_flat_form
[a
].size()-1)==count
&& (d_flat_form
[b
].size()-1)==count
){
1545 conc
= ac
.eqNode( bc
);
1549 //if lengths are the same, apply LengthEq
1550 std::vector
< Node
> lexp2
;
1551 Node lcc
= getLength( bc
, lexp2
);
1552 if( areEqual( lcurr
, lcc
) ){
1553 Trace("strings-ff-debug") << "Infer " << ac
<< " == " << bc
<< " since " << lcurr
<< " == " << lcc
<< std::endl
;
1554 //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
1555 Trace("strings-ff-debug") << "Explanation for " << lcurr
<< " is ";
1556 for( unsigned j
=0; j
<lexp
.size(); j
++ ) { Trace("strings-ff-debug") << lexp
[j
] << std::endl
; }
1557 Trace("strings-ff-debug") << "Explanation for " << lcc
<< " is ";
1558 for( unsigned j
=0; j
<lexp2
.size(); j
++ ) { Trace("strings-ff-debug") << lexp2
[j
] << std::endl
; }
1559 exp
.insert( exp
.end(), lexp
.begin(), lexp
.end() );
1560 exp
.insert( exp
.end(), lexp2
.begin(), lexp2
.end() );
1561 addToExplanation( lcurr
, lcc
, exp
);
1562 conc
= ac
.eqNode( bc
);
1572 if( !conc
.isNull() ){
1573 Trace("strings-ff-debug") << "Found inference : " << conc
<< " based on equality " << a
<< " == " << b
<< " " << r
<< " " << inf_type
<< std::endl
;
1574 addToExplanation( a
, b
, exp
);
1575 //explain why prefixes up to now were the same
1576 for( unsigned j
=0; j
<count
; j
++ ){
1577 Trace("strings-ff-debug") << "Add at " << d_flat_form_index
[a
][j
] << " " << d_flat_form_index
[b
][j
] << std::endl
;
1578 addToExplanation( a
[d_flat_form_index
[a
][j
]], b
[d_flat_form_index
[b
][j
]], exp
);
1580 //explain why other components up to now are empty
1581 for( unsigned t
=0; t
<2; t
++ ){
1582 Node c
= t
==0 ? a
: b
;
1583 int jj
= t
==0 ? d_flat_form_index
[a
][count
] : ( inf_type
==2 ? ( r
==0 ? c
.getNumChildren() : -1 ) : d_flat_form_index
[b
][count
] );
1585 for( int j
=0; j
<jj
; j
++ ){
1586 if( areEqual( c
[j
], d_emptyString
) ){
1587 addToExplanation( c
[j
], d_emptyString
, exp
);
1591 for( int j
=(c
.getNumChildren()-1); j
>jj
; --j
){
1592 if( areEqual( c
[j
], d_emptyString
) ){
1593 addToExplanation( c
[j
], d_emptyString
, exp
);
1598 //if( exp_n.empty() ){
1599 sendInference( exp
, conc
, inf_type
==0? "F_Const" : ( inf_type
==1 ? "F_LengthEq" : ( inf_type
==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
1609 }while( inelig
.size()<it
->second
.size() );
1611 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1612 std::reverse( d_flat_form
[it
->second
[i
]].begin(), d_flat_form
[it
->second
[i
]].end() );
1613 std::reverse( d_flat_form_index
[it
->second
[i
]].begin(), d_flat_form_index
[it
->second
[i
]].end() );
1619 if( !hasProcessed() ){
1620 // simple extended func reduction
1621 Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl
;
1622 checkExtfReduction( 1 );
1623 Trace("strings-process") << "Done check extended function reduction" << std::endl
;
1628 Node
TheoryStrings::checkCycles( Node eqc
, std::vector
< Node
>& curr
, std::vector
< Node
>& exp
){
1629 if( std::find( curr
.begin(), curr
.end(), eqc
)!=curr
.end() ){
1632 }else if( std::find( d_strings_eqc
.begin(), d_strings_eqc
.end(), eqc
)==d_strings_eqc
.end() ){
1633 curr
.push_back( eqc
);
1634 //look at all terms in this equivalence class
1635 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1636 while( !eqc_i
.isFinished() ) {
1638 if( d_congruent
.find( n
)==d_congruent
.end() ){
1639 if( n
.getKind() == kind::STRING_CONCAT
){
1640 Trace("strings-cycle") << eqc
<< " check term : " << n
<< " in " << eqc
<< std::endl
;
1641 if( eqc
!=d_emptyString_r
){
1642 d_eqc
[eqc
].push_back( n
);
1644 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1645 Node nr
= getRepresentative( n
[i
] );
1646 if( eqc
==d_emptyString_r
){
1647 //for empty eqc, ensure all components are empty
1648 if( nr
!=d_emptyString_r
){
1649 std::vector
< Node
> exp
;
1650 exp
.push_back( n
.eqNode( d_emptyString
) );
1651 sendInference( exp
, n
[i
].eqNode( d_emptyString
), "I_CYCLE_E" );
1652 return Node::null();
1655 if( nr
!=d_emptyString_r
){
1656 d_flat_form
[n
].push_back( nr
);
1657 d_flat_form_index
[n
].push_back( i
);
1659 //for non-empty eqc, recurse and see if we find a loop
1660 Node ncy
= checkCycles( nr
, curr
, exp
);
1661 if( !ncy
.isNull() ){
1662 Trace("strings-cycle") << eqc
<< " cycle: " << ncy
<< " at " << n
<< "[" << i
<< "] : " << n
[i
] << std::endl
;
1663 addToExplanation( n
, eqc
, exp
);
1664 addToExplanation( nr
, n
[i
], exp
);
1666 //can infer all other components must be empty
1667 for( unsigned j
=0; j
<n
.getNumChildren(); j
++ ){
1668 //take first non-empty
1669 if( j
!=i
&& !areEqual( n
[j
], d_emptyString
) ){
1670 sendInference( exp
, n
[j
].eqNode( d_emptyString
), "I_CYCLE" );
1671 return Node::null();
1674 Trace("strings-error") << "Looping term should be congruent : " << n
<< " " << eqc
<< " " << ncy
<< std::endl
;
1675 //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
1681 if( hasProcessed() ){
1682 return Node::null();
1692 //now we can add it to the list of equivalence classes
1693 d_strings_eqc
.push_back( eqc
);
1697 return Node::null();
1701 void TheoryStrings::checkNormalForms(){
1702 if( !options::stringEagerLen() ){
1703 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
1704 Node eqc
= d_strings_eqc
[i
];
1705 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1706 while( !eqc_i
.isFinished() ) {
1708 if( d_congruent
.find( n
)==d_congruent
.end() ){
1709 registerTerm( n
, 2 );
1715 if( !hasProcessed() ){
1716 Trace("strings-process") << "Normalize equivalence classes...." << std::endl
;
1717 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
1718 d_normal_forms
.clear();
1719 d_normal_forms_exp
.clear();
1720 std::map
< Node
, Node
> nf_to_eqc
;
1721 std::map
< Node
, Node
> eqc_to_exp
;
1722 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
1723 Node eqc
= d_strings_eqc
[i
];
1724 Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc
<< std::endl
;
1725 std::vector
< Node
> nf
;
1726 std::vector
< Node
> nf_exp
;
1727 normalizeEquivalenceClass( eqc
, nf
, nf_exp
);
1728 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl
;
1729 if( hasProcessed() ){
1732 Node nf_term
= mkConcat( nf
);
1733 if( nf_to_eqc
.find( nf_term
)!=nf_to_eqc
.end() ) {
1734 //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
1735 //two equivalence classes have same normal form, merge
1736 nf_exp
.push_back( eqc_to_exp
[nf_to_eqc
[nf_term
]] );
1737 Node eq
= eqc
.eqNode( nf_to_eqc
[nf_term
] );
1738 sendInference( nf_exp
, eq
, "Normal_Form" );
1740 nf_to_eqc
[nf_term
] = eqc
;
1741 eqc_to_exp
[eqc
] = mkAnd( nf_exp
);
1744 Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc
<< std::endl
;
1747 if(Trace
.isOn("strings-nf")) {
1748 Trace("strings-nf") << "**** Normal forms are : " << std::endl
;
1749 for( std::map
< Node
, Node
>::iterator it
= nf_to_eqc
.begin(); it
!= nf_to_eqc
.end(); ++it
){
1750 Trace("strings-nf") << " N[" << it
->second
<< "] = " << it
->first
<< std::endl
;
1752 Trace("strings-nf") << std::endl
;
1754 if( !hasProcessed() ){
1755 checkExtendedFuncsEval( 1 );
1756 Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1757 if( !hasProcessed() ){
1758 if( !options::stringEagerLen() ){
1760 if( hasProcessed() ){
1764 //process disequalities between equivalence classes
1766 Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1769 Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache
.size() << ", conflict = " << d_conflict
<< std::endl
;
1773 //nf_exp is conjunction
1774 bool TheoryStrings::normalizeEquivalenceClass( Node eqc
, std::vector
< Node
> & nf
, std::vector
< Node
> & nf_exp
) {
1775 Trace("strings-process-debug") << "Process equivalence class " << eqc
<< std::endl
;
1776 if( areEqual( eqc
, d_emptyString
) ) {
1777 for( unsigned j
=0; j
<d_eqc
[eqc
].size(); j
++ ){
1778 Node n
= d_eqc
[eqc
][j
];
1779 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1780 Assert( areEqual( n
[i
], d_emptyString
) );
1784 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : empty." << std::endl
;
1785 d_normal_forms_base
[eqc
] = d_emptyString
;
1786 d_normal_forms
[eqc
].clear();
1787 d_normal_forms_exp
[eqc
].clear();
1791 if( d_normal_forms
.find(eqc
)==d_normal_forms
.end() ){
1792 //phi => t = s1 * ... * sn
1793 // normal form for each non-variable term in this eqc (s1...sn)
1794 std::vector
< std::vector
< Node
> > normal_forms
;
1795 // explanation for each normal form (phi)
1796 std::vector
< std::vector
< Node
> > normal_forms_exp
;
1797 // dependency information
1798 std::vector
< std::map
< Node
, std::map
< bool, int > > > normal_forms_exp_depend
;
1799 // record terms for each normal form (t)
1800 std::vector
< Node
> normal_form_src
;
1802 result
= getNormalForms(eqc
, normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
);
1803 if( hasProcessed() ){
1806 if( processNEqc(normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
) ){
1810 //construct the normal form
1811 if( normal_forms
.empty() ){
1812 Trace("strings-solve-debug2") << "construct the normal form" << std::endl
;
1813 getConcatVec( eqc
, nf
);
1814 d_normal_forms_base
[eqc
] = eqc
;
1817 //nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
1818 //nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
1819 //Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
1820 //d_normal_forms_base[eqc] = normal_form_src[nf_index];
1822 std::vector
< Node
>::iterator itn
= std::find( normal_form_src
.begin(), normal_form_src
.end(), eqc
);
1823 if( itn
!=normal_form_src
.end() ){
1824 nf_index
= itn
- normal_form_src
.begin();
1825 Trace("strings-solve-debug2") << "take normal form " << nf_index
<< std::endl
;
1826 Assert( normal_form_src
[nf_index
]==eqc
);
1828 //just take the first normal form
1829 Trace("strings-solve-debug2") << "take the first normal form" << std::endl
;
1831 nf
.insert( nf
.end(), normal_forms
[nf_index
].begin(), normal_forms
[nf_index
].end() );
1832 nf_exp
.insert( nf_exp
.end(), normal_forms_exp
[nf_index
].begin(), normal_forms_exp
[nf_index
].end() );
1833 //if( eqc!=normal_form_src[nf_index] ){
1834 // nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
1836 Trace("strings-solve-debug2") << "take normal form ... done" << std::endl
;
1837 d_normal_forms_base
[eqc
] = normal_form_src
[nf_index
];
1839 //track dependencies
1840 for( unsigned i
=0; i
<normal_forms_exp
[nf_index
].size(); i
++ ){
1841 Node exp
= normal_forms_exp
[nf_index
][i
];
1842 for( unsigned r
=0; r
<2; r
++ ){
1843 d_normal_forms_exp_depend
[eqc
][exp
][r
==0] = normal_forms_exp_depend
[nf_index
][exp
][r
==0];
1848 d_normal_forms
[eqc
].insert( d_normal_forms
[eqc
].end(), nf
.begin(), nf
.end() );
1849 d_normal_forms_exp
[eqc
].insert( d_normal_forms_exp
[eqc
].end(), nf_exp
.begin(), nf_exp
.end() );
1851 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : returned, size = " << nf
.size() << std::endl
;
1853 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : already computed, size = " << d_normal_forms
[eqc
].size() << std::endl
;
1854 nf
.insert( nf
.end(), d_normal_forms
[eqc
].begin(), d_normal_forms
[eqc
].end() );
1855 nf_exp
.insert( nf_exp
.end(), d_normal_forms_exp
[eqc
].begin(), d_normal_forms_exp
[eqc
].end() );
1862 bool TheoryStrings::getNormalForms( Node
&eqc
, std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
1863 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
) {
1864 Trace("strings-process-debug") << "Get normal forms " << eqc
<< std::endl
;
1865 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1866 while( !eqc_i
.isFinished() ){
1868 if( d_congruent
.find( n
)==d_congruent
.end() ){
1869 if( n
.getKind() == kind::CONST_STRING
|| n
.getKind() == kind::STRING_CONCAT
){
1870 Trace("strings-process-debug") << "Get Normal Form : Process term " << n
<< " in eqc " << eqc
<< std::endl
;
1871 std::vector
< Node
> nf_n
;
1872 std::vector
< Node
> nf_exp_n
;
1873 std::map
< Node
, std::map
< bool, int > > nf_exp_depend_n
;
1874 if( n
.getKind()==kind::CONST_STRING
){
1875 if( n
!=d_emptyString
) {
1876 nf_n
.push_back( n
);
1878 }else if( n
.getKind()==kind::STRING_CONCAT
){
1879 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
1880 Node nr
= d_equalityEngine
.getRepresentative( n
[i
] );
1881 Trace("strings-process-debug") << "Normalizing subterm " << n
[i
] << " = " << nr
<< std::endl
;
1882 Assert( d_normal_forms
.find( nr
)!=d_normal_forms
.end() );
1883 unsigned orig_size
= nf_n
.size();
1884 unsigned add_size
= d_normal_forms
[nr
].size();
1885 //if not the empty string, add to current normal form
1886 if( !d_normal_forms
[nr
].empty() ){
1887 for( unsigned r
=0; r
<d_normal_forms
[nr
].size(); r
++ ) {
1888 if( Trace
.isOn("strings-error") ) {
1889 if( d_normal_forms
[nr
][r
].getKind()==kind::STRING_CONCAT
){
1890 Trace("strings-error") << "Strings::Error: From eqc = " << eqc
<< ", " << n
<< " index " << i
<< ", bad normal form : ";
1891 for( unsigned rr
=0; rr
<d_normal_forms
[nr
].size(); rr
++ ) {
1892 Trace("strings-error") << d_normal_forms
[nr
][rr
] << " ";
1894 Trace("strings-error") << std::endl
;
1897 Assert( d_normal_forms
[nr
][r
].getKind()!=kind::STRING_CONCAT
);
1899 nf_n
.insert( nf_n
.end(), d_normal_forms
[nr
].begin(), d_normal_forms
[nr
].end() );
1902 for( unsigned j
=0; j
<d_normal_forms_exp
[nr
].size(); j
++ ){
1903 Node exp
= d_normal_forms_exp
[nr
][j
];
1904 nf_exp_n
.push_back( exp
);
1906 for( unsigned k
=0; k
<2; k
++ ){
1907 int prev_dep
= d_normal_forms_exp_depend
[nr
][exp
][k
==1];
1909 nf_exp_depend_n
[exp
][false] = orig_size
+ prev_dep
;
1911 //store forward index (converted back to reverse index below)
1912 nf_exp_depend_n
[exp
][true] = orig_size
+ ( add_size
- prev_dep
);
1917 Node eq
= n
[i
].eqNode( nr
);
1918 nf_exp_n
.push_back( eq
);
1920 nf_exp_depend_n
[eq
][false] = orig_size
;
1921 nf_exp_depend_n
[eq
][true] = orig_size
+ add_size
;
1924 //convert forward indices to reverse indices
1925 int total_size
= nf_n
.size();
1926 for( std::map
< Node
, std::map
< bool, int > >::iterator it
= nf_exp_depend_n
.begin(); it
!= nf_exp_depend_n
.end(); ++it
){
1927 it
->second
[true] = total_size
- it
->second
[true];
1928 Assert( it
->second
[true]>=0 );
1931 //if not equal to self
1932 if( nf_n
.size()>1 || ( nf_n
.size()==1 && nf_n
[0].getKind()==kind::CONST_STRING
) ){
1933 if( nf_n
.size()>1 ) {
1934 for( unsigned i
=0; i
<nf_n
.size(); i
++ ){
1935 if( Trace
.isOn("strings-error") ){
1936 Trace("strings-error") << "Cycle for normal form ";
1937 printConcat(nf_n
,"strings-error");
1938 Trace("strings-error") << "..." << nf_n
[i
] << std::endl
;
1940 Assert( !areEqual( nf_n
[i
], n
) );
1943 normal_forms
.push_back(nf_n
);
1944 normal_form_src
.push_back(n
);
1945 normal_forms_exp
.push_back(nf_exp_n
);
1946 normal_forms_exp_depend
.push_back(nf_exp_depend_n
);
1948 //this was redundant: combination of self + empty string(s)
1949 Node nn
= nf_n
.size()==0 ? d_emptyString
: nf_n
[0];
1950 Assert( areEqual( nn
, eqc
) );
1951 //Assert( areEqual( nf_n[0], eqc ) );
1953 if( !areEqual( nn, eqc ) ){
1954 std::vector< Node > ant;
1955 ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
1956 ant.push_back( n.eqNode( eqc ) );
1957 Node conc = Rewriter::rewrite( nn.eqNode( eqc ) );
1958 sendInference( ant, conc, "CYCLE-T" );
1968 if(Trace
.isOn("strings-solve")) {
1969 if( !normal_forms
.empty() ) {
1970 Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc
<< " : " << std::endl
;
1971 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
1972 Trace("strings-solve") << "#" << i
<< " (from " << normal_form_src
[i
] << ") : ";
1973 for( unsigned j
=0; j
<normal_forms
[i
].size(); j
++ ) {
1975 Trace("strings-solve") << ", ";
1977 Trace("strings-solve") << normal_forms
[i
][j
];
1979 Trace("strings-solve") << std::endl
;
1980 Trace("strings-solve") << " Explanation is : ";
1981 if(normal_forms_exp
[i
].size() == 0) {
1982 Trace("strings-solve") << "NONE";
1984 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
1986 Trace("strings-solve") << " AND ";
1988 Trace("strings-solve") << normal_forms_exp
[i
][j
];
1990 Trace("strings-solve") << std::endl
;
1991 Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl
;
1992 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
1993 Trace("strings-solve") << " " << normal_forms_exp
[i
][j
] << " -> ";
1994 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][false] << ",";
1995 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][true] << std::endl
;
1998 Trace("strings-solve") << std::endl
;
2002 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc
<< std::endl
;
2008 void TheoryStrings::getExplanationVectorForPrefix( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2009 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2010 unsigned i
, unsigned j
, int index
, bool isRev
, std::vector
< Node
>& curr_exp
) {
2011 if( index
==-1 || !options::stringMinPrefixExplain() ){
2012 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
2013 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[j
].begin(), normal_forms_exp
[j
].end() );
2015 Trace("strings-explain-prefix") << "Get explanation for prefix " << index
<< " of normal forms " << i
<< " and " << j
<< ", reverse = " << isRev
<< std::endl
;
2016 for( unsigned r
=0; r
<2; r
++ ){
2017 int tindex
= r
==0 ? i
: j
;
2018 for( unsigned k
=0; k
<normal_forms_exp
[tindex
].size(); k
++ ){
2019 Node exp
= normal_forms_exp
[tindex
][k
];
2020 int dep
= normal_forms_exp_depend
[tindex
][exp
][isRev
];
2022 curr_exp
.push_back( exp
);
2023 Trace("strings-explain-prefix-debug") << " include : " << exp
<< std::endl
;
2025 Trace("strings-explain-prefix-debug") << " exclude : " << exp
<< std::endl
;
2029 Trace("strings-explain-prefix") << "Included " << curr_exp
.size() << " / " << ( normal_forms_exp
[i
].size() + normal_forms_exp
[j
].size() ) << std::endl
;
2031 if( normal_form_src
[i
]!=normal_form_src
[j
] ){
2032 curr_exp
.push_back( normal_form_src
[i
].eqNode( normal_form_src
[j
] ) );
2036 bool TheoryStrings::processNEqc( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2037 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
) {
2038 bool flag_lb
= false;
2039 std::vector
< Node
> c_lb_exp
;
2040 int c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
;
2041 for(unsigned i
=0; i
<normal_forms
.size()-1; i
++) {
2042 //unify each normalform[j] with normal_forms[i]
2043 for(unsigned j
=i
+1; j
<normal_forms
.size(); j
++ ) {
2044 Trace("strings-solve") << "Strings: Process normal form #" << i
<< " against #" << j
<< "..." << std::endl
;
2045 if( isNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] ) ) {
2046 Trace("strings-solve") << "Strings: Already cached." << std::endl
;
2048 //process the reverse direction first (check for easy conflicts and inferences)
2049 if( processReverseNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
) ){
2053 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
2058 if( processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, false ) ){
2059 //added a lemma, return
2064 //if we are at the end
2065 if(index
==normal_forms
[i
].size() || index
==normal_forms
[j
].size() ) {
2066 Assert( index
==normal_forms
[i
].size() && index
==normal_forms
[j
].size() );
2068 //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
2070 std::vector
< Node
> lexp
;
2071 Node length_term_i
= getLength( normal_forms
[i
][index
], lexp
);
2072 Node length_term_j
= getLength( normal_forms
[j
][index
], lexp
);
2073 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
2074 if( !areDisequal(length_term_i
, length_term_j
) && !areEqual(length_term_i
, length_term_j
) &&
2075 normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
) {
2076 //length terms are equal, merge equivalence classes if not already done so
2077 Node length_eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
);
2078 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl
;
2079 //try to make the lengths equal via splitting on demand
2080 sendSplit( length_term_i
, length_term_j
, "Len-Split(Diseq)" );
2081 length_eq
= Rewriter::rewrite( length_eq
);
2082 d_pending_req_phase
[ length_eq
] = true;
2085 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl
;
2088 if( detectLoop(normal_forms
, i
, j
, index
, loop_in_i
, loop_in_j
) ){
2092 c_loop_n_index
= loop_in_i
!=-1 ? i
: j
;
2093 c_other_n_index
= loop_in_i
!=-1 ? j
: i
;
2094 c_loop_index
= loop_in_i
!=-1 ? loop_in_i
: loop_in_j
;
2097 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, false, c_lb_exp
);
2099 if(options::stringLB() == 0) {
2102 if(processLoop(c_lb_exp
, normal_forms
, normal_form_src
, c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
)) {
2109 std::vector
< Node
> antec
;
2110 Trace("strings-solve-debug") << "No loops detected." << std::endl
;
2111 if( normal_forms
[i
][index
].getKind() == kind::CONST_STRING
|| normal_forms
[j
][index
].getKind() == kind::CONST_STRING
) {
2112 unsigned const_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? i
: j
;
2113 unsigned nconst_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? j
: i
;
2114 Node const_str
= normal_forms
[const_k
][index
];
2115 Node other_str
= normal_forms
[nconst_k
][index
];
2116 Assert( other_str
.getKind()!=kind::CONST_STRING
, "Other string is not constant." );
2117 Assert( other_str
.getKind()!=kind::STRING_CONCAT
, "Other string is not CONCAT." );
2118 if( !d_equalityEngine
.areDisequal(other_str
, d_emptyString
, true) ) {
2119 sendSplit( other_str
, d_emptyString
, "Len-Split(CST)" );
2121 Assert(areDisequal(other_str
, d_emptyString
), "CST Split on empty Var");
2122 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, false, antec
);
2123 Node xnz
= other_str
.eqNode(d_emptyString
).negate();
2124 antec
.push_back( xnz
);
2126 if( normal_forms
[nconst_k
].size() > index
+ 1 && normal_forms
[nconst_k
][index
+ 1].isConst() ) {
2127 CVC4::String stra
= const_str
.getConst
<String
>();
2128 CVC4::String strb
= normal_forms
[nconst_k
][index
+ 1].getConst
<String
>();
2129 CVC4::String stra1
= stra
.substr(1);
2130 size_t p
= stra
.size() - stra1
.overlap(strb
);
2131 size_t p2
= stra1
.find(strb
);
2132 p
= p2
==std::string::npos
? p
: ( p
>p2
+1? p2
+1 : p
);
2133 Node prea
= p
==stra
.size()? const_str
: NodeManager::currentNM()->mkConst(stra
.substr(0, p
));
2134 Node sk
= mkSkolemCached( other_str
, prea
, sk_id_c_spt
, "c_spt" );
2135 conc
= other_str
.eqNode( mkConcat(prea
, sk
) );
2136 Trace("strings-csp") << "Const Split: " << prea
<< " is removed from " << stra
<< " due to " << strb
<< std::endl
;
2139 Node firstChar
= const_str
.getConst
<String
>().size() == 1 ? const_str
:
2140 NodeManager::currentNM()->mkConst( const_str
.getConst
<String
>().substr(0, 1) );
2141 Node sk
= mkSkolemCached( other_str
, firstChar
, sk_id_vc_spt
, "c_spt" );
2142 conc
= other_str
.eqNode( mkConcat(firstChar
, sk
) );
2143 Trace("strings-csp") << "Const Split: " << firstChar
<< " is removed from " << const_str
<< " (normal) " << std::endl
;
2146 conc
= Rewriter::rewrite( conc
);
2147 sendInference( antec
, conc
, "S-Split(CST-P)", true );
2151 std::vector
< Node
> antec_new_lits
;
2152 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, false, antec
);
2154 Node ldeq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
).negate();
2155 if( d_equalityEngine
.areDisequal( length_term_i
, length_term_j
, true ) ){
2156 antec
.push_back( ldeq
);
2158 antec_new_lits
.push_back(ldeq
);
2162 for(unsigned xory
=0; xory
<2; xory
++) {
2163 Node x
= xory
==0 ? normal_forms
[i
][index
] : normal_forms
[j
][index
];
2164 Node xgtz
= x
.eqNode( d_emptyString
).negate();
2165 if( d_equalityEngine
.areDisequal( x
, d_emptyString
, true ) ) {
2166 antec
.push_back( xgtz
);
2168 antec_new_lits
.push_back( xgtz
);
2171 Node sk
= mkSkolemCached( normal_forms
[i
][index
], normal_forms
[j
][index
], sk_id_v_spt
, "v_spt", 1 );
2172 Node eq1
= normal_forms
[i
][index
].eqNode( mkConcat(normal_forms
[j
][index
], sk
) );
2173 Node eq2
= normal_forms
[j
][index
].eqNode( mkConcat(normal_forms
[i
][index
], sk
) );
2174 if( options::stringCheckEntailLen() ){
2176 for( unsigned e
=0; e
<2; e
++ ){
2177 Node lt1
= e
==0 ? length_term_i
: length_term_j
;
2178 Node lt2
= e
==0 ? length_term_j
: length_term_i
;
2179 Node ent_lit
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
, lt1
, lt2
) );
2180 std::pair
<bool, Node
> et
= d_valuation
.entailmentCheck(THEORY_OF_TYPE_BASED
, ent_lit
);
2182 Trace("strings-entail") << "Strings entailment : " << ent_lit
<< " is entailed in the current context." << std::endl
;
2183 Trace("strings-entail") << " explanation was : " << et
.second
<< std::endl
;
2184 conc
= e
==0 ? eq1
: eq2
;
2185 antec_new_lits
.push_back( et
.second
);
2190 if( conc
.isNull() ){
2191 conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR
, eq1
, eq2
));
2195 sendInference( antec
, antec_new_lits
, conc
, "S-Split(VAR)", true );
2196 //++(d_statistics.d_eq_splits);
2210 if(processLoop(c_lb_exp
, normal_forms
, normal_form_src
, c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
)) {
2218 bool TheoryStrings::processReverseNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2219 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2220 unsigned i
, unsigned j
) {
2221 //reverse normal form of i, j
2222 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2223 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2226 bool ret
= processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, true );
2228 //reverse normal form of i, j
2229 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2230 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2235 bool TheoryStrings::processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2236 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2237 unsigned i
, unsigned j
, unsigned& index
, bool isRev
) {
2241 //if we are at the end
2242 if(index
==normal_forms
[i
].size() || index
==normal_forms
[j
].size() ) {
2243 if( index
==normal_forms
[i
].size() && index
==normal_forms
[j
].size() ) {
2246 //the remainder must be empty
2247 unsigned k
= index
==normal_forms
[i
].size() ? j
: i
;
2248 unsigned index_k
= index
;
2249 //Node eq_exp = mkAnd( curr_exp );
2250 std::vector
< Node
> curr_exp
;
2251 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, isRev
, curr_exp
);
2252 while(!d_conflict
&& index_k
<normal_forms
[k
].size()) {
2253 //can infer that this string must be empty
2254 Node eq
= normal_forms
[k
][index_k
].eqNode( d_emptyString
);
2255 //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
2256 Assert( !areEqual( d_emptyString
, normal_forms
[k
][index_k
] ) );
2257 sendInference( curr_exp
, eq
, "EQ_Endpoint" );
2263 Trace("strings-solve-debug") << "Process " << normal_forms
[i
][index
] << " ... " << normal_forms
[j
][index
] << std::endl
;
2264 if( normal_forms
[i
][index
]==normal_forms
[j
][index
] ){
2265 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl
;
2269 Assert( !areEqual(normal_forms
[i
][index
], normal_forms
[j
][index
]) );
2270 std::vector
< Node
> temp_exp
;
2271 Node length_term_i
= getLength( normal_forms
[i
][index
], temp_exp
);
2272 Node length_term_j
= getLength( normal_forms
[j
][index
], temp_exp
);
2273 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
2274 if( areEqual( length_term_i
, length_term_j
) ){
2275 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl
;
2276 Node eq
= normal_forms
[i
][index
].eqNode( normal_forms
[j
][index
] );
2277 //eq = Rewriter::rewrite( eq );
2278 Node length_eq
= length_term_i
.eqNode( length_term_j
);
2279 //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
2280 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, isRev
, temp_exp
);
2281 temp_exp
.push_back(length_eq
);
2282 sendInference( temp_exp
, eq
, "LengthEq" );
2284 }else if( ( normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[i
].size()-1 ) ||
2285 ( normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[j
].size()-1 ) ){
2286 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl
;
2288 std::vector
< Node
> antec
;
2289 //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
2290 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, isRev
, antec
);
2291 std::vector
< Node
> eqn
;
2292 for( unsigned r
=0; r
<2; r
++ ) {
2293 int index_k
= index
;
2294 int k
= r
==0 ? i
: j
;
2295 std::vector
< Node
> eqnc
;
2296 for( unsigned index_l
=index_k
; index_l
<normal_forms
[k
].size(); index_l
++ ) {
2298 eqnc
.insert(eqnc
.begin(), normal_forms
[k
][index_l
] );
2300 eqnc
.push_back( normal_forms
[k
][index_l
] );
2303 eqn
.push_back( mkConcat( eqnc
) );
2305 if( !areEqual( eqn
[0], eqn
[1] ) ) {
2306 conc
= eqn
[0].eqNode( eqn
[1] );
2307 sendInference( antec
, conc
, "ENDPOINT", true );
2310 Assert( normal_forms
[i
].size()==normal_forms
[j
].size() );
2311 index
= normal_forms
[i
].size();
2313 } else if( normal_forms
[i
][index
].isConst() && normal_forms
[j
][index
].isConst() ){
2314 Node const_str
= normal_forms
[i
][index
];
2315 Node other_str
= normal_forms
[j
][index
];
2316 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str
<< " vs " << other_str
<< std::endl
;
2317 unsigned len_short
= const_str
.getConst
<String
>().size() <= other_str
.getConst
<String
>().size() ? const_str
.getConst
<String
>().size() : other_str
.getConst
<String
>().size();
2318 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
);
2320 //same prefix/suffix
2321 //k is the index of the string that is shorter
2322 int k
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? i
: j
;
2323 int l
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? j
: i
;
2325 int new_len
= normal_forms
[l
][index
].getConst
<String
>().size() - len_short
;
2326 Node remainderStr
= NodeManager::currentNM()->mkConst( normal_forms
[l
][index
].getConst
<String
>().substr(0, new_len
) );
2327 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
2328 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
2330 Node remainderStr
= NodeManager::currentNM()->mkConst(normal_forms
[l
][index
].getConst
<String
>().substr(len_short
));
2331 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
2332 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
2334 normal_forms
[l
][index
] = normal_forms
[k
][index
];
2338 std::vector
< Node
> antec
;
2339 //curr_exp is conflict
2340 //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
2341 getExplanationVectorForPrefix( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, isRev
, antec
);
2342 sendInference( antec
, d_false
, "Const Conflict", true );
2352 bool TheoryStrings::detectLoop( std::vector
< std::vector
< Node
> > &normal_forms
, int i
, int j
, int index
, int &loop_in_i
, int &loop_in_j
) {
2353 int has_loop
[2] = { -1, -1 };
2354 if( options::stringLB() != 2 ) {
2355 for( unsigned r
=0; r
<2; r
++ ) {
2356 int n_index
= (r
==0 ? i
: j
);
2357 int other_n_index
= (r
==0 ? j
: i
);
2358 if( normal_forms
[other_n_index
][index
].getKind() != kind::CONST_STRING
) {
2359 for( unsigned lp
= index
+1; lp
<normal_forms
[n_index
].size(); lp
++ ){
2360 if( normal_forms
[n_index
][lp
]==normal_forms
[other_n_index
][index
] ){
2368 if( has_loop
[0]!=-1 || has_loop
[1]!=-1 ) {
2369 loop_in_i
= has_loop
[0];
2370 loop_in_j
= has_loop
[1];
2378 bool TheoryStrings::processLoop( std::vector
< Node
> &antec
, std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2379 int i
, int j
, int loop_n_index
, int other_n_index
, int loop_index
, int index
) {
2380 if( options::stringAbortLoop() ){
2381 Message() << "Looping word equation encountered." << std::endl
;
2385 Trace("strings-loop") << "Detected possible loop for " << normal_forms
[loop_n_index
][loop_index
] << std::endl
;
2386 Trace("strings-loop") << " ... (X)= " << normal_forms
[other_n_index
][index
] << std::endl
;
2388 Trace("strings-loop") << " ... T(Y.Z)= ";
2389 std::vector
< Node
> vec_t
;
2390 for(int lp
=index
; lp
<loop_index
; ++lp
) {
2391 if(lp
!= index
) Trace("strings-loop") << " ++ ";
2392 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
2393 vec_t
.push_back( normal_forms
[loop_n_index
][lp
] );
2395 Node t_yz
= mkConcat( vec_t
);
2396 Trace("strings-loop") << " (" << t_yz
<< ")" << std::endl
;
2397 Trace("strings-loop") << " ... S(Z.Y)= ";
2398 std::vector
< Node
> vec_s
;
2399 for(int lp
=index
+1; lp
<(int)normal_forms
[other_n_index
].size(); ++lp
) {
2400 if(lp
!= index
+1) Trace("strings-loop") << " ++ ";
2401 Trace("strings-loop") << normal_forms
[other_n_index
][lp
];
2402 vec_s
.push_back( normal_forms
[other_n_index
][lp
] );
2404 Node s_zy
= mkConcat( vec_s
);
2405 Trace("strings-loop") << " (" << s_zy
<< ")" << std::endl
;
2406 Trace("strings-loop") << " ... R= ";
2407 std::vector
< Node
> vec_r
;
2408 for(int lp
=loop_index
+1; lp
<(int)normal_forms
[loop_n_index
].size(); ++lp
) {
2409 if(lp
!= loop_index
+1) Trace("strings-loop") << " ++ ";
2410 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
2411 vec_r
.push_back( normal_forms
[loop_n_index
][lp
] );
2413 Node r
= mkConcat( vec_r
);
2414 Trace("strings-loop") << " (" << r
<< ")" << std::endl
;
2416 //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
2417 //TODO: can be more general
2418 if( s_zy
.isConst() && r
.isConst() && r
!= d_emptyString
) {
2421 if(s_zy
.getConst
<String
>().tailcmp( r
.getConst
<String
>(), c
) ) {
2423 s_zy
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, c
) );
2426 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
<< ", c=" << c
<< std::endl
;
2431 Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl
;
2432 sendInference( antec
, conc
, "Loop Conflict", true );
2437 //require that x is non-empty
2438 if( !areDisequal( normal_forms
[loop_n_index
][loop_index
], d_emptyString
) ){
2439 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
2440 sendSplit( normal_forms
[loop_n_index
][loop_index
], d_emptyString
, "Len-Split(Loop-X)" );
2441 } else if( !areDisequal( t_yz
, d_emptyString
) && t_yz
.getKind()!=kind::CONST_STRING
) {
2442 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
2443 sendSplit( t_yz
, d_emptyString
, "Len-Split(Loop-YZ)" );
2446 antec
.push_back( normal_forms
[loop_n_index
][loop_index
].eqNode( d_emptyString
).negate() );
2447 if( t_yz
.getKind()!=kind::CONST_STRING
) {
2448 antec
.push_back( t_yz
.eqNode( d_emptyString
).negate() );
2450 Node ant
= mkExplain( antec
);
2451 if(d_loop_antec
.find(ant
) == d_loop_antec
.end()) {
2452 d_loop_antec
.insert(ant
);
2456 r
== d_emptyString
&&
2458 s_zy
.getConst
<String
>().isRepeated()
2460 Node rep_c
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, 1) );
2461 Trace("strings-loop") << "Special case (X)=" << normal_forms
[other_n_index
][index
] << " " << std::endl
;
2462 Trace("strings-loop") << "... (C)=" << rep_c
<< " " << std::endl
;
2464 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][index
],
2465 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
2466 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, rep_c
) ) );
2468 } else if(t_yz
.isConst()) {
2469 Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl
;
2470 CVC4::String s
= t_yz
.getConst
< CVC4::String
>();
2471 unsigned size
= s
.size();
2472 std::vector
< Node
> vconc
;
2473 for(unsigned len
=1; len
<=size
; len
++) {
2474 Node y
= NodeManager::currentNM()->mkConst(s
.substr(0, len
));
2475 Node z
= NodeManager::currentNM()->mkConst(s
.substr(len
, size
- len
));
2478 if(r
!= d_emptyString
) {
2479 std::vector
< Node
> v2(vec_r
);
2480 v2
.insert(v2
.begin(), y
);
2481 v2
.insert(v2
.begin(), z
);
2482 restr
= mkConcat( z
, y
);
2483 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( v2
) ));
2485 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( z
, y
) ));
2490 Node conc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][index
],
2491 NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
2492 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, y
),
2493 NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
,
2494 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, restr
))));
2495 cc
= cc
==d_true
? conc2
: NodeManager::currentNM()->mkNode( kind::AND
, cc
, conc2
);
2496 d_regexp_ant
[conc2
] = ant
;
2497 vconc
.push_back(cc
);
2499 conc
= vconc
.size()==0 ? Node::null() : vconc
.size()==1 ? vconc
[0] : NodeManager::currentNM()->mkNode(kind::OR
, vconc
);
2501 Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl
;
2503 Node sk_w
= mkSkolemS( "w_loop" );
2504 Node sk_y
= mkSkolemS( "y_loop", 1 );
2505 Node sk_z
= mkSkolemS( "z_loop" );
2506 //t1 * ... * tn = y * z
2507 Node conc1
= t_yz
.eqNode( mkConcat( sk_y
, sk_z
) );
2508 // s1 * ... * sk = z * y * r
2509 vec_r
.insert(vec_r
.begin(), sk_y
);
2510 vec_r
.insert(vec_r
.begin(), sk_z
);
2511 Node conc2
= s_zy
.eqNode( mkConcat( vec_r
) );
2512 Node conc3
= normal_forms
[other_n_index
][index
].eqNode( mkConcat( sk_y
, sk_w
) );
2513 Node restr
= r
== d_emptyString
? s_zy
: mkConcat( sk_z
, sk_y
);
2514 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, sk_w
,
2515 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
2516 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, restr
) ) );
2518 std::vector
< Node
> vec_conc
;
2519 vec_conc
.push_back(conc1
); vec_conc
.push_back(conc2
); vec_conc
.push_back(conc3
);
2520 vec_conc
.push_back(str_in_re
);
2521 //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
2522 conc
= NodeManager::currentNM()->mkNode( kind::AND
, vec_conc
);
2525 //set its antecedant to ant, to say when it is relevant
2526 if(!str_in_re
.isNull()) {
2527 d_regexp_ant
[str_in_re
] = ant
;
2530 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
2531 if( options::stringProcessLoop() ){
2532 sendLemma( ant
, conc
, "F-LOOP" );
2533 ++(d_statistics
.d_loop_lemmas
);
2535 d_out
->setIncomplete();
2540 Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant
<< " has already added." << std::endl
;
2541 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
2550 //return true for lemma, false if we succeed
2551 bool TheoryStrings::processDeq( Node ni
, Node nj
) {
2552 //Assert( areDisequal( ni, nj ) );
2553 if( d_normal_forms
[ni
].size()>1 || d_normal_forms
[nj
].size()>1 ){
2554 std::vector
< Node
> nfi
;
2555 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
2556 std::vector
< Node
> nfj
;
2557 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
2559 int revRet
= processReverseDeq( nfi
, nfj
, ni
, nj
);
2565 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
2567 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
2570 while( index
<nfi
.size() || index
<nfj
.size() ){
2571 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, false );
2575 Assert( index
<nfi
.size() && index
<nfj
.size() );
2576 Node i
= nfi
[index
];
2577 Node j
= nfj
[index
];
2578 Trace("strings-solve-debug") << "...Processing(DEQ) " << i
<< " " << j
<< std::endl
;
2579 if( !areEqual( i
, j
) ) {
2580 Assert( i
.getKind()!=kind::CONST_STRING
|| j
.getKind()!=kind::CONST_STRING
);
2581 std::vector
< Node
> lexp
;
2582 Node li
= getLength( i
, lexp
);
2583 Node lj
= getLength( j
, lexp
);
2584 if( areDisequal(li
, lj
) ){
2585 //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
2587 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl
;
2589 std::vector
< Node
> antec
;
2590 std::vector
< Node
> antec_new_lits
;
2591 antec
.insert( antec
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
2592 antec
.insert( antec
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
2594 if( areDisequal( ni
, nj
) ){
2595 antec
.push_back( ni
.eqNode( nj
).negate() );
2597 antec_new_lits
.push_back( ni
.eqNode( nj
).negate() );
2599 antec_new_lits
.push_back( li
.eqNode( lj
).negate() );
2600 std::vector
< Node
> conc
;
2601 Node sk1
= mkSkolemCached( i
, j
, sk_id_deq_x
, "x_dsplit" );
2602 Node sk2
= mkSkolemCached( i
, j
, sk_id_deq_y
, "y_dsplit" );
2603 Node sk3
= mkSkolemCached( i
, j
, sk_id_deq_z
, "z_dsplit", 1 );
2604 //Node nemp = sk3.eqNode(d_emptyString).negate();
2605 //conc.push_back(nemp);
2606 Node lsk1
= mkLength( sk1
);
2607 conc
.push_back( lsk1
.eqNode( li
) );
2608 Node lsk2
= mkLength( sk2
);
2609 conc
.push_back( lsk2
.eqNode( lj
) );
2610 conc
.push_back( NodeManager::currentNM()->mkNode( kind::OR
, j
.eqNode( mkConcat( sk1
, sk3
) ), i
.eqNode( mkConcat( sk2
, sk3
) ) ) );
2611 sendInference( antec
, antec_new_lits
, NodeManager::currentNM()->mkNode( kind::AND
, conc
), "D-DISL-Split" );
2612 ++(d_statistics
.d_deq_splits
);
2614 }else if( areEqual( li
, lj
) ){
2615 Assert( !areDisequal( i
, j
) );
2616 //splitting on demand : try to make them disequal
2617 Node eq
= i
.eqNode( j
);
2618 sendSplit( i
, j
, "S-Split(DEQL)" );
2619 eq
= Rewriter::rewrite( eq
);
2620 d_pending_req_phase
[ eq
] = false;
2623 //splitting on demand : try to make lengths equal
2624 Node eq
= li
.eqNode( lj
);
2625 sendSplit( li
, lj
, "D-Split" );
2626 eq
= Rewriter::rewrite( eq
);
2627 d_pending_req_phase
[ eq
] = true;
2639 int TheoryStrings::processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
) {
2640 //reverse normal form of i, j
2641 std::reverse( nfi
.begin(), nfi
.end() );
2642 std::reverse( nfj
.begin(), nfj
.end() );
2645 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, true );
2647 //reverse normal form of i, j
2648 std::reverse( nfi
.begin(), nfi
.end() );
2649 std::reverse( nfj
.begin(), nfj
.end() );
2654 int TheoryStrings::processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
) {
2655 while( index
<nfi
.size() || index
<nfj
.size() ) {
2656 if( index
>=nfi
.size() || index
>=nfj
.size() ) {
2657 Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl
;
2658 std::vector
< Node
> ant
;
2659 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
2660 Node lni
= getLengthExp( ni
, ant
, d_normal_forms_base
[ni
] );
2661 Node lnj
= getLengthExp( nj
, ant
, d_normal_forms_base
[nj
] );
2662 ant
.push_back( lni
.eqNode( lnj
) );
2663 ant
.insert( ant
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
2664 ant
.insert( ant
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
2665 std::vector
< Node
> cc
;
2666 std::vector
< Node
>& nfk
= index
>=nfi
.size() ? nfj
: nfi
;
2667 for( unsigned index_k
=index
; index_k
<nfk
.size(); index_k
++ ){
2668 cc
.push_back( nfk
[index_k
].eqNode( d_emptyString
) );
2670 Node conc
= cc
.size()==1 ? cc
[0] : NodeManager::currentNM()->mkNode( kind::AND
, cc
);
2671 conc
= Rewriter::rewrite( conc
);
2672 sendInference( ant
, conc
, "Disequality Normalize Empty", true);
2675 Node i
= nfi
[index
];
2676 Node j
= nfj
[index
];
2677 Trace("strings-solve-debug") << "...Processing(QED) " << i
<< " " << j
<< std::endl
;
2678 if( !areEqual( i
, j
) ) {
2679 if( i
.getKind()==kind::CONST_STRING
&& j
.getKind()==kind::CONST_STRING
) {
2680 unsigned int len_short
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
.getConst
<String
>().size() : j
.getConst
<String
>().size();
2681 bool isSameFix
= isRev
? i
.getConst
<String
>().rstrncmp(j
.getConst
<String
>(), len_short
): i
.getConst
<String
>().strncmp(j
.getConst
<String
>(), len_short
);
2683 //same prefix/suffix
2684 //k is the index of the string that is shorter
2685 Node nk
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
: j
;
2686 Node nl
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? j
: i
;
2689 int new_len
= nl
.getConst
<String
>().size() - len_short
;
2690 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr(0, new_len
) );
2691 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
2693 remainderStr
= NodeManager::currentNM()->mkConst( j
.getConst
<String
>().substr(len_short
) );
2694 Trace("strings-solve-debug-test") << "Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
2696 if( i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ) {
2697 nfj
.insert( nfj
.begin() + index
+ 1, remainderStr
);
2698 nfj
[index
] = nfi
[index
];
2700 nfi
.insert( nfi
.begin() + index
+ 1, remainderStr
);
2701 nfi
[index
] = nfj
[index
];
2707 std::vector
< Node
> lexp
;
2708 Node li
= getLength( i
, lexp
);
2709 Node lj
= getLength( j
, lexp
);
2710 if( areEqual( li
, lj
) && areDisequal( i
, j
) ) {
2711 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i
<< " " << j
<< std::endl
;
2712 //we are done: D-Remove
2725 void TheoryStrings::addNormalFormPair( Node n1
, Node n2
){
2726 if( !isNormalFormPair( n1
, n2
) ){
2727 //Assert( !isNormalFormPair( n1, n2 ) );
2729 NodeListMap::iterator nf_i
= d_nf_pairs
.find( n1
);
2730 if( nf_i
== d_nf_pairs
.end() ){
2731 if( d_nf_pairs
.find( n2
)!=d_nf_pairs
.end() ){
2732 addNormalFormPair( n2
, n1
);
2735 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
2736 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
2737 d_nf_pairs
.insertDataFromContextMemory( n1
, lst
);
2738 Trace("strings-nf") << "Create cache for " << n1
<< std::endl
;
2740 lst
= (*nf_i
).second
;
2742 Trace("strings-nf") << "Add normal form pair : " << n1
<< " " << n2
<< std::endl
;
2743 lst
->push_back( n2
);
2744 Assert( isNormalFormPair( n1
, n2
) );
2746 Trace("strings-nf-debug") << "Already a normal form pair " << n1
<< " " << n2
<< std::endl
;
2750 bool TheoryStrings::isNormalFormPair( Node n1
, Node n2
) {
2751 //TODO: modulo equality?
2752 return isNormalFormPair2( n1
, n2
) || isNormalFormPair2( n2
, n1
);
2755 bool TheoryStrings::isNormalFormPair2( Node n1
, Node n2
) {
2756 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
2758 NodeListMap::iterator nf_i
= d_nf_pairs
.find( n1
);
2759 if( nf_i
!= d_nf_pairs
.end() ) {
2760 lst
= (*nf_i
).second
;
2761 for( NodeList::const_iterator i
= lst
->begin(); i
!= lst
->end(); ++i
) {
2771 void TheoryStrings::registerTerm( Node n
, int effort
) {
2772 // 0 : upon preregistration or internal assertion
2773 // 1 : upon occurrence in length term
2774 // 2 : before normal form computation
2775 // 3 : called on normal form terms
2776 bool do_register
= false;
2777 if( options::stringEagerLen() ){
2778 do_register
= effort
==0;
2780 do_register
= effort
>0 || n
.getKind()!=kind::STRING_CONCAT
;
2783 if(d_registered_terms_cache
.find(n
) == d_registered_terms_cache
.end()) {
2784 d_registered_terms_cache
.insert(n
);
2785 Debug("strings-register") << "TheoryStrings::registerTerm() " << n
<< ", effort = " << effort
<< std::endl
;
2786 if(n
.getType().isString()) {
2787 //register length information:
2788 // for variables, split on empty vs positive length
2789 // for concat/const, introduce proxy var and state length relation
2790 if( n
.getKind()!=kind::STRING_CONCAT
&& n
.getKind()!=kind::CONST_STRING
) {
2791 if( d_length_intro_vars
.find(n
)==d_length_intro_vars
.end() ) {
2792 sendLengthLemma( n
);
2793 ++(d_statistics
.d_splits
);
2796 Node sk
= mkSkolemS("lsym", 2);
2797 StringsProxyVarAttribute spva
;
2798 sk
.setAttribute(spva
,true);
2799 Node eq
= Rewriter::rewrite( sk
.eqNode(n
) );
2800 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq
<< std::endl
;
2801 d_proxy_var
[n
] = sk
;
2802 Trace("strings-assert") << "(assert " << eq
<< ")" << std::endl
;
2804 Node skl
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk
);
2806 if( n
.getKind() == kind::STRING_CONCAT
) {
2807 std::vector
<Node
> node_vec
;
2808 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
2809 if( n
[i
].getAttribute(StringsProxyVarAttribute()) ){
2810 Assert( d_proxy_var_to_length
.find( n
[i
] )!=d_proxy_var_to_length
.end() );
2811 node_vec
.push_back( d_proxy_var_to_length
[n
[i
]] );
2813 Node lni
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
[i
] );
2814 node_vec
.push_back(lni
);
2817 lsum
= NodeManager::currentNM()->mkNode( kind::PLUS
, node_vec
);
2818 } else if( n
.getKind() == kind::CONST_STRING
) {
2819 lsum
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( n
.getConst
<String
>().size() ) );
2821 lsum
= Rewriter::rewrite( lsum
);
2822 d_proxy_var_to_length
[sk
] = lsum
;
2823 Node ceq
= Rewriter::rewrite( skl
.eqNode( lsum
) );
2824 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq
<< std::endl
;
2825 Trace("strings-lemma-debug") << " prerewrite : " << skl
.eqNode( lsum
) << std::endl
;
2826 Trace("strings-assert") << "(assert " << ceq
<< ")" << std::endl
;
2830 AlwaysAssert(false, "String Terms only in registerTerm.");
2836 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, std::vector
< Node
>& exp_n
, Node eq
, const char * c
, bool asLemma
) {
2837 eq
= eq
.isNull() ? d_false
: Rewriter::rewrite( eq
);
2839 if( Trace
.isOn("strings-infer-debug") ){
2840 Trace("strings-infer-debug") << "By " << c
<< ", infer : " << eq
<< " from: " << std::endl
;
2841 for( unsigned i
=0; i
<exp
.size(); i
++ ){
2842 Trace("strings-infer-debug") << " " << exp
[i
] << std::endl
;
2844 for( unsigned i
=0; i
<exp_n
.size(); i
++ ){
2845 Trace("strings-infer-debug") << " N:" << exp_n
[i
] << std::endl
;
2847 //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
2849 //check if we should send a lemma or an inference
2850 if( asLemma
|| eq
==d_false
|| eq
.getKind()==kind::OR
|| !exp_n
.empty() || options::stringInferAsLemmas() ){
2852 if( options::stringRExplainLemmas() ){
2853 eq_exp
= mkExplain( exp
, exp_n
);
2856 eq_exp
= mkAnd( exp_n
);
2857 }else if( exp_n
.empty() ){
2858 eq_exp
= mkAnd( exp
);
2860 std::vector
< Node
> ev
;
2861 ev
.insert( ev
.end(), exp
.begin(), exp
.end() );
2862 ev
.insert( ev
.end(), exp_n
.begin(), exp_n
.end() );
2863 eq_exp
= NodeManager::currentNM()->mkNode( kind::AND
, ev
);
2866 sendLemma( eq_exp
, eq
, c
);
2868 sendInfer( mkAnd( exp
), eq
, c
);
2873 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, Node eq
, const char * c
, bool asLemma
) {
2874 std::vector
< Node
> exp_n
;
2875 sendInference( exp
, exp_n
, eq
, c
, asLemma
);
2878 void TheoryStrings::sendLemma( Node ant
, Node conc
, const char * c
) {
2879 if( conc
.isNull() || conc
== d_false
) {
2880 d_out
->conflict(ant
);
2881 Trace("strings-conflict") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
2882 Trace("strings-lemma") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
2883 Trace("strings-assert") << "(assert (not " << ant
<< ")) ; conflict " << c
<< std::endl
;
2887 if( ant
== d_true
) {
2890 lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, ant
, conc
);
2892 Trace("strings-lemma") << "Strings::Lemma " << c
<< " : " << lem
<< std::endl
;
2893 Trace("strings-assert") << "(assert " << lem
<< ") ; lemma " << c
<< std::endl
;
2894 d_lemma_cache
.push_back( lem
);
2898 void TheoryStrings::sendInfer( Node eq_exp
, Node eq
, const char * c
) {
2899 if( options::stringInferSym() ){
2900 std::vector
< Node
> vars
;
2901 std::vector
< Node
> subs
;
2902 std::vector
< Node
> unproc
;
2903 inferSubstitutionProxyVars( eq_exp
, vars
, subs
, unproc
);
2904 if( unproc
.empty() ){
2905 Trace("strings-lemma-debug") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
2906 Node eqs
= eq
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
2907 Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs
<< std::endl
;
2908 for( unsigned i
=0; i
<vars
.size(); i
++ ){
2909 Trace("strings-lemma-debug") << " " << vars
[i
] << " -> " << subs
[i
] << std::endl
;
2911 sendLemma( d_true
, eqs
, c
);
2914 for( unsigned i
=0; i
<unproc
.size(); i
++ ){
2915 Trace("strings-lemma-debug") << " non-trivial exp : " << unproc
[i
] << std::endl
;
2919 Trace("strings-lemma") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
2920 Trace("strings-assert") << "(assert (=> " << eq_exp
<< " " << eq
<< ")) ; infer " << c
<< std::endl
;
2921 d_pending
.push_back( eq
);
2922 d_pending_exp
[eq
] = eq_exp
;
2923 d_infer
.push_back( eq
);
2924 d_infer_exp
.push_back( eq_exp
);
2928 void TheoryStrings::sendSplit( Node a
, Node b
, const char * c
, bool preq
) {
2929 Node eq
= a
.eqNode( b
);
2930 eq
= Rewriter::rewrite( eq
);
2931 Node neq
= NodeManager::currentNM()->mkNode( kind::NOT
, eq
);
2932 Node lemma_or
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, neq
);
2933 Trace("strings-lemma") << "Strings::Lemma " << c
<< " SPLIT : " << lemma_or
<< std::endl
;
2934 d_lemma_cache
.push_back(lemma_or
);
2935 d_pending_req_phase
[eq
] = preq
;
2936 ++(d_statistics
.d_splits
);
2940 void TheoryStrings::sendLengthLemma( Node n
){
2941 Node n_len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
);
2942 if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
2943 Node n_len_eq_z
= n_len
.eqNode( d_zero
);
2944 Node n_len_eq_z_2
= n
.eqNode( d_emptyString
);
2945 n_len_eq_z
= Rewriter::rewrite( n_len_eq_z
);
2946 n_len_eq_z_2
= Rewriter::rewrite( n_len_eq_z_2
);
2947 Node n_len_geq_zero
= NodeManager::currentNM()->mkNode( kind::OR
, NodeManager::currentNM()->mkNode( kind::AND
, n_len_eq_z
, n_len_eq_z_2
),
2948 NodeManager::currentNM()->mkNode( kind::GT
, n_len
, d_zero
) );
2949 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero
<< std::endl
;
2950 d_out
->lemma(n_len_geq_zero
);
2951 d_out
->requirePhase( n_len_eq_z
, true );
2952 d_out
->requirePhase( n_len_eq_z_2
, true );
2954 //AJR: probably a good idea
2955 if( options::stringLenGeqZ() ){
2956 Node n_len_geq
= NodeManager::currentNM()->mkNode( kind::GEQ
, n_len
, d_zero
);
2957 n_len_geq
= Rewriter::rewrite( n_len_geq
);
2958 d_out
->lemma( n_len_geq
);
2962 void TheoryStrings::inferSubstitutionProxyVars( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::vector
< Node
>& unproc
) {
2963 if( n
.getKind()==kind::AND
){
2964 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2965 inferSubstitutionProxyVars( n
[i
], vars
, subs
, unproc
);
2968 }else if( n
.getKind()==kind::EQUAL
){
2969 Node ns
= n
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
2970 ns
= Rewriter::rewrite( ns
);
2971 if( ns
.getKind()==kind::EQUAL
){
2974 for( unsigned i
=0; i
<2; i
++ ){
2976 if( ns
[i
].getAttribute(StringsProxyVarAttribute()) ){
2978 }else if( ns
[i
].isConst() ){
2979 NodeNodeMap::const_iterator it
= d_proxy_var
.find( ns
[i
] );
2980 if( it
!=d_proxy_var
.end() ){
2986 if( v
.getNumChildren()==0 ){
2990 //both sides involved in proxy var
3001 subs
.push_back( s
);
3002 vars
.push_back( v
);
3010 unproc
.push_back( n
);
3015 Node
TheoryStrings::mkConcat( Node n1
, Node n2
) {
3016 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
) );
3019 Node
TheoryStrings::mkConcat( Node n1
, Node n2
, Node n3
) {
3020 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
, n3
) );
3023 Node
TheoryStrings::mkConcat( const std::vector
< Node
>& c
) {
3024 return Rewriter::rewrite( c
.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, c
) : ( c
.size()==1 ? c
[0] : d_emptyString
) );
3027 Node
TheoryStrings::mkLength( Node t
) {
3028 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
) );
3031 Node
TheoryStrings::mkSkolemCached( Node a
, Node b
, int id
, const char * c
, int isLenSplit
){
3032 //return mkSkolemS( c, isLenSplit );
3033 std::map
< int, Node
>::iterator it
= d_skolem_cache
[a
][b
].find( id
);
3034 if( it
==d_skolem_cache
[a
][b
].end() ){
3035 Node sk
= mkSkolemS( c
, isLenSplit
);
3036 d_skolem_cache
[a
][b
][id
] = sk
;
3043 //isLenSplit: 0-yes, 1-no, 2-ignore
3044 Node
TheoryStrings::mkSkolemS( const char *c
, int isLenSplit
) {
3045 Node n
= NodeManager::currentNM()->mkSkolem( c
, NodeManager::currentNM()->stringType(), "string sko" );
3046 d_length_intro_vars
.insert(n
);
3047 ++(d_statistics
.d_new_skolems
);
3048 if(isLenSplit
== 0) {
3049 sendLengthLemma( n
);
3050 ++(d_statistics
.d_splits
);
3051 } else if(isLenSplit
== 1) {
3052 d_equalityEngine
.assertEquality(n
.eqNode(d_emptyString
), false, d_true
);
3053 Node len_n_gt_z
= NodeManager::currentNM()->mkNode(kind::GT
,
3054 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, n
), d_zero
);
3055 Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z
<< std::endl
;
3056 Trace("strings-assert") << "(assert " << len_n_gt_z
<< ")" << std::endl
;
3057 d_out
->lemma(len_n_gt_z
);
3062 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
) {
3063 std::vector
< Node
> an
;
3064 return mkExplain( a
, an
);
3067 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
) {
3068 std::vector
< TNode
> antec_exp
;
3069 for( unsigned i
=0; i
<a
.size(); i
++ ) {
3070 if( std::find( a
.begin(), a
.begin() + i
, a
[i
] )==a
.begin() + i
) {
3072 Debug("strings-explain") << "Ask for explanation of " << a
[i
] << std::endl
;
3074 if(a
[i
].getKind() == kind::EQUAL
) {
3075 //assert( hasTerm(a[i][0]) );
3076 //assert( hasTerm(a[i][1]) );
3077 Assert( areEqual(a
[i
][0], a
[i
][1]) );
3078 if( a
[i
][0]==a
[i
][1] ){
3081 } else if( a
[i
].getKind()==kind::NOT
&& a
[i
][0].getKind()==kind::EQUAL
) {
3082 Assert( hasTerm(a
[i
][0][0]) );
3083 Assert( hasTerm(a
[i
][0][1]) );
3084 AlwaysAssert( d_equalityEngine
.areDisequal(a
[i
][0][0], a
[i
][0][1], true) );
3085 }else if( a
[i
].getKind() == kind::AND
){
3086 for( unsigned j
=0; j
<a
[i
].getNumChildren(); j
++ ){
3087 a
.push_back( a
[i
][j
] );
3092 unsigned ps
= antec_exp
.size();
3093 explain(a
[i
], antec_exp
);
3094 Debug("strings-explain") << "Done, explanation was : " << std::endl
;
3095 for( unsigned j
=ps
; j
<antec_exp
.size(); j
++ ) {
3096 Debug("strings-explain") << " " << antec_exp
[j
] << std::endl
;
3098 Debug("strings-explain") << std::endl
;
3102 for( unsigned i
=0; i
<an
.size(); i
++ ) {
3103 if( std::find( an
.begin(), an
.begin() + i
, an
[i
] )==an
.begin() + i
){
3104 Debug("strings-explain") << "Add to explanation (new literal) " << an
[i
] << std::endl
;
3105 antec_exp
.push_back(an
[i
]);
3109 if( antec_exp
.empty() ) {
3111 } else if( antec_exp
.size()==1 ) {
3114 ant
= NodeManager::currentNM()->mkNode( kind::AND
, antec_exp
);
3116 ant
= Rewriter::rewrite( ant
);
3120 Node
TheoryStrings::mkAnd( std::vector
< Node
>& a
) {
3121 std::vector
< Node
> au
;
3122 for( unsigned i
=0; i
<a
.size(); i
++ ){
3123 if( std::find( au
.begin(), au
.end(), a
[i
] )==au
.end() ){
3124 au
.push_back( a
[i
] );
3129 } else if( au
.size() == 1 ) {
3132 return NodeManager::currentNM()->mkNode( kind::AND
, au
);
3136 void TheoryStrings::getConcatVec( Node n
, std::vector
< Node
>& c
) {
3137 if( n
.getKind()==kind::STRING_CONCAT
) {
3138 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
3139 if( !areEqual( n
[i
], d_emptyString
) ) {
3140 c
.push_back( n
[i
] );
3148 void TheoryStrings::checkDeqNF() {
3149 std::vector
< std::vector
< Node
> > cols
;
3150 std::vector
< Node
> lts
;
3151 std::map
< Node
, std::map
< Node
, bool > > processed
;
3153 //for each pair of disequal strings, must determine whether their lengths are equal or disequal
3154 bool addedLSplit
= false;
3155 for( NodeList::const_iterator id
= d_ee_disequalities
.begin(); id
!= d_ee_disequalities
.end(); ++id
) {
3158 for( unsigned i
=0; i
<2; i
++ ){
3159 n
[i
] = d_equalityEngine
.getRepresentative( eq
[i
] );
3161 if( processed
[n
[0]].find( n
[1] )==processed
[n
[0]].end() ){
3162 processed
[n
[0]][n
[1]] = true;
3164 for( unsigned i
=0; i
<2; i
++ ){
3165 EqcInfo
* ei
= getOrMakeEqcInfo( n
[i
], false );
3166 lt
[i
] = ei
? ei
->d_length_term
: Node::null();
3167 if( lt
[i
].isNull() ){
3170 lt
[i
] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
[i
] );
3172 if( !areEqual( lt
[0], lt
[1] ) && !areDisequal( lt
[0], lt
[1] ) ){
3174 sendSplit( lt
[0], lt
[1], "DEQ-LENGTH-SP" );
3180 separateByLength( d_strings_eqc
, cols
, lts
);
3181 for( unsigned i
=0; i
<cols
.size(); i
++ ){
3182 if( cols
[i
].size()>1 && d_lemma_cache
.empty() ){
3183 Trace("strings-solve") << "- Verify disequalities are processed for " << cols
[i
][0] << ", normal form : ";
3184 printConcat( d_normal_forms
[cols
[i
][0]], "strings-solve" );
3185 Trace("strings-solve") << "... #eql = " << cols
[i
].size() << std::endl
;
3186 //must ensure that normal forms are disequal
3187 for( unsigned j
=0; j
<cols
[i
].size(); j
++ ){
3188 for( unsigned k
=(j
+1); k
<cols
[i
].size(); k
++ ){
3189 //for strings that are disequal, but have the same length
3190 if( areDisequal( cols
[i
][j
], cols
[i
][k
] ) ){
3191 Assert( !d_conflict
);
3192 Trace("strings-solve") << "- Compare " << cols
[i
][j
] << " ";
3193 printConcat( d_normal_forms
[cols
[i
][j
]], "strings-solve" );
3194 Trace("strings-solve") << " against " << cols
[i
][k
] << " ";
3195 printConcat( d_normal_forms
[cols
[i
][k
]], "strings-solve" );
3196 Trace("strings-solve") << "..." << std::endl
;
3197 if( processDeq( cols
[i
][j
], cols
[i
][k
] ) ){
3208 void TheoryStrings::checkLengthsEqc() {
3209 if( options::stringLenNorm() ){
3210 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ){
3211 //if( d_normal_forms[nodes[i]].size()>1 ) {
3212 Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc
[i
] << std::endl
;
3213 //check if there is a length term for this equivalence class
3214 EqcInfo
* ei
= getOrMakeEqcInfo( d_strings_eqc
[i
], false );
3215 Node lt
= ei
? ei
->d_length_term
: Node::null();
3216 if( !lt
.isNull() ) {
3217 Node llt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
3218 //now, check if length normalization has occurred
3219 if( ei
->d_normalized_length
.get().isNull() ) {
3220 //if not, add the lemma
3221 std::vector
< Node
> ant
;
3222 ant
.insert( ant
.end(), d_normal_forms_exp
[d_strings_eqc
[i
]].begin(), d_normal_forms_exp
[d_strings_eqc
[i
]].end() );
3223 ant
.push_back( d_normal_forms_base
[d_strings_eqc
[i
]].eqNode( lt
) );
3224 Node lc
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, mkConcat( d_normal_forms
[d_strings_eqc
[i
]] ) );
3225 lc
= Rewriter::rewrite( lc
);
3226 Node eq
= llt
.eqNode( lc
);
3228 ei
->d_normalized_length
.set( eq
);
3229 sendInference( ant
, eq
, "LEN-NORM", true );
3233 Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc
[i
] << " " << d_eqc_to_len_term
[d_strings_eqc
[i
]] << std::endl
;
3234 if( !options::stringEagerLen() ){
3235 Node c
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
3236 registerTerm( c
, 3 );
3239 NodeNodeMap::const_iterator it = d_proxy_var.find( c );
3240 if( it!=d_proxy_var.end() ){
3241 Node pv = (*it).second;
3242 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
3243 Node pvl = d_proxy_var_to_length[pv];
3244 Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
3245 sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
3252 // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
3258 void TheoryStrings::checkCardinality() {
3259 //int cardinality = options::stringCharCardinality();
3260 //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
3262 //AJR: this will create a partition of eqc, where each collection has length that are pairwise propagated to be equal.
3263 // 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).
3264 // TODO: revisit this?
3265 std::vector
< std::vector
< Node
> > cols
;
3266 std::vector
< Node
> lts
;
3267 separateByLength( d_strings_eqc
, cols
, lts
);
3269 for( unsigned i
= 0; i
<cols
.size(); ++i
) {
3271 Trace("strings-card") << "Number of strings with length equal to " << lr
<< " is " << cols
[i
].size() << std::endl
;
3272 if( cols
[i
].size() > 1 ) {
3274 unsigned card_need
= 1;
3275 double curr
= (double)cols
[i
].size();
3276 while( curr
>d_card_size
){
3277 curr
= curr
/(double)d_card_size
;
3280 Trace("strings-card") << "Need length " << card_need
<< " for this number of strings (where alphabet size is " << d_card_size
<< ")." << std::endl
;
3281 Node cmp
= NodeManager::currentNM()->mkNode( kind::GEQ
, lr
, NodeManager::currentNM()->mkConst( Rational( card_need
) ) );
3282 cmp
= Rewriter::rewrite( cmp
);
3284 unsigned int int_k
= (unsigned int)card_need
;
3285 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
3286 itr1
!= cols
[i
].end(); ++itr1
) {
3287 for( std::vector
< Node
>::iterator itr2
= itr1
+ 1;
3288 itr2
!= cols
[i
].end(); ++itr2
) {
3289 if(!areDisequal( *itr1
, *itr2
)) {
3291 sendSplit( *itr1
, *itr2
, "CARD-SP" );
3296 EqcInfo
* ei
= getOrMakeEqcInfo( lr
, true );
3297 Trace("strings-card") << "Previous cardinality used for " << lr
<< " is " << ((int)ei
->d_cardinality_lem_k
.get()-1) << std::endl
;
3298 if( int_k
+1 > ei
->d_cardinality_lem_k
.get() ){
3299 Node k_node
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k
) );
3300 //add cardinality lemma
3301 Node dist
= NodeManager::currentNM()->mkNode( kind::DISTINCT
, cols
[i
] );
3302 std::vector
< Node
> vec_node
;
3303 vec_node
.push_back( dist
);
3304 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
3305 itr1
!= cols
[i
].end(); ++itr1
) {
3306 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr1
);
3308 Node len_eq_lr
= len
.eqNode(lr
);
3309 vec_node
.push_back( len_eq_lr
);
3312 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, cols
[i
][0] );
3313 Node cons
= NodeManager::currentNM()->mkNode( kind::GEQ
, len
, k_node
);
3314 cons
= Rewriter::rewrite( cons
);
3315 ei
->d_cardinality_lem_k
.set( int_k
+1 );
3317 sendInference( d_empty_vec
, vec_node
, cons
, "CARDINALITY", true );
3326 void TheoryStrings::getEquivalenceClasses( std::vector
< Node
>& eqcs
) {
3327 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
3328 while( !eqcs_i
.isFinished() ) {
3329 Node eqc
= (*eqcs_i
);
3330 //if eqc.getType is string
3331 if (eqc
.getType().isString()) {
3332 eqcs
.push_back( eqc
);
3338 void TheoryStrings::getFinalNormalForm( Node n
, std::vector
< Node
>& nf
, std::vector
< Node
>& exp
) {
3339 if( n
!=d_emptyString
) {
3340 if( n
.getKind()==kind::STRING_CONCAT
) {
3341 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
3342 getFinalNormalForm( n
[i
], nf
, exp
);
3345 Trace("strings-debug") << "Get final normal form " << n
<< std::endl
;
3346 Assert( d_equalityEngine
.hasTerm( n
) );
3347 Node nr
= d_equalityEngine
.getRepresentative( n
);
3348 EqcInfo
*eqc_n
= getOrMakeEqcInfo( nr
, false );
3349 Node nc
= eqc_n
? eqc_n
->d_const_term
.get() : Node::null();
3350 if( !nc
.isNull() ) {
3353 exp
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, n
, nc
) );
3356 Assert( d_normal_forms
.find( nr
)!=d_normal_forms
.end() );
3357 if( d_normal_forms
[nr
][0]==nr
) {
3358 Assert( d_normal_forms
[nr
].size()==1 );
3361 exp
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, n
, nr
) );
3364 for( unsigned i
=0; i
<d_normal_forms
[nr
].size(); i
++ ) {
3365 Assert( d_normal_forms
[nr
][i
]!=nr
);
3366 getFinalNormalForm( d_normal_forms
[nr
][i
], nf
, exp
);
3368 exp
.insert( exp
.end(), d_normal_forms_exp
[nr
].begin(), d_normal_forms_exp
[nr
].end() );
3371 Trace("strings-ind-nf") << "The final normal form of " << n
<< " is " << nf
<< std::endl
;
3376 void TheoryStrings::separateByLength(std::vector
< Node
>& n
,
3377 std::vector
< std::vector
< Node
> >& cols
,
3378 std::vector
< Node
>& lts
) {
3379 unsigned leqc_counter
= 0;
3380 std::map
< Node
, unsigned > eqc_to_leqc
;
3381 std::map
< unsigned, Node
> leqc_to_eqc
;
3382 std::map
< unsigned, std::vector
< Node
> > eqc_to_strings
;
3383 for( unsigned i
=0; i
<n
.size(); i
++ ) {
3385 Assert( d_equalityEngine
.getRepresentative(eqc
)==eqc
);
3386 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
3387 Node lt
= ei
? ei
->d_length_term
: Node::null();
3389 lt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
3390 Node r
= d_equalityEngine
.getRepresentative( lt
);
3391 if( eqc_to_leqc
.find( r
)==eqc_to_leqc
.end() ){
3392 eqc_to_leqc
[r
] = leqc_counter
;
3393 leqc_to_eqc
[leqc_counter
] = r
;
3396 eqc_to_strings
[ eqc_to_leqc
[r
] ].push_back( eqc
);
3398 eqc_to_strings
[leqc_counter
].push_back( eqc
);
3402 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= eqc_to_strings
.begin(); it
!= eqc_to_strings
.end(); ++it
){
3403 cols
.push_back( std::vector
< Node
>() );
3404 cols
.back().insert( cols
.back().end(), it
->second
.begin(), it
->second
.end() );
3405 lts
.push_back( leqc_to_eqc
[it
->first
] );
3409 void TheoryStrings::printConcat( std::vector
< Node
>& n
, const char * c
) {
3410 for( unsigned i
=0; i
<n
.size(); i
++ ){
3411 if( i
>0 ) Trace(c
) << " ++ ";
3419 void TheoryStrings::updateMpl( Node n, int b ) {
3420 if(d_mpl.find(n) == d_mpl.end()) {
3421 //d_curr_cardinality.get();
3423 } else if(b < d_mpl[n]) {
3429 //// Regular Expressions
3430 Node
TheoryStrings::mkRegExpAntec(Node atom
, Node ant
) {
3431 if(d_regexp_ant
.find(atom
) == d_regexp_ant
.end()) {
3432 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, atom
) );
3434 Node n
= d_regexp_ant
[atom
];
3435 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, n
) );
3439 Node
TheoryStrings::normalizeRegexp(Node r
) {
3441 if(d_nf_regexps
.find(r
) != d_nf_regexps
.end()) {
3442 nf_r
= d_nf_regexps
[r
];
3444 std::vector
< Node
> nf_exp
;
3445 if(!d_regexp_opr
.checkConstRegExp(r
)) {
3446 switch( r
.getKind() ) {
3447 case kind::REGEXP_EMPTY
:
3448 case kind::REGEXP_SIGMA
: {
3451 case kind::STRING_TO_REGEXP
: {
3452 if(r
[0].isConst()) {
3455 if(d_normal_forms
.find( r
[0] ) != d_normal_forms
.end()) {
3456 nf_r
= mkConcat( d_normal_forms
[r
[0]] );
3457 Debug("regexp-nf") << "Term: " << r
[0] << " has a normal form " << nf_r
<< std::endl
;
3458 nf_exp
.insert(nf_exp
.end(), d_normal_forms_exp
[r
[0]].begin(), d_normal_forms_exp
[r
[0]].end());
3459 nf_r
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, nf_r
) );
3463 case kind::REGEXP_CONCAT
:
3464 case kind::REGEXP_UNION
:
3465 case kind::REGEXP_INTER
: {
3467 std::vector
< Node
> vec_nodes
;
3468 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
3469 Node rtmp
= normalizeRegexp(r
[i
]);
3470 vec_nodes
.push_back(rtmp
);
3476 Node rtmp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(r
.getKind(), vec_nodes
);
3477 nf_r
= Rewriter::rewrite( rtmp
);
3480 case kind::REGEXP_STAR
: {
3481 Node rtmp
= normalizeRegexp(r
[0]);
3483 rtmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, rtmp
);
3484 nf_r
= Rewriter::rewrite( rtmp
);
3492 d_nf_regexps
[r
] = nf_r
;
3493 d_nf_regexps_exp
[r
] = nf_exp
;
3498 bool TheoryStrings::normalizePosMemberships(std::map
< Node
, std::vector
< Node
> > &memb_with_exps
) {
3499 std::map
< Node
, std::vector
< Node
> > unprocessed_x_exps
;
3500 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships
;
3501 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships_bases
;
3502 bool addLemma
= false;
3504 Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl
;
3506 for(NodeListMap::const_iterator itr_xr
= d_pos_memberships
.begin();
3507 itr_xr
!= d_pos_memberships
.end(); ++itr_xr
) {
3508 Node x
= (*itr_xr
).first
;
3509 NodeList
* lst
= (*itr_xr
).second
;
3511 std::vector
< Node
> nf_x_exp
;
3512 if(d_normal_forms
.find( x
) != d_normal_forms
.end()) {
3513 //nf_x = mkConcat( d_normal_forms[x] );
3514 nf_x_exp
.insert(nf_x_exp
.end(), d_normal_forms_exp
[x
].begin(), d_normal_forms_exp
[x
].end());
3515 //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
3519 Trace("regexp-nf") << "Checking Memberships for N(" << x
<< ") = " << nf_x
<< " :" << std::endl
;
3521 std::vector
< Node
> vec_x
;
3522 std::vector
< Node
> vec_r
;
3523 for(NodeList::const_iterator itr_lst
= lst
->begin();
3524 itr_lst
!= lst
->end(); ++itr_lst
) {
3526 Node nf_r
= normalizeRegexp((*lst
)[0]);
3527 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, nf_r
);
3528 if(d_processed_memberships
.find(memb
) == d_processed_memberships
.end()) {
3529 if(d_regexp_opr
.checkConstRegExp(nf_r
)) {
3533 Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r
<< ") = " << nf_r
<< std::endl
;
3534 //TODO: handle symbolic ones
3537 d_processed_memberships
.insert(memb
);
3540 if(!vec_x
.empty()) {
3541 if(unprocessed_x_exps
.find(nf_x
) == unprocessed_x_exps
.end()) {
3542 unprocessed_x_exps
[nf_x
] = nf_x_exp
;
3543 unprocessed_memberships
[nf_x
] = vec_r
;
3544 unprocessed_memberships_bases
[nf_x
] = vec_x
;
3546 unprocessed_x_exps
[nf_x
].insert(unprocessed_x_exps
[nf_x
].end(), nf_x_exp
.begin(), nf_x_exp
.end());
3547 unprocessed_memberships
[nf_x
].insert(unprocessed_memberships
[nf_x
].end(), vec_r
.begin(), vec_r
.end());
3548 unprocessed_memberships_bases
[nf_x
].insert(unprocessed_memberships_bases
[nf_x
].end(), vec_x
.begin(), vec_x
.end());
3553 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= unprocessed_memberships
.begin();
3554 itr
!= unprocessed_memberships
.end(); ++itr
) {
3555 Node nf_x
= itr
->first
;
3556 std::vector
< Node
> exp( unprocessed_x_exps
[nf_x
] );
3557 Node r
= itr
->second
[0];
3559 Node inter_r
= d_nf_regexps
[r
];
3560 exp
.insert(exp
.end(), d_nf_regexps_exp
[r
].begin(), d_nf_regexps_exp
[r
].end());
3561 Node x
= unprocessed_memberships_bases
[itr
->first
][0];
3562 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
);
3563 exp
.push_back(memb
);
3564 for(std::size_t i
=1; i
< itr
->second
.size(); i
++) {
3566 Node r2
= itr
->second
[i
];
3567 Node inter_r2
= d_nf_regexps
[r2
];
3568 exp
.insert(exp
.end(), d_nf_regexps_exp
[r2
].begin(), d_nf_regexps_exp
[r2
].end());
3569 Node x2
= unprocessed_memberships_bases
[itr
->first
][i
];
3570 memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x2
, r2
);
3571 exp
.push_back(memb
);
3573 bool spflag
= false;
3574 inter_r
= d_regexp_opr
.intersect(inter_r
, inter_r2
, spflag
);
3575 if(inter_r
== d_emptyRegexp
) {
3578 sendInference( d_empty_vec
, exp
, conc
, "INTERSECT CONFLICT", true );
3585 memb
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, inter_r
) );
3586 memb_with_exps
[memb
] = exp
;
3595 bool TheoryStrings::applyRConsume( CVC4::String
&s
, Node
&r
) {
3596 Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s
<< ", r= " << r
<< std::endl
;
3597 Assert( d_regexp_opr
.checkConstRegExp(r
) );
3599 if( !s
.isEmptyString() ) {
3602 for(unsigned i
=0; i
<s
.size(); ++i
) {
3603 CVC4::String c
= s
.substr(i
, 1);
3605 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
3609 } else if(rt
== 2) {
3619 Node
TheoryStrings::applyRSplit(Node s1
, Node s2
, Node r
) {
3620 Assert(d_regexp_opr
.checkConstRegExp(r
));
3622 std::vector
< std::pair
< Node
, Node
> > vec_can
;
3623 d_regexp_opr
.splitRegExp(r
, vec_can
);
3624 //TODO: lazy cache or eager?
3625 std::vector
< Node
> vec_or
;
3627 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
3628 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
3629 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
3630 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
3631 vec_or
.push_back( c
);
3633 Node conc
= vec_or
.size()==0? Node::null() : vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
3637 bool TheoryStrings::applyRLen(std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
3638 if(XinR_with_exps
.size() > 0) {
3639 //TODO: get vector, var, store.
3646 bool TheoryStrings::checkMembershipsWithoutLength(
3647 std::map
< Node
, std::vector
< Node
> > &memb_with_exps
,
3648 std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
3649 for(std::map
< Node
, std::vector
< Node
> >::iterator itr
= memb_with_exps
.begin(); itr
!= memb_with_exps
.end(); ++itr
) {
3650 Node memb
= itr
->first
;
3654 memb
= Rewriter::rewrite( memb
);
3655 if(memb
== d_false
) {
3657 sendInference(d_empty_vec
, itr
->second
, conc
, "MEMBERSHIP CONFLICT", true);
3661 Assert(memb
== d_true
);
3663 } else if(s
.getKind() == kind::VARIABLE
) {
3665 XinR_with_exps
[itr
->first
] = itr
->second
;
3667 Assert(s
.getKind() == kind::STRING_CONCAT
);
3669 for( unsigned i
=0; i
<s
.getNumChildren(); i
++ ) {
3670 if(s
[i
].isConst()) {
3671 CVC4::String
str( s
[0].getConst
< String
>() );
3672 //R-Consume, see Tianyi's thesis
3673 if(!applyRConsume(str
, r
)) {
3674 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Consume CONFLICT", true);
3679 //R-Split, see Tianyi's thesis
3680 if(i
== s
.getNumChildren() - 1) {
3682 Node memb2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
[i
], r
);
3683 XinR_with_exps
[itr
->first
] = itr
->second
;
3686 std::vector
< Node
> vec_s2
;
3687 for( unsigned j
=i
+1; j
<s
.getNumChildren(); j
++ ) {
3688 vec_s2
.push_back(s
[j
]);
3690 Node s2
= mkConcat(vec_s2
);
3691 conc
= applyRSplit(s1
, s2
, r
);
3692 if(conc
== d_true
) {
3694 } else if(conc
.isNull() || conc
== d_false
) {
3695 conc
= Node::null();
3696 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Split Conflict", true);
3700 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Split", true);
3712 bool TheoryStrings::checkMemberships2() {
3713 bool addedLemma
= false;
3714 d_nf_regexps
.clear();
3715 d_nf_regexps_exp
.clear();
3716 std::map
< Node
, std::vector
< Node
> > memb_with_exps
;
3717 std::map
< Node
, std::vector
< Node
> > XinR_with_exps
;
3719 addedLemma
= normalizePosMemberships( memb_with_exps
);
3722 addedLemma
|= checkMembershipsWithoutLength( memb_with_exps
, XinR_with_exps
);
3723 //TODO: check addlemma
3724 if (!addedLemma
&& !d_conflict
) {
3725 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= XinR_with_exps
.begin();
3726 itr
!= XinR_with_exps
.end(); ++itr
) {
3727 std::vector
<Node
> vec_or
;
3728 d_regexp_opr
.disjunctRegExp( itr
->first
, vec_or
);
3729 Node tmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_or
);
3730 Trace("regexp-process") << "Got r: " << itr
->first
<< " to " << tmp
<< std::endl
;
3732 if(r.getKind() == kind::REGEXP_STAR) {
3734 addedLemma = applyRLen(XinR_with_exps);
3740 Assert(false); //TODO:tmp
3747 void TheoryStrings::checkMemberships() {
3748 bool addedLemma
= false;
3749 bool changed
= false;
3750 std::vector
< Node
> processed
;
3751 std::vector
< Node
> cprocessed
;
3753 Trace("regexp-debug") << "Checking Memberships ... " << std::endl
;
3754 //if(options::stringEIT()) {
3755 //TODO: Opt for normal forms
3756 for(NodeListMap::const_iterator itr_xr
= d_pos_memberships
.begin();
3757 itr_xr
!= d_pos_memberships
.end(); ++itr_xr
) {
3758 bool spflag
= false;
3759 Node x
= (*itr_xr
).first
;
3760 NodeList
* lst
= (*itr_xr
).second
;
3761 Trace("regexp-debug") << "Checking Memberships for " << x
<< std::endl
;
3762 if(d_inter_index
.find(x
) == d_inter_index
.end()) {
3763 d_inter_index
[x
] = 0;
3765 int cur_inter_idx
= d_inter_index
[x
];
3766 if(cur_inter_idx
!= (int)lst
->size()) {
3767 if(lst
->size() == 1) {
3768 d_inter_cache
[x
] = (*lst
)[0];
3769 d_inter_index
[x
] = 1;
3770 Trace("regexp-debug") << "... only one choice " << std::endl
;
3771 } else if(lst
->size() > 1) {
3773 if(d_inter_cache
.find(x
) != d_inter_cache
.end()) {
3774 r
= d_inter_cache
[x
];
3780 NodeList::const_iterator itr_lst
= lst
->begin();
3781 for(int i
=0; i
<cur_inter_idx
; i
++) {
3784 Trace("regexp-debug") << "... staring from : " << cur_inter_idx
<< ", we have " << lst
->size() << std::endl
;
3785 for(;itr_lst
!= lst
->end(); ++itr_lst
) {
3787 r
= d_regexp_opr
.intersect(r
, r2
, spflag
);
3790 } else if(r
== d_emptyRegexp
) {
3791 std::vector
< Node
> vec_nodes
;
3793 for(NodeList::const_iterator itr2
= lst
->begin();
3794 itr2
!= itr_lst
; ++itr2
) {
3795 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, *itr2
);
3796 vec_nodes
.push_back( n
);
3799 sendInference(vec_nodes
, conc
, "INTERSECT CONFLICT", true);
3808 if(!d_conflict
&& !spflag
) {
3809 d_inter_cache
[x
] = r
;
3810 d_inter_index
[x
] = (int)lst
->size();
3817 Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma
<< std::endl
;
3819 for( unsigned i
=0; i
<d_regexp_memberships
.size(); i
++ ) {
3820 //check regular expression membership
3821 Node assertion
= d_regexp_memberships
[i
];
3822 if( d_regexp_ucached
.find(assertion
) == d_regexp_ucached
.end()
3823 && d_regexp_ccached
.find(assertion
) == d_regexp_ccached
.end() ) {
3824 Trace("strings-regexp") << "We have regular expression assertion : " << assertion
<< std::endl
;
3825 Node atom
= assertion
.getKind()==kind::NOT
? assertion
[0] : assertion
;
3826 bool polarity
= assertion
.getKind()!=kind::NOT
;
3830 std::vector
< Node
> rnfexp
;
3832 if(options::stringOpt1()) {
3834 x
= getNormalString( x
, rnfexp
);
3837 if(!d_regexp_opr
.checkConstRegExp(r
)) {
3838 r
= getNormalSymRegExp(r
, rnfexp
);
3841 Trace("strings-regexp-nf") << "Term " << atom
<< " is normalized to " << x
<< " IN " << r
<< std::endl
;
3843 Node tmp
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
) );
3848 d_regexp_ccached
.insert(assertion
);
3850 } else if(tmp
== d_false
) {
3851 Node antec
= mkRegExpAntec(assertion
, mkExplain(rnfexp
));
3852 Node conc
= Node::null();
3853 sendLemma(antec
, conc
, "REGEXP NF Conflict");
3861 flag
= checkPDerivative(x
, r
, atom
, addedLemma
, processed
, cprocessed
, rnfexp
);
3862 if(options::stringOpt2() && flag
) {
3863 if(d_regexp_opr
.checkConstRegExp(r
) && x
.getKind()==kind::STRING_CONCAT
) {
3864 std::vector
< std::pair
< Node
, Node
> > vec_can
;
3865 d_regexp_opr
.splitRegExp(r
, vec_can
);
3866 //TODO: lazy cache or eager?
3867 std::vector
< Node
> vec_or
;
3868 std::vector
< Node
> vec_s2
;
3869 for(unsigned int s2i
=1; s2i
<x
.getNumChildren(); s2i
++) {
3870 vec_s2
.push_back(x
[s2i
]);
3873 Node s2
= mkConcat(vec_s2
);
3874 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
3875 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
3876 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
3877 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
3878 vec_or
.push_back( c
);
3880 Node conc
= vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
3881 //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
3882 Node antec
= mkRegExpAntec(atom
, mkExplain(rnfexp
));
3883 if(conc
== d_true
) {
3885 cprocessed
.push_back( assertion
);
3887 processed
.push_back( assertion
);
3890 sendLemma(antec
, conc
, "RegExp-CST-SP");
3897 if(! options::stringExp()) {
3898 throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
3902 //check if the term is atomic
3903 Node xr
= getRepresentative( x
);
3904 //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
3905 //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
3907 if( true || r
.getKind()!=kind::REGEXP_STAR
|| ( d_normal_forms
[xr
].size()==1 && x
.getKind()!=kind::STRING_CONCAT
) ){
3908 Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr
<< std::endl
;
3909 //if so, do simple unrolling
3910 std::vector
< Node
> nvec
;
3912 /*if(xr.isConst()) {
3913 Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r) );
3914 if(tmp==d_true || tmp==d_false) {
3916 tmp = tmp==d_true? d_false : d_true;
3918 nvec.push_back( tmp );
3923 d_regexp_opr
.simplify(atom
, nvec
, polarity
);
3925 Node antec
= assertion
;
3926 if(d_regexp_ant
.find(assertion
) != d_regexp_ant
.end()) {
3927 antec
= d_regexp_ant
[assertion
];
3928 for(std::vector
< Node
>::const_iterator itr
=nvec
.begin(); itr
<nvec
.end(); itr
++) {
3929 if(itr
->getKind() == kind::STRING_IN_REGEXP
) {
3930 if(d_regexp_ant
.find( *itr
) == d_regexp_ant
.end()) {
3931 d_regexp_ant
[ *itr
] = antec
;
3936 antec
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, antec
, mkExplain(rnfexp
)) );
3937 Node conc
= nvec
.size()==1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
3938 conc
= Rewriter::rewrite(conc
);
3939 sendLemma( antec
, conc
, "REGEXP" );
3942 cprocessed
.push_back( assertion
);
3944 processed
.push_back( assertion
);
3946 //d_regexp_ucached[assertion] = true;
3948 Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr
<< " = ";
3949 for( unsigned j
=0; j
<d_normal_forms
[xr
].size(); j
++ ){
3950 Trace("strings-regexp") << d_normal_forms
[xr
][j
] << " ";
3952 Trace("strings-regexp") << ", polarity = " << polarity
<< std::endl
;
3953 //otherwise, distribute unrolling over parts
3956 if( d_normal_forms
[xr
].size()>1 ){
3957 p1
= d_normal_forms
[xr
][0];
3958 std::vector
< Node
> cc
;
3959 cc
.insert( cc
.begin(), d_normal_forms
[xr
].begin() + 1, d_normal_forms
[xr
].end() );
3960 p2
= mkConcat( cc
);
3963 Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl
;
3964 std::vector
< Node
> antec
;
3965 std::vector
< Node
> antecn
;
3966 antec
.insert( antec
.begin(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
3968 antec
.push_back( x
.eqNode( xr
) );
3970 antecn
.push_back( assertion
);
3971 Node ant
= mkExplain( antec
, antecn
);
3972 Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl
;
3975 if( d_normal_forms
[xr
].size()==0 ){
3977 }else if( d_normal_forms
[xr
].size()==1 ){
3978 Trace("strings-regexp-debug") << "Case 1\n";
3979 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
);
3981 Trace("strings-regexp-debug") << "Case 2\n";
3982 std::vector
< Node
> conc_c
;
3983 Node s11
= mkSkolemS( "s11" );
3984 Node s12
= mkSkolemS( "s12" );
3985 Node s21
= mkSkolemS( "s21" );
3986 Node s22
= mkSkolemS( "s22" );
3987 conc
= p1
.eqNode( mkConcat(s11
, s12
) );
3988 conc_c
.push_back(conc
);
3989 conc
= p2
.eqNode( mkConcat(s21
, s22
) );
3990 conc_c
.push_back(conc
);
3991 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
);
3992 conc_c
.push_back(conc
);
3993 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]);
3994 conc_c
.push_back(conc
);
3995 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
);
3996 conc_c
.push_back(conc
);
3997 conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, conc_c
));
3998 Node eqz
= Rewriter::rewrite(x
.eqNode(d_emptyString
));
3999 conc
= NodeManager::currentNM()->mkNode(kind::OR
, eqz
, conc
);
4000 d_pending_req_phase
[eqz
] = true;
4003 if( d_normal_forms
[xr
].size()==0 ){
4005 }else if( d_normal_forms
[xr
].size()==1 ){
4006 Trace("strings-regexp-debug") << "Case 3\n";
4007 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
).negate();
4009 Trace("strings-regexp-debug") << "Case 4\n";
4010 Node len1
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p1
);
4011 Node len2
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p2
);
4012 Node bi
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4013 Node bj
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4014 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, bi
, bj
);
4015 Node g1
= NodeManager::currentNM()->mkNode(kind::AND
,
4016 NodeManager::currentNM()->mkNode(kind::GEQ
, bi
, d_zero
),
4017 NodeManager::currentNM()->mkNode(kind::GEQ
, len1
, bi
),
4018 NodeManager::currentNM()->mkNode(kind::GEQ
, bj
, d_zero
),
4019 NodeManager::currentNM()->mkNode(kind::GEQ
, len2
, bj
));
4020 Node s11
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, d_zero
, bi
);
4021 Node s12
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, bi
, NodeManager::currentNM()->mkNode(kind::MINUS
, len1
, bi
));
4022 Node s21
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, d_zero
, bj
);
4023 Node s22
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, bj
, NodeManager::currentNM()->mkNode(kind::MINUS
, len2
, bj
));
4024 Node cc1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
).negate();
4025 Node cc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]).negate();
4026 Node cc3
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
).negate();
4027 conc
= NodeManager::currentNM()->mkNode(kind::OR
, cc1
, cc2
, cc3
);
4028 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
4029 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
4030 conc
= NodeManager::currentNM()->mkNode(kind::AND
, x
.eqNode(d_emptyString
).negate(), conc
);
4034 ant
= mkRegExpAntec(assertion
, ant
);
4035 sendLemma(ant
, conc
, "REGEXP CSTAR");
4037 if( conc
==d_false
){
4038 d_regexp_ccached
.insert( assertion
);
4040 cprocessed
.push_back( assertion
);
4043 d_regexp_ccached
.insert(assertion
);
4055 for( unsigned i
=0; i
<processed
.size(); i
++ ) {
4056 d_regexp_ucached
.insert(processed
[i
]);
4058 for( unsigned i
=0; i
<cprocessed
.size(); i
++ ) {
4059 d_regexp_ccached
.insert(cprocessed
[i
]);
4065 bool TheoryStrings::checkPDerivative(Node x
, Node r
, Node atom
, bool &addedLemma
,
4066 std::vector
< Node
> &processed
, std::vector
< Node
> &cprocessed
, std::vector
< Node
> &nf_exp
) {
4067 /*if(d_opt_regexp_gcd) {
4068 if(d_membership_length.find(atom) == d_membership_length.end()) {
4069 addedLemma = addMembershipLength(atom);
4070 d_membership_length[atom] = true;
4072 Trace("strings-regexp") << "Membership length is already added." << std::endl;
4075 Node antnf
= mkExplain(nf_exp
);
4077 if(areEqual(x
, d_emptyString
)) {
4079 switch(d_regexp_opr
.delta(r
, exp
)) {
4081 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
4082 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
4083 sendLemma(antec
, exp
, "RegExp Delta");
4085 d_regexp_ccached
.insert(atom
);
4089 d_regexp_ccached
.insert(atom
);
4093 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
4094 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
4095 Node conc
= Node::null();
4096 sendLemma(antec
, conc
, "RegExp Delta CONFLICT");
4098 d_regexp_ccached
.insert(atom
);
4106 /*Node xr = getRepresentative( x );
4108 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
4109 Node nn = Rewriter::rewrite( n );
4111 d_regexp_ccached.insert(atom);
4113 } else if(nn == d_false) {
4114 Node antec = mkRegExpAntec(atom, x.eqNode(xr));
4115 Node conc = Node::null();
4116 sendLemma(antec, conc, "RegExp Delta CONFLICT");
4118 d_regexp_ccached.insert(atom);
4122 Node sREant
= mkRegExpAntec(atom
, d_true
);
4123 sREant
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, sREant
, antnf
));
4124 if(deriveRegExp( x
, r
, sREant
)) {
4126 processed
.push_back( atom
);
4133 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex
* ti
, std::vector
< Node
>& vecc
) {
4134 Node n
= ti
->d_data
;
4136 //construct the constant
4137 Node c
= mkConcat( vecc
);
4138 if( !areEqual( n
, c
) ){
4139 Trace("strings-debug") << "Constant eqc : " << c
<< " for " << n
<< std::endl
;
4140 Trace("strings-debug") << " ";
4141 for( unsigned i
=0; i
<vecc
.size(); i
++ ){
4142 Trace("strings-debug") << vecc
[i
] << " ";
4144 Trace("strings-debug") << std::endl
;
4146 unsigned countc
= 0;
4147 std::vector
< Node
> exp
;
4148 while( count
<n
.getNumChildren() ){
4149 while( count
<n
.getNumChildren() && areEqual( n
[count
], d_emptyString
) ){
4150 addToExplanation( n
[count
], d_emptyString
, exp
);
4153 if( count
<n
.getNumChildren() ){
4154 Trace("strings-debug") << "...explain " << n
[count
] << " " << vecc
[countc
] << std::endl
;
4155 if( !areEqual( n
[count
], vecc
[countc
] ) ){
4156 Node nrr
= getRepresentative( n
[count
] );
4157 Assert( !d_eqc_to_const_exp
[nrr
].isNull() );
4158 addToExplanation( n
[count
], d_eqc_to_const_base
[nrr
], exp
);
4159 exp
.push_back( d_eqc_to_const_exp
[nrr
] );
4161 addToExplanation( n
[count
], vecc
[countc
], exp
);
4167 //exp contains an explanation of n==c
4168 Assert( countc
==vecc
.size() );
4170 sendInference( exp
, n
.eqNode( c
), "I_CONST_MERGE" );
4172 }else if( !hasProcessed() ){
4173 Node nr
= getRepresentative( n
);
4174 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( nr
);
4175 if( it
==d_eqc_to_const
.end() ){
4176 Trace("strings-debug") << "Set eqc const " << n
<< " to " << c
<< std::endl
;
4177 d_eqc_to_const
[nr
] = c
;
4178 d_eqc_to_const_base
[nr
] = n
;
4179 d_eqc_to_const_exp
[nr
] = mkAnd( exp
);
4180 }else if( c
!=it
->second
){
4182 Trace("strings-debug") << "Conflict, other constant was " << it
->second
<< ", this constant was " << c
<< std::endl
;
4183 if( d_eqc_to_const_exp
[nr
].isNull() ){
4184 // n==c ^ n == c' => false
4185 addToExplanation( n
, it
->second
, exp
);
4187 // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
4188 exp
.push_back( d_eqc_to_const_exp
[nr
] );
4189 addToExplanation( n
, d_eqc_to_const_base
[nr
], exp
);
4191 sendInference( exp
, d_false
, "I_CONST_CONFLICT" );
4194 Trace("strings-debug") << "Duplicate constant." << std::endl
;
4199 for( std::map
< Node
, TermIndex
>::iterator it
= ti
->d_children
.begin(); it
!= ti
->d_children
.end(); ++it
){
4200 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( it
->first
);
4201 if( itc
!=d_eqc_to_const
.end() ){
4202 vecc
.push_back( itc
->second
);
4203 checkConstantEquivalenceClasses( &it
->second
, vecc
);
4205 if( hasProcessed() ){
4212 void TheoryStrings::checkExtendedFuncs() {
4213 if( options::stringExp() ){
4214 checkExtfReduction( 2 );
4216 if( !hasProcessed() ){
4217 //collect all remaining extended functions
4218 std::vector
< Node
> pnContains
;
4219 std::map
< bool, std::vector
< Node
> > pnMem
;
4220 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
4222 Node n
= (*it
).first
;
4223 if( n
.getKind()==kind::STRING_STRCTN
) {
4224 if( d_extf_pol
[n
]!=1 ){
4225 Assert( d_extf_pol
[n
]==-1 );
4226 pnContains
.push_back( n
);
4228 }else if( n
.getKind()==kind::STRING_IN_REGEXP
) {
4229 bool pol
= d_extf_pol
[n
]==1;
4230 Assert( d_extf_pol
[n
]==1 || d_extf_pol
[n
]==-1 );
4231 pnMem
[pol
].push_back( n
);
4235 Trace("strings-process-debug") << "Checking negative contains..." << std::endl
;
4236 checkNegContains( pnContains
);
4237 Trace("strings-process-debug") << "Done check negative contain constraints, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
4238 if( !hasProcessed() ) {
4239 Trace("strings-process") << "Adding memberships..." << std::endl
;
4240 //add all non-evaluated memberships
4241 for( std::map
< bool, std::vector
< Node
> >::iterator it
=pnMem
.begin(); it
!= pnMem
.end(); ++it
){
4242 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
4243 Trace("strings-process-debug") << " add membership : " << it
->second
[i
] << ", pol = " << it
->first
<< std::endl
;
4244 addMembership( it
->first
? it
->second
[i
] : it
->second
[i
].negate() );
4247 Trace("strings-process") << "Checking memberships..." << std::endl
;
4249 Trace("strings-process") << "Done check memberships, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
4254 void TheoryStrings::checkNegContains( std::vector
< Node
>& negContains
) {
4255 for( unsigned i
=0; i
<negContains
.size(); i
++ ){
4256 Node atom
= negContains
[i
];
4257 Trace("strings-ctn") << "We have negative contain assertion : (not " << atom
<< " )" << std::endl
;
4258 //should have already reduced these things by now
4259 Assert( !areEqual( atom
[1], d_emptyString
) );
4260 Assert( !areEqual( atom
[1], atom
[0] ) );
4263 if(options::stringExp()) {
4264 for( unsigned i
=0; i
<negContains
.size(); i
++ ){
4265 Node atom
= negContains
[i
];
4268 std::vector
< Node
> lexp
;
4269 Node lenx
= getLength( x
, lexp
);
4270 Node lens
= getLength( s
, lexp
);
4271 if( areEqual(lenx
, lens
) ){
4272 if(d_neg_ctn_eqlen
.find(atom
) == d_neg_ctn_eqlen
.end()) {
4273 lexp
.push_back( lenx
.eqNode(lens
) );
4274 lexp
.push_back( atom
.negate() );
4275 Node xneqs
= x
.eqNode(s
).negate();
4276 d_neg_ctn_eqlen
.insert( atom
);
4277 sendInference( lexp
, xneqs
, "NEG-CTN-EQL", true );
4279 }else if( !areDisequal( lenx
, lens
) ){
4280 if(d_neg_ctn_ulen
.find(atom
) == d_neg_ctn_ulen
.end()) {
4281 lenx
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, x
);
4282 lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
4283 d_neg_ctn_ulen
.insert( atom
);
4284 sendSplit( lenx
, lens
, "NEG-CTN-SP" );
4287 if(d_neg_ctn_cached
.find(atom
) == d_neg_ctn_cached
.end()) {
4288 lenx
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, x
);
4289 lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
4290 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4291 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
4292 Node g1
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode( kind::GEQ
, b1
, d_zero
),
4293 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode( kind::MINUS
, lenx
, lens
), b1
) ) );
4294 Node b2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4295 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, x
, NodeManager::currentNM()->mkNode( kind::PLUS
, b1
, b2
), d_one
);
4296 Node s5
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, s
, b2
, d_one
);
4298 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b2
);//, s1, s3, s4, s6);
4300 std::vector
< Node
> vec_nodes
;
4301 Node cc
= NodeManager::currentNM()->mkNode( kind::GEQ
, b2
, d_zero
);
4302 vec_nodes
.push_back(cc
);
4303 cc
= NodeManager::currentNM()->mkNode( kind::GT
, lens
, b2
);
4304 vec_nodes
.push_back(cc
);
4306 cc
= s2
.eqNode(s5
).negate();
4307 vec_nodes
.push_back(cc
);
4309 Node conc
= NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
4310 conc
= NodeManager::currentNM()->mkNode( kind::EXISTS
, b2v
, conc
);
4311 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, g1
, conc
);
4312 conc
= NodeManager::currentNM()->mkNode( kind::FORALL
, b1v
, conc
);
4313 Node xlss
= NodeManager::currentNM()->mkNode( kind::GT
, lens
, lenx
);
4314 conc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR
, xlss
, conc
) );
4316 d_neg_ctn_cached
.insert( atom
);
4317 std::vector
< Node
> exp
;
4318 exp
.push_back( atom
.negate() );
4319 sendInference( d_empty_vec
, exp
, conc
, "NEG-CTN-BRK", true );
4320 //d_pending_req_phase[xlss] = true;
4325 if( !negContains
.empty() ){
4326 throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
4331 CVC4::String
TheoryStrings::getHeadConst( Node x
) {
4333 return x
.getConst
< String
>();
4334 } else if( x
.getKind() == kind::STRING_CONCAT
) {
4335 if( x
[0].isConst() ) {
4336 return x
[0].getConst
< String
>();
4338 return d_emptyString
.getConst
< String
>();
4341 return d_emptyString
.getConst
< String
>();
4345 bool TheoryStrings::addMembershipLength(Node atom
) {
4349 /*std::vector< int > co;
4351 for(unsigned int k=0; k<lts.size(); ++k) {
4352 if(lts[k].isConst() && lts[k].getType().isInteger()) {
4353 int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
4354 co[0] += cols[k].size() * len;
4356 co.push_back( cols[k].size() );
4360 for(unsigned k=1; k<co.size(); ++k) {
4361 g_co = gcd(g_co, co[k]);
4366 bool TheoryStrings::deriveRegExp( Node x
, Node r
, Node ant
) {
4368 Assert(x
!= d_emptyString
);
4369 Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x
<< ", r= " << r
<< std::endl
;
4371 // Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
4372 // Node r = Rewriter::rewrite( n );
4374 // sendLemma(ant, r, "REGEXP REWRITE");
4378 CVC4::String s
= getHeadConst( x
);
4379 if( !s
.isEmptyString() && d_regexp_opr
.checkConstRegExp( r
) ) {
4380 Node conc
= Node::null();
4383 for(unsigned i
=0; i
<s
.size(); ++i
) {
4384 CVC4::String c
= s
.substr(i
, 1);
4386 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
4390 } else if(rt
== 2) {
4399 Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
4402 Assert( x
.getKind() == kind::STRING_CONCAT
);
4403 std::vector
< Node
> vec_nodes
;
4404 for(unsigned int i
=1; i
<x
.getNumChildren(); ++i
) {
4405 vec_nodes
.push_back( x
[i
] );
4407 Node left
= mkConcat( vec_nodes
);
4408 left
= Rewriter::rewrite( left
);
4409 conc
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, left
, dc
);
4411 /*std::vector< Node > sdc;
4412 d_regexp_opr.simplify(conc, sdc, true);
4413 if(sdc.size() == 1) {
4416 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
4420 sendLemma(ant
, conc
, "RegExp-Derive");
4427 void TheoryStrings::addMembership(Node assertion
) {
4428 bool polarity
= assertion
.getKind() != kind::NOT
;
4429 TNode atom
= polarity
? assertion
: assertion
[0];
4434 NodeListMap::iterator itr_xr
= d_pos_memberships
.find( x
);
4435 if( itr_xr
== d_pos_memberships
.end() ){
4436 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
4437 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
4438 d_pos_memberships
.insertDataFromContextMemory( x
, lst
);
4440 lst
= (*itr_xr
).second
;
4443 for( NodeList::const_iterator itr
= lst
->begin(); itr
!= lst
->end(); ++itr
) {
4448 lst
->push_back( r
);
4449 } else if(!options::stringIgnNegMembership()) {
4450 /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
4452 Node r2 = d_regexp_opr.complement(r, rt);
4453 Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
4456 NodeListMap::iterator itr_xr
= d_neg_memberships
.find( x
);
4457 if( itr_xr
== d_neg_memberships
.end() ){
4458 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
4459 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
4460 d_neg_memberships
.insertDataFromContextMemory( x
, lst
);
4462 lst
= (*itr_xr
).second
;
4465 for( NodeList::const_iterator itr
= lst
->begin(); itr
!= lst
->end(); ++itr
) {
4470 lst
->push_back( r
);
4473 if(polarity
|| !options::stringIgnNegMembership()) {
4474 d_regexp_memberships
.push_back( assertion
);
4478 Node
TheoryStrings::getNormalString( Node x
, std::vector
<Node
> &nf_exp
){
4480 Node xr
= getRepresentative( x
);
4481 if( d_normal_forms
.find( xr
) != d_normal_forms
.end() ){
4482 Node ret
= mkConcat( d_normal_forms
[xr
] );
4483 nf_exp
.insert( nf_exp
.end(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
4484 addToExplanation( x
, d_normal_forms_base
[xr
], nf_exp
);
4485 Trace("strings-debug") << "Term: " << x
<< " has a normal form " << ret
<< std::endl
;
4488 if(x
.getKind() == kind::STRING_CONCAT
) {
4489 std::vector
< Node
> vec_nodes
;
4490 for(unsigned i
=0; i
<x
.getNumChildren(); i
++) {
4491 Node nc
= getNormalString( x
[i
], nf_exp
);
4492 vec_nodes
.push_back( nc
);
4494 return mkConcat( vec_nodes
);
4501 Node
TheoryStrings::getNormalSymRegExp(Node r
, std::vector
<Node
> &nf_exp
) {
4503 switch( r
.getKind() ) {
4504 case kind::REGEXP_EMPTY
:
4505 case kind::REGEXP_SIGMA
:
4507 case kind::STRING_TO_REGEXP
: {
4508 if(!r
[0].isConst()) {
4509 Node tmp
= getNormalString( r
[0], nf_exp
);
4511 ret
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, tmp
);
4516 case kind::REGEXP_CONCAT
: {
4517 std::vector
< Node
> vec_nodes
;
4518 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4519 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4521 ret
= mkConcat(vec_nodes
);
4524 case kind::REGEXP_UNION
: {
4525 std::vector
< Node
> vec_nodes
;
4526 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4527 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4529 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
) );
4532 case kind::REGEXP_INTER
: {
4533 std::vector
< Node
> vec_nodes
;
4534 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4535 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4537 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER
, vec_nodes
) );
4540 case kind::REGEXP_STAR
: {
4541 ret
= getNormalSymRegExp( r
[0], nf_exp
);
4542 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, ret
) );
4545 //case kind::REGEXP_PLUS:
4546 //case kind::REGEXP_OPT:
4547 //case kind::REGEXP_RANGE:
4549 Trace("strings-error") << "Unsupported term: " << r
<< " in normalization SymRegExp." << std::endl
;
4551 //return Node::null();
4558 //// Finite Model Finding
4560 Node
TheoryStrings::getNextDecisionRequest() {
4561 if( options::stringFMF() && !d_conflict
){
4562 Node in_var_lsum
= d_input_var_lsum
.get();
4563 //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
4564 //initialize the term we will minimize
4565 if( in_var_lsum
.isNull() && !d_input_vars
.empty() ){
4566 Trace("strings-fmf-debug") << "Input variables: ";
4567 std::vector
< Node
> ll
;
4568 for(NodeSet::key_iterator itr
= d_input_vars
.key_begin();
4569 itr
!= d_input_vars
.key_end(); ++itr
) {
4570 Trace("strings-fmf-debug") << " " << (*itr
) ;
4571 ll
.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr
) );
4573 Trace("strings-fmf-debug") << std::endl
;
4574 in_var_lsum
= ll
.size()==1 ? ll
[0] : NodeManager::currentNM()->mkNode( kind::PLUS
, ll
);
4575 in_var_lsum
= Rewriter::rewrite( in_var_lsum
);
4576 d_input_var_lsum
.set( in_var_lsum
);
4578 if( !in_var_lsum
.isNull() ){
4579 //Trace("strings-fmf") << "Get next decision request." << std::endl;
4580 //check if we need to decide on something
4581 int decideCard
= d_curr_cardinality
.get();
4582 if( d_cardinality_lits
.find( decideCard
)!=d_cardinality_lits
.end() ){
4584 Node cnode
= d_cardinality_lits
[ d_curr_cardinality
.get() ];
4585 if( d_valuation
.hasSatValue( cnode
, value
) ) {
4587 d_curr_cardinality
.set( d_curr_cardinality
.get() + 1 );
4588 decideCard
= d_curr_cardinality
.get();
4589 Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl
;
4592 Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl
;
4595 Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl
;
4598 if( decideCard
!=-1 ){
4599 if( d_cardinality_lits
.find( decideCard
)==d_cardinality_lits
.end() ){
4600 Node lit
= NodeManager::currentNM()->mkNode( kind::LEQ
, in_var_lsum
, NodeManager::currentNM()->mkConst( Rational( decideCard
) ) );
4601 lit
= Rewriter::rewrite( lit
);
4602 d_cardinality_lits
[decideCard
] = lit
;
4603 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lit
, lit
.negate() );
4604 Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem
<< ", decideCard = " << decideCard
<< std::endl
;
4605 d_out
->lemma( lem
);
4606 d_out
->requirePhase( lit
, true );
4608 Node lit
= d_cardinality_lits
[ decideCard
];
4609 Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit
<< std::endl
;
4615 return Node::null();
4618 void TheoryStrings::collectExtendedFuncTerms( Node n
, std::map
< Node
, bool >& visited
) {
4619 if( visited
.find( n
)==visited
.end() ){
4621 if( n
.getKind()==kind::STRING_SUBSTR
|| n
.getKind()==kind::STRING_STRIDOF
||
4622 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
4623 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
4624 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
4625 if( d_ext_func_terms
.find( n
)==d_ext_func_terms
.end() ){
4626 Trace("strings-extf-debug2") << "Found extended function : " << n
<< std::endl
;
4627 d_ext_func_terms
[n
] = true;
4630 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
4631 collectExtendedFuncTerms( n
[i
], visited
);
4637 TheoryStrings::Statistics::Statistics():
4638 d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
4639 d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
4640 d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
4641 d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
4642 d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
4644 smtStatisticsRegistry()->registerStat(&d_splits
);
4645 smtStatisticsRegistry()->registerStat(&d_eq_splits
);
4646 smtStatisticsRegistry()->registerStat(&d_deq_splits
);
4647 smtStatisticsRegistry()->registerStat(&d_loop_lemmas
);
4648 smtStatisticsRegistry()->registerStat(&d_new_skolems
);
4651 TheoryStrings::Statistics::~Statistics(){
4652 smtStatisticsRegistry()->unregisterStat(&d_splits
);
4653 smtStatisticsRegistry()->unregisterStat(&d_eq_splits
);
4654 smtStatisticsRegistry()->unregisterStat(&d_deq_splits
);
4655 smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas
);
4656 smtStatisticsRegistry()->unregisterStat(&d_new_skolems
);
4659 }/* CVC4::theory::strings namespace */
4660 }/* CVC4::theory namespace */
4661 }/* CVC4 namespace */