From a3bcd08dad775e676947f85236b95fbdfc1f6127 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Jan 2020 08:49:14 -0600
Subject: [PATCH] Fix parameteric sorts involving Booleans in sygus default
 grammars (#3629)

---
 .../quantifiers/sygus/sygus_grammar_cons.cpp  | 36 +++++++++++--------
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress0/sygus/issue3624.sy      |  8 +++++
 3 files changed, 31 insertions(+), 14 deletions(-)
 create mode 100644 test/regress/regress0/sygus/issue3624.sy

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 389cf34de..a1b46f1ac 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -525,10 +525,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   collectSygusGrammarTypesFor(range, types);
 
   // create placeholder for boolean type (kept apart since not collected)
-  std::stringstream ssb;
-  ssb << fun << "_Bool";
-  std::string dbname = ssb.str();
-  TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres);
 
   // create placeholders for collected types
   std::vector<TypeNode> unres_types;
@@ -560,13 +556,27 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     type_to_unres[types[i]] = unres_t;
     sygus_to_builtin[unres_t] = types[i];
   }
+  // make Boolean type
+  std::stringstream ssb;
+  ssb << fun << "_Bool";
+  std::string dbname = ssb.str();
+  sdts.push_back(SygusDatatypeGenerator(dbname));
+  unsigned boolIndex = types.size();
+  TypeNode btype = nm->booleanType();
+  TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres);
+  types.push_back(btype);
+  unres_types.push_back(unres_bt);
+  type_to_unres[btype] = unres_bt;
+  sygus_to_builtin[unres_bt] = btype;
+
   // We ensure an ordering on types such that parametric types are processed
   // before their consitituents. Since parametric types were added before their
   // arguments in collectSygusGrammarTypesFor above, we will construct the
   // sygus grammars by iterating on types in reverse order. This ensures
   // that we know all constructors coming from other types (e.g. select(A,i))
-  // by the time we process the type.
-  for (int i = (types.size() - 1); i >= 0; --i)
+  // by the time we process the type. We start with types.size()-2, since
+  // we construct the grammar for the Boolean type last.
+  for (int i = (types.size() - 2); i >= 0; --i)
   {
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     TypeNode unres_t = unres_types[i];
@@ -865,8 +875,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }
   }
   std::map<TypeNode, unsigned>::iterator itgat;
-  // initialize the datatypes
-  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  // initialize the datatypes (except for the last one, reserved for Bool)
+  for (unsigned i = 0, size = types.size() - 1; i < size; ++i)
   {
     sdts[i].d_sdt.initializeDatatype(types[i], bvl, true, true);
     Trace("sygus-grammar-def")
@@ -1107,9 +1117,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }
   }
   //------ make Boolean type
-  TypeNode btype = nm->booleanType();
-  sdts.push_back(SygusDatatypeGenerator(dbname));
-  SygusDatatypeGenerator& sdtBool = sdts.back();
+  SygusDatatypeGenerator& sdtBool = sdts[boolIndex];
   Trace("sygus-grammar-def") << "Make grammar for " << btype << std::endl;
   //add variables
   for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
@@ -1135,8 +1143,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     std::vector<TypeNode> cargsEmpty;
     sdtBool.addConstructor(consts[i], ss.str(), cargsEmpty);
   }
-  // add predicates for types
-  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  // add predicates for non-Boolean types
+  for (unsigned i = 0, size = types.size() - 1; i < size; ++i)
   {
     if (!types[i].isFirstClass())
     {
@@ -1218,7 +1226,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }
   }
   if( range==btype ){
-    startIndex = sdts.size() - 1;
+    startIndex = boolIndex;
   }
   sdtBool.d_sdt.initializeDatatype(btype, bvl, true, true);
   Trace("sygus-grammar-def")
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a04619342..ed9ddda1b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -935,6 +935,7 @@ set(regress_0_tests
   regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/issue3356-syg-inf-usort.smt2
+  regress0/sygus/issue3624.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy
diff --git a/test/regress/regress0/sygus/issue3624.sy b/test/regress/regress0/sygus/issue3624.sy
new file mode 100644
index 000000000..cc677bb9c
--- /dev/null
+++ b/test/regress/regress0/sygus/issue3624.sy
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(declare-var A Bool)
+(declare-var B (Array Int Bool))
+(synth-fun secure-sync ((A Bool) (B (Array Int Bool))) Bool)
+(constraint (secure-sync A B))
+(check-synth)
-- 
2.30.2