diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 16:48:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 16:48:10 -0500 |
commit | 22780596b561dff9b0eb5b0620252280a678944e (patch) | |
tree | 796c7a3a270f0509f36762ba88e938c644d9dfd4 /src/theory/quantifiers | |
parent | e0633c091c37b79f9e3a2517cf95113c788db083 (diff) |
Convert more uses of strings to words (#4584)
Towards theory of sequences.
This PR also adds support for sequences in default sygus grammars.
Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 8df43087f..074b023a2 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -459,6 +459,10 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( // theory of strings shares the integer type TypeNode intType = NodeManager::currentNM()->integerType(); collectSygusGrammarTypesFor(intType,types); + if (range.isSequence()) + { + collectSygusGrammarTypesFor(range.getSequenceElementType(), types); + } } else if (range.isFunction()) { @@ -805,7 +809,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(kind, cargsBinary); } } - else if (types[i].isString()) + else if (types[i].isStringLike()) { // concatenation std::vector<TypeNode> cargsBinary; @@ -823,6 +827,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<TypeNode> cargsLen; cargsLen.push_back(unres_t); sdts[i_intType].addConstructor(STRING_LENGTH, cargsLen); + if (types[i].isSequence()) + { + TypeNode etype = types[i].getSequenceElementType(); + // retrieve element unresolved type + Assert(type_to_unres.find(etype) != type_to_unres.end()); + TypeNode unresElemType = type_to_unres[etype]; + + Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl; + std::vector<TypeNode> cargsSeqUnit; + cargsSeqUnit.push_back(unresElemType); + sdts[i].addConstructor(SEQ_UNIT, cargsSeqUnit); + } } else if (types[i].isArray()) { |