git.libre-soc.org Git - cvc5.git/commit

author	Aina Niemetz <aina.niemetz@gmail.com>
	Tue, 9 Nov 2021 02:51:58 +0000 (18:51 -0800)
committer	GitHub <noreply@github.com>
	Tue, 9 Nov 2021 02:51:58 +0000 (02:51 +0000)
commit	1d145ff68ba6e4abaf77adfe97b072f63c4d7231
tree	91b6725801e183e3a9f928a9f0dcaedd17c15776	tree
parent	7391d16bf8669060043e9cff17b9e76ff15ef19e	commit \| 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.

22 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Solver.java		diff \| blob \| history
src/api/java/jni/solver.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_entail.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
test/python/unit/api/test_solver.py		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/theory/regexp_operation_black.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history

RSS Atom