From: Andrew Reynolds Date: Fri, 12 Oct 2018 20:44:22 +0000 (-0500) Subject: Improvements to rewrite rules from inputs (#2625) X-Git-Tag: cvc5-1.0.0~4428 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8597f207187baff3b9f8cc5d8955e5b96d6d57d0;p=cvc5.git Improvements to rewrite rules from inputs (#2625) --- 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 visited; + std::unordered_map contains; + std::unordered_map::iterator it; + std::vector 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 @@ -38,6 +38,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. diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2e5252529..e65d57770 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1259,6 +1259,14 @@ header = "options/quantifiers_options.h" default = "true" 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" 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 terms; // all variables (free constants) appearing in the input std::vector 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 > tvars; - std::vector allVarTypes; - std::vector allVars; - unsigned varCounter = 0; + // does the input contain a Boolean variable? + bool hasBoolVar = false; + // the types of subterms of our input + std::map typesFound; // standard constants for each type (e.g. true, false for Bool) std::map > 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 > tvars; + std::vector allVarTypes; + std::vector allVars; + unsigned varCounter = 0; + for (std::pair 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 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& 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 > fvs; @@ -363,13 +368,23 @@ bool SygusSampler::isOrdered(Node n) std::map::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