Improvements to rewrite rules from inputs (#2625)

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