From: ajreynol Date: Wed, 10 May 2017 15:35:38 +0000 (-0500) Subject: Do not split on cardinality for string equivalence classes with non-constant lengths... X-Git-Tag: cvc5-1.0.0~5807 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b045d1d06f2d28957ccca6ed7d9e6458b4a96b79;p=cvc5.git Do not split on cardinality for string equivalence classes with non-constant lengths if disequalities already imply sufficient lower bound. Fixes bug 799. --- 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; imkNode( 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( rmkConst( 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::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)