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/expr/node_manager.h | |
| 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/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d0c607a4b..1208a0e03 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -394,7 +394,7 @@ class NodeManager * - We can avoid creating a temporary vector in some cases, e.g., when we * want to create a node with a fixed, large number of children * - It makes sure that calls to `mkNode` that braced-init-lists work as - * expected, e.g., mkNode(REGEXP_EMPTY, {}) will call this overload instead + * expected, e.g., mkNode(REGEXP_NONE, {}) will call this overload instead * of creating a node with a null node as a child. */ Node mkNode(Kind kind, std::initializer_list<TNode> children); |