diff options
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 95 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 4 |
4 files changed, 103 insertions, 14 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f873b94f2..e15fc85bb 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -273,8 +273,9 @@ void BoundedIntegers::process( Node q, Node n, bool pol, } } -bool BoundedIntegers::needsCheck( Theory::Effort e ) { - return e==Theory::EFFORT_LAST_CALL; +bool BoundedIntegers::needsCheck(Theory::Effort e) +{ + return e == Theory::EFFORT_LAST_CALL; } void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 8791b54b5..f03a9dc90 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -18,6 +18,8 @@ #include "theory/strings/theory_strings_rewriter.h" #include "util/rational.h" +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace strings { @@ -90,23 +92,100 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a << ", " << b << ")" << std::endl; - // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) + NodeManager* nm = NodeManager::currentNM(); + + if (id == SK_FIRST_CTN_POST) + { + // SK_FIRST_CTN_POST(x, y) ---> + // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y))) + id = SK_SUFFIX_REM; + Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre"); + b = Rewriter::rewrite(nm->mkNode( + PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b))); + } + + if (id == SK_ID_C_SPT) + { + // SK_ID_C_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y)) + id = SK_SUFFIX_REM; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } + else if (id == SK_ID_VC_SPT) + { + // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1) + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_VC_SPT_REV) + { + // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1)) + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode( + MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)))); + } + else if (id == SK_ID_DC_SPT) + { + // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1) + id = SK_PREFIX; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_DC_SPT_REM) + { + // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1) + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_DEQ_X) + { + // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x)) + id = SK_PREFIX; + Node aOld = a; + a = b; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, aOld)); + } + else if (id == SK_ID_DEQ_Y) + { + // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y)) + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } + + if (id == SK_SUFFIX_REM) { + //std::cout << "suffix" << a << " " << b << std::endl; + } + if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR) { Node s = a[0]; Node n = a[1]; Node m = a[2]; - if (m.getKind() == kind::STRING_STRIDOF && m[0] == s) + + if (n == d_zero) + { + // SK_PURIFY((str.substr x 0 m)) ---> SK_PREFIX(x, m) + id = SK_PREFIX; + a = s; + b = m; + } + else if (TheoryStringsRewriter::checkEntailArith( + nm->mkNode(PLUS, n, m), nm->mkNode(STRING_LENGTH, s))) { - if (n == d_zero && m[2] == d_zero) - { - id = SK_FIRST_CTN_PRE; - a = m[0]; - b = m[1]; - } + // SK_PURIFY((str.substr x n m)) ---> SK_SUFFIX_REM(x, n) + // if n + m >= (str.len x) + id = SK_SUFFIX_REM; + a = s; + b = n; } } + if (id == SK_PREFIX && b.getKind() == kind::STRING_STRIDOF && a == b[0] + && b[2] == d_zero) + { + // SK_PREFIX(x, (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) + id = SK_FIRST_CTN_PRE; + b = b[1]; + } + if (id == SK_FIRST_CTN_PRE) { // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 67f032193..0883eebfa 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3290,7 +3290,6 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, Node firstChar = stra.size() == 1 ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( 1 ) : stra.prefix( 1 ) ); Node sk = d_sk_cache.mkSkolemCached( other_str, - firstChar, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, "c_spt"); @@ -3688,11 +3687,10 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = d_sk_cache.mkSkolemCached( - nconst_k, firstChar, SkolemCache::SK_ID_DC_SPT, "dc_spt"); + nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); registerLength(sk, LENGTH_ONE); Node skr = d_sk_cache.mkSkolemCached(nconst_k, - firstChar, SkolemCache::SK_ID_DC_SPT_REM, "dc_spt_rem"); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); @@ -4023,6 +4021,15 @@ void TheoryStrings::registerTerm( Node n, int effort ) { Trace("strings-assert") << "(assert " << lem << ")" << std::endl; d_out->lemma(lem); } + else if (n.getKind() == STRING_STRIDOF) + { + Node len = mkLength(n[0]); + Node lem = nm->mkNode( + AND, + nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), + nm->mkNode(LT, n, len)); + d_out->lemma(lem); + } } bool TheoryStrings::sendInternalInference(std::vector<Node>& exp, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f5571349f..fe059e663 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1777,7 +1777,6 @@ set(regress_2_tests regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 regress2/strings/issue918.smt2 - regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 regress2/strings/repl-repl.smt2 regress2/strings/replaceall-diffrange.smt2 @@ -2151,6 +2150,9 @@ set(regression_disabled_tests regress2/quantifiers/small-bug1-fixpoint-3.smt2 regress2/xs-11-20-5-2-5-3.smt regress2/xs-11-20-5-2-5-3.smt2 + # This test does not seem to terminate with aggressive skolem sharing (PR + # #2761) + regress2/strings/non_termination_regular_expression6.smt2 ) #-----------------------------------------------------------------------------# |