diff options
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 */ |