From: Tianyi Liang Date: Fri, 5 Dec 2014 00:17:55 +0000 (-0600) Subject: Relaxed the constant requirement for regular expression loop; X-Git-Tag: cvc5-1.0.0~6472 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f8c5e78d97eb7ddc3a29392c9ca18c627279fa2b;p=cvc5.git Relaxed the constant requirement for regular expression loop; Added "ignoring negative membership" option (fragment checking is not provided, and users must make sure the constraint is in the fragment; otherwise, the solution may not be correct). --- diff --git a/src/theory/strings/options b/src/theory/strings/options index 10f22b05a..dc8c50966 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -23,6 +23,9 @@ option stringOpt1 strings-opt1 --strings-opt1 bool :default true option stringOpt2 strings-opt2 --strings-opt2 bool :default false internal option2 for strings: constant regexp splitting +option stringIgnNegMembership strings-inm --strings-inm bool :default false + internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now) + expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" the cardinality of the characters used by the theory of strings, default 256 diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 765fb586e..2347af3e6 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -716,12 +716,17 @@ void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) std::pair< std::set, SetNodes > p(cset, vset); d_fset_cache[r] = p; - Trace("regexp-fset") << "FSET( " << mkString(r) << " ) = { "; - for(std::set::const_iterator itr = cset.begin(); - itr != cset.end(); itr++) { - Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr) << ","; - } - Trace("regexp-fset") << " }" << std::endl; + if(Trace.isOn("regexp-fset")) { + Trace("regexp-fset") << "FSET(" << mkString(r) << ") = {"; + for(std::set::const_iterator itr = cset.begin(); + itr != cset.end(); itr++) { + if(itr != cset.begin()) { + Trace("regexp-fset") << ","; + } + Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr); + } + Trace("regexp-fset") << "}" << std::endl; + } } } @@ -1319,7 +1324,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > r1 = r2; r2 = tmpNode; } - Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; + Trace("regexp-int") << "Starting INTERSECT(" << cnt << "):\n "<< mkString(r1) << ",\n " << mkString(r2) << std::endl; //if(Trace.isOn("regexp-debug")) { // Trace("regexp-debug") << "... with cache:\n"; // for(std::map< PairNodes, Node >::const_iterator itr=cache.begin(); @@ -1372,21 +1377,27 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > Unreachable(); } } - if(Trace.isOn("regexp-debug")) { - Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = "; + if(Trace.isOn("regexp-int-debug")) { + Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {"; for(std::vector::const_iterator itr = cset.begin(); itr != cset.end(); itr++) { CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); - Trace("regexp-debug") << c << ", "; + if(itr != cset.begin()) { + Trace("regexp-int-debug") << ", "; + } + Trace("regexp-int-debug") << c; } - Trace("regexp-debug") << std::endl; + Trace("regexp-int-debug") << std::endl; } std::map< PairNodes, Node > cacheX; for(std::vector::const_iterator itr = cset.begin(); itr != cset.end(); itr++) { CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) ); + Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl; Node r1l = derivativeSingle(r1, c); Node r2l = derivativeSingle(r2, c); + Trace("regexp-int-debug") << " ... got partial(r1,c) = " << mkString(r1l) << std::endl; + Trace("regexp-int-debug") << " ... got partial(r2,c) = " << mkString(r2l) << std::endl; Node rt; if(r1l > r2l) { @@ -1401,11 +1412,13 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > std::map< PairNodes, Node > cache2(cache); cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); rt = intersectInternal(r1l, r2l, cache2, cnt+1); - - rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, - NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); cacheX[ pp ] = rt; } + + rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, + NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) ); + + Trace("regexp-int-debug") << " ... got p(r1,c) && p(r2,c) = " << mkString(rt) << std::endl; vec_nodes.push_back(rt); } rNode = Rewriter::rewrite( vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : @@ -1418,7 +1431,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > d_inter_cache[p] = rNode; } } - Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; + Trace("regexp-int") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; return rNode; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0df551847..384d4567b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -589,7 +589,9 @@ void TheoryStrings::check(Effort e) { //must record string in regular expressions if ( atom.getKind() == kind::STRING_IN_REGEXP ) { addMembership(assertion); - d_equalityEngine.assertPredicate(atom, polarity, fact); + //if(polarity || !options::stringIgnNegMembership()) { + d_equalityEngine.assertPredicate(atom, polarity, fact); + //} } else if (atom.getKind() == kind::STRING_STRCTN) { if(polarity) { d_str_pos_ctn.push_back( atom ); @@ -3460,7 +3462,7 @@ void TheoryStrings::addMembership(Node assertion) { } } lst->push_back( r ); - } else { + } else if(!options::stringIgnNegMembership()) { /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); @@ -3483,7 +3485,10 @@ void TheoryStrings::addMembership(Node assertion) { } lst->push_back( r ); } - d_regexp_memberships.push_back( assertion ); + // old + if(polarity || !options::stringIgnNegMembership()) { + d_regexp_memberships.push_back( assertion ); + } } Node TheoryStrings::getNormalString(Node x, std::vector &nf_exp) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index dfec0a795..6fcbdfff3 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -748,18 +748,26 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(r.getKind() == kind::REGEXP_STAR) { retNode = r; } else { + TNode n1 = Rewriter::rewrite( node[1] ); + if(!n1.isConst()) { + throw LogicException("re.loop contains non-constant integer (1)."); + } CVC4::Rational RMAXINT(LONG_MAX); - Assert(node[1].getConst() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); - unsigned l = node[1].getConst().getNumerator().toUnsignedInt(); + Assert(n1.getConst() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); + unsigned l = n1.getConst().getNumerator().toUnsignedInt(); std::vector< Node > vec_nodes; for(unsigned i=0; imkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(CVC4::String(""))) : vec_nodes.size()==1 ? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes)); - Assert(node[2].getConst() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); - unsigned u = node[2].getConst().getNumerator().toUnsignedInt(); + Assert(n2.getConst() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); + unsigned u = n2.getConst().getNumerator().toUnsignedInt(); if(u <= l) { retNode = n; } else { diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 8a51ea36c..55059fa77 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -388,18 +388,18 @@ public: if (!t.isInteger()) { throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2"); } - if(!(*it).isConst()) { - throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2"); - } + //if(!(*it).isConst()) { + //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2"); + //} ++it; if(it != it_end) { t = (*it).getType(check); if (!t.isInteger()) { throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3"); } - if(!(*it).isConst()) { - throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3"); - } + //if(!(*it).isConst()) { + //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3"); + //} //if(++it != it_end) { // throw TypeCheckingExceptionPrivate(n, "too many regexp"); //} diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 865d05cd2..8a2674cee 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ + regexp002.smt2 \ regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ @@ -53,8 +54,8 @@ TESTS = \ FAILING_TESTS = EXTRA_DIST = $(TESTS) \ + artemis-0512-nonterm.smt2 \ fmf001.smt2 \ - regexp002.smt2 \ type002.smt2 # slow after changes on Nov 20 : artemis-0512-nonterm.smt2 diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 index 18541af4e..8c29ccb38 100644 --- a/test/regress/regress0/strings/regexp002.smt2 +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -1,6 +1,10 @@ (set-logic QF_S) (set-info :status sat) (set-option :strings-exp true) +; this option requires user to check whether the constraint is in the fragment +; currently we do not provide only positive membership constraint checking +; if users use this option but the constraint is not in this fragment, the result will fail +(set-option :strings-inm true) (declare-fun x () String) (declare-fun y () String)