Improvements to rewrite rules from inputs (#2625)

7 files changed, 186 insertions, 56 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 4bbfb5df8..3905ad5c9 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -63,6 +63,61 @@ bool hasSubterm(TNode n, TNode t, bool strict)
   return false;
 }
 
+bool hasSubtermMulti(TNode n, TNode t)
+{
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+  std::unordered_map<TNode, bool, TNodeHashFunction> contains;
+  std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      if (cur == t)
+      {
+        visited[cur] = true;
+        contains[cur] = true;
+      }
+      else
+      {
+        visited[cur] = false;
+        visit.push_back(cur);
+        for (const Node& cc : cur)
+        {
+          visit.push_back(cc);
+        }
+      }
+    }
+    else if (!it->second)
+    {
+      bool doesContain = false;
+      for (const Node& cn : cur)
+      {
+        it = contains.find(cn);
+        Assert(it != visited.end());
+        if (it->second)
+        {
+          if (doesContain)
+          {
+            // two children have t, return true
+            return true;
+          }
+          doesContain = true;
+        }
+      }
+      contains[cur] = doesContain;
+      visited[cur] = true;
+    }
+  } while (!visit.empty());
+  return false;
+}
+
 struct HasBoundVarTag
 {
 };
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 7453bc292..d825d7f57 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -39,6 +39,11 @@ namespace expr {
 bool hasSubterm(TNode n, TNode t, bool strict = false);
 
 /**
+ * Check if the node n has >1 occurrences of a subterm t.
+ */
+bool hasSubtermMulti(TNode n, TNode t);
+
+/**
  * Returns true iff the node n contains a bound variable, that is a node of
  * kind BOUND_VARIABLE. This bound variable may or may not be free.
  * @param n The node under investigation
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2e5252529..e65d57770 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1260,6 +1260,14 @@ header = "options/quantifiers_options.h"
   help       = "filter candidate rewrites based on congruence"
 
 [[option]]
+  name       = "sygusRewSynthFilterNonLinear"
+  category   = "regular"
+  long       = "sygus-rr-synth-filter-nl"
+  type       = "bool"
+  default    = "false"
+  help       = "filter non-linear candidate rewrites"
+
+[[option]]
   name       = "sygusRewVerify"
   category   = "regular"
   long       = "sygus-rr-verify"
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 14dea3908..7e687329b 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -57,16 +57,10 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   std::vector<Node> terms;
   // all variables (free constants) appearing in the input
   std::vector<Node> vars;
-
-  // We will generate a fixed number of variables per type. These are the
-  // variables that appear as free variables in the rewrites we generate.
-  unsigned nvars = options::sygusRewSynthInputNVars();
-  // must have at least one variable per type
-  nvars = nvars < 1 ? 1 : nvars;
-  std::map<TypeNode, std::vector<Node> > tvars;
-  std::vector<TypeNode> allVarTypes;
-  std::vector<Node> allVars;
-  unsigned varCounter = 0;
+  // does the input contain a Boolean variable?
+  bool hasBoolVar = false;
+  // the types of subterms of our input
+  std::map<TypeNode, bool> typesFound;
   // standard constants for each type (e.g. true, false for Bool)
   std::map<TypeNode, std::vector<Node> > consts;
 
@@ -116,44 +110,26 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         {
           Trace("srs-input-debug") << "...children are valid" << std::endl;
           Trace("srs-input-debug") << "Add term " << cur << std::endl;
+          TypeNode tn = cur.getType();
           if (cur.isVar())
           {
             vars.push_back(cur);
+            if (tn.isBoolean())
+            {
+              hasBoolVar = true;
+            }
           }
           // register type information
-          TypeNode tn = cur.getType();
-          if (tvars.find(tn) == tvars.end())
+          if (typesFound.find(tn) == typesFound.end())
           {
-            // Only make one Boolean variable unless option is set. This ensures
-            // we do not compute purely Boolean rewrites by default.
-            unsigned useNVars =
-                (options::sygusRewSynthInputUseBool() || !tn.isBoolean())
-                    ? nvars
-                    : 1;
-            for (unsigned i = 0; i < useNVars; i++)
-            {
-              // We must have a good name for these variables, these are
-              // the ones output in rewrite rules. We choose
-              // a,b,c,...,y,z,x1,x2,...
-              std::stringstream ssv;
-              if (varCounter < 26)
-              {
-                ssv << String::convertUnsignedIntToChar(varCounter + 32);
-              }
-              else
-              {
-                ssv << "x" << (varCounter - 26);
-              }
-              varCounter++;
-              Node v = nm->mkBoundVar(ssv.str(), tn);
-              tvars[tn].push_back(v);
-              allVars.push_back(v);
-              allVarTypes.push_back(tn);
-            }
-            // also add the standard constants for this type
+            typesFound[tn] = true;
+            // add the standard constants for this type
             theory::quantifiers::CegGrammarConstructor::mkSygusConstantsForType(
                 tn, consts[tn]);
-            visit.insert(visit.end(), consts[tn].begin(), consts[tn].end());
+            // We prepend them so that they come first in the grammar
+            // construction. The motivation is we'd prefer seeing e.g. "true"
+            // instead of (= x x) as a canonical term.
+            terms.insert(terms.begin(), consts[tn].begin(), consts[tn].end());
           }
           terms.push_back(cur);
         }
@@ -163,6 +139,51 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   }
   Trace("srs-input") << "...finished." << std::endl;
 
+  Trace("srs-input") << "Make synth variables for types..." << std::endl;
+  // We will generate a fixed number of variables per type. These are the
+  // variables that appear as free variables in the rewrites we generate.
+  unsigned nvars = options::sygusRewSynthInputNVars();
+  // must have at least one variable per type
+  nvars = nvars < 1 ? 1 : nvars;
+  std::map<TypeNode, std::vector<Node> > tvars;
+  std::vector<TypeNode> allVarTypes;
+  std::vector<Node> allVars;
+  unsigned varCounter = 0;
+  for (std::pair<const TypeNode, bool> tfp : typesFound)
+  {
+    TypeNode tn = tfp.first;
+    // If we are not interested in purely propositional rewrites, we only
+    // need to make one Boolean variable if the input has a Boolean variable.
+    // This ensures that no type in our grammar has zero constructors. If
+    // our input does not contain a Boolean variable, we need not allocate any
+    // Boolean variables here.
+    unsigned useNVars =
+        (options::sygusRewSynthInputUseBool() || !tn.isBoolean())
+            ? nvars
+            : (hasBoolVar ? 1 : 0);
+    for (unsigned i = 0; i < useNVars; i++)
+    {
+      // We must have a good name for these variables, these are
+      // the ones output in rewrite rules. We choose
+      // a,b,c,...,y,z,x1,x2,...
+      std::stringstream ssv;
+      if (varCounter < 26)
+      {
+        ssv << String::convertUnsignedIntToChar(varCounter + 32);
+      }
+      else
+      {
+        ssv << "x" << (varCounter - 26);
+      }
+      varCounter++;
+      Node v = nm->mkBoundVar(ssv.str(), tn);
+      tvars[tn].push_back(v);
+      allVars.push_back(v);
+      allVarTypes.push_back(tn);
+    }
+  }
+  Trace("srs-input") << "...finished." << std::endl;
+
   Trace("srs-input") << "Convert subterms to free variable form..."
                      << std::endl;
   // Replace all free variables with bound variables. This ensures that
@@ -249,11 +270,18 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     TypeNode ctt = ct.getType();
     Assert(tvars.find(ctt) != tvars.end());
     std::vector<Type> argList;
-    for (const Node& v : tvars[ctt])
+    // we add variable constructors if we are not Boolean, we are interested
+    // in purely propositional rewrites (via the option), or this term is
+    // a Boolean variable.
+    if (!ctt.isBoolean() || options::sygusRewSynthInputUseBool()
+        || ct.getKind() == BOUND_VARIABLE)
     {
-      std::stringstream ssc;
-      ssc << "C_" << i << "_" << v;
-      datatypes[i].addSygusConstructor(v.toExpr(), ssc.str(), argList);
+      for (const Node& v : tvars[ctt])
+      {
+        std::stringstream ssc;
+        ssc << "C_" << i << "_" << v;
+        datatypes[i].addSygusConstructor(v.toExpr(), ssc.str(), argList);
+      }
     }
     // add the constructor for the operator if it is not a variable
     if (ct.getKind() != BOUND_VARIABLE)
@@ -337,6 +365,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         datatypes[i].addSygusConstructor(op.toExpr(), ssc.str(), argList);
       }
     }
+    Assert(datatypes[i].getNumConstructors() > 0);
     datatypes[i].setSygus(ctt.toType(), sygusVarListE, false, false);
   }
   Trace("srs-input") << "...finished." << std::endl;
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