Support default sygus grammar construction for sets (#3842)

Fixes #3645.

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 259f9c642f931b8ed1ce70602ca36be2730f0b31..17cc6bf9e252ea9b7a5fc96c9bb1437de6653701 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -409,7 +409,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   {
     ops.push_back(nm->mkConst(String("")));
   }
-  else if (type.isArray())
+  else if (type.isArray() || type.isSet())
   {
     // generate constant array over the first element of the constituent type
     Node c = type.mkGroundTerm();
@@ -443,6 +443,10 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
         collectSygusGrammarTypesFor(range.getArrayIndexType(), types);
         collectSygusGrammarTypesFor(range.getArrayConstituentType(), types);
       }
+      else if (range.isSet())
+      {
+        collectSygusGrammarTypesFor(range.getSetElementType(), types);
+      }
       else if (range.isString() )
       {
         // theory of strings shares the integer type
@@ -791,22 +795,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       Trace("sygus-grammar-def")
           << "...building for array type " << types[i] << "\n";
-      Trace("sygus-grammar-def") << "......finding unres type for index type "
-                                 << types[i].getArrayIndexType() << "\n";
+      TypeNode indexType = types[i].getArrayIndexType();
+      TypeNode elemType = types[i].getArrayConstituentType();
+      Trace("sygus-grammar-def")
+          << "......finding unres type for index type " << indexType << "\n";
       // retrieve index and constituent unresolved types
-      Assert(std::find(types.begin(), types.end(), types[i].getArrayIndexType())
-             != types.end());
-      unsigned i_indexType = std::distance(
-          types.begin(),
-          std::find(types.begin(), types.end(), types[i].getArrayIndexType()));
-      TypeNode unres_indexType = unres_types[i_indexType];
-      Assert(std::find(
-                 types.begin(), types.end(), types[i].getArrayConstituentType())
-             != types.end());
+      Assert(type_to_unres.find(indexType) != type_to_unres.end());
+      TypeNode unres_indexType = type_to_unres[indexType];
+      Assert(std::find(types.begin(), types.end(), elemType) != types.end());
+      // must get this index since we add to sdt[i_constituentType] below.
       unsigned i_constituentType = std::distance(
-          types.begin(),
-          std::find(
-              types.begin(), types.end(), types[i].getArrayConstituentType()));
+          types.begin(), std::find(types.begin(), types.end(), elemType));
       TypeNode unres_constituentType = unres_types[i_constituentType];
       // add (store ArrayType IndexType ConstituentType)
       Trace("sygus-grammar-def") << "...add for STORE\n";
@@ -824,6 +823,30 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       cargsSelect.push_back(unres_indexType);
       sdts[i_constituentType].addConstructor(SELECT, cargsSelect);
     }
+    else if (types[i].isSet())
+    {
+      TypeNode etype = types[i].getSetElementType();
+      // retrieve element unresolved type
+      Assert(type_to_unres.find(etype) != type_to_unres.end());
+      TypeNode unresElemType = type_to_unres[etype];
+
+      // add for singleton
+      Trace("sygus-grammar-def") << "...add for singleton" << std::endl;
+      std::vector<TypeNode> cargsSingleton;
+      cargsSingleton.push_back(unresElemType);
+      sdts[i].addConstructor(SINGLETON, cargsSingleton);
+
+      // add for union, difference, intersection
+      std::vector<Kind> bin_kinds = {UNION, INTERSECTION, SETMINUS};
+      std::vector<TypeNode> cargsBinary;
+      cargsBinary.push_back(unres_t);
+      cargsBinary.push_back(unres_t);
+      for (const Kind k : bin_kinds)
+      {
+        Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+        sdts[i].addConstructor(k, cargsBinary);
+      }
+    }
     else if (types[i].isDatatype())
     {
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
@@ -1197,6 +1220,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         sdtBool.addConstructor(dt[kind].getTester(), sst.str(), cargsTester);
       }
     }
+    else if (types[i].isSet())
+    {
+      // add for member
+      TypeNode etype = types[i].getSetElementType();
+      Assert(type_to_unres.find(etype) != type_to_unres.end());
+      TypeNode unresElemType = type_to_unres[etype];
+      std::vector<TypeNode> cargsMember;
+      cargsMember.push_back(unresElemType);
+      cargsMember.push_back(unres_types[iuse]);
+      Trace("sygus-grammar-def") << "...for MEMBER" << std::endl;
+      sdtBool.addConstructor(MEMBER, cargsMember);
+    }
   }
   // add Boolean connectives, if not in a degenerate case of (recursively)
   // having only constant constructors

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a7d93124678c2948fc0c0ddabcbde816a1c3da6d..5eaaf3e6705355c6a764199c6bc9aa6851e362d1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -968,6 +968,7 @@ set(regress_0_tests
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/issue3356-syg-inf-usort.smt2
   regress0/sygus/issue3624.sy
+  regress0/sygus/issue3645-grammar-sets.smt2
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy
@@ -1870,6 +1871,7 @@ set(regress_1_tests
   regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
+  regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
   regress1/sygus/strings-any-term1.sy
@@ -2017,6 +2019,7 @@ set(regress_2_tests
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
+  regress2/sygus/sets-fun-test.sy
   regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/sygus/vcb.sy

diff --git a/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2
new file mode 100644 (file)
index 0000000..22a5e07
--- /dev/null
+++ b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () (Set (_ BitVec 2)))
+(declare-fun b () (Set (_ BitVec 2)))
+(assert (= a b))
+(check-sat)

diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy
new file mode 100644 (file)
index 0000000..2843257
--- /dev/null
+++ b/test/regress/regress1/sygus/sets-pred-test.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun P ((x (Set Int))) Bool)
+
+(constraint (not (P (as emptyset (Set Int)))))
+(constraint (not (P (insert 1 2 (as emptyset (Set Int))))))
+(constraint (P (insert 0 (as emptyset (Set Int)))))
+(constraint (P (insert 0 4 5 (as emptyset (Set Int)))))
+(constraint (not (P (singleton 45))))
+
+(check-synth)

diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy
new file mode 100644 (file)
index 0000000..987d6a7
--- /dev/null
+++ b/test/regress/regress2/sygus/sets-fun-test.sy
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun f ((x Int)) (Set Int))
+
+(constraint (member 45 (f 45)))
+(constraint (member 8 (f 8)))
+(constraint (member 0 (f 3)))
+
+(check-synth)