summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/strings_options.toml63
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp53
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp5
-rw-r--r--src/theory/quantifiers/sygus/sygus_enumerator.cpp16
-rw-r--r--src/theory/quantifiers/sygus/sygus_enumerator.h4
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp50
-rw-r--r--src/theory/quantifiers/sygus_sampler.h6
-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--src/theory/strings/theory_strings_rewriter.h2
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h4
12 files changed, 307 insertions, 80 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/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a8d9d93bc..cb2968bd5 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1090,8 +1090,6 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
{
if (bv != bvr)
{
- Trace("sygus-rr-verify")
- << "Testing rewrite rule " << bv << " ---> " << bvr << std::endl;
// add to the sampler database object
std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
d_sampler[a].find(tn);
@@ -1101,55 +1099,8 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
d_tds, nv, options::sygusSamples(), false);
its = d_sampler[a].find(tn);
}
- // see if they evaluate to same thing on all sample points
- bool ptDisequal = false;
- unsigned pt_index = 0;
- Node bve, bvre;
- for (unsigned i = 0, npoints = its->second.getNumSamplePoints();
- i < npoints;
- i++)
- {
- bve = its->second.evaluate(bv, i);
- bvre = its->second.evaluate(bvr, i);
- if (bve != bvre)
- {
- ptDisequal = true;
- pt_index = i;
- break;
- }
- }
- // bv and bvr should be equivalent under examples
- if (ptDisequal)
- {
- // we have detected unsoundness in the rewriter
- Options& nodeManagerOptions =
- NodeManager::currentNM()->getOptions();
- std::ostream* out = nodeManagerOptions.getOut();
- (*out) << "(unsound-rewrite " << bv << " " << bvr << ")"
- << std::endl;
- // debugging information
- (*out) << "; unsound: are not equivalent for : " << std::endl;
- std::vector<Node> vars;
- its->second.getVariables(vars);
- std::vector<Node> pt;
- its->second.getSamplePoint(pt_index, pt);
- Assert(vars.size() == pt.size());
- for (unsigned i = 0, size = pt.size(); i < size; i++)
- {
- (*out) << "; unsound: " << vars[i] << " -> " << pt[i]
- << std::endl;
- }
- Assert(bve != bvre);
- (*out) << "; unsound: where they evaluate to " << bve << " and "
- << bvre << std::endl;
-
- if (options::sygusRewVerifyAbort())
- {
- AlwaysAssert(
- false,
- "--sygus-rr-verify detected unsoundness in the rewriter!");
- }
- }
+ // check equivalent
+ its->second.checkEquivalent(bv, bvr);
}
}
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 307ffeeed..cafa4a749 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/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index d4b4dd0bf..9981b5141 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -145,7 +145,8 @@ SygusEnumerator::TermCache::TermCache()
d_isSygusType(false),
d_numConClasses(0),
d_sizeEnum(0),
- d_isComplete(false)
+ d_isComplete(false),
+ d_sampleRrVInit(false)
{
}
void SygusEnumerator::TermCache::initialize(Node e,
@@ -311,6 +312,19 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
{
Node bn = d_tds->sygusToBuiltin(n);
Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
+ if (options::sygusRewVerify())
+ {
+ if (bn != bnr)
+ {
+ if (!d_sampleRrVInit)
+ {
+ d_sampleRrVInit = true;
+ d_samplerRrV.initializeSygus(
+ d_tds, d_enum, options::sygusSamples(), false);
+ }
+ d_samplerRrV.checkEquivalent(bn, bnr);
+ }
+ }
// must be unique up to rewriting
if (d_bterms.find(bnr) != d_bterms.end())
{
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index af6bb03f0..716a047d2 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -179,6 +179,10 @@ class SygusEnumerator : public EnumValGenerator
unsigned d_sizeEnum;
/** whether this term cache is complete */
bool d_isComplete;
+ /** sampler (for --sygus-rr-verify) */
+ quantifiers::SygusSampler d_samplerRrV;
+ /** is the above sampler initialized? */
+ bool d_sampleRrVInit;
};
/** above cache for each sygus type */
std::map<TypeNode, TermCache> d_tcache;
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 8834fe751..f1908fc19 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -769,6 +769,56 @@ void SygusSampler::registerSygusType(TypeNode tn)
}
}
+void SygusSampler::checkEquivalent(Node bv, Node bvr)
+{
+ Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
+ << std::endl;
+
+ // see if they evaluate to same thing on all sample points
+ bool ptDisequal = false;
+ unsigned pt_index = 0;
+ Node bve, bvre;
+ for (unsigned i = 0, npoints = getNumSamplePoints(); i < npoints; i++)
+ {
+ bve = evaluate(bv, i);
+ bvre = evaluate(bvr, i);
+ if (bve != bvre)
+ {
+ ptDisequal = true;
+ pt_index = i;
+ break;
+ }
+ }
+ // bv and bvr should be equivalent under examples
+ if (ptDisequal)
+ {
+ // we have detected unsoundness in the rewriter
+ Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
+ std::ostream* out = nodeManagerOptions.getOut();
+ (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
+ // debugging information
+ (*out) << "; unsound: are not equivalent for : " << std::endl;
+ std::vector<Node> vars;
+ getVariables(vars);
+ std::vector<Node> pt;
+ getSamplePoint(pt_index, pt);
+ Assert(vars.size() == pt.size());
+ for (unsigned i = 0, size = pt.size(); i < size; i++)
+ {
+ (*out) << "; unsound: " << vars[i] << " -> " << pt[i] << std::endl;
+ }
+ Assert(bve != bvre);
+ (*out) << "; unsound: where they evaluate to " << bve << " and " << bvre
+ << std::endl;
+
+ if (options::sygusRewVerifyAbort())
+ {
+ AlwaysAssert(false,
+ "--sygus-rr-verify detected unsoundness in the rewriter!");
+ }
+ }
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 98f52992b..28f715b34 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -165,6 +165,12 @@ class SygusSampler : public LazyTrieEvaluator
*/
bool containsFreeVariables(Node a, Node b, bool strict = false);
//--------------------------end queries about terms
+ /** check equivalent
+ *
+ * Check whether bv and bvr are equivalent on all sample points, print
+ * an error if not. Used with --sygus-rr-verify.
+ */
+ void checkEquivalent(Node bv, Node bvr);
protected:
/** sygus term database of d_qe */
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index b6604d6e0..276cb70d6 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 ccf99fa4d..13d1e74d8 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3214,7 +3214,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");
@@ -3608,11 +3607,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 ) );
@@ -3931,6 +3929,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 79667b9aa..cbb298c5f 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())
@@ -2379,6 +2375,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");
@@ -2601,6 +2598,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");
}
}
@@ -3345,6 +3343,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
@@ -3611,6 +3614,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());
bool changed = false;
@@ -3846,6 +3854,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);
@@ -3928,6 +3941,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(
@@ -3941,7 +3958,7 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict)
}
bool ret = checkEntailArithInternal(ar);
- if (!ret)
+ if (!ret && options::stringsRewriterApprox())
{
// try with approximations
ret = checkEntailArithApprox(ar);
@@ -4417,6 +4434,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;
@@ -4503,6 +4525,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;
@@ -4733,7 +4760,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/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 8b0072f52..81bc29ad6 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -472,7 +472,7 @@ class TheoryStringsRewriter {
* @return true node if it can be shown that `a` contains `b`, false node if
* it can be shown that `a` does not contain `b`, null node otherwise
*/
- static Node checkEntailContains(Node a, Node b, bool fullRewriter = false);
+ static Node checkEntailContains(Node a, Node b, bool fullRewriter = true);
/** entail non-empty
*
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 79a50d533..39aed79c0 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -448,6 +448,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node x = d_nm->mkVar("x", strType);
Node y = d_nm->mkVar("y", strType);
Node negOne = d_nm->mkConst(Rational(-1));
+ 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));
@@ -648,6 +649,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 b = d_nm->mkConst(::CVC4::String("B"));
Node c = d_nm->mkConst(::CVC4::String("C"));
Node abc = d_nm->mkConst(::CVC4::String("ABC"));
@@ -659,6 +661,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
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