From e38d8cfd44d29547be464c8e7a6b9ad2ce7b9fe1 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 7 Nov 2018 17:12:38 -0600 Subject: [PATCH] Adding default SyGuS grammar construction for arrays (#2685) --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 65 +++++++++++++++++++ test/regress/CMakeLists.txt | 2 + .../regress0/sygus/array-grammar-select.sy | 15 +++++ .../regress0/sygus/array-grammar-store.sy | 14 ++++ 4 files changed, 96 insertions(+) create mode 100644 test/regress/regress0/sygus/array-grammar-select.sy create mode 100644 test/regress/regress0/sygus/array-grammar-store.sy 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(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(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()); + 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()); + 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) -- 2.30.2