diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 68b1945fc..aba409109 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -156,6 +156,10 @@ void Smt2::addStringOperators() { addOperator(api::STRING_CHARAT, "str.at"); addOperator(api::STRING_INDEXOF, "str.indexof"); addOperator(api::STRING_REPLACE, "str.replace"); + addOperator(api::STRING_PREFIX, "str.prefixof"); + addOperator(api::STRING_SUFFIX, "str.suffixof"); + addOperator(api::STRING_FROM_CODE, "str.from_code"); + addOperator(api::STRING_IS_DIGIT, "str.is_digit"); addOperator(api::STRING_REPLACE_RE, "str.replace_re"); addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); if (!strictModeEnabled()) @@ -163,11 +167,20 @@ void Smt2::addStringOperators() { addOperator(api::STRING_TOLOWER, "str.tolower"); addOperator(api::STRING_TOUPPER, "str.toupper"); addOperator(api::STRING_REV, "str.rev"); + // sequence versions + addOperator(api::SEQ_CONCAT, "seq.++"); + addOperator(api::SEQ_LENGTH, "seq.len"); + addOperator(api::SEQ_EXTRACT, "seq.extract"); + addOperator(api::SEQ_AT, "seq.at"); + addOperator(api::SEQ_CONTAINS, "seq.contains"); + addOperator(api::SEQ_INDEXOF, "seq.indexof"); + addOperator(api::SEQ_REPLACE, "seq.replace"); + addOperator(api::SEQ_PREFIX, "seq.prefixof"); + addOperator(api::SEQ_SUFFIX, "seq.suffixof"); + addOperator(api::SEQ_REV, "seq.rev"); + addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all"); + addOperator(api::SEQ_UNIT, "seq.unit"); } - addOperator(api::STRING_PREFIX, "str.prefixof"); - addOperator(api::STRING_SUFFIX, "str.suffixof"); - addOperator(api::STRING_FROM_CODE, "str.from_code"); - addOperator(api::STRING_IS_DIGIT, "str.is_digit"); // at the moment, we only use this syntax for smt2.6 if (getLanguage() == language::input::LANG_SMTLIB_V2_6 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -692,6 +705,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } defineVar("re.allchar", d_solver->mkRegexpSigma()); + // Boolean is a placeholder + defineVar("seq.empty", + d_solver->mkEmptySequence(d_solver->getBooleanSort())); + addStringOperators(); } |