From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 7 Nov 2018 23:12:38 +0000 (-0600)
Subject: Adding default SyGuS grammar construction for arrays (#2685)
X-Git-Tag: cvc5-1.0.0~4370
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e38d8cfd44d29547be464c8e7a6b9ad2ce7b9fe1;p=cvc5.git

Adding default SyGuS grammar construction for arrays (#2685)
---

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d6dfb3d26..b0471147d 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -371,6 +371,11 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   {
     ops.push_back(nm->mkConst(String("")));
   }
+  else if (type.isArray())
+  {
+    // TODO #2694 : generate constant array over the first element of the
+    // constituent type
+  }
   // TODO #1178 : add other missing types
 }
 
@@ -395,6 +400,15 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
           }
         }
       }
+      else if (range.isArray())
+      {
+        ArrayType arrayType = static_cast<ArrayType>(range.toType());
+        // add index and constituent type
+        collectSygusGrammarTypesFor(
+            TypeNode::fromType(arrayType.getIndexType()), types);
+        collectSygusGrammarTypesFor(
+            TypeNode::fromType(arrayType.getConstituentType()), types);
+      }
     }
   }
 }
@@ -638,6 +652,57 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         weights[i].push_back(-1);
       }
     }
+    else if (types[i].isArray())
+    {
+      ArrayType arrayType = static_cast<ArrayType>(types[i].toType());
+      Trace("sygus-grammar-def")
+          << "...building for array type " << arrayType << "\n";
+      Trace("sygus-grammar-def")
+          << "......finding unres type for index type "
+          << arrayType.getIndexType() << " with typenode "
+          << TypeNode::fromType(arrayType.getIndexType()) << "\n";
+      // retrieve index and constituent unresolved types
+      Assert(std::find(types.begin(),
+                       types.end(),
+                       TypeNode::fromType(arrayType.getIndexType()))
+             != types.end());
+      unsigned i_indexType = std::distance(
+          types.begin(),
+          std::find(types.begin(),
+                    types.end(),
+                    TypeNode::fromType(arrayType.getIndexType())));
+      Type unres_indexType = unres_types[i_indexType];
+      Assert(std::find(types.begin(),
+                       types.end(),
+                       TypeNode::fromType(arrayType.getConstituentType()))
+             != types.end());
+      unsigned i_constituentType = std::distance(
+          types.begin(),
+          std::find(types.begin(),
+                    types.end(),
+                    TypeNode::fromType(arrayType.getConstituentType())));
+      Type unres_constituentType = unres_types[i_constituentType];
+      // add (store ArrayType IndexType ConstituentType)
+      Trace("sygus-grammar-def") << "...add for STORE\n";
+      ops[i].push_back(nm->operatorOf(STORE).toExpr());
+      cnames[i].push_back(kindToString(STORE));
+      cargs[i].push_back(std::vector<Type>());
+      cargs[i].back().push_back(unres_t);
+      cargs[i].back().push_back(unres_indexType);
+      cargs[i].back().push_back(unres_constituentType);
+      pcs[i].push_back(nullptr);
+      weights[i].push_back(-1);
+      // add to constituent type : (select ArrayType IndexType)
+      Trace("sygus-grammar-def") << "...add select for constituent type"
+                                 << unres_constituentType << "\n";
+      ops[i_constituentType].push_back(nm->operatorOf(SELECT).toExpr());
+      cnames[i_constituentType].push_back(kindToString(SELECT));
+      cargs[i_constituentType].push_back(std::vector<Type>());
+      cargs[i_constituentType].back().push_back(unres_t);
+      cargs[i_constituentType].back().push_back(unres_indexType);
+      pcs[i_constituentType].push_back(nullptr);
+      weights[i_constituentType].push_back(-1);
+    }
     else if (types[i].isDatatype())
     {
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5304fcab5..c4dbab1dd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -840,6 +840,8 @@ set(regress_0_tests
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
+  regress0/sygus/array-grammar-select.sy
+  regress0/sygus/array-grammar-store.sy
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
   regress0/sygus/c100.sy
diff --git a/test/regress/regress0/sygus/array-grammar-select.sy b/test/regress/regress0/sygus/array-grammar-select.sy
new file mode 100644
index 000000000..d216bbb24
--- /dev/null
+++ b/test/regress/regress0/sygus/array-grammar-select.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALIA)
+
+(synth-fun f
+  ((s (Array Int Int)) (t Int))
+  Int
+  )
+
+(declare-var x (Array Int Int))
+
+(constraint (= (= (select x 0) (select x 1)) (= (f x 0) (f x 1))))
+
+
+(check-synth)
diff --git a/test/regress/regress0/sygus/array-grammar-store.sy b/test/regress/regress0/sygus/array-grammar-store.sy
new file mode 100644
index 000000000..70525e83b
--- /dev/null
+++ b/test/regress/regress0/sygus/array-grammar-store.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ABV)
+
+(synth-fun f
+  ((s (Array (BitVec 4) (BitVec 4))) (t (BitVec 4)))
+  (Array (BitVec 4) (BitVec 4))
+  )
+
+(declare-var x (Array (BitVec 4) (BitVec 4)))
+
+(constraint (= (= (store x #b0000 #b0000) (store x #b0001 #b0000)) (= (f x #b0000) (f x #b0001))))
+
+(check-synth)