diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 16:18:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-12 16:18:06 -0500 |
| commit | bee3c7f6840e531bc91d990b98f2b331d1f2f82c (patch) | |
| tree | 31fdeb3e8ae206fb2b0d78993a009771aeec4b9b /src/theory | |
| parent | ad18e6d4bab518a29648823eca9ba5ee1ebc8400 (diff) | |
Fix default grammar construction for arrays when no free variables are present (#3225)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a6b051e58..e7f447ca1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -385,8 +385,9 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, } else if (type.isArray()) { - // TODO #2694 : generate constant array over the first element of the - // constituent type + // generate constant array over the first element of the constituent type + Node c = type.mkGroundTerm(); + ops.push_back(c); } // TODO #1178 : add other missing types } @@ -1032,6 +1033,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + Trace("sygus-grammar-def") << "...finished" << std::endl; Assert( types.size()==datatypes.size() ); return TypeNode::fromType( types[0] ); } |