summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_algorithm.cpp55
-rw-r--r--src/expr/node_algorithm.h5
-rw-r--r--src/options/quantifiers_options.toml8
-rw-r--r--src/preprocessing/passes/synth_rew_rules.cpp117
-rw-r--r--src/theory/quantifiers/candidate_rewrite_filter.cpp17
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp27
-rw-r--r--src/theory/quantifiers/sygus_sampler.h13
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp75
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h74
9 files changed, 314 insertions, 77 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 4bbfb5df8..3905ad5c9 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -63,6 +63,61 @@ bool hasSubterm(TNode n, TNode t, bool strict)
return false;
}
+bool hasSubtermMulti(TNode n, TNode t)
+{
+ std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+ std::unordered_map<TNode, bool, TNodeHashFunction> contains;
+ std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ if (cur == t)
+ {
+ visited[cur] = true;
+ contains[cur] = true;
+ }
+ else
+ {
+ visited[cur] = false;
+ visit.push_back(cur);
+ for (const Node& cc : cur)
+ {
+ visit.push_back(cc);
+ }
+ }
+ }
+ else if (!it->second)
+ {
+ bool doesContain = false;
+ for (const Node& cn : cur)
+ {
+ it = contains.find(cn);
+ Assert(it != visited.end());
+ if (it->second)
+ {
+ if (doesContain)
+ {
+ // two children have t, return true
+ return true;
+ }
+ doesContain = true;
+ }
+ }
+ contains[cur] = doesContain;
+ visited[cur] = true;
+ }
+ } while (!visit.empty());
+ return false;
+}
+
struct HasBoundVarTag
{
};
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 7453bc292..d825d7f57 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -39,6 +39,11 @@ namespace expr {
bool hasSubterm(TNode n, TNode t, bool strict = false);
/**
+ * Check if the node n has >1 occurrences of a subterm t.
+ */
+bool hasSubtermMulti(TNode n, TNode t);
+
+/**
* Returns true iff the node n contains a bound variable, that is a node of
* kind BOUND_VARIABLE. This bound variable may or may not be free.
* @param n The node under investigation
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 6ee7dc7c5..f3baa8214 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1260,6 +1260,14 @@ header = "options/quantifiers_options.h"
help = "filter candidate rewrites based on congruence"
[[option]]
+ name = "sygusRewSynthFilterNonLinear"
+ category = "regular"
+ long = "sygus-rr-synth-filter-nl"
+ type = "bool"
+ default = "false"
+ help = "filter non-linear candidate rewrites"
+
+[[option]]
name = "sygusRewVerify"
category = "regular"
long = "sygus-rr-verify"
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 14dea3908..7e687329b 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -57,16 +57,10 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
std::vector<Node> terms;
// all variables (free constants) appearing in the input
std::vector<Node> vars;
-
- // We will generate a fixed number of variables per type. These are the
- // variables that appear as free variables in the rewrites we generate.
- unsigned nvars = options::sygusRewSynthInputNVars();
- // must have at least one variable per type
- nvars = nvars < 1 ? 1 : nvars;
- std::map<TypeNode, std::vector<Node> > tvars;
- std::vector<TypeNode> allVarTypes;
- std::vector<Node> allVars;
- unsigned varCounter = 0;
+ // does the input contain a Boolean variable?
+ bool hasBoolVar = false;
+ // the types of subterms of our input
+ std::map<TypeNode, bool> typesFound;
// standard constants for each type (e.g. true, false for Bool)
std::map<TypeNode, std::vector<Node> > consts;
@@ -116,44 +110,26 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
{
Trace("srs-input-debug") << "...children are valid" << std::endl;
Trace("srs-input-debug") << "Add term " << cur << std::endl;
+ TypeNode tn = cur.getType();
if (cur.isVar())
{
vars.push_back(cur);
+ if (tn.isBoolean())
+ {
+ hasBoolVar = true;
+ }
}
// register type information
- TypeNode tn = cur.getType();
- if (tvars.find(tn) == tvars.end())
+ if (typesFound.find(tn) == typesFound.end())
{
- // Only make one Boolean variable unless option is set. This ensures
- // we do not compute purely Boolean rewrites by default.
- unsigned useNVars =
- (options::sygusRewSynthInputUseBool() || !tn.isBoolean())
- ? nvars
- : 1;
- for (unsigned i = 0; i < useNVars; i++)
- {
- // We must have a good name for these variables, these are
- // the ones output in rewrite rules. We choose
- // a,b,c,...,y,z,x1,x2,...
- std::stringstream ssv;
- if (varCounter < 26)
- {
- ssv << String::convertUnsignedIntToChar(varCounter + 32);
- }
- else
- {
- ssv << "x" << (varCounter - 26);
- }
- varCounter++;
- Node v = nm->mkBoundVar(ssv.str(), tn);
- tvars[tn].push_back(v);
- allVars.push_back(v);
- allVarTypes.push_back(tn);
- }
- // also add the standard constants for this type
+ typesFound[tn] = true;
+ // add the standard constants for this type
theory::quantifiers::CegGrammarConstructor::mkSygusConstantsForType(
tn, consts[tn]);
- visit.insert(visit.end(), consts[tn].begin(), consts[tn].end());
+ // We prepend them so that they come first in the grammar
+ // construction. The motivation is we'd prefer seeing e.g. "true"
+ // instead of (= x x) as a canonical term.
+ terms.insert(terms.begin(), consts[tn].begin(), consts[tn].end());
}
terms.push_back(cur);
}
@@ -163,6 +139,51 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
}
Trace("srs-input") << "...finished." << std::endl;
+ Trace("srs-input") << "Make synth variables for types..." << std::endl;
+ // We will generate a fixed number of variables per type. These are the
+ // variables that appear as free variables in the rewrites we generate.
+ unsigned nvars = options::sygusRewSynthInputNVars();
+ // must have at least one variable per type
+ nvars = nvars < 1 ? 1 : nvars;
+ std::map<TypeNode, std::vector<Node> > tvars;
+ std::vector<TypeNode> allVarTypes;
+ std::vector<Node> allVars;
+ unsigned varCounter = 0;
+ for (std::pair<const TypeNode, bool> tfp : typesFound)
+ {
+ TypeNode tn = tfp.first;
+ // If we are not interested in purely propositional rewrites, we only
+ // need to make one Boolean variable if the input has a Boolean variable.
+ // This ensures that no type in our grammar has zero constructors. If
+ // our input does not contain a Boolean variable, we need not allocate any
+ // Boolean variables here.
+ unsigned useNVars =
+ (options::sygusRewSynthInputUseBool() || !tn.isBoolean())
+ ? nvars
+ : (hasBoolVar ? 1 : 0);
+ for (unsigned i = 0; i < useNVars; i++)
+ {
+ // We must have a good name for these variables, these are
+ // the ones output in rewrite rules. We choose
+ // a,b,c,...,y,z,x1,x2,...
+ std::stringstream ssv;
+ if (varCounter < 26)
+ {
+ ssv << String::convertUnsignedIntToChar(varCounter + 32);
+ }
+ else
+ {
+ ssv << "x" << (varCounter - 26);
+ }
+ varCounter++;
+ Node v = nm->mkBoundVar(ssv.str(), tn);
+ tvars[tn].push_back(v);
+ allVars.push_back(v);
+ allVarTypes.push_back(tn);
+ }
+ }
+ Trace("srs-input") << "...finished." << std::endl;
+
Trace("srs-input") << "Convert subterms to free variable form..."
<< std::endl;
// Replace all free variables with bound variables. This ensures that
@@ -249,11 +270,18 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
TypeNode ctt = ct.getType();
Assert(tvars.find(ctt) != tvars.end());
std::vector<Type> argList;
- for (const Node& v : tvars[ctt])
+ // we add variable constructors if we are not Boolean, we are interested
+ // in purely propositional rewrites (via the option), or this term is
+ // a Boolean variable.
+ if (!ctt.isBoolean() || options::sygusRewSynthInputUseBool()
+ || ct.getKind() == BOUND_VARIABLE)
{
- std::stringstream ssc;
- ssc << "C_" << i << "_" << v;
- datatypes[i].addSygusConstructor(v.toExpr(), ssc.str(), argList);
+ for (const Node& v : tvars[ctt])
+ {
+ std::stringstream ssc;
+ ssc << "C_" << i << "_" << v;
+ datatypes[i].addSygusConstructor(v.toExpr(), ssc.str(), argList);
+ }
}
// add the constructor for the operator if it is not a variable
if (ct.getKind() != BOUND_VARIABLE)
@@ -337,6 +365,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
datatypes[i].addSygusConstructor(op.toExpr(), ssc.str(), argList);
}
}
+ Assert(datatypes[i].getNumConstructors() > 0);
datatypes[i].setSygus(ctt.toType(), sygusVarListE, false, false);
}
Trace("srs-input") << "...finished." << std::endl;
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index c49557fa9..0d3878149 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -242,13 +242,18 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
// whether we will keep this pair
bool keep = true;
- // ----- check ordering redundancy
- if (options::sygusRewSynthFilterOrder())
+ // ----- check redundancy based on variables
+ if (options::sygusRewSynthFilterOrder()
+ || options::sygusRewSynthFilterNonLinear())
{
- bool nor = d_ss->isOrdered(bn);
- bool eqor = d_ss->isOrdered(beq_n);
- Trace("cr-filter-debug") << "Ordered? : " << nor << " " << eqor
- << std::endl;
+ bool nor = d_ss->checkVariables(bn,
+ options::sygusRewSynthFilterOrder(),
+ options::sygusRewSynthFilterNonLinear());
+ bool eqor = d_ss->checkVariables(beq_n,
+ options::sygusRewSynthFilterOrder(),
+ options::sygusRewSynthFilterNonLinear());
+ Trace("cr-filter-debug")
+ << "Variables ok? : " << nor << " " << eqor << std::endl;
if (eqor || nor)
{
// if only one is ordered, then we require that the ordered one's
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index e30fda8f9..8834fe751 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -14,6 +14,7 @@
#include "theory/quantifiers/sygus_sampler.h"
+#include "expr/node_algorithm.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
@@ -341,7 +342,11 @@ void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
} while (!visit.empty());
}
-bool SygusSampler::isOrdered(Node n)
+bool SygusSampler::isOrdered(Node n) { return checkVariables(n, true, false); }
+
+bool SygusSampler::isLinear(Node n) { return checkVariables(n, false, true); }
+
+bool SygusSampler::checkVariables(Node n, bool checkOrder, bool checkLinear)
{
// compute free variables in n for each type
std::map<unsigned, std::vector<Node> > fvs;
@@ -363,13 +368,23 @@ bool SygusSampler::isOrdered(Node n)
std::map<Node, unsigned>::iterator itv = d_var_index.find(cur);
if (itv != d_var_index.end())
{
- unsigned tnid = d_type_ids[cur];
- // if this variable is out of order
- if (itv->second != fvs[tnid].size())
+ if (checkOrder)
{
- return false;
+ unsigned tnid = d_type_ids[cur];
+ // if this variable is out of order
+ if (itv->second != fvs[tnid].size())
+ {
+ return false;
+ }
+ fvs[tnid].push_back(cur);
+ }
+ if (checkLinear)
+ {
+ if (expr::hasSubtermMulti(n, cur))
+ {
+ return false;
+ }
}
- fvs[tnid].push_back(cur);
}
}
for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++)
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 64706264a..98f52992b 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -144,6 +144,19 @@ class SygusSampler : public LazyTrieEvaluator
* y and y+x are not.
*/
bool isOrdered(Node n);
+ /** is linear
+ *
+ * This returns whether n contains at most one occurrence of each free
+ * variable. For example, x, x+y are linear, but x+x, (x-y)+y, (x+0)+(x+0) are
+ * non-linear.
+ */
+ bool isLinear(Node n);
+ /** check variables
+ *
+ * This returns false if !isOrdered(n) and checkOrder is true or !isLinear(n)
+ * if checkLinear is true, or false otherwise.
+ */
+ bool checkVariables(Node n, bool checkOrder, bool checkLinear);
/** contains free variables
*
* Returns true if the free variables of b are a subset of those in a, where
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 28883b6b9..407279d22 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2108,8 +2108,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
}
}
}
-
- if (node[0].getKind() == kind::STRING_SUBSTR)
+ 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)
@@ -2121,6 +2120,27 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
return returnRewrite(node, ret, "ctn-substr");
}
}
+ else if (node[0].getKind() == kind::STRING_STRREPL)
+ {
+ if (node[0][0] == node[0][2])
+ {
+ // (str.contains (str.replace x y x) y) ---> (str.contains x y)
+ if (node[0][1] == node[1])
+ {
+ Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
+ return returnRewrite(node, ret, "ctn-repl-to-ctn");
+ }
+
+ // (str.contains (str.replace x y x) z) ---> (str.contains x z)
+ // if (str.len z) <= 1
+ Node one = nm->mkConst(Rational(1));
+ if (checkEntailArith(one, len_n2))
+ {
+ Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
+ return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn");
+ }
+ }
+ }
if (node[1].getKind() == kind::STRING_STRREPL)
{
@@ -3344,6 +3364,9 @@ bool TheoryStringsRewriter::componentContainsBase(
{
Assert(n1rb.isNull());
Assert(n1re.isNull());
+
+ NodeManager* nm = NodeManager::currentNM();
+
if (n1 == n2)
{
return true;
@@ -3362,8 +3385,7 @@ bool TheoryStringsRewriter::componentContainsBase(
{
if (computeRemainder)
{
- n1rb = NodeManager::currentNM()->mkConst(
- ::CVC4::String(s.prefix(s.size() - t.size())));
+ n1rb = nm->mkConst(::CVC4::String(s.prefix(s.size() - t.size())));
}
return true;
}
@@ -3374,8 +3396,7 @@ bool TheoryStringsRewriter::componentContainsBase(
{
if (computeRemainder)
{
- n1re = NodeManager::currentNM()->mkConst(
- ::CVC4::String(s.suffix(s.size() - t.size())));
+ n1re = nm->mkConst(::CVC4::String(s.suffix(s.size() - t.size())));
}
return true;
}
@@ -3389,12 +3410,11 @@ bool TheoryStringsRewriter::componentContainsBase(
{
if (f > 0)
{
- n1rb = NodeManager::currentNM()->mkConst(
- ::CVC4::String(s.prefix(f)));
+ n1rb = nm->mkConst(::CVC4::String(s.prefix(f)));
}
if (s.size() > f + t.size())
{
- n1re = NodeManager::currentNM()->mkConst(
+ n1re = nm->mkConst(
::CVC4::String(s.suffix(s.size() - (f + t.size()))));
}
}
@@ -3413,10 +3433,8 @@ bool TheoryStringsRewriter::componentContainsBase(
{
bool success = true;
Node start_pos = n2[1];
- Node end_pos =
- NodeManager::currentNM()->mkNode(kind::PLUS, n2[1], n2[2]);
- Node len_n2s =
- NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n2[0]);
+ Node end_pos = nm->mkNode(kind::PLUS, n2[1], n2[2]);
+ Node len_n2s = nm->mkNode(kind::STRING_LENGTH, n2[0]);
if (dir == 1)
{
// To be a suffix, start + length must be greater than
@@ -3444,22 +3462,39 @@ bool TheoryStringsRewriter::componentContainsBase(
}
if (dir != 1)
{
- n1rb = NodeManager::currentNM()->mkNode(
- kind::STRING_SUBSTR,
- n2[0],
- NodeManager::currentNM()->mkConst(Rational(0)),
- start_pos);
+ n1rb = nm->mkNode(kind::STRING_SUBSTR,
+ n2[0],
+ nm->mkConst(Rational(0)),
+ start_pos);
}
if (dir != -1)
{
- n1re = NodeManager::currentNM()->mkNode(
- kind::STRING_SUBSTR, n2[0], end_pos, len_n2s);
+ n1re = nm->mkNode(kind::STRING_SUBSTR, n2[0], end_pos, len_n2s);
}
}
return true;
}
}
}
+
+ if (!computeRemainder && dir == 0)
+ {
+ if (n1.getKind() == STRING_STRREPL)
+ {
+ // (str.contains (str.replace x y z) w) ---> true
+ // if (str.contains x w) --> true and (str.contains z w) ---> true
+ Node xCtnW = Rewriter::rewrite(nm->mkNode(STRING_STRCTN, n1[0], n2));
+ if (xCtnW.isConst() && xCtnW.getConst<bool>())
+ {
+ Node zCtnW =
+ Rewriter::rewrite(nm->mkNode(STRING_STRCTN, n1[2], n2));
+ if (zCtnW.isConst() && zCtnW.getConst<bool>())
+ {
+ return true;
+ }
+ }
+ }
+ }
}
}
return false;
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index cc29efb23..f82140181 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -80,6 +80,24 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
TS_ASSERT_DIFFERS(res_t1, res_t2);
}
+ void testCheckEntailArith()
+ {
+ TypeNode intType = d_nm->integerType();
+ TypeNode strType = d_nm->stringType();
+
+ Node z = d_nm->mkVar("z", strType);
+ Node n = d_nm->mkVar("n", intType);
+ Node one = d_nm->mkConst(Rational(1));
+
+ // 1 >= (str.len (str.substr z n 1)) ---> true
+ Node substr_z = d_nm->mkNode(kind::STRING_LENGTH,
+ d_nm->mkNode(kind::STRING_SUBSTR, z, n, one));
+ TS_ASSERT(TheoryStringsRewriter::checkEntailArith(one, substr_z));
+
+ // (str.len (str.substr z n 1)) >= 1 ---> false
+ TS_ASSERT(!TheoryStringsRewriter::checkEntailArith(substr_z, one));
+ }
+
void testCheckEntailArithWithAssumption()
{
TypeNode intType = d_nm->integerType();
@@ -497,9 +515,11 @@ 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 one = d_nm->mkConst(Rational(2));
+ Node one = d_nm->mkConst(Rational(1));
+ Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
Node four = d_nm->mkConst(Rational(4));
+ Node t = d_nm->mkConst(true);
Node f = d_nm->mkConst(false);
// Same normal form for:
@@ -644,6 +664,58 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node ctn_yxxy = d_nm->mkNode(kind::STRING_STRCTN, yx, xy);
Node eq_yxxy = d_nm->mkNode(kind::EQUAL, yx, xy);
sameNormalForm(ctn_yxxy, eq_yxxy);
+
+ // (str.contains (str.replace x y x) x) ---> true
+ ctn_repl = d_nm->mkNode(
+ kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), x);
+ sameNormalForm(ctn_repl, t);
+
+ // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true
+ ctn_repl = d_nm->mkNode(
+ kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx), x);
+ sameNormalForm(ctn_repl, t);
+
+ // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x)
+ // ---> true
+ ctn_repl = d_nm->mkNode(
+ kind::STRING_STRCTN,
+ d_nm->mkNode(kind::STRING_CONCAT,
+ z,
+ d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx)),
+ x);
+ sameNormalForm(ctn_repl, t);
+
+ // Same normal form for:
+ //
+ // (str.contains (str.replace x y x) y)
+ //
+ // (str.contains x y)
+ Node lhs = d_nm->mkNode(
+ kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), y);
+ Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, y);
+ sameNormalForm(lhs, rhs);
+
+ // Same normal form for:
+ //
+ // (str.contains (str.replace x y x) "B")
+ //
+ // (str.contains x "B")
+ lhs = d_nm->mkNode(
+ kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), b);
+ rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b);
+ sameNormalForm(lhs, rhs);
+
+ // Same normal form for:
+ //
+ // (str.contains (str.replace x y x) (str.substr z n 1))
+ //
+ // (str.contains x (str.substr z n 1))
+ Node substr_z = d_nm->mkNode(kind::STRING_SUBSTR, z, n, one);
+ lhs = d_nm->mkNode(kind::STRING_STRCTN,
+ d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+ substr_z);
+ rhs = d_nm->mkNode(kind::STRING_STRCTN, x, substr_z);
+ sameNormalForm(lhs, rhs);
}
void testInferEqsFromContains()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback