diff options
Diffstat (limited to 'src/theory/quantifiers')
| -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 |
3 files changed, 45 insertions, 12 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 |