diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:06:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-12 18:06:27 -0700 |
commit | 470bff2ea4b964f08a93c551f3f8722f66c738ad (patch) | |
tree | 6a69ac4d89d976ea552e6e6786c4cc8a2cf9291d /src/theory | |
parent | 3f960e4f3744121efddd19b12806fee660887497 (diff) | |
parent | 8597f207187baff3b9f8cc5d8955e5b96d6d57d0 (diff) |
Merge branch 'master' into subsolverParamssubsolverParams
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_filter.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 13 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 75 |
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; |