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 /src/theory/quantifiers/sygus_sampler.h | |
parent | 3f960e4f3744121efddd19b12806fee660887497 (diff) | |
parent | 8597f207187baff3b9f8cc5d8955e5b96d6d57d0 (diff) |
Merge branch 'master' into subsolverParamssubsolverParams
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 13 |
1 files changed, 13 insertions, 0 deletions
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 |