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 | |
parent | 3f960e4f3744121efddd19b12806fee660887497 (diff) | |
parent | 8597f207187baff3b9f8cc5d8955e5b96d6d57d0 (diff) |
Merge branch 'master' into subsolverParamssubsolverParams
-rw-r--r-- | src/expr/node_algorithm.cpp | 55 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 5 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 117 | ||||
-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 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 74 |
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() |