summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/strings_options.toml63
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp5
-rw-r--r--src/theory/strings/skolem_cache.cpp108
-rw-r--r--src/theory/strings/theory_strings.cpp21
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp55
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h2
6 files changed, 227 insertions, 27 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index fd00b8917..dd9599c5c 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -216,3 +216,66 @@ header = "options/strings_options.h"
default = "true"
read_only = true
help = "do flat form inferences"
+
+[[option]]
+ name = "stringsCacheSkolems"
+ category = "expert"
+ long = "strings-cache-skolems"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Cache skolems in string reductions"
+
+[[option]]
+ name = "stringsNormalizeSkolems"
+ category = "expert"
+ long = "strings-normalize-skolems"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Normalize string skolems before looking them up in the cache"
+
+[[option]]
+ name = "stringsRewriterEntailChecks"
+ category = "expert"
+ long = "strings-rewriter-entail-checks"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Enable the entailment checks in the strings rewriter"
+
+[[option]]
+ name = "stringsRewriterApprox"
+ category = "expert"
+ long = "strings-rewriter-entail-approx"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Enable the entailment checks in the strings rewriter"
+
+[[option]]
+ name = "stringsRewriterEntailContainsChecks"
+ category = "expert"
+ long = "strings-rewriter-entail-contains-checks"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Enable the contains entailment checks in the strings rewriter"
+
+[[option]]
+ name = "stringsRewriterMultisetReasoning"
+ category = "expert"
+ long = "strings-rewriter-multiset-reasoning"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Enable multiset reasoning in the strings rewriter"
+
+[[option]]
+ name = "stringsRewriterStripConstantEndpoints"
+ category = "expert"
+ long = "strings-rewriter-strip-constant-endpoints"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "Enable stripping of constant endpoints"
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..669b424a4 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -14,10 +14,13 @@
#include "theory/strings/skolem_cache.h"
+#include "options/strings_options.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
#include "util/rational.h"
+using namespace CVC4::kind;
+
namespace CVC4 {
namespace theory {
namespace strings {
@@ -42,6 +45,13 @@ Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
Node SkolemCache::mkTypedSkolemCached(
TypeNode tn, Node a, Node b, SkolemId id, const char* c)
{
+ if (!options::stringsCacheSkolems())
+ {
+ Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
+ d_allSkolems.insert(n);
+ return n;
+ }
+
a = a.isNull() ? a : Rewriter::rewrite(a);
b = b.isNull() ? b : Rewriter::rewrite(b);
@@ -87,26 +97,108 @@ bool SkolemCache::isSkolem(Node n) const
std::tuple<SkolemCache::SkolemId, Node, Node>
SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
{
+ if (!options::stringsNormalizeSkolems())
+ {
+ return std::make_tuple(id, a, 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 6333bfee1..14216f8aa 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3274,7 +3274,6 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
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");
@@ -3662,11 +3661,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 ) );
@@ -3985,6 +3983,23 @@ 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 lower = n[2];
+ if (!TheoryStringsRewriter::checkEntailArith(lower)) {
+ lower = d_zero;
+ }
+ Node neg = Rewriter::rewrite(nm->mkNode(EQUAL, n, d_neg_one));
+ Node geq = Rewriter::rewrite(nm->mkNode(GEQ, n, lower));
+ Node lem = nm->mkNode(OR, neg, geq);
+ Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl;
+ Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
+ //d_out->lemma(lem);
+ //d_out->requirePhase(neg, true);
+
+ lem = Rewriter::rewrite(nm->mkNode(GT, nm->mkNode(STRING_LENGTH, n[0]), n));
+ d_out->lemma(lem);
+ }
}
bool TheoryStrings::sendInternalInference(std::vector<Node>& exp,
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2e50ade0c..ec9a46e3a 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -624,6 +624,13 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node)
}
}
+ if (checkEntailArith(node[0], node[1], true)
+ || checkEntailArith(node[1], node[0], true))
+ {
+ Node ret = nm->mkConst(false);
+ return returnRewrite(node, ret, "int-eq-false");
+ }
+
return node;
}
@@ -1967,6 +1974,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
{
Node ret = NodeManager::currentNM()->mkNode(
kind::STRING_STRCTN, mkConcat(kind::STRING_CONCAT, nc1), node[1]);
+ Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl;
return returnRewrite(node, ret, "ctn-strip-endpt");
}
@@ -2093,18 +2101,6 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
}
}
}
- else if (node[0].getKind() == kind::STRING_SUBSTR)
- {
- // (str.contains (str.substr x n (str.len y)) y) --->
- // (= (str.substr x n (str.len y)) y)
- //
- // TODO: Remove with under-/over-approximation
- if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
- {
- Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
- return returnRewrite(node, ret, "ctn-substr");
- }
- }
else if (node[0].getKind() == kind::STRING_STRREPL)
{
if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
@@ -2395,6 +2391,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
{
Node ret = mkConcat(kind::STRING_CONCAT, children0);
ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
+ Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl;
// For example:
// str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
return returnRewrite(node, ret, "rpl-pull-endpt");
@@ -2617,6 +2614,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
node[2]));
cc.insert(cc.end(), ce.begin(), ce.end());
Node ret = mkConcat(kind::STRING_CONCAT, cc);
+ Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl;
return returnRewrite(node, ret, "rpl-pull-endpt");
}
}
@@ -3361,6 +3359,11 @@ int TheoryStringsRewriter::componentContains(std::vector<Node>& n1,
bool computeRemainder,
int remainderDir)
{
+ if (!options::stringsRewriterEntailContainsChecks())
+ {
+ return -1;
+ }
+
Assert(nb.empty());
Assert(ne.empty());
// if n2 is a singleton, we can do optimized version here
@@ -3627,6 +3630,11 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
std::vector<Node>& ne,
int dir)
{
+ if (!options::stringsRewriterStripConstantEndpoints())
+ {
+ return false;
+ }
+
Assert(nb.empty());
Assert(ne.empty());
@@ -3870,6 +3878,11 @@ Node TheoryStringsRewriter::checkEntailContains(Node a,
Node b,
bool fullRewriter)
{
+ if (!options::stringsRewriterEntailContainsChecks())
+ {
+ return Node::null();
+ }
+
NodeManager* nm = NodeManager::currentNM();
Node ctn = nm->mkNode(kind::STRING_STRCTN, a, b);
@@ -3952,6 +3965,10 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict)
return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
}
+ if (!options::stringsRewriterEntailChecks()) {
+ return false;
+ }
+
Node ar =
strict
? NodeManager::currentNM()->mkNode(
@@ -3965,7 +3982,7 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict)
}
bool ret = checkEntailArithInternal(ar);
- if (!ret)
+ if (!ret && options::stringsRewriterApprox())
{
// try with approximations
ret = checkEntailArithApprox(ar);
@@ -4441,6 +4458,11 @@ void TheoryStringsRewriter::getArithApproximations(Node a,
bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b)
{
+ if (!options::stringsRewriterMultisetReasoning())
+ {
+ return false;
+ }
+
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> avec;
@@ -4527,6 +4549,11 @@ bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b)
Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a)
{
+ if (!options::stringsRewriterMultisetReasoning())
+ {
+ return Node::null();
+ }
+
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> avec;
@@ -4757,7 +4784,7 @@ Node TheoryStringsRewriter::getConstantArithBound(Node a, bool isLower)
ret = NodeManager::currentNM()->mkConst(Rational(0));
}
}
- else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
+ else if (options::stringsRewriterEntailChecks() && (a.getKind() == kind::PLUS || a.getKind() == kind::MULT))
{
std::vector<Node> children;
bool success = true;
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 00eb0b495..86f5cd5d6 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -700,6 +700,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node empty = d_nm->mkConst(::CVC4::String(""));
Node a = d_nm->mkConst(::CVC4::String("A"));
+ Node aac = d_nm->mkConst(::CVC4::String("AAC"));
Node ab = d_nm->mkConst(::CVC4::String("AB"));
Node b = d_nm->mkConst(::CVC4::String("B"));
Node c = d_nm->mkConst(::CVC4::String("C"));
@@ -713,6 +714,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node z = d_nm->mkVar("z", strType);
Node n = d_nm->mkVar("n", intType);
Node m = d_nm->mkVar("m", intType);
+ Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback