diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 31 | ||||
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/bug799-min.smt2 | 18 |
3 files changed, 47 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 42e43b543..6526b68cf 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2212,7 +2212,7 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > normal_forms_exp_depend.push_back( std::map< Node, std::map< bool, int > >() ); }else{ if(Trace.isOn("strings-solve")) { - Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; + Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc << " : " << std::endl; for( unsigned i=0; i<normal_forms.size(); i++ ) { Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : "; for( unsigned j=0; j<normal_forms[i].size(); j++ ) { @@ -3725,9 +3725,32 @@ void TheoryStrings::checkCardinality() { card_need++; } Trace("strings-card") << "Need length " << card_need << " for this number of strings (where alphabet size is " << d_card_size << ")." << std::endl; - Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) ); - cmp = Rewriter::rewrite( cmp ); - if( cmp!=d_true ){ + //check if we need to split + bool needsSplit = true; + if( lr.isConst() ){ + // if constant, compare + Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) ); + cmp = Rewriter::rewrite( cmp ); + needsSplit = cmp!=d_true; + }else{ + // find the minimimum constant that we are unknown to be disequal from, or otherwise stop if we increment such that cardinality does not apply + unsigned r=0; + bool success = true; + while( r<card_need && success ){ + Node rr = NodeManager::currentNM()->mkConst<Rational>( Rational(r) ); + if( areDisequal( rr, lr ) ){ + r++; + }else{ + success = false; + } + } + if( r>0 ){ + Trace("strings-card") << "Symbolic length " << lr << " must be at least " << r << " due to constant disequalities." << std::endl; + } + needsSplit = r<card_need; + } + + if( needsSplit ){ unsigned int int_k = (unsigned int)card_need; for( std::vector< Node >::iterator itr1 = cols[i].begin(); itr1 != cols[i].end(); ++itr1) { diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 41c500170..5c89c8472 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -87,7 +87,8 @@ TESTS = \ strings-index-empty.smt2 \ bug768.smt2 \ username_checker_min.smt2 \ - repl-empty-sem.smt2 + repl-empty-sem.smt2 \ + bug799-min.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/bug799-min.smt2 b/test/regress/regress0/strings/bug799-min.smt2 new file mode 100644 index 000000000..06acffc97 --- /dev/null +++ b/test/regress/regress0/strings/bug799-min.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --incremental --strings-exp +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun u () String) +(declare-fun s () String) + +(assert (= (str.len u) 9)) +(assert (= (str.at u 1) s)) +(assert (= (str.at u 2) "4")) +(assert (= (str.at u 7) "5")) +(assert (= (str.at u 8) "6")) + +(push 1) +(assert (str.in.re s (re.range "0" "3"))) + +(check-sat) |