diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-20 14:45:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-20 14:45:26 -0500 |
| commit | 549060790c9e91d9fc37b882e137bb36e5b538ea (patch) | |
| tree | 146d966b1188d3e134b1bb700ab6a08262fb07e0 /src/theory/quantifiers/sygus_sampler.h | |
| parent | 5f1cdd91a5e03dd29b660c841032d5b2a31ea634 (diff) | |
Reenable filtering based on ordering in sygus sampler (#1784)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 18b8f5511..a66e7ee21 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -207,10 +207,11 @@ class SygusSampler : public LazyTrieEvaluator bool isOrdered(Node n); /** contains free variables * - * Returns true if all free variables of a are contained in b. Free variables - * are those that occur in the range d_type_vars. + * Returns true if the free variables of b are a subset of those in a, where + * we require a strict subset if strict is true. Free variables are those that + * occur in the range d_type_vars. */ - bool containsFreeVariables(Node a, Node b); + bool containsFreeVariables(Node a, Node b, bool strict = false); protected: /** sygus term database of d_qe */ |