From 4270c3d6b8fa45e66a79c928267a0757954d8004 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Dec 2021 11:12:10 -0600
Subject: [PATCH] Fixes for sygus-rr-synth-input (#7716)

Includes aborting when no non-constant subterms exist, a spurious assertion failure, and bad variable names.

Fixes cvc5/cvc5-projects#351

Fixes cvc5/cvc5-projects#353
---
 src/preprocessing/passes/synth_rew_rules.cpp | 21 ++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index a54d220e5..4adfa1fd6 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -146,13 +146,13 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   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().quantifiers.sygusRewSynthInputNVars;
+  uint64_t nvars = options().quantifiers.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;
+  uint64_t varCounter = 0;
   for (std::pair<const TypeNode, bool> tfp : typesFound)
   {
     TypeNode tn = tfp.first;
@@ -161,11 +161,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     // 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 =
+    uint64_t useNVars =
         (options().quantifiers.sygusRewSynthInputUseBool || !tn.isBoolean())
             ? nvars
             : (hasBoolVar ? 1 : 0);
-    for (unsigned i = 0; i < useNVars; i++)
+    for (uint64_t i = 0; i < useNVars; i++)
     {
       // We must have a good name for these variables, these are
       // the ones output in rewrite rules. We choose
@@ -173,7 +173,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
       std::stringstream ssv;
       if (varCounter < 26)
       {
-        ssv << static_cast<char>(varCounter + 61);
+        ssv << static_cast<char>(varCounter + static_cast<uint64_t>('A'));
       }
       else
       {
@@ -188,6 +188,14 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   }
   Trace("srs-input") << "...finished." << std::endl;
 
+  // if the problem is trivial, e.g. contains no non-constant terms, then we
+  // exit with an exception.
+  if (allVars.empty())
+  {
+    throw Exception("No terms to consider for synthesizing rewrites");
+    return PreprocessingPassResult::NO_CONFLICT;
+  }
+
   Trace("srs-input") << "Convert subterms to free variable form..."
                      << std::endl;
   // Replace all free variables with bound variables. This ensures that
@@ -271,7 +279,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
     // add the variables for the type
     TypeNode ctt = ct.getType();
-    Assert(tvars.find(ctt) != tvars.end());
     std::vector<TypeNode> argList;
     // we add variable constructors if we are not Boolean, we are interested
     // in purely propositional rewrites (via the option), or this term is
@@ -279,6 +286,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool
         || ct.getKind() == BOUND_VARIABLE)
     {
+      Assert(tvars.find(ctt) != tvars.end())
+          << "Unexpected type " << ctt << " for " << ct;
       for (const Node& v : tvars[ctt])
       {
         std::stringstream ssc;
-- 
2.30.2