mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

renamed compl method (compl is a reserved c++ keyword) to complement

Browse source
This commit is contained in:
Margus Veanes 2020-08-21 17:34:15 -07:00
parent 4dd9249a95
commit 1e29ba76d0
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.cpp
View file

@ -1685,7 +1685,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
return i1.plus(); return i1.plus();
case OP_RE_COMPLEMENT: case OP_RE_COMPLEMENT:
i1 = get_info_rec(e->get_arg(0)); i1 = get_info_rec(e->get_arg(0));
return i1.compl(); return i1.complement();
case OP_RE_LOOP: case OP_RE_LOOP:
i1 = get_info_rec(e->get_arg(0)); i1 = get_info_rec(e->get_arg(0));
lower_bound = e->get_decl()->get_parameter(0).get_int(); lower_bound = e->get_decl()->get_parameter(0).get_int();
@ -1754,7 +1754,7 @@ seq_util::rex::info seq_util::rex::info::opt() const {
return seq_util::rex::info(classical, classical, interpreted, nonbranching, normalized, monadic, false, l_true, 0, star_height); return seq_util::rex::info(classical, classical, interpreted, nonbranching, normalized, monadic, false, l_true, 0, star_height);
} }
seq_util::rex::info seq_util::rex::info::compl() const { seq_util::rex::info seq_util::rex::info::complement() const {
if (is_known()) { if (is_known()) {
lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef)); lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef));
unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0); unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0);

2
src/ast/seq_decl_plugin.h
View file

@ -479,7 +479,7 @@ public:
info star() const; info star() const;
info plus() const; info plus() const;
info opt() const; info opt() const;
info compl() const; info complement() const;
info concat(info & rhs, bool lhs_is_concat) const; info concat(info & rhs, bool lhs_is_concat) const;
info disj(info& rhs) const; info disj(info& rhs) const;
info conj(info& rhs) const; info conj(info& rhs) const;