1 /********************* */
2 /*! \file theory_strings.cpp
4 ** Original author: Tianyi Liang
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Martin Brain <>, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Implementation of the theory of strings.
14 ** Implementation of the theory of strings.
18 #include "theory/strings/theory_strings.h"
19 #include "theory/valuation.h"
20 #include "expr/kind.h"
21 #include "theory/rewriter.h"
22 #include "expr/command.h"
23 #include "theory/theory_model.h"
24 #include "smt/logic_exception.h"
25 #include "theory/strings/options.h"
26 #include "theory/strings/type_enumerator.h"
27 #include "theory/strings/theory_strings_rewriter.h"
31 using namespace CVC4::context
;
37 Node
TheoryStrings::TermIndex::add( Node n
, unsigned index
, TheoryStrings
* t
, Node er
, std::vector
< Node
>& c
) {
38 if( index
==n
.getNumChildren() ){
39 if( d_data
.isNull() ){
44 Assert( index
<n
.getNumChildren() );
45 Node nir
= t
->getRepresentative( n
[index
] );
46 //if it is empty, and doing CONCAT, ignore
47 if( nir
==er
&& n
.getKind()==kind::STRING_CONCAT
){
48 return add( n
, index
+1, t
, er
, c
);
51 return d_children
[nir
].add( n
, index
+1, t
, er
, c
);
57 TheoryStrings::TheoryStrings(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
)
58 : Theory(THEORY_STRINGS
, c
, u
, out
, valuation
, logicInfo
),
61 d_equalityEngine(d_notify
, c
, "theory::strings::TheoryStrings", true),
67 d_length_intro_vars(u
),
68 d_registered_terms_cache(u
),
71 d_extf_infer_cache(c
),
74 d_proxy_var_to_length(u
),
79 d_regexp_memberships(c
),
86 d_processed_memberships(c
),
90 d_cardinality_lits(u
),
91 d_curr_cardinality(c
, 0)
93 // The kinds we are treating as function application in congruence
94 d_equalityEngine
.addFunctionKind(kind::STRING_IN_REGEXP
);
95 d_equalityEngine
.addFunctionKind(kind::STRING_LENGTH
);
96 d_equalityEngine
.addFunctionKind(kind::STRING_CONCAT
);
97 d_equalityEngine
.addFunctionKind(kind::STRING_STRCTN
);
98 d_equalityEngine
.addFunctionKind(kind::STRING_SUBSTR
);
99 d_equalityEngine
.addFunctionKind(kind::STRING_ITOS
);
100 d_equalityEngine
.addFunctionKind(kind::STRING_STOI
);
101 if( options::stringLazyPreproc() ){
102 d_equalityEngine
.addFunctionKind(kind::STRING_U16TOS
);
103 d_equalityEngine
.addFunctionKind(kind::STRING_STOU16
);
104 d_equalityEngine
.addFunctionKind(kind::STRING_U32TOS
);
105 d_equalityEngine
.addFunctionKind(kind::STRING_STOU32
);
106 d_equalityEngine
.addFunctionKind(kind::STRING_STRIDOF
);
107 d_equalityEngine
.addFunctionKind(kind::STRING_STRREPL
);
110 d_zero
= NodeManager::currentNM()->mkConst( Rational( 0 ) );
111 d_one
= NodeManager::currentNM()->mkConst( Rational( 1 ) );
112 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
113 std::vector
< Node
> nvec
;
114 d_emptyRegexp
= NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY
, nvec
);
115 d_true
= NodeManager::currentNM()->mkConst( true );
116 d_false
= NodeManager::currentNM()->mkConst( false );
121 TheoryStrings::~TheoryStrings() {
125 Node
TheoryStrings::getRepresentative( Node t
) {
126 if( d_equalityEngine
.hasTerm( t
) ){
127 return d_equalityEngine
.getRepresentative( t
);
133 bool TheoryStrings::hasTerm( Node a
){
134 return d_equalityEngine
.hasTerm( a
);
137 bool TheoryStrings::areEqual( Node a
, Node b
){
140 }else if( hasTerm( a
) && hasTerm( b
) ){
141 return d_equalityEngine
.areEqual( a
, b
);
147 bool TheoryStrings::areDisequal( Node a
, Node b
){
151 if( a
.getType().isString() ) {
152 for( unsigned i
=0; i
<2; i
++ ) {
153 Node ac
= a
.getKind()==kind::STRING_CONCAT
? a
[i
==0 ? 0 : a
.getNumChildren()-1] : a
;
154 Node bc
= b
.getKind()==kind::STRING_CONCAT
? b
[i
==0 ? 0 : b
.getNumChildren()-1] : b
;
155 if( ac
.isConst() && bc
.isConst() ){
156 CVC4::String as
= ac
.getConst
<String
>();
157 CVC4::String bs
= bc
.getConst
<String
>();
158 int slen
= as
.size() > bs
.size() ? bs
.size() : as
.size();
159 bool flag
= i
== 1 ? as
.rstrncmp(bs
, slen
): as
.strncmp(bs
, slen
);
166 if( hasTerm( a
) && hasTerm( b
) ) {
167 if( d_equalityEngine
.areDisequal( a
, b
, false ) ){
175 Node
TheoryStrings::getLengthExp( Node t
, std::vector
< Node
>& exp
, Node te
) {
176 Assert( areEqual( t
, te
) );
177 EqcInfo
* ei
= getOrMakeEqcInfo( t
, false );
178 Node length_term
= ei
? ei
->d_length_term
: Node::null();
179 if( length_term
.isNull() ){
180 //typically shouldnt be necessary
183 Debug("strings") << "TheoryStrings::getLengthTerm " << t
<< " is " << length_term
<< std::endl
;
184 addToExplanation( length_term
, te
, exp
);
185 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, length_term
) );
188 Node
TheoryStrings::getLength( Node t
, std::vector
< Node
>& exp
) {
189 return getLengthExp( t
, exp
, t
);
192 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
193 d_equalityEngine
.setMasterEqualityEngine(eq
);
196 void TheoryStrings::addSharedTerm(TNode t
) {
197 Debug("strings") << "TheoryStrings::addSharedTerm(): "
198 << t
<< " " << t
.getType().isBoolean() << endl
;
199 d_equalityEngine
.addTriggerTerm(t
, THEORY_STRINGS
);
200 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl
;
203 EqualityStatus
TheoryStrings::getEqualityStatus(TNode a
, TNode b
) {
204 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
205 if (d_equalityEngine
.areEqual(a
, b
)) {
206 // The terms are implied to be equal
207 return EQUALITY_TRUE
;
209 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
210 // The terms are implied to be dis-equal
211 return EQUALITY_FALSE
;
214 return EQUALITY_UNKNOWN
;
217 void TheoryStrings::propagate(Effort e
) {
218 // direct propagation now
221 bool TheoryStrings::propagate(TNode literal
) {
222 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< ")" << std::endl
;
223 // If already in conflict, no more propagation
225 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< "): already in conflict" << std::endl
;
229 bool ok
= d_out
->propagate(literal
);
237 void TheoryStrings::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
238 Debug("strings-explain") << "Explain " << literal
<< " " << d_conflict
<< std::endl
;
239 bool polarity
= literal
.getKind() != kind::NOT
;
240 TNode atom
= polarity
? literal
: literal
[0];
241 unsigned ps
= assumptions
.size();
242 std::vector
< TNode
> tassumptions
;
243 if (atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
244 if( atom
[0]!=atom
[1] ){
245 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, tassumptions
);
248 d_equalityEngine
.explainPredicate(atom
, polarity
, tassumptions
);
250 for( unsigned i
=0; i
<tassumptions
.size(); i
++ ){
251 if( std::find( assumptions
.begin(), assumptions
.end(), tassumptions
[i
] )==assumptions
.end() ){
252 assumptions
.push_back( tassumptions
[i
] );
255 Debug("strings-explain-debug") << "Explanation for " << literal
<< " was " << std::endl
;
256 for( unsigned i
=ps
; i
<assumptions
.size(); i
++ ){
257 Debug("strings-explain-debug") << " " << assumptions
[i
] << std::endl
;
261 Node
TheoryStrings::explain( TNode literal
){
262 std::vector
< TNode
> assumptions
;
263 explain( literal
, assumptions
);
264 if( assumptions
.empty() ){
266 }else if( assumptions
.size()==1 ){
267 return assumptions
[0];
269 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
273 /////////////////////////////////////////////////////////////////////////////
275 /////////////////////////////////////////////////////////////////////////////
278 void TheoryStrings::presolve() {
279 Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl
;
281 if(!options::stdASCII()) {
287 /////////////////////////////////////////////////////////////////////////////
289 /////////////////////////////////////////////////////////////////////////////
292 void TheoryStrings::collectModelInfo( TheoryModel
* m
, bool fullModel
) {
293 Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel
<< std::endl
;
294 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl
;
295 m
->assertEqualityEngine( &d_equalityEngine
);
297 std::vector
< Node
> nodes
;
298 getEquivalenceClasses( nodes
);
299 std::map
< Node
, Node
> processed
;
300 std::vector
< std::vector
< Node
> > col
;
301 std::vector
< Node
> lts
;
302 separateByLength( nodes
, col
, lts
);
303 //step 1 : get all values for known lengths
304 std::vector
< Node
> lts_values
;
305 std::map
< unsigned, bool > values_used
;
306 for( unsigned i
=0; i
<col
.size(); i
++ ) {
307 Trace("strings-model") << "Checking length for {";
308 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
310 Trace("strings-model") << ", ";
312 Trace("strings-model") << col
[i
][j
];
314 Trace("strings-model") << " } (length is " << lts
[i
] << ")" << std::endl
;
315 if( lts
[i
].isConst() ) {
316 lts_values
.push_back( lts
[i
] );
317 Assert(lts
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
318 unsigned lvalue
= lts
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt();
319 values_used
[ lvalue
] = true;
321 //get value for lts[i];
322 if( !lts
[i
].isNull() ){
323 Node v
= d_valuation
.getModelValue(lts
[i
]);
324 Trace("strings-model") << "Model value for " << lts
[i
] << " is " << v
<< std::endl
;
325 lts_values
.push_back( v
);
326 Assert(v
.getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
327 unsigned lvalue
= v
.getConst
<Rational
>().getNumerator().toUnsignedInt();
328 values_used
[ lvalue
] = true;
330 //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
332 lts_values
.push_back( Node::null() );
336 ////step 2 : assign arbitrary values for unknown lengths?
337 // confirmed by calculus invariant, see paper
338 Trace("strings-model") << "Assign to equivalence classes..." << std::endl
;
339 //step 3 : assign values to equivalence classes that are pure variables
340 for( unsigned i
=0; i
<col
.size(); i
++ ){
341 std::vector
< Node
> pure_eq
;
342 Trace("strings-model") << "The equivalence classes ";
343 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
344 Trace("strings-model") << col
[i
][j
] << " ";
345 //check if col[i][j] has only variables
346 EqcInfo
* ei
= getOrMakeEqcInfo( col
[i
][j
], false );
347 Node cst
= ei
? ei
->d_const_term
: Node::null();
349 Assert( d_normal_forms
.find( col
[i
][j
] )!=d_normal_forms
.end() );
350 if( d_normal_forms
[col
[i
][j
]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
351 pure_eq
.push_back( col
[i
][j
] );
354 processed
[col
[i
][j
]] = cst
;
357 Trace("strings-model") << "have length " << lts_values
[i
] << std::endl
;
359 //assign a new length if necessary
360 if( !pure_eq
.empty() ){
361 if( lts_values
[i
].isNull() ){
363 while( values_used
.find( lvalue
)!=values_used
.end() ){
366 Trace("strings-model") << "*** Decide to make length of " << lvalue
<< std::endl
;
367 lts_values
[i
] = NodeManager::currentNM()->mkConst( Rational( lvalue
) );
368 values_used
[ lvalue
] = true;
370 Trace("strings-model") << "Need to assign values of length " << lts_values
[i
] << " to equivalence classes ";
371 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
372 Trace("strings-model") << pure_eq
[j
] << " ";
374 Trace("strings-model") << std::endl
;
377 //use type enumerator
378 Assert(lts_values
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
379 StringEnumeratorLength
sel(lts_values
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt());
380 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
381 Assert( !sel
.isFinished() );
383 while( d_equalityEngine
.hasTerm( c
) ){
385 Assert( !sel
.isFinished() );
389 Trace("strings-model") << "*** Assigned constant " << c
<< " for " << pure_eq
[j
] << std::endl
;
390 processed
[pure_eq
[j
]] = c
;
391 m
->assertEquality( pure_eq
[j
], c
, true );
395 Trace("strings-model") << "String Model : Pure Assigned." << std::endl
;
396 //step 4 : assign constants to all other equivalence classes
397 for( unsigned i
=0; i
<nodes
.size(); i
++ ){
398 if( processed
.find( nodes
[i
] )==processed
.end() ){
399 Assert( d_normal_forms
.find( nodes
[i
] )!=d_normal_forms
.end() );
400 Trace("strings-model") << "Construct model for " << nodes
[i
] << " based on normal form ";
401 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
402 if( j
>0 ) Trace("strings-model") << " ++ ";
403 Trace("strings-model") << d_normal_forms
[nodes
[i
]][j
];
404 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
405 if( !r
.isConst() && processed
.find( r
)==processed
.end() ){
406 Trace("strings-model") << "(UNPROCESSED)";
409 Trace("strings-model") << std::endl
;
410 std::vector
< Node
> nc
;
411 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
412 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
413 Assert( r
.isConst() || processed
.find( r
)!=processed
.end() );
414 nc
.push_back(r
.isConst() ? r
: processed
[r
]);
416 Node cc
= mkConcat( nc
);
417 Assert( cc
.getKind()==kind::CONST_STRING
);
418 Trace("strings-model") << "*** Determined constant " << cc
<< " for " << nodes
[i
] << std::endl
;
419 processed
[nodes
[i
]] = cc
;
420 m
->assertEquality( nodes
[i
], cc
, true );
423 //Trace("strings-model") << "String Model : Assigned." << std::endl;
424 Trace("strings-model") << "String Model : Finished." << std::endl
;
427 /////////////////////////////////////////////////////////////////////////////
429 /////////////////////////////////////////////////////////////////////////////
432 void TheoryStrings::preRegisterTerm(TNode n
) {
433 if( d_registered_terms_cache
.find(n
) == d_registered_terms_cache
.end() ) {
434 //check for logic exceptions
435 if( !options::stringExp() ){
436 if( n
.getKind()==kind::STRING_STRIDOF
||
437 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
438 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
439 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
440 std::stringstream ss
;
441 ss
<< "Term of kind " << n
.getKind() << " not supported in default mode, try --strings-exp";
442 throw LogicException(ss
.str());
445 switch( n
.getKind() ) {
447 d_equalityEngine
.addTriggerEquality(n
);
450 case kind::STRING_IN_REGEXP
: {
451 d_out
->requirePhase(n
, true);
452 d_equalityEngine
.addTriggerPredicate(n
);
453 d_equalityEngine
.addTerm(n
[0]);
454 d_equalityEngine
.addTerm(n
[1]);
458 if( n
.getType().isString() ) {
461 if( n
.getKind() == kind::VARIABLE
&& options::stringFMF() ) {
462 d_input_vars
.insert(n
);
464 } else if (n
.getType().isBoolean()) {
465 // Get triggered for both equal and dis-equal
466 d_equalityEngine
.addTriggerPredicate(n
);
468 // Function applications/predicates
469 d_equalityEngine
.addTerm(n
);
473 d_registered_terms_cache
.insert(n
);
477 Node
TheoryStrings::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
482 void TheoryStrings::check(Effort e
) {
483 if (done() && !fullEffort(e
)) {
487 TimerStat::CodeTimer
checkTimer(d_checkTime
);
492 /*if(getLogicInfo().hasEverything()) {
493 WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n"
494 << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl;
498 if( !done() && !hasTerm( d_emptyString
) ) {
499 preRegisterTerm( d_emptyString
);
502 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
503 Trace("strings-check") << "Theory of strings, check : " << e
<< std::endl
;
504 while ( !done() && !d_conflict
) {
505 // Get all the assertions
506 Assertion assertion
= get();
507 TNode fact
= assertion
.assertion
;
509 Trace("strings-assertion") << "get assertion: " << fact
<< endl
;
510 polarity
= fact
.getKind() != kind::NOT
;
511 atom
= polarity
? fact
: fact
[0];
513 //run preprocess on memberships
514 if( options::stringLazyPreproc() ){
515 checkReduction( atom
, polarity
? 1 : -1, 0 );
518 //assert pending fact
519 assertPendingFact( atom
, polarity
, fact
);
523 if( e
== EFFORT_FULL
&& !d_conflict
&& !d_valuation
.needCheck() ) {
524 Trace("strings-check") << "Theory of strings full effort check " << std::endl
;
526 if(Trace
.isOn("strings-eqc")) {
527 for( unsigned t
=0; t
<2; t
++ ) {
528 eq::EqClassesIterator eqcs2_i
= eq::EqClassesIterator( &d_equalityEngine
);
529 Trace("strings-eqc") << (t
==0 ? "STRINGS:" : "OTHER:") << std::endl
;
530 while( !eqcs2_i
.isFinished() ){
531 Node eqc
= (*eqcs2_i
);
532 bool print
= (t
==0 && eqc
.getType().isString() ) || (t
==1 && !eqc
.getType().isString() );
534 eq::EqClassIterator eqc2_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
535 Trace("strings-eqc") << "Eqc( " << eqc
<< " ) : { ";
536 while( !eqc2_i
.isFinished() ) {
537 if( (*eqc2_i
)!=eqc
&& (*eqc2_i
).getKind()!=kind::EQUAL
){
538 Trace("strings-eqc") << (*eqc2_i
) << " ";
542 Trace("strings-eqc") << " } " << std::endl
;
543 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
545 Trace("strings-eqc-debug") << "* Length term : " << ei
->d_length_term
.get() << std::endl
;
546 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei
->d_cardinality_lem_k
.get() << std::endl
;
547 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei
->d_normalized_length
.get() << std::endl
;
552 Trace("strings-eqc") << std::endl
;
554 Trace("strings-eqc") << std::endl
;
557 bool addedLemma
= false;
560 Trace("strings-process") << "----check, next round---" << std::endl
;
562 Trace("strings-process") << "Done check init, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
563 if( !hasProcessed() ){
564 checkExtendedFuncsEval();
565 Trace("strings-process") << "Done check extended functions eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
566 if( !hasProcessed() ){
568 Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
569 if( !hasProcessed() ){
571 Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
572 if( !hasProcessed() ){
573 if( options::stringEagerLen() ){
575 Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
577 if( !hasProcessed() ){
578 checkExtendedFuncs();
579 Trace("strings-process") << "Done check extended functions, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
580 if( !hasProcessed() ){
582 Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
590 addedFact
= !d_pending
.empty();
591 addedLemma
= !d_lemma_cache
.empty();
594 }while( !d_conflict
&& !addedLemma
&& addedFact
);
596 Trace("strings-check") << "Theory of strings done full effort check " << addedLemma
<< " " << d_conflict
<< std::endl
;
598 Trace("strings-check") << "Theory of strings, done check : " << e
<< std::endl
;
599 Assert( d_pending
.empty() );
600 Assert( d_lemma_cache
.empty() );
603 void TheoryStrings::checkExtfReduction( int effort
) {
604 Trace("strings-process-debug") << "Checking preprocess at effort " << effort
<< ", #to process=" << d_ext_func_terms
.size() << "..." << std::endl
;
605 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
606 Trace("strings-process-debug2") << (*it
).first
<< ", active=" << !(*it
).second
<< std::endl
;
608 Node n
= (*it
).first
;
609 checkReduction( n
, d_extf_pol
[n
], effort
);
610 if( hasProcessed() ){
617 void TheoryStrings::checkReduction( Node atom
, int pol
, int effort
) {
618 //determine the effort level to process the extf at
619 // 0 - at assertion time, 1+ - after no other reduction is applicable
621 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
622 if( pol
==1 && atom
[1].getKind()==kind::REGEXP_RANGE
){
625 }else if( atom
.getKind()==kind::STRING_STRCTN
){
630 if( options::stringLazyPreproc() ){
631 if( atom
.getKind()==kind::STRING_SUBSTR
){
632 r_effort
= options::stringLazyPreproc2() ? 1 : 0;
634 r_effort
= options::stringLazyPreproc2() ? 2 : 0;
638 if( effort
==r_effort
){
639 if( d_preproc_cache
.find( atom
)==d_preproc_cache
.end() ){
640 d_preproc_cache
[ atom
] = true;
641 Trace("strings-process-debug") << "Process reduction for " << atom
<< std::endl
;
642 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
643 if( atom
[1].getKind()==kind::REGEXP_RANGE
){
644 Node eq
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, atom
[0]));
645 sendLemma( atom
, eq
, "RE-Range-Len" );
647 }else if( atom
.getKind()==kind::STRING_STRCTN
){
650 //would have already reduced by now
651 Assert( !areEqual( s
, d_emptyString
) && !areEqual( s
, x
) );
652 Node sk1
= mkSkolemCached( x
, s
, sk_id_ctn_pre
, "sc1" );
653 Node sk2
= mkSkolemCached( x
, s
, sk_id_ctn_post
, "sc2" );
654 Node eq
= Rewriter::rewrite( x
.eqNode( mkConcat( sk1
, s
, sk2
) ) );
655 sendLemma( atom
, eq
, "POS-CTN" );
657 // for STRING_SUBSTR,
658 // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
659 std::vector
< Node
> new_nodes
;
660 Node res
= d_preproc
.decompose( atom
, new_nodes
);
662 if( !new_nodes
.empty() ){
663 Node nnlem
= new_nodes
.size()==1 ? new_nodes
[0] : NodeManager::currentNM()->mkNode( kind::AND
, new_nodes
);
664 nnlem
= Rewriter::rewrite( nnlem
);
665 Trace("strings-red-lemma") << "Reduction_" << effort
<< " lemma : " << nnlem
<< std::endl
;
666 Trace("strings-red-lemma") << "...from " << atom
<< std::endl
;
667 sendLemma( d_true
, nnlem
, "Reduction" );
674 TheoryStrings::EqcInfo::EqcInfo( context::Context
* c
) : d_const_term(c
), d_length_term(c
), d_cardinality_lem_k(c
), d_normalized_length(c
) {
678 TheoryStrings::EqcInfo
* TheoryStrings::getOrMakeEqcInfo( Node eqc
, bool doMake
) {
679 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( eqc
);
680 if( eqc_i
==d_eqc_info
.end() ){
682 EqcInfo
* ei
= new EqcInfo( getSatContext() );
683 d_eqc_info
[eqc
] = ei
;
689 return (*eqc_i
).second
;
694 /** Conflict when merging two constants */
695 void TheoryStrings::conflict(TNode a
, TNode b
){
697 Debug("strings-conflict") << "Making conflict..." << std::endl
;
700 if (a
.getKind() == kind::CONST_BOOLEAN
) {
701 conflictNode
= explain( a
.iffNode(b
) );
703 conflictNode
= explain( a
.eqNode(b
) );
705 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode
<< std::endl
;
706 d_out
->conflict( conflictNode
);
710 /** called when a new equivalance class is created */
711 void TheoryStrings::eqNotifyNewClass(TNode t
){
712 if( t
.getKind() == kind::CONST_STRING
){
713 EqcInfo
* ei
=getOrMakeEqcInfo( t
, true );
714 ei
->d_const_term
= t
;
716 if( t
.getKind() == kind::STRING_LENGTH
){
717 Trace("strings-debug") << "New length eqc : " << t
<< std::endl
;
718 Node r
= d_equalityEngine
.getRepresentative(t
[0]);
719 EqcInfo
* ei
= getOrMakeEqcInfo( r
, true );
720 ei
->d_length_term
= t
[0];
724 /** called when two equivalance classes will merge */
725 void TheoryStrings::eqNotifyPreMerge(TNode t1
, TNode t2
){
726 EqcInfo
* e2
= getOrMakeEqcInfo(t2
, false);
728 EqcInfo
* e1
= getOrMakeEqcInfo( t1
);
729 //add information from e2 to e1
730 if( !e2
->d_const_term
.get().isNull() ){
731 e1
->d_const_term
.set( e2
->d_const_term
);
733 if( !e2
->d_length_term
.get().isNull() ){
734 e1
->d_length_term
.set( e2
->d_length_term
);
736 if( e2
->d_cardinality_lem_k
.get()>e1
->d_cardinality_lem_k
.get() ) {
737 e1
->d_cardinality_lem_k
.set( e2
->d_cardinality_lem_k
);
739 if( !e2
->d_normalized_length
.get().isNull() ){
740 e1
->d_normalized_length
.set( e2
->d_normalized_length
);
744 if( hasTerm( d_zero ) ){
746 if( areEqual(d_zero, t1) ){
748 }else if( areEqual(d_zero, t2) ){
751 if( !leqc.isNull() ){
752 //scan equivalence class to see if we apply
753 eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
754 while( !eqc_i.isFinished() ){
756 if( n.getKind()==kind::STRING_LENGTH ){
757 if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
758 //apply the rule length(n[0])==0 => n[0] == ""
759 Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
760 d_pending.push_back( eq );
761 Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
762 d_pending_exp[eq] = eq_exp;
763 Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
764 d_infer.push_back(eq);
765 d_infer_exp.push_back(eq_exp);
775 /** called when two equivalance classes have merged */
776 void TheoryStrings::eqNotifyPostMerge(TNode t1
, TNode t2
) {
780 /** called when two equivalance classes are disequal */
781 void TheoryStrings::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
785 void TheoryStrings::computeCareGraph(){
786 Theory::computeCareGraph();
789 void TheoryStrings::assertPendingFact(Node atom
, bool polarity
, Node exp
) {
790 Trace("strings-pending") << "Assert pending fact : " << atom
<< " " << polarity
<< " from " << exp
<< std::endl
;
791 Assert(atom
.getKind() != kind::OR
, "Infer error: a split.");
792 if( atom
.getKind()==kind::EQUAL
){
793 Trace("strings-pending-debug") << " Register term" << std::endl
;
794 //AJR : is this necessary?
795 for( unsigned j
=0; j
<2; j
++ ) {
796 if( !d_equalityEngine
.hasTerm( atom
[j
] ) && atom
[j
].getType().isString() ) {
798 registerTerm( atom
[j
] );
801 Trace("strings-pending-debug") << " Now assert equality" << std::endl
;
802 Trace("strings-pending-debug") << atom
<< std::endl
;
803 Trace("strings-pending-debug") << Rewriter::rewrite( atom
) << std::endl
;
804 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
805 Trace("strings-pending-debug") << " Finished assert equality" << std::endl
;
807 if( atom
.getKind()==kind::STRING_IN_REGEXP
) {
808 if( d_ext_func_terms
.find( atom
)==d_ext_func_terms
.end() ){
809 Trace("strings-extf-debug") << "Found extended function (membership) : " << atom
<< std::endl
;
810 d_ext_func_terms
[atom
] = true;
813 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
815 Trace("strings-pending-debug") << " Now collect terms" << std::endl
;
816 //collect extended function terms in the atom
817 std::map
< Node
, bool > visited
;
818 collectExtendedFuncTerms( atom
, visited
);
819 Trace("strings-pending-debug") << " Finished collect terms" << std::endl
;
822 void TheoryStrings::doPendingFacts() {
824 while( !d_conflict
&& i
<d_pending
.size() ) {
825 Node fact
= d_pending
[i
];
826 Node exp
= d_pending_exp
[ fact
];
827 if(fact
.getKind() == kind::AND
) {
828 for(size_t j
=0; j
<fact
.getNumChildren(); j
++) {
829 bool polarity
= fact
[j
].getKind() != kind::NOT
;
830 TNode atom
= polarity
? fact
[j
] : fact
[j
][0];
831 assertPendingFact(atom
, polarity
, exp
);
834 bool polarity
= fact
.getKind() != kind::NOT
;
835 TNode atom
= polarity
? fact
: fact
[0];
836 assertPendingFact(atom
, polarity
, exp
);
841 d_pending_exp
.clear();
844 void TheoryStrings::doPendingLemmas() {
845 if( !d_conflict
&& !d_lemma_cache
.empty() ){
846 for( unsigned i
=0; i
<d_lemma_cache
.size(); i
++ ){
847 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache
[i
] << std::endl
;
848 d_out
->lemma( d_lemma_cache
[i
] );
850 for( std::map
< Node
, bool >::iterator it
= d_pending_req_phase
.begin(); it
!= d_pending_req_phase
.end(); ++it
){
851 Trace("strings-pending") << "Require phase : " << it
->first
<< ", polarity = " << it
->second
<< std::endl
;
852 d_out
->requirePhase( it
->first
, it
->second
);
855 d_lemma_cache
.clear();
856 d_pending_req_phase
.clear();
859 bool TheoryStrings::hasProcessed() {
860 return d_conflict
|| !d_lemma_cache
.empty() || !d_pending
.empty();
863 void TheoryStrings::addToExplanation( Node a
, Node b
, std::vector
< Node
>& exp
) {
865 Debug("strings-explain") << "Add to explanation : " << a
<< " == " << b
<< std::endl
;
866 Assert( areEqual( a
, b
) );
867 exp
.push_back( a
.eqNode( b
) );
871 void TheoryStrings::addToExplanation( Node lit
, std::vector
< Node
>& exp
) {
873 exp
.push_back( lit
);
877 bool TheoryStrings::getNormalForms(Node
&eqc
, std::vector
< Node
> & visited
, std::vector
< Node
> & nf
,
878 std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< Node
> &normal_form_src
) {
879 Trace("strings-process-debug") << "Get normal forms " << eqc
<< std::endl
;
881 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
882 while( !eqc_i
.isFinished() ) {
884 if( d_congruent
.find( n
)==d_congruent
.end() ){
885 if( n
.getKind() == kind::CONST_STRING
|| n
.getKind() == kind::STRING_CONCAT
) {
886 Trace("strings-process-debug") << "Get Normal Form : Process term " << n
<< " in eqc " << eqc
<< std::endl
;
887 std::vector
<Node
> nf_n
;
888 std::vector
<Node
> nf_exp_n
;
890 if( n
.getKind() == kind::CONST_STRING
) {
891 if( n
!=d_emptyString
) {
894 } else if( n
.getKind() == kind::STRING_CONCAT
){
895 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
896 Node nr
= d_equalityEngine
.getRepresentative( n
[i
] );
897 std::vector
< Node
> nf_temp
;
898 std::vector
< Node
> nf_exp_temp
;
899 Trace("strings-process-debug") << "Normalizing subterm " << n
[i
] << " = " << nr
<< std::endl
;
900 bool nresult
= false;
902 nf_temp
.push_back( nr
);
904 nresult
= normalizeEquivalenceClass( nr
, visited
, nf_temp
, nf_exp_temp
);
905 if( hasProcessed() ) {
909 //successfully computed normal form
910 if( nf
.size()!=1 || nf
[0]!=d_emptyString
) {
911 if( Trace
.isOn("strings-error") ) {
912 for( unsigned r
=0; r
<nf_temp
.size(); r
++ ) {
913 if( nresult
&& nf_temp
[r
].getKind()==kind::STRING_CONCAT
) {
914 Trace("strings-error") << "Strings::Error: From eqc = " << eqc
<< ", " << n
<< " index " << i
<< ", bad normal form : ";
915 for( unsigned rr
=0; rr
<nf_temp
.size(); rr
++ ) {
916 Trace("strings-error") << nf_temp
[rr
] << " ";
918 Trace("strings-error") << std::endl
;
920 Assert( !nresult
|| nf_temp
[r
].getKind()!=kind::STRING_CONCAT
);
923 nf_n
.insert( nf_n
.end(), nf_temp
.begin(), nf_temp
.end() );
925 nf_exp_n
.insert( nf_exp_n
.end(), nf_exp_temp
.begin(), nf_exp_temp
.end() );
927 nf_exp_n
.push_back( n
[i
].eqNode( nr
) );
930 //Trace("strings-process-debug") << "....Caused already asserted
931 for( unsigned j
=i
+1; j
<n
.getNumChildren(); j
++ ) {
932 if( !areEqual( n
[j
], d_emptyString
) ) {
933 nf_n
.push_back( n
[j
] );
936 if( nf_n
.size()>1 ) {
943 //if not equal to self
944 //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){
945 if( nf_n
.size()>1 || ( nf_n
.size()==1 && nf_n
[0].getKind()==kind::CONST_STRING
) ) {
946 if( nf_n
.size()>1 ) {
947 Trace("strings-process-debug") << "Check for cycle lemma for normal form ";
948 printConcat(nf_n
,"strings-process-debug");
949 Trace("strings-process-debug") << "..." << std::endl
;
950 for( unsigned i
=0; i
<nf_n
.size(); i
++ ) {
951 //if a component is equal to whole,
952 if( areEqual( nf_n
[i
], n
) ){
953 //all others must be empty
954 std::vector
< Node
> ant
;
956 ant
.push_back( nf_n
[i
].eqNode( n
) );
958 ant
.insert( ant
.end(), nf_exp_n
.begin(), nf_exp_n
.end() );
959 std::vector
< Node
> cc
;
960 for( unsigned j
=0; j
<nf_n
.size(); j
++ ){
962 cc
.push_back( nf_n
[j
].eqNode( d_emptyString
) );
965 std::vector
< Node
> empty_vec
;
966 Node conc
= cc
.size()==1 ? cc
[0] : NodeManager::currentNM()->mkNode( kind::AND
, cc
);
967 conc
= Rewriter::rewrite( conc
);
968 sendInfer( mkAnd( ant
), conc
, "CYCLE" );
974 Trace("strings-process-debug") << "Will have cycle lemma at higher level!" << std::endl
;
975 //we have a normal form that will cause a component lemma at a higher level
976 normal_forms
.clear();
977 normal_forms_exp
.clear();
978 normal_form_src
.clear();
980 normal_forms
.push_back(nf_n
);
981 normal_forms_exp
.push_back(nf_exp_n
);
982 normal_form_src
.push_back(n
);
987 Node nn
= nf_n
.size()==0 ? d_emptyString
: nf_n
[0];
988 //Assert( areEqual( nf_n[0], eqc ) );
989 if( !areEqual( nn
, eqc
) ){
990 std::vector
< Node
> ant
;
991 ant
.insert( ant
.end(), nf_exp_n
.begin(), nf_exp_n
.end() );
992 ant
.push_back( n
.eqNode( eqc
) );
993 Node conc
= Rewriter::rewrite( nn
.eqNode( eqc
) );
994 sendInfer( mkAnd( ant
), conc
, "CYCLE-T" );
1005 if(Trace
.isOn("strings-solve")) {
1006 if( !normal_forms
.empty() ) {
1007 Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc
<< " : " << std::endl
;
1008 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
1009 Trace("strings-solve") << "#" << i
<< " (from " << normal_form_src
[i
] << ") : ";
1010 //mergeCstVec(normal_forms[i]);
1011 for( unsigned j
=0; j
<normal_forms
[i
].size(); j
++ ) {
1013 Trace("strings-solve") << ", ";
1015 Trace("strings-solve") << normal_forms
[i
][j
];
1017 Trace("strings-solve") << std::endl
;
1018 Trace("strings-solve") << " Explanation is : ";
1019 if(normal_forms_exp
[i
].size() == 0) {
1020 Trace("strings-solve") << "NONE";
1022 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
1024 Trace("strings-solve") << " AND ";
1026 Trace("strings-solve") << normal_forms_exp
[i
][j
];
1029 Trace("strings-solve") << std::endl
;
1032 //std::vector< Node > nf;
1033 //nf.push_back( eqc );
1034 //normal_forms.push_back(nf);
1035 //std::vector< Node > nf_exp_def;
1036 //normal_forms_exp.push_back(nf_exp_def);
1037 //normal_form_src.push_back(eqc);
1038 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc
<< std::endl
;
1044 void TheoryStrings::mergeCstVec(std::vector
< Node
> &vec_strings
) {
1045 std::vector
< Node
>::iterator itr
= vec_strings
.begin();
1046 while(itr
!= vec_strings
.end()) {
1047 if(itr
->isConst()) {
1048 std::vector
< Node
>::iterator itr2
= itr
+ 1;
1049 if(itr2
== vec_strings
.end()) {
1051 } else if(itr2
->isConst()) {
1052 CVC4::String s1
= itr
->getConst
<String
>();
1053 CVC4::String s2
= itr2
->getConst
<String
>();
1054 *itr
= NodeManager::currentNM()->mkConst(s1
.concat(s2
));
1055 vec_strings
.erase(itr2
);
1065 bool TheoryStrings::detectLoop( std::vector
< std::vector
< Node
> > &normal_forms
,
1066 int i
, int j
, int index_i
, int index_j
,
1067 int &loop_in_i
, int &loop_in_j
) {
1068 int has_loop
[2] = { -1, -1 };
1069 if( options::stringLB() != 2 ) {
1070 for( unsigned r
=0; r
<2; r
++ ) {
1071 int index
= (r
==0 ? index_i
: index_j
);
1072 int other_index
= (r
==0 ? index_j
: index_i
);
1073 int n_index
= (r
==0 ? i
: j
);
1074 int other_n_index
= (r
==0 ? j
: i
);
1075 if( normal_forms
[other_n_index
][other_index
].getKind() != kind::CONST_STRING
) {
1076 for( unsigned lp
= index
+1; lp
<normal_forms
[n_index
].size(); lp
++ ){
1077 if( normal_forms
[n_index
][lp
]==normal_forms
[other_n_index
][other_index
] ){
1085 if( has_loop
[0]!=-1 || has_loop
[1]!=-1 ) {
1086 loop_in_i
= has_loop
[0];
1087 loop_in_j
= has_loop
[1];
1094 bool TheoryStrings::processLoop(std::vector
< Node
> &antec
,
1095 std::vector
< std::vector
< Node
> > &normal_forms
,
1096 std::vector
< Node
> &normal_form_src
,
1097 int i
, int j
, int loop_n_index
, int other_n_index
,
1098 int loop_index
, int index
, int other_index
) {
1100 Trace("strings-loop") << "Detected possible loop for " << normal_forms
[loop_n_index
][loop_index
] << std::endl
;
1101 Trace("strings-loop") << " ... (X)= " << normal_forms
[other_n_index
][other_index
] << std::endl
;
1103 Trace("strings-loop") << " ... T(Y.Z)= ";
1104 std::vector
< Node
> vec_t
;
1105 for(int lp
=index
; lp
<loop_index
; ++lp
) {
1106 if(lp
!= index
) Trace("strings-loop") << " ++ ";
1107 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
1108 vec_t
.push_back( normal_forms
[loop_n_index
][lp
] );
1110 Node t_yz
= mkConcat( vec_t
);
1111 Trace("strings-loop") << " (" << t_yz
<< ")" << std::endl
;
1112 Trace("strings-loop") << " ... S(Z.Y)= ";
1113 std::vector
< Node
> vec_s
;
1114 for(int lp
=other_index
+1; lp
<(int)normal_forms
[other_n_index
].size(); ++lp
) {
1115 if(lp
!= other_index
+1) Trace("strings-loop") << " ++ ";
1116 Trace("strings-loop") << normal_forms
[other_n_index
][lp
];
1117 vec_s
.push_back( normal_forms
[other_n_index
][lp
] );
1119 Node s_zy
= mkConcat( vec_s
);
1120 Trace("strings-loop") << " (" << s_zy
<< ")" << std::endl
;
1121 Trace("strings-loop") << " ... R= ";
1122 std::vector
< Node
> vec_r
;
1123 for(int lp
=loop_index
+1; lp
<(int)normal_forms
[loop_n_index
].size(); ++lp
) {
1124 if(lp
!= loop_index
+1) Trace("strings-loop") << " ++ ";
1125 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
1126 vec_r
.push_back( normal_forms
[loop_n_index
][lp
] );
1128 Node r
= mkConcat( vec_r
);
1129 Trace("strings-loop") << " (" << r
<< ")" << std::endl
;
1131 //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
1132 //TODO: can be more general
1133 if( s_zy
.isConst() && r
.isConst() && r
!= d_emptyString
) {
1136 if(s_zy
.getConst
<String
>().tailcmp( r
.getConst
<String
>(), c
) ) {
1138 s_zy
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, c
) );
1141 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
<< ", c=" << c
<< std::endl
;
1146 Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl
;
1147 sendLemma( mkExplain( antec
), conc
, "Loop Conflict" );
1152 //require that x is non-empty
1153 if( !areDisequal( normal_forms
[loop_n_index
][loop_index
], d_emptyString
) ){
1154 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
1155 sendSplit( normal_forms
[loop_n_index
][loop_index
], d_emptyString
, "Len-Split(Loop-X)" );
1156 } else if( !areDisequal( t_yz
, d_emptyString
) && t_yz
.getKind()!=kind::CONST_STRING
) {
1157 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
1158 sendSplit( t_yz
, d_emptyString
, "Len-Split(Loop-YZ)" );
1161 antec
.push_back( normal_forms
[loop_n_index
][loop_index
].eqNode( d_emptyString
).negate() );
1162 if( t_yz
.getKind()!=kind::CONST_STRING
) {
1163 antec
.push_back( t_yz
.eqNode( d_emptyString
).negate() );
1165 Node ant
= mkExplain( antec
);
1166 if(d_loop_antec
.find(ant
) == d_loop_antec
.end()) {
1167 d_loop_antec
.insert(ant
);
1171 r
== d_emptyString
&&
1173 s_zy
.getConst
<String
>().isRepeated()
1175 Node rep_c
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, 1) );
1176 Trace("strings-loop") << "Special case (X)=" << normal_forms
[other_n_index
][other_index
] << " " << std::endl
;
1177 Trace("strings-loop") << "... (C)=" << rep_c
<< " " << std::endl
;
1179 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][other_index
],
1180 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
1181 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, rep_c
) ) );
1183 } else if(t_yz
.isConst()) {
1184 Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl
;
1185 CVC4::String s
= t_yz
.getConst
< CVC4::String
>();
1186 unsigned size
= s
.size();
1187 std::vector
< Node
> vconc
;
1188 for(unsigned len
=1; len
<=size
; len
++) {
1189 Node y
= NodeManager::currentNM()->mkConst(s
.substr(0, len
));
1190 Node z
= NodeManager::currentNM()->mkConst(s
.substr(len
, size
- len
));
1193 if(r
!= d_emptyString
) {
1194 std::vector
< Node
> v2(vec_r
);
1195 v2
.insert(v2
.begin(), y
);
1196 v2
.insert(v2
.begin(), z
);
1197 restr
= mkConcat( z
, y
);
1198 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( v2
) ));
1200 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( z
, y
) ));
1205 Node conc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][other_index
],
1206 NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
1207 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, y
),
1208 NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
,
1209 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, restr
))));
1210 cc
= cc
==d_true
? conc2
: NodeManager::currentNM()->mkNode( kind::AND
, cc
, conc2
);
1211 d_regexp_ant
[conc2
] = ant
;
1212 vconc
.push_back(cc
);
1214 conc
= vconc
.size()==0 ? Node::null() : vconc
.size()==1 ? vconc
[0] : NodeManager::currentNM()->mkNode(kind::OR
, vconc
);
1216 Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl
;
1218 Node sk_w
= mkSkolemS( "w_loop" );
1219 Node sk_y
= mkSkolemS( "y_loop", 1 );
1220 Node sk_z
= mkSkolemS( "z_loop" );
1221 //t1 * ... * tn = y * z
1222 Node conc1
= t_yz
.eqNode( mkConcat( sk_y
, sk_z
) );
1223 // s1 * ... * sk = z * y * r
1224 vec_r
.insert(vec_r
.begin(), sk_y
);
1225 vec_r
.insert(vec_r
.begin(), sk_z
);
1226 Node conc2
= s_zy
.eqNode( mkConcat( vec_r
) );
1227 Node conc3
= normal_forms
[other_n_index
][other_index
].eqNode( mkConcat( sk_y
, sk_w
) );
1228 Node restr
= r
== d_emptyString
? s_zy
: mkConcat( sk_z
, sk_y
);
1229 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, sk_w
,
1230 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
1231 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, restr
) ) );
1233 std::vector
< Node
> vec_conc
;
1234 vec_conc
.push_back(conc1
); vec_conc
.push_back(conc2
); vec_conc
.push_back(conc3
);
1235 vec_conc
.push_back(str_in_re
);
1236 //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
1237 conc
= NodeManager::currentNM()->mkNode( kind::AND
, vec_conc
);
1240 //set its antecedant to ant, to say when it is relevant
1241 if(!str_in_re
.isNull()) {
1242 d_regexp_ant
[str_in_re
] = ant
;
1245 sendLemma( ant
, conc
, "F-LOOP" );
1246 ++(d_statistics
.d_loop_lemmas
);
1249 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
1251 Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant
<< " has already added." << std::endl
;
1252 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
1258 Node
TheoryStrings::mkSkolemCached( Node a
, Node b
, int id
, const char * c
, int isLenSplit
){
1259 //return mkSkolemS( c, isLenSplit );
1260 std::map
< int, Node
>::iterator it
= d_skolem_cache
[a
][b
].find( id
);
1261 if( it
==d_skolem_cache
[a
][b
].end() ){
1262 Node sk
= mkSkolemS( c
, isLenSplit
);
1263 d_skolem_cache
[a
][b
][id
] = sk
;
1271 bool TheoryStrings::processNEqc(std::vector
< std::vector
< Node
> > &normal_forms
,
1272 std::vector
< std::vector
< Node
> > &normal_forms_exp
,
1273 std::vector
< Node
> &normal_form_src
) {
1274 bool flag_lb
= false;
1275 std::vector
< Node
> c_lb_exp
;
1276 int c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
, c_other_index
;
1277 for(unsigned i
=0; i
<normal_forms
.size()-1; i
++) {
1278 //unify each normalform[j] with normal_forms[i]
1279 for(unsigned j
=i
+1; j
<normal_forms
.size(); j
++ ) {
1280 Trace("strings-solve") << "Strings: Process normal form #" << i
<< " against #" << j
<< "..." << std::endl
;
1281 if( isNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] ) ) {
1282 Trace("strings-solve") << "Strings: Already cached." << std::endl
;
1284 //the current explanation for why the prefix is equal
1285 std::vector
< Node
> curr_exp
;
1286 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
1287 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[j
].begin(), normal_forms_exp
[j
].end() );
1288 if( normal_form_src
[i
]!=normal_form_src
[j
] ){
1289 curr_exp
.push_back( normal_form_src
[i
].eqNode( normal_form_src
[j
] ) );
1292 //process the reverse direction first (check for easy conflicts and inferences)
1293 if( processReverseNEq( normal_forms
, normal_form_src
, curr_exp
, i
, j
) ){
1297 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
1298 unsigned index_i
= 0;
1299 unsigned index_j
= 0;
1304 if( processSimpleNEq( normal_forms
, normal_form_src
, curr_exp
, i
, j
, index_i
, index_j
, false ) ){
1305 //added a lemma, return
1310 //if we are at the end
1311 if(index_i
==normal_forms
[i
].size() || index_j
==normal_forms
[j
].size() ) {
1312 Assert( index_i
==normal_forms
[i
].size() && index_j
==normal_forms
[j
].size() );
1314 //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
1316 std::vector
< Node
> lexp
;
1317 Node length_term_i
= getLength( normal_forms
[i
][index_i
], lexp
);
1318 Node length_term_j
= getLength( normal_forms
[j
][index_j
], lexp
);
1319 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
1320 if( !areDisequal(length_term_i
, length_term_j
) && !areEqual(length_term_i
, length_term_j
) &&
1321 normal_forms
[i
][index_i
].getKind()!=kind::CONST_STRING
&& normal_forms
[j
][index_j
].getKind()!=kind::CONST_STRING
) {
1322 //length terms are equal, merge equivalence classes if not already done so
1323 Node length_eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
);
1324 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl
;
1325 //try to make the lengths equal via splitting on demand
1326 sendSplit( length_term_i
, length_term_j
, "Len-Split(Diseq)" );
1327 length_eq
= Rewriter::rewrite( length_eq
);
1328 d_pending_req_phase
[ length_eq
] = true;
1331 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl
;
1334 if( detectLoop(normal_forms
, i
, j
, index_i
, index_j
, loop_in_i
, loop_in_j
) ){
1338 c_loop_n_index
= loop_in_i
!=-1 ? i
: j
;
1339 c_other_n_index
= loop_in_i
!=-1 ? j
: i
;
1340 c_loop_index
= loop_in_i
!=-1 ? loop_in_i
: loop_in_j
;
1341 c_index
= loop_in_i
!=-1 ? index_i
: index_j
;
1342 c_other_index
= loop_in_i
!=-1 ? index_j
: index_i
;
1344 c_lb_exp
= curr_exp
;
1346 if(options::stringLB() == 0) {
1349 if(processLoop(c_lb_exp
, normal_forms
, normal_form_src
,
1350 c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
, c_other_index
)) {
1357 std::vector
< Node
> antec
;
1358 Trace("strings-solve-debug") << "No loops detected." << std::endl
;
1359 if( normal_forms
[i
][index_i
].getKind() == kind::CONST_STRING
|| normal_forms
[j
][index_j
].getKind() == kind::CONST_STRING
) {
1360 unsigned const_k
= normal_forms
[i
][index_i
].getKind() == kind::CONST_STRING
? i
: j
;
1361 unsigned const_index_k
= normal_forms
[i
][index_i
].getKind() == kind::CONST_STRING
? index_i
: index_j
;
1362 unsigned nconst_k
= normal_forms
[i
][index_i
].getKind() == kind::CONST_STRING
? j
: i
;
1363 unsigned nconst_index_k
= normal_forms
[i
][index_i
].getKind() == kind::CONST_STRING
? index_j
: index_i
;
1364 Node const_str
= normal_forms
[const_k
][const_index_k
];
1365 Node other_str
= normal_forms
[nconst_k
][nconst_index_k
];
1366 Assert( other_str
.getKind()!=kind::CONST_STRING
, "Other string is not constant." );
1367 Assert( other_str
.getKind()!=kind::STRING_CONCAT
, "Other string is not CONCAT." );
1368 if( !areDisequal(other_str
, d_emptyString
) ) {
1369 sendSplit( other_str
, d_emptyString
, "Len-Split(CST)" );
1371 Assert(areDisequal(other_str
, d_emptyString
), "CST Split on empty Var");
1372 antec
.insert( antec
.end(), curr_exp
.begin(), curr_exp
.end() );
1373 Node xnz
= other_str
.eqNode(d_emptyString
).negate();
1374 antec
.push_back( xnz
);
1376 if( normal_forms
[nconst_k
].size() > nconst_index_k
+ 1 && normal_forms
[nconst_k
][nconst_index_k
+ 1].isConst() ) {
1377 CVC4::String stra
= const_str
.getConst
<String
>();
1378 CVC4::String strb
= normal_forms
[nconst_k
][nconst_index_k
+ 1].getConst
<String
>();
1379 CVC4::String stra1
= stra
.substr(1);
1380 size_t p
= stra
.size() - stra1
.overlap(strb
);
1381 size_t p2
= stra1
.find(strb
);
1382 p
= p2
==std::string::npos
? p
: ( p
>p2
+1? p2
+1 : p
);
1383 Node prea
= p
==stra
.size()? const_str
: NodeManager::currentNM()->mkConst(stra
.substr(0, p
));
1384 Node sk
= mkSkolemCached( other_str
, prea
, sk_id_c_spt
, "c_spt" );
1385 conc
= other_str
.eqNode( mkConcat(prea
, sk
) );
1386 Trace("strings-csp") << "Const Split: " << prea
<< " is removed from " << stra
<< " due to " << strb
<< std::endl
;
1389 Node firstChar
= const_str
.getConst
<String
>().size() == 1 ? const_str
:
1390 NodeManager::currentNM()->mkConst( const_str
.getConst
<String
>().substr(0, 1) );
1391 Node sk
= mkSkolemCached( other_str
, firstChar
, sk_id_vc_spt
, "c_spt" );
1392 conc
= other_str
.eqNode( mkConcat(firstChar
, sk
) );
1393 Trace("strings-csp") << "Const Split: " << firstChar
<< " is removed from " << const_str
<< " (normal) " << std::endl
;
1396 conc
= Rewriter::rewrite( conc
);
1397 sendLemma( mkExplain( antec
), conc
, "S-Split(CST-P)" );
1398 //sendInfer(mkAnd( antec ), conc, "S-Split(CST-P)");
1402 std::vector
< Node
> antec_new_lits
;
1403 antec
.insert(antec
.end(), curr_exp
.begin(), curr_exp
.end() );
1405 Node ldeq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
).negate();
1406 if( d_equalityEngine
.areDisequal( length_term_i
, length_term_j
, true ) ){
1407 antec
.push_back( ldeq
);
1409 antec_new_lits
.push_back(ldeq
);
1413 for(unsigned xory
=0; xory
<2; xory
++) {
1414 Node x
= xory
==0 ? normal_forms
[i
][index_i
] : normal_forms
[j
][index_j
];
1415 Node xgtz
= x
.eqNode( d_emptyString
).negate();
1416 if( d_equalityEngine
.areDisequal( x
, d_emptyString
, true ) ) {
1417 antec
.push_back( xgtz
);
1419 antec_new_lits
.push_back( xgtz
);
1423 Node sk
= mkSkolemCached( normal_forms
[i
][index_i
], normal_forms
[j
][index_j
], sk_id_v_spt
, "v_spt", 1 );
1424 Node eq1
= normal_forms
[i
][index_i
].eqNode( mkConcat(normal_forms
[j
][index_j
], sk
) );
1425 Node eq2
= normal_forms
[j
][index_j
].eqNode( mkConcat(normal_forms
[i
][index_i
], sk
) );
1426 conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR
, eq1
, eq2
));
1428 Node ant
= mkExplain( antec
, antec_new_lits
);
1429 sendLemma( ant
, conc
, "S-Split(VAR)" );
1430 //sendInfer( ant, conc, "S-Split(VAR)" );
1431 //++(d_statistics.d_eq_splits);
1445 if(processLoop(c_lb_exp
, normal_forms
, normal_form_src
,
1446 c_i
, c_j
, c_loop_n_index
, c_other_n_index
, c_loop_index
, c_index
, c_other_index
)) {
1454 bool TheoryStrings::processReverseNEq( std::vector
< std::vector
< Node
> > &normal_forms
,
1455 std::vector
< Node
> &normal_form_src
, std::vector
< Node
> &curr_exp
, unsigned i
, unsigned j
) {
1456 //reverse normal form of i, j
1457 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
1458 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
1460 std::vector
< Node
> t_curr_exp
;
1461 t_curr_exp
.insert( t_curr_exp
.begin(), curr_exp
.begin(), curr_exp
.end() );
1462 unsigned index_i
= 0;
1463 unsigned index_j
= 0;
1464 bool ret
= processSimpleNEq( normal_forms
, normal_form_src
, t_curr_exp
, i
, j
, index_i
, index_j
, true );
1466 //reverse normal form of i, j
1467 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
1468 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
1473 bool TheoryStrings::processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
,
1474 std::vector
< Node
> &normal_form_src
, std::vector
< Node
> &curr_exp
,
1475 unsigned i
, unsigned j
, unsigned& index_i
, unsigned& index_j
, bool isRev
) {
1479 //if we are at the end
1480 if(index_i
==normal_forms
[i
].size() || index_j
==normal_forms
[j
].size() ) {
1481 if( index_i
==normal_forms
[i
].size() && index_j
==normal_forms
[j
].size() ) {
1484 //the remainder must be empty
1485 unsigned k
= index_i
==normal_forms
[i
].size() ? j
: i
;
1486 unsigned index_k
= index_i
==normal_forms
[i
].size() ? index_j
: index_i
;
1487 Node eq_exp
= mkAnd( curr_exp
);
1488 while(!d_conflict
&& index_k
<normal_forms
[k
].size()) {
1489 //can infer that this string must be empty
1490 Node eq
= normal_forms
[k
][index_k
].eqNode( d_emptyString
);
1491 //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
1492 Assert( !areEqual( d_emptyString
, normal_forms
[k
][index_k
] ) );
1493 sendInfer( eq_exp
, eq
, "EQ_Endpoint" );
1499 Trace("strings-solve-debug") << "Process " << normal_forms
[i
][index_i
] << " ... " << normal_forms
[j
][index_j
] << std::endl
;
1500 if(areEqual(normal_forms
[i
][index_i
], normal_forms
[j
][index_j
])) {
1501 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl
;
1502 //terms are equal, continue
1503 if( normal_forms
[i
][index_i
]!=normal_forms
[j
][index_j
] ){
1504 Node eq
= normal_forms
[i
][index_i
].eqNode(normal_forms
[j
][index_j
]);
1505 Trace("strings-solve-debug") << "Add to explanation : " << eq
<< std::endl
;
1506 curr_exp
.push_back(eq
);
1512 std::vector
< Node
> temp_exp
;
1513 Node length_term_i
= getLength( normal_forms
[i
][index_i
], temp_exp
);
1514 Node length_term_j
= getLength( normal_forms
[j
][index_j
], temp_exp
);
1515 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
1516 if( areEqual( length_term_i
, length_term_j
) ){
1517 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl
;
1518 Node eq
= normal_forms
[i
][index_i
].eqNode( normal_forms
[j
][index_j
] );
1519 //eq = Rewriter::rewrite( eq );
1520 Node length_eq
= length_term_i
.eqNode( length_term_j
);
1521 temp_exp
.insert(temp_exp
.end(), curr_exp
.begin(), curr_exp
.end() );
1522 temp_exp
.push_back(length_eq
);
1523 sendInfer( mkAnd( temp_exp
), eq
, "LengthEq" );
1525 }else if( ( normal_forms
[i
][index_i
].getKind()!=kind::CONST_STRING
&& index_i
==normal_forms
[i
].size()-1 ) ||
1526 ( normal_forms
[j
][index_j
].getKind()!=kind::CONST_STRING
&& index_j
==normal_forms
[j
].size()-1 ) ){
1527 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl
;
1529 std::vector
< Node
> antec
;
1530 antec
.insert(antec
.end(), curr_exp
.begin(), curr_exp
.end() );
1531 std::vector
< Node
> eqn
;
1532 for( unsigned r
=0; r
<2; r
++ ) {
1533 int index_k
= r
==0 ? index_i
: index_j
;
1534 int k
= r
==0 ? i
: j
;
1535 std::vector
< Node
> eqnc
;
1536 for( unsigned index_l
=index_k
; index_l
<normal_forms
[k
].size(); index_l
++ ) {
1538 eqnc
.insert(eqnc
.begin(), normal_forms
[k
][index_l
] );
1540 eqnc
.push_back( normal_forms
[k
][index_l
] );
1543 eqn
.push_back( mkConcat( eqnc
) );
1545 if( !areEqual( eqn
[0], eqn
[1] ) ) {
1546 conc
= eqn
[0].eqNode( eqn
[1] );
1547 sendLemma( mkExplain( antec
), conc
, "ENDPOINT" );
1548 //sendInfer( mkAnd( antec ), conc, "ENDPOINT" );
1551 index_i
= normal_forms
[i
].size();
1552 index_j
= normal_forms
[j
].size();
1554 } else if(normal_forms
[i
][index_i
].isConst() && normal_forms
[j
][index_j
].isConst()) {
1555 Node const_str
= normal_forms
[i
][index_i
];
1556 Node other_str
= normal_forms
[j
][index_j
];
1557 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str
<< " vs " << other_str
<< std::endl
;
1558 unsigned len_short
= const_str
.getConst
<String
>().size() <= other_str
.getConst
<String
>().size() ? const_str
.getConst
<String
>().size() : other_str
.getConst
<String
>().size();
1559 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
);
1561 //same prefix/suffix
1562 //k is the index of the string that is shorter
1563 int k
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? i
: j
;
1564 int index_k
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? index_i
: index_j
;
1565 int l
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? j
: i
;
1566 int index_l
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? index_j
: index_i
;
1568 int new_len
= normal_forms
[l
][index_l
].getConst
<String
>().size() - len_short
;
1569 Node remainderStr
= NodeManager::currentNM()->mkConst( normal_forms
[l
][index_l
].getConst
<String
>().substr(0, new_len
) );
1570 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index_l
] << " into " << normal_forms
[k
][index_k
] << ", " << remainderStr
<< std::endl
;
1571 normal_forms
[l
].insert( normal_forms
[l
].begin()+index_l
+ 1, remainderStr
);
1573 Node remainderStr
= NodeManager::currentNM()->mkConst(normal_forms
[l
][index_l
].getConst
<String
>().substr(len_short
));
1574 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index_l
] << " into " << normal_forms
[k
][index_k
] << ", " << remainderStr
<< std::endl
;
1575 normal_forms
[l
].insert( normal_forms
[l
].begin()+index_l
+ 1, remainderStr
);
1577 normal_forms
[l
][index_l
] = normal_forms
[k
][index_k
];
1582 std::vector
< Node
> antec
;
1583 //curr_exp is conflict
1584 antec
.insert(antec
.end(), curr_exp
.begin(), curr_exp
.end() );
1585 Node ant
= mkExplain( antec
);
1586 sendLemma( ant
, d_false
, "Const Conflict" );
1597 //nf_exp is conjunction
1598 bool TheoryStrings::normalizeEquivalenceClass( Node eqc
, std::vector
< Node
> & visited
, std::vector
< Node
> & nf
, std::vector
< Node
> & nf_exp
) {
1599 Trace("strings-process-debug") << "Process equivalence class " << eqc
<< std::endl
;
1600 if( std::find( visited
.begin(), visited
.end(), eqc
)!=visited
.end() ){
1601 getConcatVec( eqc
, nf
);
1602 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : already visited." << std::endl
;
1604 } else if( areEqual( eqc
, d_emptyString
) ) {
1605 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1606 while( !eqc_i
.isFinished() ) {
1608 if( d_congruent
.find( n
)==d_congruent
.end() ){
1609 if( n
.getKind()==kind::STRING_CONCAT
){
1610 //std::vector< Node > exp;
1611 //exp.push_back( n.eqNode( d_emptyString ) );
1612 //Node ant = mkExplain( exp );
1613 Node ant
= n
.eqNode( d_emptyString
);
1614 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1615 if( !areEqual( n
[i
], d_emptyString
) ){
1616 //sendLemma( ant, n[i].eqNode( d_emptyString ), "CYCLE" );
1617 sendInfer( ant
, n
[i
].eqNode( d_emptyString
), "CYCLE" );
1625 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : empty." << std::endl
;
1626 d_normal_forms_base
[eqc
] = d_emptyString
;
1627 d_normal_forms
[eqc
].clear();
1628 d_normal_forms_exp
[eqc
].clear();
1631 visited
.push_back( eqc
);
1633 if(d_normal_forms
.find(eqc
)==d_normal_forms
.end() ) {
1634 //phi => t = s1 * ... * sn
1635 // normal form for each non-variable term in this eqc (s1...sn)
1636 std::vector
< std::vector
< Node
> > normal_forms
;
1637 // explanation for each normal form (phi)
1638 std::vector
< std::vector
< Node
> > normal_forms_exp
;
1639 // record terms for each normal form (t)
1640 std::vector
< Node
> normal_form_src
;
1642 result
= getNormalForms(eqc
, visited
, nf
, normal_forms
, normal_forms_exp
, normal_form_src
);
1643 if( hasProcessed() ) {
1645 } else if( result
) {
1646 if(processNEqc(normal_forms
, normal_forms_exp
, normal_form_src
)) {
1651 //construct the normal form
1652 if( normal_forms
.empty() ){
1653 Trace("strings-solve-debug2") << "construct the normal form" << std::endl
;
1654 getConcatVec( eqc
, nf
);
1656 Trace("strings-solve-debug2") << "just take the first normal form" << std::endl
;
1657 //just take the first normal form
1658 nf
.insert( nf
.end(), normal_forms
[0].begin(), normal_forms
[0].end() );
1659 nf_exp
.insert( nf_exp
.end(), normal_forms_exp
[0].begin(), normal_forms_exp
[0].end() );
1660 if( eqc
!=normal_form_src
[0] ){
1661 nf_exp
.push_back( eqc
.eqNode( normal_form_src
[0] ) );
1663 Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl
;
1666 d_normal_forms_base
[eqc
] = normal_form_src
.empty() ? eqc
: normal_form_src
[0];
1667 d_normal_forms
[eqc
].insert( d_normal_forms
[eqc
].end(), nf
.begin(), nf
.end() );
1668 d_normal_forms_exp
[eqc
].insert( d_normal_forms_exp
[eqc
].end(), nf_exp
.begin(), nf_exp
.end() );
1669 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : returned, size = " << nf
.size() << std::endl
;
1671 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : already computed, size = " << d_normal_forms
[eqc
].size() << std::endl
;
1672 nf
.insert( nf
.end(), d_normal_forms
[eqc
].begin(), d_normal_forms
[eqc
].end() );
1673 nf_exp
.insert( nf_exp
.end(), d_normal_forms_exp
[eqc
].begin(), d_normal_forms_exp
[eqc
].end() );
1681 //return true for lemma, false if we succeed
1682 bool TheoryStrings::processDeq( Node ni
, Node nj
) {
1683 //Assert( areDisequal( ni, nj ) );
1684 if( d_normal_forms
[ni
].size()>1 || d_normal_forms
[nj
].size()>1 ){
1685 std::vector
< Node
> nfi
;
1686 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
1687 std::vector
< Node
> nfj
;
1688 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
1690 int revRet
= processReverseDeq( nfi
, nfj
, ni
, nj
);
1696 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
1698 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
1701 while( index
<nfi
.size() || index
<nfj
.size() ){
1702 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, false );
1706 Assert( index
<nfi
.size() && index
<nfj
.size() );
1707 Node i
= nfi
[index
];
1708 Node j
= nfj
[index
];
1709 Trace("strings-solve-debug") << "...Processing(DEQ) " << i
<< " " << j
<< std::endl
;
1710 if( !areEqual( i
, j
) ) {
1711 Assert( i
.getKind()!=kind::CONST_STRING
|| j
.getKind()!=kind::CONST_STRING
);
1712 std::vector
< Node
> lexp
;
1713 Node li
= getLength( i
, lexp
);
1714 Node lj
= getLength( j
, lexp
);
1715 if( areDisequal(li
, lj
) ){
1716 //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
1718 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl
;
1720 std::vector
< Node
> antec
;
1721 std::vector
< Node
> antec_new_lits
;
1722 antec
.insert( antec
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
1723 antec
.insert( antec
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
1725 if( areDisequal( ni
, nj
) ){
1726 antec
.push_back( ni
.eqNode( nj
).negate() );
1728 antec_new_lits
.push_back( ni
.eqNode( nj
).negate() );
1730 antec_new_lits
.push_back( li
.eqNode( lj
).negate() );
1731 std::vector
< Node
> conc
;
1732 Node sk1
= mkSkolemCached( i
, j
, sk_id_deq_x
, "x_dsplit" );
1733 Node sk2
= mkSkolemCached( i
, j
, sk_id_deq_y
, "y_dsplit" );
1734 Node sk3
= mkSkolemCached( i
, j
, sk_id_deq_z
, "z_dsplit", 1 );
1735 //Node nemp = sk3.eqNode(d_emptyString).negate();
1736 //conc.push_back(nemp);
1737 Node lsk1
= mkLength( sk1
);
1738 conc
.push_back( lsk1
.eqNode( li
) );
1739 Node lsk2
= mkLength( sk2
);
1740 conc
.push_back( lsk2
.eqNode( lj
) );
1741 conc
.push_back( NodeManager::currentNM()->mkNode( kind::OR
, j
.eqNode( mkConcat( sk1
, sk3
) ), i
.eqNode( mkConcat( sk2
, sk3
) ) ) );
1742 sendLemma( mkExplain( antec
, antec_new_lits
), NodeManager::currentNM()->mkNode( kind::AND
, conc
), "D-DISL-Split" );
1743 ++(d_statistics
.d_deq_splits
);
1745 }else if( areEqual( li
, lj
) ){
1746 Assert( !areDisequal( i
, j
) );
1747 //splitting on demand : try to make them disequal
1748 Node eq
= i
.eqNode( j
);
1749 sendSplit( i
, j
, "S-Split(DEQL)" );
1750 eq
= Rewriter::rewrite( eq
);
1751 d_pending_req_phase
[ eq
] = false;
1754 //splitting on demand : try to make lengths equal
1755 Node eq
= li
.eqNode( lj
);
1756 sendSplit( li
, lj
, "D-Split" );
1757 eq
= Rewriter::rewrite( eq
);
1758 d_pending_req_phase
[ eq
] = true;
1770 int TheoryStrings::processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
) {
1771 //reverse normal form of i, j
1772 std::reverse( nfi
.begin(), nfi
.end() );
1773 std::reverse( nfj
.begin(), nfj
.end() );
1776 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, true );
1778 //reverse normal form of i, j
1779 std::reverse( nfi
.begin(), nfi
.end() );
1780 std::reverse( nfj
.begin(), nfj
.end() );
1785 int TheoryStrings::processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
) {
1786 while( index
<nfi
.size() || index
<nfj
.size() ) {
1787 if( index
>=nfi
.size() || index
>=nfj
.size() ) {
1788 Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl
;
1789 std::vector
< Node
> ant
;
1790 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
1791 Node lni
= getLengthExp( ni
, ant
, d_normal_forms_base
[ni
] );
1792 Node lnj
= getLengthExp( nj
, ant
, d_normal_forms_base
[nj
] );
1793 ant
.push_back( lni
.eqNode( lnj
) );
1794 ant
.insert( ant
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
1795 ant
.insert( ant
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
1796 std::vector
< Node
> cc
;
1797 std::vector
< Node
>& nfk
= index
>=nfi
.size() ? nfj
: nfi
;
1798 for( unsigned index_k
=index
; index_k
<nfk
.size(); index_k
++ ){
1799 cc
.push_back( nfk
[index_k
].eqNode( d_emptyString
) );
1801 Node conc
= cc
.size()==1 ? cc
[0] : NodeManager::currentNM()->mkNode( kind::AND
, cc
);
1802 conc
= Rewriter::rewrite( conc
);
1803 sendLemma(mkExplain( ant
), conc
, "Disequality Normalize Empty");
1804 //sendInfer(mkAnd( ant ), conc, "Disequality Normalize Empty");
1807 Node i
= nfi
[index
];
1808 Node j
= nfj
[index
];
1809 Trace("strings-solve-debug") << "...Processing(QED) " << i
<< " " << j
<< std::endl
;
1810 if( !areEqual( i
, j
) ) {
1811 if( i
.getKind()==kind::CONST_STRING
&& j
.getKind()==kind::CONST_STRING
) {
1812 unsigned int len_short
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
.getConst
<String
>().size() : j
.getConst
<String
>().size();
1813 bool isSameFix
= isRev
? i
.getConst
<String
>().rstrncmp(j
.getConst
<String
>(), len_short
): i
.getConst
<String
>().strncmp(j
.getConst
<String
>(), len_short
);
1815 //same prefix/suffix
1816 //k is the index of the string that is shorter
1817 Node nk
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
: j
;
1818 Node nl
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? j
: i
;
1821 int new_len
= nl
.getConst
<String
>().size() - len_short
;
1822 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr(0, new_len
) );
1823 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
1825 remainderStr
= NodeManager::currentNM()->mkConst( j
.getConst
<String
>().substr(len_short
) );
1826 Trace("strings-solve-debug-test") << "Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
1828 if( i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ) {
1829 nfj
.insert( nfj
.begin() + index
+ 1, remainderStr
);
1830 nfj
[index
] = nfi
[index
];
1832 nfi
.insert( nfi
.begin() + index
+ 1, remainderStr
);
1833 nfi
[index
] = nfj
[index
];
1839 std::vector
< Node
> lexp
;
1840 Node li
= getLength( i
, lexp
);
1841 Node lj
= getLength( j
, lexp
);
1842 if( areEqual( li
, lj
) && areDisequal( i
, j
) ) {
1843 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i
<< " " << j
<< std::endl
;
1844 //we are done: D-Remove
1857 void TheoryStrings::addNormalFormPair( Node n1
, Node n2
) {
1858 if( !isNormalFormPair( n1
, n2
) ){
1859 //Assert( !isNormalFormPair( n1, n2 ) );
1861 NodeListMap::iterator nf_i
= d_nf_pairs
.find( n1
);
1862 if( nf_i
== d_nf_pairs
.end() ){
1863 if( d_nf_pairs
.find( n2
)!=d_nf_pairs
.end() ){
1864 addNormalFormPair( n2
, n1
);
1867 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
1868 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
1869 d_nf_pairs
.insertDataFromContextMemory( n1
, lst
);
1870 Trace("strings-nf") << "Create cache for " << n1
<< std::endl
;
1872 lst
= (*nf_i
).second
;
1874 Trace("strings-nf") << "Add normal form pair : " << n1
<< " " << n2
<< std::endl
;
1875 lst
->push_back( n2
);
1876 Assert( isNormalFormPair( n1
, n2
) );
1878 Trace("strings-nf-debug") << "Already a normal form pair " << n1
<< " " << n2
<< std::endl
;
1881 bool TheoryStrings::isNormalFormPair( Node n1
, Node n2
) {
1882 //TODO: modulo equality?
1883 return isNormalFormPair2( n1
, n2
) || isNormalFormPair2( n2
, n1
);
1885 bool TheoryStrings::isNormalFormPair2( Node n1
, Node n2
) {
1886 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
1888 NodeListMap::iterator nf_i
= d_nf_pairs
.find( n1
);
1889 if( nf_i
!= d_nf_pairs
.end() ) {
1890 lst
= (*nf_i
).second
;
1891 for( NodeList::const_iterator i
= lst
->begin(); i
!= lst
->end(); ++i
) {
1901 bool TheoryStrings::registerTerm( Node n
) {
1902 if(d_registered_terms_cache
.find(n
) == d_registered_terms_cache
.end()) {
1903 d_registered_terms_cache
.insert(n
);
1904 Debug("strings-register") << "TheoryStrings::registerTerm() " << n
<< endl
;
1905 if(n
.getType().isString()) {
1906 //register length information:
1907 // for variables, split on empty vs positive length
1908 // for concat/const, introduce proxy var and state length relation
1909 if( n
.getKind()!=kind::STRING_CONCAT
&& n
.getKind()!=kind::CONST_STRING
) {
1910 if( d_length_intro_vars
.find(n
)==d_length_intro_vars
.end() ) {
1911 sendLengthLemma( n
);
1912 ++(d_statistics
.d_splits
);
1915 Node sk
= mkSkolemS("lsym", 2);
1916 StringsProxyVarAttribute spva
;
1917 sk
.setAttribute(spva
,true);
1918 Node eq
= Rewriter::rewrite( sk
.eqNode(n
) );
1919 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq
<< std::endl
;
1920 d_proxy_var
[n
] = sk
;
1921 Trace("strings-assert") << "(assert " << eq
<< ")" << std::endl
;
1923 Node skl
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk
);
1925 if( n
.getKind() == kind::STRING_CONCAT
) {
1926 std::vector
<Node
> node_vec
;
1927 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
1928 if( n
[i
].getAttribute(StringsProxyVarAttribute()) ){
1929 Assert( d_proxy_var_to_length
.find( n
[i
] )!=d_proxy_var_to_length
.end() );
1930 node_vec
.push_back( d_proxy_var_to_length
[n
[i
]] );
1932 Node lni
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
[i
] );
1933 node_vec
.push_back(lni
);
1936 lsum
= NodeManager::currentNM()->mkNode( kind::PLUS
, node_vec
);
1937 } else if( n
.getKind() == kind::CONST_STRING
) {
1938 lsum
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( n
.getConst
<String
>().size() ) );
1940 lsum
= Rewriter::rewrite( lsum
);
1941 d_proxy_var_to_length
[sk
] = lsum
;
1942 if( options::stringEagerLen() || n
.getKind()==kind::CONST_STRING
){
1943 Node ceq
= Rewriter::rewrite( skl
.eqNode( lsum
) );
1944 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq
<< std::endl
;
1945 Trace("strings-lemma-debug") << " prerewrite : " << skl
.eqNode( lsum
) << std::endl
;
1946 Trace("strings-assert") << "(assert " << ceq
<< ")" << std::endl
;
1952 AlwaysAssert(false, "String Terms only in registerTerm.");
1958 void TheoryStrings::sendLemma( Node ant
, Node conc
, const char * c
) {
1959 if( conc
.isNull() || conc
== d_false
) {
1960 d_out
->conflict(ant
);
1961 Trace("strings-conflict") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
1962 Trace("strings-lemma") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
1963 Trace("strings-assert") << "(assert (not " << ant
<< ")) ; conflict " << c
<< std::endl
;
1967 if( ant
== d_true
) {
1970 lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, ant
, conc
);
1972 Trace("strings-lemma") << "Strings::Lemma " << c
<< " : " << lem
<< std::endl
;
1973 Trace("strings-assert") << "(assert " << lem
<< ") ; lemma " << c
<< std::endl
;
1974 d_lemma_cache
.push_back( lem
);
1978 void TheoryStrings::sendInfer( Node eq_exp
, Node eq
, const char * c
) {
1979 Trace("strings-infer-debug") << "infer : " << eq
<< " from " << eq_exp
<< std::endl
;
1980 eq
= Rewriter::rewrite( eq
);
1981 if( eq
==d_false
|| eq
.getKind()==kind::OR
) {
1982 sendLemma( eq_exp
, eq
, c
);
1983 }else if( eq
!=d_true
){
1984 if( options::stringInferSym() ){
1985 std::vector
< Node
> vars
;
1986 std::vector
< Node
> subs
;
1987 std::vector
< Node
> unproc
;
1988 inferSubstitutionProxyVars( eq_exp
, vars
, subs
, unproc
);
1989 if( unproc
.empty() ){
1990 Trace("strings-lemma-debug") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
1991 Node eqs
= eq
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
1992 Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs
<< std::endl
;
1993 for( unsigned i
=0; i
<vars
.size(); i
++ ){
1994 Trace("strings-lemma-debug") << " " << vars
[i
] << " -> " << subs
[i
] << std::endl
;
1996 sendLemma( d_true
, eqs
, c
);
1999 for( unsigned i
=0; i
<unproc
.size(); i
++ ){
2000 Trace("strings-lemma-debug") << " non-trivial exp : " << unproc
[i
] << std::endl
;
2004 Trace("strings-lemma") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
2005 Trace("strings-assert") << "(assert (=> " << eq_exp
<< " " << eq
<< ")) ; infer " << c
<< std::endl
;
2006 d_pending
.push_back( eq
);
2007 d_pending_exp
[eq
] = eq_exp
;
2008 d_infer
.push_back( eq
);
2009 d_infer_exp
.push_back( eq_exp
);
2013 void TheoryStrings::sendSplit( Node a
, Node b
, const char * c
, bool preq
) {
2014 Node eq
= a
.eqNode( b
);
2015 eq
= Rewriter::rewrite( eq
);
2016 Node neq
= NodeManager::currentNM()->mkNode( kind::NOT
, eq
);
2017 Node lemma_or
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, neq
);
2018 Trace("strings-lemma") << "Strings::Lemma " << c
<< " SPLIT : " << lemma_or
<< std::endl
;
2019 d_lemma_cache
.push_back(lemma_or
);
2020 d_pending_req_phase
[eq
] = preq
;
2021 ++(d_statistics
.d_splits
);
2025 void TheoryStrings::sendLengthLemma( Node n
){
2026 Node n_len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
);
2027 if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
2028 Node n_len_eq_z
= n_len
.eqNode( d_zero
);
2029 //registerTerm( d_emptyString );
2030 Node n_len_eq_z_2
= n
.eqNode( d_emptyString
);
2031 n_len_eq_z
= Rewriter::rewrite( n_len_eq_z
);
2032 n_len_eq_z_2
= Rewriter::rewrite( n_len_eq_z_2
);
2033 Node n_len_geq_zero
= NodeManager::currentNM()->mkNode( kind::OR
, NodeManager::currentNM()->mkNode( kind::AND
, n_len_eq_z
, n_len_eq_z_2
),
2034 NodeManager::currentNM()->mkNode( kind::GT
, n_len
, d_zero
) );
2035 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero
<< std::endl
;
2036 d_out
->lemma(n_len_geq_zero
);
2037 d_out
->requirePhase( n_len_eq_z
, true );
2038 d_out
->requirePhase( n_len_eq_z_2
, true );
2040 //AJR: probably a good idea
2041 if( options::stringLenGeqZ() ){
2042 Node n_len_geq
= NodeManager::currentNM()->mkNode( kind::GEQ
, n_len
, d_zero
);
2043 n_len_geq
= Rewriter::rewrite( n_len_geq
);
2044 d_out
->lemma( n_len_geq
);
2048 void TheoryStrings::inferSubstitutionProxyVars( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::vector
< Node
>& unproc
) {
2049 if( n
.getKind()==kind::AND
){
2050 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2051 inferSubstitutionProxyVars( n
[i
], vars
, subs
, unproc
);
2054 }else if( n
.getKind()==kind::EQUAL
){
2055 Node ns
= n
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
2056 ns
= Rewriter::rewrite( ns
);
2057 if( ns
.getKind()==kind::EQUAL
){
2060 for( unsigned i
=0; i
<2; i
++ ){
2062 if( ns
[i
].getAttribute(StringsProxyVarAttribute()) ){
2064 }else if( ns
[i
].isConst() ){
2065 NodeNodeMap::const_iterator it
= d_proxy_var
.find( ns
[i
] );
2066 if( it
!=d_proxy_var
.end() ){
2072 if( v
.getNumChildren()==0 ){
2076 //both sides involved in proxy var
2087 subs
.push_back( s
);
2088 vars
.push_back( v
);
2096 unproc
.push_back( n
);
2101 Node
TheoryStrings::mkConcat( Node n1
, Node n2
) {
2102 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
) );
2105 Node
TheoryStrings::mkConcat( Node n1
, Node n2
, Node n3
) {
2106 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
, n3
) );
2109 Node
TheoryStrings::mkConcat( const std::vector
< Node
>& c
) {
2110 return Rewriter::rewrite( c
.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, c
) : ( c
.size()==1 ? c
[0] : d_emptyString
) );
2113 Node
TheoryStrings::mkLength( Node t
) {
2114 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
) );
2117 //isLenSplit: 0-yes, 1-no, 2-ignore
2118 Node
TheoryStrings::mkSkolemS( const char *c
, int isLenSplit
) {
2119 Node n
= NodeManager::currentNM()->mkSkolem( c
, NodeManager::currentNM()->stringType(), "string sko" );
2120 d_length_intro_vars
.insert(n
);
2121 ++(d_statistics
.d_new_skolems
);
2122 if(isLenSplit
== 0) {
2123 sendLengthLemma( n
);
2124 ++(d_statistics
.d_splits
);
2125 } else if(isLenSplit
== 1) {
2126 d_equalityEngine
.assertEquality(n
.eqNode(d_emptyString
), false, d_true
);
2127 Node len_n_gt_z
= NodeManager::currentNM()->mkNode(kind::GT
,
2128 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, n
), d_zero
);
2129 Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z
<< std::endl
;
2130 Trace("strings-assert") << "(assert " << len_n_gt_z
<< ")" << std::endl
;
2131 d_out
->lemma(len_n_gt_z
);
2136 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
) {
2137 std::vector
< Node
> an
;
2138 return mkExplain( a
, an
);
2141 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
) {
2142 std::vector
< TNode
> antec_exp
;
2143 for( unsigned i
=0; i
<a
.size(); i
++ ) {
2144 if( std::find( a
.begin(), a
.begin() + i
, a
[i
] )==a
.begin() + i
) {
2146 Debug("strings-explain") << "Ask for explanation of " << a
[i
] << std::endl
;
2148 if(a
[i
].getKind() == kind::EQUAL
) {
2149 //assert( hasTerm(a[i][0]) );
2150 //assert( hasTerm(a[i][1]) );
2151 Assert( areEqual(a
[i
][0], a
[i
][1]) );
2152 if( a
[i
][0]==a
[i
][1] ){
2155 } else if( a
[i
].getKind()==kind::NOT
&& a
[i
][0].getKind()==kind::EQUAL
) {
2156 Assert( hasTerm(a
[i
][0][0]) );
2157 Assert( hasTerm(a
[i
][0][1]) );
2158 AlwaysAssert( d_equalityEngine
.areDisequal(a
[i
][0][0], a
[i
][0][1], true) );
2159 }else if( a
[i
].getKind() == kind::AND
){
2160 for( unsigned j
=0; j
<a
[i
].getNumChildren(); j
++ ){
2161 a
.push_back( a
[i
][j
] );
2166 unsigned ps
= antec_exp
.size();
2167 explain(a
[i
], antec_exp
);
2168 Debug("strings-explain") << "Done, explanation was : " << std::endl
;
2169 for( unsigned j
=ps
; j
<antec_exp
.size(); j
++ ) {
2170 Debug("strings-explain") << " " << antec_exp
[j
] << std::endl
;
2172 Debug("strings-explain") << std::endl
;
2176 for( unsigned i
=0; i
<an
.size(); i
++ ) {
2177 if( std::find( an
.begin(), an
.begin() + i
, an
[i
] )==an
.begin() + i
){
2178 Debug("strings-explain") << "Add to explanation (new literal) " << an
[i
] << std::endl
;
2179 antec_exp
.push_back(an
[i
]);
2183 if( antec_exp
.empty() ) {
2185 } else if( antec_exp
.size()==1 ) {
2188 ant
= NodeManager::currentNM()->mkNode( kind::AND
, antec_exp
);
2190 ant
= Rewriter::rewrite( ant
);
2194 Node
TheoryStrings::mkAnd( std::vector
< Node
>& a
) {
2195 std::vector
< Node
> au
;
2196 for( unsigned i
=0; i
<a
.size(); i
++ ){
2197 if( std::find( au
.begin(), au
.end(), a
[i
] )==au
.end() ){
2198 au
.push_back( a
[i
] );
2203 } else if( au
.size() == 1 ) {
2206 return NodeManager::currentNM()->mkNode( kind::AND
, au
);
2210 void TheoryStrings::getConcatVec( Node n
, std::vector
< Node
>& c
) {
2211 if( n
.getKind()==kind::STRING_CONCAT
) {
2212 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
2213 if( !areEqual( n
[i
], d_emptyString
) ) {
2214 c
.push_back( n
[i
] );
2222 void TheoryStrings::debugPrintFlatForms( const char * tc
){
2223 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
2224 Node eqc
= d_strings_eqc
[k
];
2225 if( d_eqc
[eqc
].size()>1 ){
2226 Trace( tc
) << "EQC [" << eqc
<< "]" << std::endl
;
2228 Trace( tc
) << "eqc [" << eqc
<< "]";
2230 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
2231 if( itc
!=d_eqc_to_const
.end() ){
2232 Trace( tc
) << " C: " << itc
->second
;
2233 if( d_eqc
[eqc
].size()>1 ){
2234 Trace( tc
) << std::endl
;
2237 if( d_eqc
[eqc
].size()>1 ){
2238 for( unsigned i
=0; i
<d_eqc
[eqc
].size(); i
++ ){
2239 Node n
= d_eqc
[eqc
][i
];
2241 for( unsigned j
=0; j
<d_flat_form
[n
].size(); j
++ ){
2242 Node fc
= d_flat_form
[n
][j
];
2243 itc
= d_eqc_to_const
.find( fc
);
2245 if( itc
!=d_eqc_to_const
.end() ){
2246 Trace( tc
) << itc
->second
;
2252 Trace( tc
) << ", from " << n
;
2254 Trace( tc
) << std::endl
;
2257 Trace( tc
) << std::endl
;
2260 Trace( tc
) << std::endl
;
2263 void TheoryStrings::checkFlatForms() {
2264 //first check for cycles, while building ordering of equivalence classes
2266 d_flat_form
.clear();
2267 d_flat_form_index
.clear();
2268 Trace("strings-process") << "Check equivalence classes cycles...." << std::endl
;
2269 //rebuild strings eqc based on acyclic ordering
2270 std::vector
< Node
> eqc
;
2271 eqc
.insert( eqc
.end(), d_strings_eqc
.begin(), d_strings_eqc
.end() );
2272 d_strings_eqc
.clear();
2273 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
2274 std::vector
< Node
> curr
;
2275 std::vector
< Node
> exp
;
2276 checkCycles( eqc
[i
], curr
, exp
);
2277 if( hasProcessed() ){
2281 Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << std::endl
;
2282 if( !hasProcessed() ){
2283 //debug print flat forms
2284 if( Trace
.isOn("strings-ff") ){
2285 Trace("strings-ff") << "Flat forms : " << std::endl
;
2286 debugPrintFlatForms( "strings-ff" );
2288 //inferences without recursively expanding flat forms
2289 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
2290 Node eqc
= d_strings_eqc
[k
];
2292 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
2293 if( itc
!=d_eqc_to_const
.end() ){
2294 c
= itc
->second
; //use?
2296 std::map
< Node
, std::vector
< Node
> >::iterator it
= d_eqc
.find( eqc
);
2297 if( it
!=d_eqc
.end() && it
->second
.size()>1 ){
2298 //iterate over start index
2299 for( unsigned start
=0; start
<it
->second
.size()-1; start
++ ){
2300 for( unsigned r
=0; r
<2; r
++ ){
2302 std::vector
< Node
> inelig
;
2303 for( unsigned i
=0; i
<=start
; i
++ ){
2304 inelig
.push_back( it
->second
[start
] );
2306 Node a
= it
->second
[start
];
2309 std::vector
< Node
> exp
;
2310 //std::vector< Node > exp_n;
2313 if( count
==d_flat_form
[a
].size() ){
2314 for( unsigned i
=start
+1; i
<it
->second
.size(); i
++ ){
2316 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
2317 if( count
<d_flat_form
[b
].size() ){
2319 std::vector
< Node
> conc_c
;
2320 for( unsigned j
=count
; j
<d_flat_form
[b
].size(); j
++ ){
2321 conc_c
.push_back( b
[d_flat_form_index
[b
][j
]].eqNode( d_emptyString
) );
2323 Assert( !conc_c
.empty() );
2324 conc
= mkAnd( conc_c
);
2327 //swap, will enforce is empty past current
2328 a
= it
->second
[i
]; b
= it
->second
[start
];
2332 inelig
.push_back( it
->second
[i
] );
2336 Node curr
= d_flat_form
[a
][count
];
2337 Node curr_c
= d_eqc_to_const
[curr
];
2338 std::vector
< Node
> lexp
;
2339 Node lcurr
= getLength( curr
, lexp
);
2340 for( unsigned i
=1; i
<it
->second
.size(); i
++ ){
2342 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
2343 if( count
==d_flat_form
[b
].size() ){
2344 inelig
.push_back( b
);
2346 std::vector
< Node
> conc_c
;
2347 for( unsigned j
=count
; j
<d_flat_form
[a
].size(); j
++ ){
2348 conc_c
.push_back( a
[d_flat_form_index
[a
][j
]].eqNode( d_emptyString
) );
2350 Assert( !conc_c
.empty() );
2351 conc
= mkAnd( conc_c
);
2357 Node cc
= d_flat_form
[b
][count
];
2359 Node ac
= a
[d_flat_form_index
[a
][count
]];
2360 Node bc
= b
[d_flat_form_index
[b
][count
]];
2361 inelig
.push_back( b
);
2362 Assert( !areEqual( curr
, cc
) );
2363 Node cc_c
= d_eqc_to_const
[cc
];
2364 if( !curr_c
.isNull() && !cc_c
.isNull() ){
2365 //check for constant conflict
2367 Node s
= TheoryStringsRewriter::splitConstant( cc_c
, curr_c
, index
, r
==1 );
2369 addToExplanation( ac
, d_eqc_to_const_base
[curr
], exp
);
2370 addToExplanation( d_eqc_to_const_exp
[curr
], exp
);
2371 addToExplanation( bc
, d_eqc_to_const_base
[cc
], exp
);
2372 addToExplanation( d_eqc_to_const_exp
[cc
], exp
);
2377 }else if( (d_flat_form
[a
].size()-1)==count
&& (d_flat_form
[b
].size()-1)==count
){
2378 conc
= ac
.eqNode( bc
);
2382 //if lengths are the same, apply LengthEq
2383 Node lcc
= getLength( cc
, lexp
);
2384 if( areEqual( lcurr
, lcc
) ){
2385 Trace("strings-ff-debug") << "Infer " << ac
<< " == " << bc
<< " since " << lcurr
<< " == " << lcc
<< std::endl
;
2386 //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
2387 exp
.insert( exp
.end(), lexp
.begin(), lexp
.end() );
2388 addToExplanation( lcurr
, lcc
, exp
);
2389 conc
= ac
.eqNode( bc
);
2399 if( !conc
.isNull() ){
2400 Trace("strings-ff-debug") << "Found inference : " << conc
<< " based on equality " << a
<< " == " << b
<< " " << r
<< " " << inf_type
<< std::endl
;
2401 addToExplanation( a
, b
, exp
);
2402 //explain why prefixes up to now were the same
2403 for( unsigned j
=0; j
<count
; j
++ ){
2404 Trace("strings-ff-debug") << "Add at " << d_flat_form_index
[a
][j
] << " " << d_flat_form_index
[b
][j
] << std::endl
;
2405 addToExplanation( a
[d_flat_form_index
[a
][j
]], b
[d_flat_form_index
[b
][j
]], exp
);
2407 //explain why other components up to now are empty
2408 for( unsigned t
=0; t
<2; t
++ ){
2409 Node c
= t
==0 ? a
: b
;
2410 int jj
= t
==0 ? d_flat_form_index
[a
][count
] : ( inf_type
==2 ? ( r
==0 ? c
.getNumChildren() : -1 ) : d_flat_form_index
[b
][count
] );
2412 for( int j
=0; j
<jj
; j
++ ){
2413 if( areEqual( c
[j
], d_emptyString
) ){
2414 addToExplanation( c
[j
], d_emptyString
, exp
);
2418 for( int j
=(c
.getNumChildren()-1); j
>jj
; --j
){
2419 if( areEqual( c
[j
], d_emptyString
) ){
2420 addToExplanation( c
[j
], d_emptyString
, exp
);
2425 //if( exp_n.empty() ){
2426 sendInfer( mkAnd( exp
), conc
, inf_type
==0? "F_Const" : ( inf_type
==1 ? "F_LengthEq" : ( inf_type
==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
2436 }while( inelig
.size()<it
->second
.size() );
2438 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
2439 std::reverse( d_flat_form
[it
->second
[i
]].begin(), d_flat_form
[it
->second
[i
]].end() );
2440 std::reverse( d_flat_form_index
[it
->second
[i
]].begin(), d_flat_form_index
[it
->second
[i
]].end() );
2449 Node
TheoryStrings::checkCycles( Node eqc
, std::vector
< Node
>& curr
, std::vector
< Node
>& exp
){
2450 if( std::find( curr
.begin(), curr
.end(), eqc
)!=curr
.end() ){
2453 }else if( std::find( d_strings_eqc
.begin(), d_strings_eqc
.end(), eqc
)==d_strings_eqc
.end() ){
2454 curr
.push_back( eqc
);
2455 //look at all terms in this equivalence class
2456 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
2457 while( !eqc_i
.isFinished() ) {
2459 if( d_congruent
.find( n
)==d_congruent
.end() ){
2460 Trace("strings-cycle") << eqc
<< " check term : " << n
<< " in " << eqc
<< std::endl
;
2461 if( n
.getKind() == kind::STRING_CONCAT
) {
2462 if( eqc
!=d_emptyString_r
){
2463 d_eqc
[eqc
].push_back( n
);
2465 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2466 Node nr
= getRepresentative( n
[i
] );
2467 if( eqc
==d_emptyString_r
){
2468 //for empty eqc, ensure all components are empty
2469 if( nr
!=d_emptyString_r
){
2470 sendInfer( n
.eqNode( d_emptyString
), n
[i
].eqNode( d_emptyString
), "I_CYCLE_E" );
2471 return Node::null();
2474 if( nr
!=d_emptyString_r
){
2475 d_flat_form
[n
].push_back( nr
);
2476 d_flat_form_index
[n
].push_back( i
);
2478 //for non-empty eqc, recurse and see if we find a loop
2479 Node ncy
= checkCycles( nr
, curr
, exp
);
2480 if( !ncy
.isNull() ){
2481 Trace("strings-cycle") << eqc
<< " cycle: " << ncy
<< " at " << n
<< "[" << i
<< "] : " << n
[i
] << std::endl
;
2482 addToExplanation( n
, eqc
, exp
);
2483 addToExplanation( nr
, n
[i
], exp
);
2485 //can infer all other components must be empty
2486 for( unsigned j
=0; j
<n
.getNumChildren(); j
++ ){
2487 //take first non-empty
2488 if( j
!=i
&& !areEqual( n
[j
], d_emptyString
) ){
2489 sendInfer( mkAnd( exp
), n
[j
].eqNode( d_emptyString
), "I_CYCLE" );
2490 return Node::null();
2493 Trace("strings-error") << "Looping term should be congruent : " << n
<< " " << eqc
<< " " << ncy
<< std::endl
;
2494 //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
2500 if( hasProcessed() ){
2501 return Node::null();
2511 //now we can add it to the list of equivalence classes
2512 d_strings_eqc
.push_back( eqc
);
2516 return Node::null();
2520 void TheoryStrings::checkNormalForms() {
2521 // simple extended func reduction
2522 Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl
;
2523 checkExtfReduction( 1 );
2524 Trace("strings-process") << "Done check extended function reduction" << std::endl
;
2525 if( !hasProcessed() ){
2526 Trace("strings-process") << "Normalize equivalence classes...." << std::endl
;
2527 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
2528 d_normal_forms
.clear();
2529 d_normal_forms_exp
.clear();
2530 std::map
< Node
, Node
> nf_to_eqc
;
2531 std::map
< Node
, Node
> eqc_to_exp
;
2532 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
2533 Node eqc
= d_strings_eqc
[i
];
2534 Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc
<< std::endl
;
2535 std::vector
< Node
> visited
;
2536 std::vector
< Node
> nf
;
2537 std::vector
< Node
> nf_exp
;
2538 normalizeEquivalenceClass(eqc
, visited
, nf
, nf_exp
);
2539 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl
;
2542 } else if ( d_pending
.empty() && d_lemma_cache
.empty() ) {
2543 Node nf_term
= mkConcat( nf
);
2544 if( nf_to_eqc
.find( nf_term
)!=nf_to_eqc
.end() ) {
2545 //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
2546 //two equivalence classes have same normal form, merge
2547 nf_exp
.push_back( eqc_to_exp
[nf_to_eqc
[nf_term
]] );
2548 Node eq
= eqc
.eqNode( nf_to_eqc
[nf_term
] );
2549 sendInfer( mkAnd( nf_exp
), eq
, "Normal_Form" );
2551 nf_to_eqc
[nf_term
] = eqc
;
2552 eqc_to_exp
[eqc
] = mkAnd( nf_exp
);
2555 Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc
<< std::endl
;
2558 if(Trace
.isOn("strings-nf")) {
2559 Trace("strings-nf") << "**** Normal forms are : " << std::endl
;
2560 for( std::map
< Node
, Node
>::iterator it
= nf_to_eqc
.begin(); it
!= nf_to_eqc
.end(); ++it
){
2561 Trace("strings-nf") << " N[" << it
->second
<< "] = " << it
->first
<< std::endl
;
2563 Trace("strings-nf") << std::endl
;
2565 if( !hasProcessed() ){
2566 checkExtendedFuncsEval( 1 );
2567 Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
2568 if( !hasProcessed() ){
2569 if( !options::stringEagerLen() ){
2571 if( hasProcessed() ){
2575 //process disequalities between equivalence classes
2577 Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
2581 Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache
.size() << ", conflict = " << d_conflict
<< std::endl
;
2584 void TheoryStrings::checkDeqNF() {
2585 std::vector
< std::vector
< Node
> > cols
;
2586 std::vector
< Node
> lts
;
2587 separateByLength( d_strings_eqc
, cols
, lts
);
2588 for( unsigned i
=0; i
<cols
.size(); i
++ ){
2589 if( cols
[i
].size()>1 && d_lemma_cache
.empty() ){
2590 Trace("strings-solve") << "- Verify disequalities are processed for " << cols
[i
][0];
2591 printConcat( d_normal_forms
[cols
[i
][0]], "strings-solve" );
2592 Trace("strings-solve") << "... #eql = " << cols
[i
].size() << std::endl
;
2593 //must ensure that normal forms are disequal
2594 for( unsigned j
=0; j
<cols
[i
].size(); j
++ ){
2595 for( unsigned k
=(j
+1); k
<cols
[i
].size(); k
++ ){
2596 if( areDisequal( cols
[i
][j
], cols
[i
][k
] ) ){
2597 Assert( !d_conflict
);
2598 //if( !areDisequal( cols[i][j], cols[i][k] ) ){
2599 // sendSplit( cols[i][j], cols[i][k], "D-NORM", true );
2602 Trace("strings-solve") << "- Compare " << cols
[i
][j
] << " ";
2603 printConcat( d_normal_forms
[cols
[i
][j
]], "strings-solve" );
2604 Trace("strings-solve") << " against " << cols
[i
][k
] << " ";
2605 printConcat( d_normal_forms
[cols
[i
][k
]], "strings-solve" );
2606 Trace("strings-solve") << "..." << std::endl
;
2607 if( processDeq( cols
[i
][j
], cols
[i
][k
] ) ){
2618 void TheoryStrings::checkLengthsEqc() {
2619 if( options::stringLenNorm() ){
2620 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ){
2621 //if( d_normal_forms[nodes[i]].size()>1 ) {
2622 Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc
[i
] << std::endl
;
2623 //check if there is a length term for this equivalence class
2624 EqcInfo
* ei
= getOrMakeEqcInfo( d_strings_eqc
[i
], false );
2625 Node lt
= ei
? ei
->d_length_term
: Node::null();
2626 if( !lt
.isNull() ) {
2627 Node llt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
2628 //now, check if length normalization has occurred
2629 if( ei
->d_normalized_length
.get().isNull() ) {
2630 //if not, add the lemma
2631 std::vector
< Node
> ant
;
2632 ant
.insert( ant
.end(), d_normal_forms_exp
[d_strings_eqc
[i
]].begin(), d_normal_forms_exp
[d_strings_eqc
[i
]].end() );
2633 ant
.push_back( d_normal_forms_base
[d_strings_eqc
[i
]].eqNode( lt
) );
2634 Node lc
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, mkConcat( d_normal_forms
[d_strings_eqc
[i
]] ) );
2635 lc
= Rewriter::rewrite( lc
);
2636 Node eq
= llt
.eqNode( lc
);
2638 ei
->d_normalized_length
.set( eq
);
2639 sendLemma( mkExplain( ant
), eq
, "LEN-NORM" );
2643 Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc
[i
] << " " << d_eqc_to_len_term
[d_strings_eqc
[i
]] << std::endl
;
2644 if( !options::stringEagerLen() ){
2645 Node c
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
2648 NodeNodeMap::const_iterator it
= d_proxy_var
.find( c
);
2649 if( it
!=d_proxy_var
.end() ){
2650 Node pv
= (*it
).second
;
2651 Assert( d_proxy_var_to_length
.find( pv
)!=d_proxy_var_to_length
.end() );
2652 Node pvl
= d_proxy_var_to_length
[pv
];
2653 Node ceq
= Rewriter::rewrite( mkLength( pv
).eqNode( pvl
) );
2654 sendLemma( d_true
, ceq
, "LEN-NORM-I" );
2660 // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
2666 void TheoryStrings::checkCardinality() {
2667 //int cardinality = options::stringCharCardinality();
2668 //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
2670 std::vector
< std::vector
< Node
> > cols
;
2671 std::vector
< Node
> lts
;
2672 separateByLength( d_strings_eqc
, cols
, lts
);
2674 for( unsigned i
= 0; i
<cols
.size(); ++i
) {
2676 Trace("strings-card") << "Number of strings with length equal to " << lr
<< " is " << cols
[i
].size() << std::endl
;
2677 if( cols
[i
].size() > 1 ) {
2679 unsigned card_need
= 1;
2680 double curr
= (double)cols
[i
].size()-1;
2681 while( curr
>d_card_size
){
2682 curr
= curr
/(double)d_card_size
;
2685 Node cmp
= NodeManager::currentNM()->mkNode( kind::GEQ
, lr
, NodeManager::currentNM()->mkConst( Rational( card_need
) ) );
2686 cmp
= Rewriter::rewrite( cmp
);
2688 unsigned int int_k
= (unsigned int)card_need
;
2689 bool allDisequal
= true;
2690 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
2691 itr1
!= cols
[i
].end(); ++itr1
) {
2692 for( std::vector
< Node
>::iterator itr2
= itr1
+ 1;
2693 itr2
!= cols
[i
].end(); ++itr2
) {
2694 if(!areDisequal( *itr1
, *itr2
)) {
2695 allDisequal
= false;
2697 sendSplit( *itr1
, *itr2
, "CARD-SP" );
2703 EqcInfo
* ei
= getOrMakeEqcInfo( lr
, true );
2704 Trace("strings-card") << "Previous cardinality used for " << lr
<< " is " << ((int)ei
->d_cardinality_lem_k
.get()-1) << std::endl
;
2705 if( int_k
+1 > ei
->d_cardinality_lem_k
.get() ){
2706 Node k_node
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k
) );
2707 //add cardinality lemma
2708 Node dist
= NodeManager::currentNM()->mkNode( kind::DISTINCT
, cols
[i
] );
2709 std::vector
< Node
> vec_node
;
2710 vec_node
.push_back( dist
);
2711 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
2712 itr1
!= cols
[i
].end(); ++itr1
) {
2713 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr1
);
2715 Node len_eq_lr
= len
.eqNode(lr
);
2716 vec_node
.push_back( len_eq_lr
);
2719 Node antc
= NodeManager::currentNM()->mkNode( kind::AND
, vec_node
);
2720 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, cols
[i
][0] );
2721 Node cons
= NodeManager::currentNM()->mkNode( kind::GEQ
, len
, k_node
);
2722 cons
= Rewriter::rewrite( cons
);
2723 ei
->d_cardinality_lem_k
.set( int_k
+1 );
2725 sendLemma( antc
, cons
, "CARDINALITY" );
2735 void TheoryStrings::getEquivalenceClasses( std::vector
< Node
>& eqcs
) {
2736 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
2737 while( !eqcs_i
.isFinished() ) {
2738 Node eqc
= (*eqcs_i
);
2739 //if eqc.getType is string
2740 if (eqc
.getType().isString()) {
2741 eqcs
.push_back( eqc
);
2747 void TheoryStrings::getFinalNormalForm( Node n
, std::vector
< Node
>& nf
, std::vector
< Node
>& exp
) {
2748 if( n
!=d_emptyString
) {
2749 if( n
.getKind()==kind::STRING_CONCAT
) {
2750 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
2751 getFinalNormalForm( n
[i
], nf
, exp
);
2754 Trace("strings-debug") << "Get final normal form " << n
<< std::endl
;
2755 Assert( d_equalityEngine
.hasTerm( n
) );
2756 Node nr
= d_equalityEngine
.getRepresentative( n
);
2757 EqcInfo
*eqc_n
= getOrMakeEqcInfo( nr
, false );
2758 Node nc
= eqc_n
? eqc_n
->d_const_term
.get() : Node::null();
2759 if( !nc
.isNull() ) {
2762 exp
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, n
, nc
) );
2765 Assert( d_normal_forms
.find( nr
)!=d_normal_forms
.end() );
2766 if( d_normal_forms
[nr
][0]==nr
) {
2767 Assert( d_normal_forms
[nr
].size()==1 );
2770 exp
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, n
, nr
) );
2773 for( unsigned i
=0; i
<d_normal_forms
[nr
].size(); i
++ ) {
2774 Assert( d_normal_forms
[nr
][i
]!=nr
);
2775 getFinalNormalForm( d_normal_forms
[nr
][i
], nf
, exp
);
2777 exp
.insert( exp
.end(), d_normal_forms_exp
[nr
].begin(), d_normal_forms_exp
[nr
].end() );
2780 Trace("strings-ind-nf") << "The final normal form of " << n
<< " is " << nf
<< std::endl
;
2785 void TheoryStrings::separateByLength(std::vector
< Node
>& n
,
2786 std::vector
< std::vector
< Node
> >& cols
,
2787 std::vector
< Node
>& lts
) {
2788 unsigned leqc_counter
= 0;
2789 std::map
< Node
, unsigned > eqc_to_leqc
;
2790 std::map
< unsigned, Node
> leqc_to_eqc
;
2791 std::map
< unsigned, std::vector
< Node
> > eqc_to_strings
;
2792 for( unsigned i
=0; i
<n
.size(); i
++ ) {
2794 Assert( d_equalityEngine
.getRepresentative(eqc
)==eqc
);
2795 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
2796 Node lt
= ei
? ei
->d_length_term
: Node::null();
2797 Trace("ajr-temp") << "Length term for " << eqc
<< " is " << lt
<< std::endl
;
2799 lt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
2800 Node r
= d_equalityEngine
.getRepresentative( lt
);
2801 Trace("ajr-temp") << "Length term rep for " << eqc
<< " is " << lt
<< std::endl
;
2802 if( eqc_to_leqc
.find( r
)==eqc_to_leqc
.end() ){
2803 eqc_to_leqc
[r
] = leqc_counter
;
2804 leqc_to_eqc
[leqc_counter
] = r
;
2807 eqc_to_strings
[ eqc_to_leqc
[r
] ].push_back( eqc
);
2809 eqc_to_strings
[leqc_counter
].push_back( eqc
);
2813 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= eqc_to_strings
.begin(); it
!= eqc_to_strings
.end(); ++it
){
2814 cols
.push_back( std::vector
< Node
>() );
2815 cols
.back().insert( cols
.back().end(), it
->second
.begin(), it
->second
.end() );
2816 lts
.push_back( leqc_to_eqc
[it
->first
] );
2820 void TheoryStrings::printConcat( std::vector
< Node
>& n
, const char * c
) {
2821 for( unsigned i
=0; i
<n
.size(); i
++ ){
2822 if( i
>0 ) Trace(c
) << " ++ ";
2830 void TheoryStrings::updateMpl( Node n, int b ) {
2831 if(d_mpl.find(n) == d_mpl.end()) {
2832 //d_curr_cardinality.get();
2834 } else if(b < d_mpl[n]) {
2840 //// Regular Expressions
2841 Node
TheoryStrings::mkRegExpAntec(Node atom
, Node ant
) {
2842 if(d_regexp_ant
.find(atom
) == d_regexp_ant
.end()) {
2843 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, atom
) );
2845 Node n
= d_regexp_ant
[atom
];
2846 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, n
) );
2850 Node
TheoryStrings::normalizeRegexp(Node r
) {
2852 if(d_nf_regexps
.find(r
) != d_nf_regexps
.end()) {
2853 nf_r
= d_nf_regexps
[r
];
2855 std::vector
< Node
> nf_exp
;
2856 if(!d_regexp_opr
.checkConstRegExp(r
)) {
2857 switch( r
.getKind() ) {
2858 case kind::REGEXP_EMPTY
:
2859 case kind::REGEXP_SIGMA
: {
2862 case kind::STRING_TO_REGEXP
: {
2863 if(r
[0].isConst()) {
2866 if(d_normal_forms
.find( r
[0] ) != d_normal_forms
.end()) {
2867 nf_r
= mkConcat( d_normal_forms
[r
[0]] );
2868 Debug("regexp-nf") << "Term: " << r
[0] << " has a normal form " << nf_r
<< std::endl
;
2869 nf_exp
.insert(nf_exp
.end(), d_normal_forms_exp
[r
[0]].begin(), d_normal_forms_exp
[r
[0]].end());
2870 nf_r
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, nf_r
) );
2874 case kind::REGEXP_CONCAT
:
2875 case kind::REGEXP_UNION
:
2876 case kind::REGEXP_INTER
: {
2878 std::vector
< Node
> vec_nodes
;
2879 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
2880 Node rtmp
= normalizeRegexp(r
[i
]);
2881 vec_nodes
.push_back(rtmp
);
2887 Node rtmp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(r
.getKind(), vec_nodes
);
2888 nf_r
= Rewriter::rewrite( rtmp
);
2891 case kind::REGEXP_STAR
: {
2892 Node rtmp
= normalizeRegexp(r
[0]);
2894 rtmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, rtmp
);
2895 nf_r
= Rewriter::rewrite( rtmp
);
2903 d_nf_regexps
[r
] = nf_r
;
2904 d_nf_regexps_exp
[r
] = nf_exp
;
2909 bool TheoryStrings::normalizePosMemberships(std::map
< Node
, std::vector
< Node
> > &memb_with_exps
) {
2910 std::map
< Node
, std::vector
< Node
> > unprocessed_x_exps
;
2911 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships
;
2912 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships_bases
;
2913 bool addLemma
= false;
2915 Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl
;
2917 for(NodeListMap::const_iterator itr_xr
= d_pos_memberships
.begin();
2918 itr_xr
!= d_pos_memberships
.end(); ++itr_xr
) {
2919 Node x
= (*itr_xr
).first
;
2920 NodeList
* lst
= (*itr_xr
).second
;
2922 std::vector
< Node
> nf_x_exp
;
2923 if(d_normal_forms
.find( x
) != d_normal_forms
.end()) {
2924 //nf_x = mkConcat( d_normal_forms[x] );
2925 nf_x_exp
.insert(nf_x_exp
.end(), d_normal_forms_exp
[x
].begin(), d_normal_forms_exp
[x
].end());
2926 //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
2930 Trace("regexp-nf") << "Checking Memberships for N(" << x
<< ") = " << nf_x
<< " :" << std::endl
;
2932 std::vector
< Node
> vec_x
;
2933 std::vector
< Node
> vec_r
;
2934 for(NodeList::const_iterator itr_lst
= lst
->begin();
2935 itr_lst
!= lst
->end(); ++itr_lst
) {
2937 Node nf_r
= normalizeRegexp((*lst
)[0]);
2938 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, nf_r
);
2939 if(d_processed_memberships
.find(memb
) == d_processed_memberships
.end()) {
2940 if(d_regexp_opr
.checkConstRegExp(nf_r
)) {
2944 Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r
<< ") = " << nf_r
<< std::endl
;
2945 //TODO: handle symbolic ones
2948 d_processed_memberships
.insert(memb
);
2951 if(!vec_x
.empty()) {
2952 if(unprocessed_x_exps
.find(nf_x
) == unprocessed_x_exps
.end()) {
2953 unprocessed_x_exps
[nf_x
] = nf_x_exp
;
2954 unprocessed_memberships
[nf_x
] = vec_r
;
2955 unprocessed_memberships_bases
[nf_x
] = vec_x
;
2957 unprocessed_x_exps
[nf_x
].insert(unprocessed_x_exps
[nf_x
].end(), nf_x_exp
.begin(), nf_x_exp
.end());
2958 unprocessed_memberships
[nf_x
].insert(unprocessed_memberships
[nf_x
].end(), vec_r
.begin(), vec_r
.end());
2959 unprocessed_memberships_bases
[nf_x
].insert(unprocessed_memberships_bases
[nf_x
].end(), vec_x
.begin(), vec_x
.end());
2964 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= unprocessed_memberships
.begin();
2965 itr
!= unprocessed_memberships
.end(); ++itr
) {
2966 Node nf_x
= itr
->first
;
2967 std::vector
< Node
> exp( unprocessed_x_exps
[nf_x
] );
2968 Node r
= itr
->second
[0];
2970 Node inter_r
= d_nf_regexps
[r
];
2971 exp
.insert(exp
.end(), d_nf_regexps_exp
[r
].begin(), d_nf_regexps_exp
[r
].end());
2972 Node x
= unprocessed_memberships_bases
[itr
->first
][0];
2973 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
);
2974 exp
.push_back(memb
);
2975 for(std::size_t i
=1; i
< itr
->second
.size(); i
++) {
2977 Node r2
= itr
->second
[i
];
2978 Node inter_r2
= d_nf_regexps
[r2
];
2979 exp
.insert(exp
.end(), d_nf_regexps_exp
[r2
].begin(), d_nf_regexps_exp
[r2
].end());
2980 Node x2
= unprocessed_memberships_bases
[itr
->first
][i
];
2981 memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x2
, r2
);
2982 exp
.push_back(memb
);
2984 bool spflag
= false;
2985 inter_r
= d_regexp_opr
.intersect(inter_r
, inter_r2
, spflag
);
2986 if(inter_r
== d_emptyRegexp
) {
2988 Node antec
= exp
.size() == 1? exp
[0] : NodeManager::currentNM()->mkNode(kind::AND
, exp
);
2990 sendLemma(antec
, conc
, "INTERSECT CONFLICT");
2997 memb
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, inter_r
) );
2998 memb_with_exps
[memb
] = exp
;
3007 bool TheoryStrings::applyRConsume( CVC4::String
&s
, Node
&r
) {
3008 Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s
<< ", r= " << r
<< std::endl
;
3009 Assert( d_regexp_opr
.checkConstRegExp(r
) );
3011 if( !s
.isEmptyString() ) {
3014 for(unsigned i
=0; i
<s
.size(); ++i
) {
3015 CVC4::String c
= s
.substr(i
, 1);
3017 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
3021 } else if(rt
== 2) {
3031 Node
TheoryStrings::applyRSplit(Node s1
, Node s2
, Node r
) {
3032 Assert(d_regexp_opr
.checkConstRegExp(r
));
3034 std::vector
< std::pair
< Node
, Node
> > vec_can
;
3035 d_regexp_opr
.splitRegExp(r
, vec_can
);
3036 //TODO: lazy cache or eager?
3037 std::vector
< Node
> vec_or
;
3039 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
3040 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
3041 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
3042 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
3043 vec_or
.push_back( c
);
3045 Node conc
= vec_or
.size()==0? Node::null() : vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
3049 bool TheoryStrings::applyRLen(std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
3050 if(XinR_with_exps
.size() > 0) {
3051 //TODO: get vector, var, store.
3058 bool TheoryStrings::checkMembershipsWithoutLength(
3059 std::map
< Node
, std::vector
< Node
> > &memb_with_exps
,
3060 std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
3061 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= memb_with_exps
.begin();
3062 itr
!= memb_with_exps
.end(); ++itr
) {
3063 Node memb
= itr
->first
;
3067 memb
= Rewriter::rewrite( memb
);
3068 if(memb
== d_false
) {
3069 Node antec
= itr
->second
.size() == 1? itr
->second
[0] : NodeManager::currentNM()->mkNode(kind::AND
, itr
->second
);
3071 sendLemma(antec
, conc
, "MEMBERSHIP CONFLICT");
3075 Assert(memb
== d_true
);
3077 } else if(s
.getKind() == kind::VARIABLE
) {
3079 XinR_with_exps
[itr
->first
] = itr
->second
;
3081 Assert(s
.getKind() == kind::STRING_CONCAT
);
3082 Node antec
= itr
->second
.size() == 1? itr
->second
[0] : NodeManager::currentNM()->mkNode(kind::AND
, itr
->second
);
3084 for( unsigned i
=0; i
<s
.getNumChildren(); i
++ ) {
3085 if(s
[i
].isConst()) {
3086 CVC4::String
str( s
[0].getConst
< String
>() );
3087 //R-Consume, see Tianyi's thesis
3088 if(!applyRConsume(str
, r
)) {
3089 sendLemma(antec
, conc
, "R-Consume CONFLICT");
3094 //R-Split, see Tianyi's thesis
3095 if(i
== s
.getNumChildren() - 1) {
3097 Node memb2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
[i
], r
);
3098 XinR_with_exps
[itr
->first
] = itr
->second
;
3101 std::vector
< Node
> vec_s2
;
3102 for( unsigned j
=i
+1; j
<s
.getNumChildren(); j
++ ) {
3103 vec_s2
.push_back(s
[j
]);
3105 Node s2
= mkConcat(vec_s2
);
3106 conc
= applyRSplit(s1
, s2
, r
);
3107 if(conc
== d_true
) {
3109 } else if(conc
.isNull() || conc
== d_false
) {
3110 conc
= Node::null();
3111 sendLemma(antec
, conc
, "R-Split Conflict");
3115 sendLemma(antec
, conc
, "R-Split");
3127 bool TheoryStrings::checkMemberships2() {
3128 bool addedLemma
= false;
3129 d_nf_regexps
.clear();
3130 d_nf_regexps_exp
.clear();
3131 std::map
< Node
, std::vector
< Node
> > memb_with_exps
;
3132 std::map
< Node
, std::vector
< Node
> > XinR_with_exps
;
3134 addedLemma
= normalizePosMemberships( memb_with_exps
);
3137 addedLemma
|= checkMembershipsWithoutLength( memb_with_exps
, XinR_with_exps
);
3138 //TODO: check addlemma
3139 if (!addedLemma
&& !d_conflict
) {
3140 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= XinR_with_exps
.begin();
3141 itr
!= XinR_with_exps
.end(); ++itr
) {
3142 std::vector
<Node
> vec_or
;
3143 d_regexp_opr
.disjunctRegExp( itr
->first
, vec_or
);
3144 Node tmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_or
);
3145 Trace("regexp-process") << "Got r: " << itr
->first
<< " to " << tmp
<< std::endl
;
3147 if(r.getKind() == kind::REGEXP_STAR) {
3149 addedLemma = applyRLen(XinR_with_exps);
3155 Assert(false); //TODO:tmp
3162 void TheoryStrings::checkMemberships() {
3163 bool addedLemma
= false;
3164 bool changed
= false;
3165 std::vector
< Node
> processed
;
3166 std::vector
< Node
> cprocessed
;
3168 Trace("regexp-debug") << "Checking Memberships ... " << std::endl
;
3169 //if(options::stringEIT()) {
3170 //TODO: Opt for normal forms
3171 for(NodeListMap::const_iterator itr_xr
= d_pos_memberships
.begin();
3172 itr_xr
!= d_pos_memberships
.end(); ++itr_xr
) {
3173 bool spflag
= false;
3174 Node x
= (*itr_xr
).first
;
3175 NodeList
* lst
= (*itr_xr
).second
;
3176 Trace("regexp-debug") << "Checking Memberships for " << x
<< std::endl
;
3177 if(d_inter_index
.find(x
) == d_inter_index
.end()) {
3178 d_inter_index
[x
] = 0;
3180 int cur_inter_idx
= d_inter_index
[x
];
3181 if(cur_inter_idx
!= (int)lst
->size()) {
3182 if(lst
->size() == 1) {
3183 d_inter_cache
[x
] = (*lst
)[0];
3184 d_inter_index
[x
] = 1;
3185 Trace("regexp-debug") << "... only one choice " << std::endl
;
3186 } else if(lst
->size() > 1) {
3188 if(d_inter_cache
.find(x
) != d_inter_cache
.end()) {
3189 r
= d_inter_cache
[x
];
3195 NodeList::const_iterator itr_lst
= lst
->begin();
3196 for(int i
=0; i
<cur_inter_idx
; i
++) {
3199 Trace("regexp-debug") << "... staring from : " << cur_inter_idx
<< ", we have " << lst
->size() << std::endl
;
3200 for(;itr_lst
!= lst
->end(); ++itr_lst
) {
3202 r
= d_regexp_opr
.intersect(r
, r2
, spflag
);
3205 } else if(r
== d_emptyRegexp
) {
3206 std::vector
< Node
> vec_nodes
;
3208 for(NodeList::const_iterator itr2
= lst
->begin();
3209 itr2
!= itr_lst
; ++itr2
) {
3210 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, *itr2
);
3211 vec_nodes
.push_back( n
);
3213 Node antec
= vec_nodes
.size() == 1? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
3215 sendLemma(antec
, conc
, "INTERSECT CONFLICT");
3224 if(!d_conflict
&& !spflag
) {
3225 d_inter_cache
[x
] = r
;
3226 d_inter_index
[x
] = (int)lst
->size();
3233 Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma
<< std::endl
;
3235 for( unsigned i
=0; i
<d_regexp_memberships
.size(); i
++ ) {
3236 //check regular expression membership
3237 Node assertion
= d_regexp_memberships
[i
];
3238 if( d_regexp_ucached
.find(assertion
) == d_regexp_ucached
.end()
3239 && d_regexp_ccached
.find(assertion
) == d_regexp_ccached
.end() ) {
3240 Trace("strings-regexp") << "We have regular expression assertion : " << assertion
<< std::endl
;
3241 Node atom
= assertion
.getKind()==kind::NOT
? assertion
[0] : assertion
;
3242 bool polarity
= assertion
.getKind()!=kind::NOT
;
3246 std::vector
< Node
> rnfexp
;
3248 if(options::stringOpt1()) {
3250 x
= getNormalString( x
, rnfexp
);
3253 if(!d_regexp_opr
.checkConstRegExp(r
)) {
3254 r
= getNormalSymRegExp(r
, rnfexp
);
3257 Trace("strings-regexp-nf") << "Term " << atom
<< " is normalized to " << x
<< " IN " << r
<< std::endl
;
3259 Node tmp
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
) );
3264 d_regexp_ccached
.insert(assertion
);
3266 } else if(tmp
== d_false
) {
3267 Node antec
= mkRegExpAntec(assertion
, mkExplain(rnfexp
));
3268 Node conc
= Node::null();
3269 sendLemma(antec
, conc
, "REGEXP NF Conflict");
3277 flag
= checkPDerivative(x
, r
, atom
, addedLemma
, processed
, cprocessed
, rnfexp
);
3278 if(options::stringOpt2() && flag
) {
3279 if(d_regexp_opr
.checkConstRegExp(r
) && x
.getKind()==kind::STRING_CONCAT
) {
3280 std::vector
< std::pair
< Node
, Node
> > vec_can
;
3281 d_regexp_opr
.splitRegExp(r
, vec_can
);
3282 //TODO: lazy cache or eager?
3283 std::vector
< Node
> vec_or
;
3284 std::vector
< Node
> vec_s2
;
3285 for(unsigned int s2i
=1; s2i
<x
.getNumChildren(); s2i
++) {
3286 vec_s2
.push_back(x
[s2i
]);
3289 Node s2
= mkConcat(vec_s2
);
3290 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
3291 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
3292 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
3293 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
3294 vec_or
.push_back( c
);
3296 Node conc
= vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
3297 //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
3298 Node antec
= mkRegExpAntec(atom
, mkExplain(rnfexp
));
3299 if(conc
== d_true
) {
3301 cprocessed
.push_back( assertion
);
3303 processed
.push_back( assertion
);
3305 } else if(conc
== d_false
) {
3306 conc
= Node::null();
3307 sendLemma(antec
, conc
, "RegExp CST-SP Conflict");
3309 sendLemma(antec
, conc
, "RegExp-CST-SP");
3316 if(! options::stringExp()) {
3317 throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
3321 //check if the term is atomic
3322 Node xr
= getRepresentative( x
);
3323 //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
3324 //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
3326 if( true || r
.getKind()!=kind::REGEXP_STAR
|| ( d_normal_forms
[xr
].size()==1 && x
.getKind()!=kind::STRING_CONCAT
) ){
3327 Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr
<< std::endl
;
3328 //if so, do simple unrolling
3329 std::vector
< Node
> nvec
;
3331 /*if(xr.isConst()) {
3332 Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r) );
3333 if(tmp==d_true || tmp==d_false) {
3335 tmp = tmp==d_true? d_false : d_true;
3337 nvec.push_back( tmp );
3342 d_regexp_opr
.simplify(atom
, nvec
, polarity
);
3344 Node antec
= assertion
;
3345 if(d_regexp_ant
.find(assertion
) != d_regexp_ant
.end()) {
3346 antec
= d_regexp_ant
[assertion
];
3347 for(std::vector
< Node
>::const_iterator itr
=nvec
.begin(); itr
<nvec
.end(); itr
++) {
3348 if(itr
->getKind() == kind::STRING_IN_REGEXP
) {
3349 if(d_regexp_ant
.find( *itr
) == d_regexp_ant
.end()) {
3350 d_regexp_ant
[ *itr
] = antec
;
3355 antec
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, antec
, mkExplain(rnfexp
)) );
3356 Node conc
= nvec
.size()==1 ? nvec
[0] :
3357 NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
3358 conc
= Rewriter::rewrite(conc
);
3359 sendLemma( antec
, conc
, "REGEXP" );
3362 cprocessed
.push_back( assertion
);
3364 processed
.push_back( assertion
);
3366 //d_regexp_ucached[assertion] = true;
3368 Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr
<< " = ";
3369 for( unsigned j
=0; j
<d_normal_forms
[xr
].size(); j
++ ){
3370 Trace("strings-regexp") << d_normal_forms
[xr
][j
] << " ";
3372 Trace("strings-regexp") << ", polarity = " << polarity
<< std::endl
;
3373 //otherwise, distribute unrolling over parts
3376 if( d_normal_forms
[xr
].size()>1 ){
3377 p1
= d_normal_forms
[xr
][0];
3378 std::vector
< Node
> cc
;
3379 cc
.insert( cc
.begin(), d_normal_forms
[xr
].begin() + 1, d_normal_forms
[xr
].end() );
3380 p2
= mkConcat( cc
);
3383 Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl
;
3384 std::vector
< Node
> antec
;
3385 std::vector
< Node
> antecn
;
3386 antec
.insert( antec
.begin(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
3388 antec
.push_back( x
.eqNode( xr
) );
3390 antecn
.push_back( assertion
);
3391 Node ant
= mkExplain( antec
, antecn
);
3392 Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl
;
3395 if( d_normal_forms
[xr
].size()==0 ){
3397 }else if( d_normal_forms
[xr
].size()==1 ){
3398 Trace("strings-regexp-debug") << "Case 1\n";
3399 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
);
3401 Trace("strings-regexp-debug") << "Case 2\n";
3402 std::vector
< Node
> conc_c
;
3403 Node s11
= mkSkolemS( "s11" );
3404 Node s12
= mkSkolemS( "s12" );
3405 Node s21
= mkSkolemS( "s21" );
3406 Node s22
= mkSkolemS( "s22" );
3407 conc
= p1
.eqNode( mkConcat(s11
, s12
) );
3408 conc_c
.push_back(conc
);
3409 conc
= p2
.eqNode( mkConcat(s21
, s22
) );
3410 conc_c
.push_back(conc
);
3411 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
);
3412 conc_c
.push_back(conc
);
3413 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]);
3414 conc_c
.push_back(conc
);
3415 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
);
3416 conc_c
.push_back(conc
);
3417 conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, conc_c
));
3418 Node eqz
= Rewriter::rewrite(x
.eqNode(d_emptyString
));
3419 conc
= NodeManager::currentNM()->mkNode(kind::OR
, eqz
, conc
);
3420 d_pending_req_phase
[eqz
] = true;
3423 if( d_normal_forms
[xr
].size()==0 ){
3425 }else if( d_normal_forms
[xr
].size()==1 ){
3426 Trace("strings-regexp-debug") << "Case 3\n";
3427 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
).negate();
3429 Trace("strings-regexp-debug") << "Case 4\n";
3430 Node len1
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p1
);
3431 Node len2
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p2
);
3432 Node bi
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
3433 Node bj
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
3434 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, bi
, bj
);
3435 Node g1
= NodeManager::currentNM()->mkNode(kind::AND
,
3436 NodeManager::currentNM()->mkNode(kind::GEQ
, bi
, d_zero
),
3437 NodeManager::currentNM()->mkNode(kind::GEQ
, len1
, bi
),
3438 NodeManager::currentNM()->mkNode(kind::GEQ
, bj
, d_zero
),
3439 NodeManager::currentNM()->mkNode(kind::GEQ
, len2
, bj
));
3440 Node s11
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, d_zero
, bi
);
3441 Node s12
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, bi
, NodeManager::currentNM()->mkNode(kind::MINUS
, len1
, bi
));
3442 Node s21
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, d_zero
, bj
);
3443 Node s22
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, bj
, NodeManager::currentNM()->mkNode(kind::MINUS
, len2
, bj
));
3444 Node cc1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
).negate();
3445 Node cc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]).negate();
3446 Node cc3
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
).negate();
3447 conc
= NodeManager::currentNM()->mkNode(kind::OR
, cc1
, cc2
, cc3
);
3448 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
3449 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
3450 conc
= NodeManager::currentNM()->mkNode(kind::AND
, x
.eqNode(d_emptyString
).negate(), conc
);
3454 ant
= mkRegExpAntec(assertion
, ant
);
3455 sendLemma(ant
, conc
, "REGEXP CSTAR");
3457 if( conc
==d_false
){
3458 d_regexp_ccached
.insert( assertion
);
3460 cprocessed
.push_back( assertion
);
3463 d_regexp_ccached
.insert(assertion
);
3475 for( unsigned i
=0; i
<processed
.size(); i
++ ) {
3476 d_regexp_ucached
.insert(processed
[i
]);
3478 for( unsigned i
=0; i
<cprocessed
.size(); i
++ ) {
3479 d_regexp_ccached
.insert(cprocessed
[i
]);
3485 bool TheoryStrings::checkPDerivative(Node x
, Node r
, Node atom
, bool &addedLemma
,
3486 std::vector
< Node
> &processed
, std::vector
< Node
> &cprocessed
, std::vector
< Node
> &nf_exp
) {
3487 /*if(d_opt_regexp_gcd) {
3488 if(d_membership_length.find(atom) == d_membership_length.end()) {
3489 addedLemma = addMembershipLength(atom);
3490 d_membership_length[atom] = true;
3492 Trace("strings-regexp") << "Membership length is already added." << std::endl;
3495 Node antnf
= mkExplain(nf_exp
);
3497 if(areEqual(x
, d_emptyString
)) {
3499 switch(d_regexp_opr
.delta(r
, exp
)) {
3501 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
3502 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
3503 sendLemma(antec
, exp
, "RegExp Delta");
3505 d_regexp_ccached
.insert(atom
);
3509 d_regexp_ccached
.insert(atom
);
3513 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
3514 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
3515 Node conc
= Node::null();
3516 sendLemma(antec
, conc
, "RegExp Delta CONFLICT");
3518 d_regexp_ccached
.insert(atom
);
3526 /*Node xr = getRepresentative( x );
3528 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
3529 Node nn = Rewriter::rewrite( n );
3531 d_regexp_ccached.insert(atom);
3533 } else if(nn == d_false) {
3534 Node antec = mkRegExpAntec(atom, x.eqNode(xr));
3535 Node conc = Node::null();
3536 sendLemma(antec, conc, "RegExp Delta CONFLICT");
3538 d_regexp_ccached.insert(atom);
3542 Node sREant
= mkRegExpAntec(atom
, d_true
);
3543 sREant
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, sREant
, antnf
));
3544 if(deriveRegExp( x
, r
, sREant
)) {
3546 processed
.push_back( atom
);
3553 void TheoryStrings::checkInit() {
3555 d_eqc_to_const
.clear();
3556 d_eqc_to_const_base
.clear();
3557 d_eqc_to_const_exp
.clear();
3558 d_eqc_to_len_term
.clear();
3559 d_term_index
.clear();
3560 d_strings_eqc
.clear();
3562 std::map
< Kind
, unsigned > ncongruent
;
3563 std::map
< Kind
, unsigned > congruent
;
3564 d_emptyString_r
= getRepresentative( d_emptyString
);
3565 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
3566 while( !eqcs_i
.isFinished() ){
3567 Node eqc
= (*eqcs_i
);
3568 TypeNode tn
= eqc
.getType();
3569 if( !tn
.isRegExp() ){
3570 if( tn
.isString() ){
3571 d_strings_eqc
.push_back( eqc
);
3573 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
3574 while( !eqc_i
.isFinished() ) {
3576 if( tn
.isInteger() ){
3577 if( n
.getKind()==kind::STRING_LENGTH
){
3578 Node nr
= getRepresentative( n
[0] );
3579 d_eqc_to_len_term
[nr
] = n
[0];
3581 }else if( n
.isConst() ){
3582 d_eqc_to_const
[eqc
] = n
;
3583 d_eqc_to_const_base
[eqc
] = n
;
3584 d_eqc_to_const_exp
[eqc
] = Node::null();
3585 }else if( n
.getNumChildren()>0 ){
3586 Kind k
= n
.getKind();
3587 if( k
!=kind::EQUAL
){
3588 if( d_congruent
.find( n
)==d_congruent
.end() ){
3589 std::vector
< Node
> c
;
3590 Node nc
= d_term_index
[k
].add( n
, 0, this, d_emptyString_r
, c
);
3592 //check if we have inferred a new equality by removal of empty components
3593 if( n
.getKind()==kind::STRING_CONCAT
&& !areEqual( nc
, n
) ){
3594 std::vector
< Node
> exp
;
3595 unsigned count
[2] = { 0, 0 };
3596 while( count
[0]<nc
.getNumChildren() || count
[1]<n
.getNumChildren() ){
3597 //explain empty prefixes
3598 for( unsigned t
=0; t
<2; t
++ ){
3599 Node nn
= t
==0 ? nc
: n
;
3600 while( count
[t
]<nn
.getNumChildren() &&
3601 ( nn
[count
[t
]]==d_emptyString
|| areEqual( nn
[count
[t
]], d_emptyString
) ) ){
3602 if( nn
[count
[t
]]!=d_emptyString
){
3603 exp
.push_back( nn
[count
[t
]].eqNode( d_emptyString
) );
3608 //explain equal components
3609 if( count
[0]<nc
.getNumChildren() ){
3610 Assert( count
[1]<n
.getNumChildren() );
3611 if( nc
[count
[0]]!=n
[count
[1]] ){
3612 exp
.push_back( nc
[count
[0]].eqNode( n
[count
[1]] ) );
3618 //infer the equality
3619 sendInfer( mkAnd( exp
), n
.eqNode( nc
), "I_Norm" );
3621 //update the extf map : only process if neither has been reduced
3622 NodeBoolMap::const_iterator it
= d_ext_func_terms
.find( n
);
3623 if( it
!=d_ext_func_terms
.end() ){
3624 if( d_ext_func_terms
.find( nc
)==d_ext_func_terms
.end() ){
3625 d_ext_func_terms
[nc
] = (*it
).second
;
3627 d_ext_func_terms
[nc
] = d_ext_func_terms
[nc
] && (*it
).second
;
3629 d_ext_func_terms
[n
] = false;
3632 //this node is congruent to another one, we can ignore it
3633 Trace("strings-process-debug") << " congruent term : " << n
<< std::endl
;
3634 d_congruent
.insert( n
);
3636 }else if( k
==kind::STRING_CONCAT
&& c
.size()==1 ){
3637 Trace("strings-process-debug") << " congruent term by singular : " << n
<< " " << c
[0] << std::endl
;
3639 if( !areEqual( c
[0], n
) ){
3640 std::vector
< Node
> exp
;
3641 //explain empty components
3642 bool foundNEmpty
= false;
3643 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
3644 if( areEqual( n
[i
], d_emptyString
) ){
3645 if( n
[i
]!=d_emptyString
){
3646 exp
.push_back( n
[i
].eqNode( d_emptyString
) );
3649 Assert( !foundNEmpty
);
3651 exp
.push_back( n
[i
].eqNode( c
[0] ) );
3656 AlwaysAssert( foundNEmpty
);
3657 //infer the equality
3658 sendInfer( mkAnd( exp
), n
.eqNode( c
[0] ), "I_Norm_S" );
3660 d_congruent
.insert( n
);
3675 if( Trace
.isOn("strings-process") ){
3676 for( std::map
< Kind
, TermIndex
>::iterator it
= d_term_index
.begin(); it
!= d_term_index
.end(); ++it
){
3677 Trace("strings-process") << " Terms[" << it
->first
<< "] = " << ncongruent
[it
->first
] << "/" << (congruent
[it
->first
]+ncongruent
[it
->first
]) << std::endl
;
3680 Trace("strings-process") << "Done check init, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
3681 //now, infer constants for equivalence classes
3682 if( !hasProcessed() ){
3686 Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl
;
3687 prevSize
= d_eqc_to_const
.size();
3688 std::vector
< Node
> vecc
;
3689 checkConstantEquivalenceClasses( &d_term_index
[kind::STRING_CONCAT
], vecc
);
3690 }while( !hasProcessed() && d_eqc_to_const
.size()>prevSize
);
3691 Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
3695 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex
* ti
, std::vector
< Node
>& vecc
) {
3696 Node n
= ti
->d_data
;
3698 //construct the constant
3699 Node c
= mkConcat( vecc
);
3700 if( !areEqual( n
, c
) ){
3701 Trace("strings-debug") << "Constant eqc : " << c
<< " for " << n
<< std::endl
;
3702 Trace("strings-debug") << " ";
3703 for( unsigned i
=0; i
<vecc
.size(); i
++ ){
3704 Trace("strings-debug") << vecc
[i
] << " ";
3706 Trace("strings-debug") << std::endl
;
3708 unsigned countc
= 0;
3709 std::vector
< Node
> exp
;
3710 while( count
<n
.getNumChildren() ){
3711 while( count
<n
.getNumChildren() && areEqual( n
[count
], d_emptyString
) ){
3712 addToExplanation( n
[count
], d_emptyString
, exp
);
3715 if( count
<n
.getNumChildren() ){
3716 Trace("strings-debug") << "...explain " << n
[count
] << " " << vecc
[countc
] << std::endl
;
3717 if( !areEqual( n
[count
], vecc
[countc
] ) ){
3718 Node nrr
= getRepresentative( n
[count
] );
3719 Assert( !d_eqc_to_const_exp
[nrr
].isNull() );
3720 addToExplanation( n
[count
], d_eqc_to_const_base
[nrr
], exp
);
3721 exp
.push_back( d_eqc_to_const_exp
[nrr
] );
3723 addToExplanation( n
[count
], vecc
[countc
], exp
);
3729 //exp contains an explanation of n==c
3730 Assert( countc
==vecc
.size() );
3732 sendInfer( mkAnd( exp
), n
.eqNode( c
), "I_CONST_MERGE" );
3734 }else if( !hasProcessed() ){
3735 Node nr
= getRepresentative( n
);
3736 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( nr
);
3737 if( it
==d_eqc_to_const
.end() ){
3738 Trace("strings-debug") << "Set eqc const " << n
<< " to " << c
<< std::endl
;
3739 d_eqc_to_const
[nr
] = c
;
3740 d_eqc_to_const_base
[nr
] = n
;
3741 d_eqc_to_const_exp
[nr
] = mkAnd( exp
);
3742 }else if( c
!=it
->second
){
3744 Trace("strings-debug") << "Conflict, other constant was " << it
->second
<< ", this constant was " << c
<< std::endl
;
3745 if( d_eqc_to_const_exp
[nr
].isNull() ){
3746 // n==c ^ n == c' => false
3747 addToExplanation( n
, it
->second
, exp
);
3749 // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
3750 exp
.push_back( d_eqc_to_const_exp
[nr
] );
3751 addToExplanation( n
, d_eqc_to_const_base
[nr
], exp
);
3753 sendLemma( mkExplain( exp
), d_false
, "I_CONST_CONFLICT" );
3756 Trace("strings-debug") << "Duplicate constant." << std::endl
;
3761 for( std::map
< Node
, TermIndex
>::iterator it
= ti
->d_children
.begin(); it
!= ti
->d_children
.end(); ++it
){
3762 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( it
->first
);
3763 if( itc
!=d_eqc_to_const
.end() ){
3764 vecc
.push_back( itc
->second
);
3765 checkConstantEquivalenceClasses( &it
->second
, vecc
);
3767 if( hasProcessed() ){
3774 void TheoryStrings::checkExtendedFuncsEval( int effort
) {
3775 Trace("strings-extf-list") << "Active extended functions, effort=" << effort
<< " : " << std::endl
;
3777 d_extf_vars
.clear();
3781 d_extf_info
.clear();
3782 Trace("strings-extf-debug") << "Checking " << d_ext_func_terms
.size() << " extended functions." << std::endl
;
3783 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
3785 Node n
= (*it
).first
;
3787 if( n
.getType().isBoolean() ){
3788 if( areEqual( n
, d_true
) ){
3790 }else if( areEqual( n
, d_false
) ){
3794 Trace("strings-extf-debug") << "Check extf " << n
<< ", pol = " << d_extf_pol
[n
] << "..." << std::endl
;
3796 std::map
< Node
, bool > visited
;
3797 collectVars( n
, d_extf_vars
[n
], visited
);
3799 //build up a best current substitution for the variables in the term, exp is explanation for substitution
3800 std::vector
< Node
> var
;
3801 std::vector
< Node
> sub
;
3802 for( std::map
< Node
, std::vector
< Node
> >::iterator itv
= d_extf_vars
[n
].begin(); itv
!= d_extf_vars
[n
].end(); ++itv
){
3803 Node nr
= itv
->first
;
3804 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( nr
);
3808 if( itc
!=d_eqc_to_const
.end() ){
3809 b
= d_eqc_to_const_base
[nr
];
3811 e
= d_eqc_to_const_exp
[nr
];
3812 }else if( effort
>0 ){
3813 b
= d_normal_forms_base
[nr
];
3814 std::vector
< Node
> expt
;
3815 s
= getNormalString( b
, expt
);
3820 for( unsigned i
=0; i
<itv
->second
.size(); i
++ ){
3821 if( itv
->second
[i
]!=s
){
3822 var
.push_back( itv
->second
[i
] );
3824 addToExplanation( itv
->second
[i
], b
, d_extf_exp
[n
] );
3825 Trace("strings-extf-debug") << " " << itv
->second
[i
] << " --> " << s
<< std::endl
;
3830 addToExplanation( e
, d_extf_exp
[n
] );
3836 Node nr
= n
.substitute( var
.begin(), var
.end(), sub
.begin(), sub
.end() );
3837 Node nrc
= Rewriter::rewrite( nr
);
3838 if( nrc
.isConst() ){
3840 d_ext_func_terms
[n
] = false;
3841 Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl
;
3842 std::vector
< Node
> exps
;
3843 Trace("strings-extf-debug") << " get symbolic definition..." << std::endl
;
3844 Node nrs
= getSymbolicDefinition( nr
, exps
);
3845 if( !nrs
.isNull() ){
3846 Trace("strings-extf-debug") << " rewrite " << nrs
<< "..." << std::endl
;
3847 nrs
= Rewriter::rewrite( nrs
);
3848 //ensure the symbolic form is non-trivial
3849 if( nrs
.isConst() ){
3850 Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl
;
3854 Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl
;
3857 if( !nrs
.isNull() ){
3858 Trace("strings-extf-debug") << " symbolic def : " << nrs
<< std::endl
;
3859 if( !areEqual( nrs
, nrc
) ){
3860 //infer symbolic unit
3861 if( n
.getType().isBoolean() ){
3862 conc
= nrc
==d_true
? nrs
: nrs
.negate();
3864 conc
= nrs
.eqNode( nrc
);
3866 d_extf_exp
[n
].clear();
3869 if( !areEqual( n
, nrc
) ){
3870 if( n
.getType().isBoolean() ){
3871 d_extf_exp
[n
].push_back( nrc
==d_true
? n
.negate() : n
);
3874 conc
= n
.eqNode( nrc
);
3878 if( !conc
.isNull() ){
3879 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< std::endl
;
3880 if( n
.getType().isInteger() || d_extf_exp
[n
].empty() ){
3881 sendLemma( mkExplain( d_extf_exp
[n
] ), conc
, effort
==0 ? "EXTF" : "EXTF-N" );
3883 sendInfer( mkAnd( d_extf_exp
[n
] ), conc
, effort
==0 ? "EXTF" : "EXTF-N" );
3886 Trace("strings-extf-debug") << " conflict, return." << std::endl
;
3890 }else if( ( nrc
.getKind()==kind::OR
&& d_extf_pol
[n
]==-1 ) || ( nrc
.getKind()==kind::AND
&& d_extf_pol
[n
]==1 ) ){
3891 //infer the consequence of each
3892 d_ext_func_terms
[n
] = false;
3893 d_extf_exp
[n
].push_back( d_extf_pol
[n
]==-1 ? n
.negate() : n
);
3894 Trace("strings-extf-debug") << " decomposable..." << std::endl
;
3895 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< ", pol = " << d_extf_pol
[n
] << std::endl
;
3896 for( unsigned i
=0; i
<nrc
.getNumChildren(); i
++ ){
3897 sendInfer( mkAnd( d_extf_exp
[n
] ), d_extf_pol
[n
]==-1 ? nrc
[i
].negate() : nrc
[i
], effort
==0 ? "EXTF_d" : "EXTF_d-N" );
3905 if( !to_reduce
.isNull() ){
3907 Trace("strings-extf") << " cannot rewrite extf : " << to_reduce
<< std::endl
;
3909 checkExtfInference( n
, to_reduce
, effort
);
3910 if( Trace
.isOn("strings-extf-list") ){
3911 Trace("strings-extf-list") << " * " << to_reduce
;
3912 if( d_extf_pol
[n
]!=0 ){
3913 Trace("strings-extf-list") << ", pol = " << d_extf_pol
[n
];
3916 Trace("strings-extf-list") << ", from " << n
;
3918 Trace("strings-extf-list") << std::endl
;
3922 Trace("strings-extf-debug") << " already reduced " << (*it
).first
<< std::endl
;
3927 void TheoryStrings::checkExtfInference( Node n
, Node nr
, int effort
){
3928 int n_pol
= d_extf_pol
[n
];
3930 //add original to explanation
3931 d_extf_exp
[n
].push_back( n_pol
==1 ? n
: n
.negate() );
3932 if( nr
.getKind()==kind::STRING_STRCTN
){
3933 if( ( n_pol
==1 && nr
[1].getKind()==kind::STRING_CONCAT
) || ( n_pol
==-1 && nr
[0].getKind()==kind::STRING_CONCAT
) ){
3934 if( d_extf_infer_cache
.find( nr
)==d_extf_infer_cache
.end() ){
3935 d_extf_infer_cache
.insert( nr
);
3936 //one argument does (not) contain each of the components of the other argument
3937 int index
= n_pol
==1 ? 1 : 0;
3938 std::vector
< Node
> children
;
3939 children
.push_back( nr
[0] );
3940 children
.push_back( nr
[1] );
3941 Node exp_n
= mkAnd( d_extf_exp
[n
] );
3942 for( unsigned i
=0; i
<nr
[index
].getNumChildren(); i
++ ){
3943 children
[index
] = nr
[index
][i
];
3944 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, children
);
3945 //can mark as reduced, since model for n => model for conc
3946 d_ext_func_terms
[conc
] = false;
3947 sendInfer( exp_n
, n_pol
==1 ? conc
: conc
.negate(), "CTN_Decompose" );
3951 //store this (reduced) assertion
3952 //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
3953 bool pol
= n_pol
==1;
3954 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() ){
3955 Trace("strings-extf-debug") << " store contains info : " << nr
[0] << " " << pol
<< " " << nr
[1] << std::endl
;
3956 d_extf_info
[nr
[0]].d_ctn
[pol
].push_back( nr
[1] );
3957 d_extf_info
[nr
[0]].d_ctn_from
[pol
].push_back( n
);
3958 //transitive closure for contains
3960 for( unsigned i
=0; i
<d_extf_info
[nr
[0]].d_ctn
[opol
].size(); i
++ ){
3961 Node onr
= d_extf_info
[nr
[0]].d_ctn
[opol
][i
];
3962 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, pol
? nr
[1] : onr
, pol
? onr
: nr
[1] ).negate();
3963 std::vector
< Node
> exp
;
3964 exp
.insert( exp
.end(), d_extf_exp
[n
].begin(), d_extf_exp
[n
].end() );
3965 Node ofrom
= d_extf_info
[nr
[0]].d_ctn_from
[opol
][i
];
3966 Assert( d_extf_exp
.find( ofrom
)!=d_extf_exp
.end() );
3967 exp
.insert( exp
.end(), d_extf_exp
[ofrom
].begin(), d_extf_exp
[ofrom
].end() );
3968 sendInfer( mkAnd( exp
), conc
, "CTN_Trans" );
3971 Trace("strings-extf-debug") << " redundant." << std::endl
;
3972 d_ext_func_terms
[n
] = false;
3979 void TheoryStrings::collectVars( Node n
, std::map
< Node
, std::vector
< Node
> >& vars
, std::map
< Node
, bool >& visited
) {
3981 if( visited
.find( n
)==visited
.end() ){
3983 if( n
.getNumChildren()>0 ){
3984 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
3985 collectVars( n
[i
], vars
, visited
);
3988 Node nr
= getRepresentative( n
);
3989 vars
[nr
].push_back( n
);
3995 Node
TheoryStrings::getSymbolicDefinition( Node n
, std::vector
< Node
>& exp
) {
3996 if( n
.getNumChildren()==0 ){
3997 NodeNodeMap::const_iterator it
= d_proxy_var
.find( n
);
3998 if( it
==d_proxy_var
.end() ){
3999 return Node::null();
4001 Node eq
= n
.eqNode( (*it
).second
);
4002 eq
= Rewriter::rewrite( eq
);
4003 if( std::find( exp
.begin(), exp
.end(), eq
)==exp
.end() ){
4004 exp
.push_back( eq
);
4006 return (*it
).second
;
4009 std::vector
< Node
> children
;
4010 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
4011 children
.push_back( n
.getOperator() );
4013 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
4014 if( n
.getKind()==kind::STRING_IN_REGEXP
&& i
==1 ){
4015 children
.push_back( n
[i
] );
4017 Node ns
= getSymbolicDefinition( n
[i
], exp
);
4019 return Node::null();
4021 children
.push_back( ns
);
4025 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
4029 void TheoryStrings::checkExtendedFuncs() {
4030 if( options::stringExp() ){
4031 checkExtfReduction( 2 );
4033 if( !hasProcessed() ){
4034 //collect all remaining extended functions
4035 std::vector
< Node
> pnContains
;
4036 std::map
< bool, std::vector
< Node
> > pnMem
;
4037 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
4039 Node n
= (*it
).first
;
4040 if( n
.getKind()==kind::STRING_STRCTN
) {
4041 if( d_extf_pol
[n
]!=1 ){
4042 Assert( d_extf_pol
[n
]==-1 );
4043 pnContains
.push_back( n
);
4045 }else if( n
.getKind()==kind::STRING_IN_REGEXP
) {
4046 bool pol
= d_extf_pol
[n
]==1;
4047 Assert( d_extf_pol
[n
]==1 || d_extf_pol
[n
]==-1 );
4048 pnMem
[pol
].push_back( n
);
4052 Trace("strings-process-debug") << "Checking negative contains..." << std::endl
;
4053 checkNegContains( pnContains
);
4054 Trace("strings-process-debug") << "Done check negative contain constraints, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
4055 if( !hasProcessed() ) {
4056 Trace("strings-process") << "Adding memberships..." << std::endl
;
4057 //add all non-evaluated memberships
4058 for( std::map
< bool, std::vector
< Node
> >::iterator it
=pnMem
.begin(); it
!= pnMem
.end(); ++it
){
4059 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
4060 Trace("strings-process-debug") << " add membership : " << it
->second
[i
] << ", pol = " << it
->first
<< std::endl
;
4061 addMembership( it
->first
? it
->second
[i
] : it
->second
[i
].negate() );
4065 Trace("strings-process") << "Done check memberships, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
4070 void TheoryStrings::checkNegContains( std::vector
< Node
>& negContains
) {
4071 for( unsigned i
=0; i
<negContains
.size(); i
++ ){
4072 Node atom
= negContains
[i
];
4073 Trace("strings-ctn") << "We have negative contain assertion : (not " << atom
<< " )" << std::endl
;
4074 //should have already reduced these things by now
4075 Assert( !areEqual( atom
[1], d_emptyString
) );
4076 Assert( !areEqual( atom
[1], atom
[0] ) );
4079 if(options::stringExp()) {
4080 for( unsigned i
=0; i
<negContains
.size(); i
++ ){
4081 Node atom
= negContains
[i
];
4084 std::vector
< Node
> lexp
;
4085 Node lenx
= getLength( x
, lexp
);
4086 Node lens
= getLength( s
, lexp
);
4087 if( areEqual(lenx
, lens
) ){
4088 if(d_neg_ctn_eqlen
.find(atom
) == d_neg_ctn_eqlen
.end()) {
4089 lexp
.push_back( lenx
.eqNode(lens
) );
4090 lexp
.push_back( atom
.negate() );
4091 Node xneqs
= x
.eqNode(s
).negate();
4092 d_neg_ctn_eqlen
.insert( atom
);
4093 sendLemma( mkExplain( lexp
), xneqs
, "NEG-CTN-EQL" );
4095 }else if( !areDisequal( lenx
, lens
) ){
4096 if(d_neg_ctn_ulen
.find(atom
) == d_neg_ctn_ulen
.end()) {
4097 lenx
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, x
);
4098 lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
4099 d_neg_ctn_ulen
.insert( atom
);
4100 sendSplit( lenx
, lens
, "NEG-CTN-SP" );
4103 if(d_neg_ctn_cached
.find(atom
) == d_neg_ctn_cached
.end()) {
4104 lenx
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, x
);
4105 lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
4106 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4107 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
4108 Node g1
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode( kind::GEQ
, b1
, d_zero
),
4109 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode( kind::MINUS
, lenx
, lens
), b1
) ) );
4110 Node b2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4111 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, x
, NodeManager::currentNM()->mkNode( kind::PLUS
, b1
, b2
), d_one
);
4112 Node s5
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, s
, b2
, d_one
);
4114 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b2
);//, s1, s3, s4, s6);
4116 std::vector
< Node
> vec_nodes
;
4117 Node cc
= NodeManager::currentNM()->mkNode( kind::GEQ
, b2
, d_zero
);
4118 vec_nodes
.push_back(cc
);
4119 cc
= NodeManager::currentNM()->mkNode( kind::GT
, lens
, b2
);
4120 vec_nodes
.push_back(cc
);
4122 cc
= s2
.eqNode(s5
).negate();
4123 vec_nodes
.push_back(cc
);
4125 Node conc
= NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
4126 conc
= NodeManager::currentNM()->mkNode( kind::EXISTS
, b2v
, conc
);
4127 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, g1
, conc
);
4128 conc
= NodeManager::currentNM()->mkNode( kind::FORALL
, b1v
, conc
);
4129 Node xlss
= NodeManager::currentNM()->mkNode( kind::GT
, lens
, lenx
);
4130 conc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR
, xlss
, conc
) );
4132 d_neg_ctn_cached
.insert( atom
);
4133 sendLemma( atom
.negate(), conc
, "NEG-CTN-BRK" );
4134 //d_pending_req_phase[xlss] = true;
4139 if( !negContains
.empty() ){
4140 throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
4145 CVC4::String
TheoryStrings::getHeadConst( Node x
) {
4147 return x
.getConst
< String
>();
4148 } else if( x
.getKind() == kind::STRING_CONCAT
) {
4149 if( x
[0].isConst() ) {
4150 return x
[0].getConst
< String
>();
4152 return d_emptyString
.getConst
< String
>();
4155 return d_emptyString
.getConst
< String
>();
4159 bool TheoryStrings::addMembershipLength(Node atom
) {
4163 /*std::vector< int > co;
4165 for(unsigned int k=0; k<lts.size(); ++k) {
4166 if(lts[k].isConst() && lts[k].getType().isInteger()) {
4167 int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
4168 co[0] += cols[k].size() * len;
4170 co.push_back( cols[k].size() );
4174 for(unsigned k=1; k<co.size(); ++k) {
4175 g_co = gcd(g_co, co[k]);
4180 bool TheoryStrings::deriveRegExp( Node x
, Node r
, Node ant
) {
4182 Assert(x
!= d_emptyString
);
4183 Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x
<< ", r= " << r
<< std::endl
;
4185 // Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
4186 // Node r = Rewriter::rewrite( n );
4188 // sendLemma(ant, r, "REGEXP REWRITE");
4192 CVC4::String s
= getHeadConst( x
);
4193 if( !s
.isEmptyString() && d_regexp_opr
.checkConstRegExp( r
) ) {
4194 Node conc
= Node::null();
4197 for(unsigned i
=0; i
<s
.size(); ++i
) {
4198 CVC4::String c
= s
.substr(i
, 1);
4200 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
4204 } else if(rt
== 2) {
4213 Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
4216 Assert( x
.getKind() == kind::STRING_CONCAT
);
4217 std::vector
< Node
> vec_nodes
;
4218 for(unsigned int i
=1; i
<x
.getNumChildren(); ++i
) {
4219 vec_nodes
.push_back( x
[i
] );
4221 Node left
= mkConcat( vec_nodes
);
4222 left
= Rewriter::rewrite( left
);
4223 conc
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, left
, dc
);
4225 /*std::vector< Node > sdc;
4226 d_regexp_opr.simplify(conc, sdc, true);
4227 if(sdc.size() == 1) {
4230 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
4234 sendLemma(ant
, conc
, "RegExp-Derive");
4241 void TheoryStrings::addMembership(Node assertion
) {
4242 bool polarity
= assertion
.getKind() != kind::NOT
;
4243 TNode atom
= polarity
? assertion
: assertion
[0];
4248 NodeListMap::iterator itr_xr
= d_pos_memberships
.find( x
);
4249 if( itr_xr
== d_pos_memberships
.end() ){
4250 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
4251 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
4252 d_pos_memberships
.insertDataFromContextMemory( x
, lst
);
4254 lst
= (*itr_xr
).second
;
4257 for( NodeList::const_iterator itr
= lst
->begin(); itr
!= lst
->end(); ++itr
) {
4262 lst
->push_back( r
);
4263 } else if(!options::stringIgnNegMembership()) {
4264 /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
4266 Node r2 = d_regexp_opr.complement(r, rt);
4267 Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
4270 NodeListMap::iterator itr_xr
= d_neg_memberships
.find( x
);
4271 if( itr_xr
== d_neg_memberships
.end() ){
4272 lst
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
4273 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
4274 d_neg_memberships
.insertDataFromContextMemory( x
, lst
);
4276 lst
= (*itr_xr
).second
;
4279 for( NodeList::const_iterator itr
= lst
->begin(); itr
!= lst
->end(); ++itr
) {
4284 lst
->push_back( r
);
4287 if(polarity
|| !options::stringIgnNegMembership()) {
4288 d_regexp_memberships
.push_back( assertion
);
4292 Node
TheoryStrings::getNormalString( Node x
, std::vector
<Node
> &nf_exp
){
4294 Node xr
= getRepresentative( x
);
4295 if( d_normal_forms
.find( xr
) != d_normal_forms
.end() ){
4296 Node ret
= mkConcat( d_normal_forms
[xr
] );
4297 nf_exp
.insert( nf_exp
.end(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
4298 addToExplanation( x
, d_normal_forms_base
[xr
], nf_exp
);
4299 Trace("strings-debug") << "Term: " << x
<< " has a normal form " << ret
<< std::endl
;
4302 if(x
.getKind() == kind::STRING_CONCAT
) {
4303 std::vector
< Node
> vec_nodes
;
4304 for(unsigned i
=0; i
<x
.getNumChildren(); i
++) {
4305 Node nc
= getNormalString( x
[i
], nf_exp
);
4306 vec_nodes
.push_back( nc
);
4308 return mkConcat( vec_nodes
);
4315 Node
TheoryStrings::getNormalSymRegExp(Node r
, std::vector
<Node
> &nf_exp
) {
4317 switch( r
.getKind() ) {
4318 case kind::REGEXP_EMPTY
:
4319 case kind::REGEXP_SIGMA
:
4321 case kind::STRING_TO_REGEXP
: {
4322 if(!r
[0].isConst()) {
4323 Node tmp
= getNormalString( r
[0], nf_exp
);
4325 ret
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, tmp
);
4330 case kind::REGEXP_CONCAT
: {
4331 std::vector
< Node
> vec_nodes
;
4332 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4333 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4335 ret
= mkConcat(vec_nodes
);
4338 case kind::REGEXP_UNION
: {
4339 std::vector
< Node
> vec_nodes
;
4340 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4341 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4343 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
) );
4346 case kind::REGEXP_INTER
: {
4347 std::vector
< Node
> vec_nodes
;
4348 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4349 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4351 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER
, vec_nodes
) );
4354 case kind::REGEXP_STAR
: {
4355 ret
= getNormalSymRegExp( r
[0], nf_exp
);
4356 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, ret
) );
4359 //case kind::REGEXP_PLUS:
4360 //case kind::REGEXP_OPT:
4361 //case kind::REGEXP_RANGE:
4363 Trace("strings-error") << "Unsupported term: " << r
<< " in normalization SymRegExp." << std::endl
;
4365 //return Node::null();
4372 //// Finite Model Finding
4374 Node
TheoryStrings::getNextDecisionRequest() {
4375 if( options::stringFMF() && !d_conflict
){
4376 Node in_var_lsum
= d_input_var_lsum
.get();
4377 //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
4378 //initialize the term we will minimize
4379 if( in_var_lsum
.isNull() && !d_input_vars
.empty() ){
4380 Trace("strings-fmf-debug") << "Input variables: ";
4381 std::vector
< Node
> ll
;
4382 for(NodeSet::key_iterator itr
= d_input_vars
.key_begin();
4383 itr
!= d_input_vars
.key_end(); ++itr
) {
4384 Trace("strings-fmf-debug") << " " << (*itr
) ;
4385 ll
.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr
) );
4387 Trace("strings-fmf-debug") << std::endl
;
4388 in_var_lsum
= ll
.size()==1 ? ll
[0] : NodeManager::currentNM()->mkNode( kind::PLUS
, ll
);
4389 in_var_lsum
= Rewriter::rewrite( in_var_lsum
);
4390 d_input_var_lsum
.set( in_var_lsum
);
4392 if( !in_var_lsum
.isNull() ){
4393 //Trace("strings-fmf") << "Get next decision request." << std::endl;
4394 //check if we need to decide on something
4395 int decideCard
= d_curr_cardinality
.get();
4396 if( d_cardinality_lits
.find( decideCard
)!=d_cardinality_lits
.end() ){
4398 Node cnode
= d_cardinality_lits
[ d_curr_cardinality
.get() ];
4399 if( d_valuation
.hasSatValue( cnode
, value
) ) {
4401 d_curr_cardinality
.set( d_curr_cardinality
.get() + 1 );
4402 decideCard
= d_curr_cardinality
.get();
4403 Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl
;
4406 Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl
;
4409 Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl
;
4412 if( decideCard
!=-1 ){
4413 if( d_cardinality_lits
.find( decideCard
)==d_cardinality_lits
.end() ){
4414 Node lit
= NodeManager::currentNM()->mkNode( kind::LEQ
, in_var_lsum
, NodeManager::currentNM()->mkConst( Rational( decideCard
) ) );
4415 lit
= Rewriter::rewrite( lit
);
4416 d_cardinality_lits
[decideCard
] = lit
;
4417 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lit
, lit
.negate() );
4418 Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem
<< ", decideCard = " << decideCard
<< std::endl
;
4419 d_out
->lemma( lem
);
4420 d_out
->requirePhase( lit
, true );
4422 Node lit
= d_cardinality_lits
[ decideCard
];
4423 Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit
<< std::endl
;
4429 return Node::null();
4432 void TheoryStrings::collectExtendedFuncTerms( Node n
, std::map
< Node
, bool >& visited
) {
4433 if( visited
.find( n
)==visited
.end() ){
4435 if( n
.getKind()==kind::STRING_SUBSTR
|| n
.getKind()==kind::STRING_STRIDOF
||
4436 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
4437 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
4438 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
4439 if( d_ext_func_terms
.find( n
)==d_ext_func_terms
.end() ){
4440 Trace("strings-extf-debug2") << "Found extended function : " << n
<< std::endl
;
4441 d_ext_func_terms
[n
] = true;
4444 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
4445 collectExtendedFuncTerms( n
[i
], visited
);
4451 TheoryStrings::Statistics::Statistics():
4452 d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
4453 d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
4454 d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
4455 d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
4456 d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
4458 StatisticsRegistry::registerStat(&d_splits
);
4459 StatisticsRegistry::registerStat(&d_eq_splits
);
4460 StatisticsRegistry::registerStat(&d_deq_splits
);
4461 StatisticsRegistry::registerStat(&d_loop_lemmas
);
4462 StatisticsRegistry::registerStat(&d_new_skolems
);
4465 TheoryStrings::Statistics::~Statistics(){
4466 StatisticsRegistry::unregisterStat(&d_splits
);
4467 StatisticsRegistry::unregisterStat(&d_eq_splits
);
4468 StatisticsRegistry::unregisterStat(&d_deq_splits
);
4469 StatisticsRegistry::unregisterStat(&d_loop_lemmas
);
4470 StatisticsRegistry::unregisterStat(&d_new_skolems
);
4473 }/* CVC4::theory::strings namespace */
4474 }/* CVC4::theory namespace */
4475 }/* CVC4 namespace */