mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

added missing return statements, reordered def of compl to match declaration order of methods

Browse source
This commit is contained in:
Margus Veanes 2020-08-21 13:20:05 -07:00
parent 1099c519ab
commit 3fb226dcd6
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/seq_decl_plugin.cpp
View file

@ -1743,7 +1743,7 @@ seq_util::rex::info seq_util::rex::info::star() const {
seq_util::rex::info seq_util::rex::info::plus() const {
if (is_known()) {
//r+ is not normalized if r is nullable, the normalized form would be r*
info(classical, classical, interpreted, nonbranching, (nullable == l_false ? normalized : false), monadic, false, nullable, min_length, star_height + 1);
return info(classical, classical, interpreted, nonbranching, (nullable == l_false ? normalized : false), monadic, false, nullable, min_length, star_height + 1);
}
else
return *this;
@ -1791,7 +1791,7 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info & rhs, bool
seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info& rhs) const {
if (is_known() || rhs.is_known()) {
//works correctly if one of the arguments is unknown
info(classical & rhs.classical,
return info(classical & rhs.classical,
standard && rhs.standard,
interpreted && rhs.interpreted,
nonbranching && rhs.nonbranching,
@ -1830,7 +1830,7 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info& rhs) const {
seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info& rhs) const {
if (is_known()) {
if (rhs.is_known()) {
info(false,
return info(false,
standard & rhs.standard,
interpreted & rhs.interpreted,
nonbranching & rhs.nonbranching,

2
src/ast/seq_decl_plugin.h
View file

@ -479,13 +479,13 @@ public:
info star() const;
info plus() const;
info opt() const;
info compl() const;
info concat(info & rhs, bool lhs_is_concat) const;
info disj(info& rhs) const;
info conj(info& rhs) const;
info diff(info& rhs) const;
info orelse(info& rhs) const;
info loop(unsigned lower) const;
info compl() const;
};
private:
seq_util& u;