summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-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
4 files changed, 100 insertions, 32 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback