diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-11-08 18:51:58 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-09 02:51:58 +0000 |
| commit | 1d145ff68ba6e4abaf77adfe97b072f63c4d7231 (patch) | |
| tree | 91b6725801e183e3a9f928a9f0dcaedd17c15776 /src/parser | |
| parent | 7391d16bf8669060043e9cff17b9e76ff15ef19e (diff) | |
regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)
This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to
REGEXP_ALLCHAR to match their SMT-LIB representation (re.none,
re.allchar). It further renames api::Solver::mkRegexpEmpty() to
mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b86c564d0..7add605c5 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -147,7 +147,7 @@ void Smt2::addDatatypesOperators() void Smt2::addStringOperators() { defineVar( "re.all", - getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())); + getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar())); addOperator(api::STRING_CONCAT, "str.++"); addOperator(api::STRING_LENGTH, "str.len"); addOperator(api::STRING_SUBSTR, "str.substr"); @@ -636,8 +636,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) defineType("RegLan", d_solver->getRegExpSort(), true, true); defineType("Int", d_solver->getIntegerSort(), true, true); - defineVar("re.none", d_solver->mkRegexpEmpty()); - defineVar("re.allchar", d_solver->mkRegexpSigma()); + defineVar("re.none", d_solver->mkRegexpNone()); + defineVar("re.allchar", d_solver->mkRegexpAllchar()); // Boolean is a placeholder defineVar("seq.empty", |