diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index c829e4b1d8c..bc12b9db2d4 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -238,7 +238,7 @@ void symex_assignt::assign_non_struct_symbol( : assignment_type; target.assignment( - make_and(state.guard.as_expr(), conjunction(guard)), + conjunction(state.guard.as_expr(), conjunction(guard)), l2_lhs, l2_full_lhs, get_original_name(l2_full_lhs), diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index f900c90f765..cbb5ee60cc6 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -138,7 +138,7 @@ exprt bdd_exprt::as_expr( if(r.else_branch().is_complement()) // else is false { exprt then_case = as_expr(r.then_branch(), cache); - return make_and(n_expr, then_case); + return conjunction(n_expr, then_case); } exprt then_case = as_expr(r.then_branch(), cache); return make_or(not_exprt(n_expr), then_case); @@ -149,7 +149,7 @@ exprt bdd_exprt::as_expr( if(r.then_branch().is_complement()) // then is false { exprt else_case = as_expr(r.else_branch(), cache); - return make_and(not_exprt(n_expr), else_case); + return conjunction(not_exprt(n_expr), else_case); } exprt else_case = as_expr(r.else_branch(), cache); return make_or(n_expr, else_case); diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 7e4739a7372..952608cdb19 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -346,25 +346,7 @@ constant_exprt make_boolean_expr(bool value) exprt make_and(exprt a, exprt b) { - PRECONDITION(a.is_boolean() && b.is_boolean()); - if(b.is_constant()) - { - if(b.get(ID_value) == ID_false) - return false_exprt{}; - return a; - } - if(a.is_constant()) - { - if(a.get(ID_value) == ID_false) - return false_exprt{}; - return b; - } - if(b.id() == ID_and) - { - b.add_to_operands(std::move(a)); - return b; - } - return and_exprt{std::move(a), std::move(b)}; + return conjunction(a, b); } bool is_null_pointer(const constant_exprt &expr) diff --git a/src/util/expr_util.h b/src/util/expr_util.h index b423dcdd9fb..2cd5d37973b 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -111,6 +111,7 @@ constant_exprt make_boolean_expr(bool); /// Conjunction of two expressions. If the second is already an `and_exprt` /// add to its operands instead of creating a new expression. If one is `true`, /// return the other expression. If one is `false` returns `false`. +DEPRECATED(SINCE(2024, 9, 10, "use conjunction(exprt, exprt) instead")) exprt make_and(exprt a, exprt b); /// Returns true if \p expr has a pointer type and a value NULL; it also returns diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 50cb5684220..cee5d722374 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -63,12 +63,37 @@ exprt disjunction(const exprt::operandst &op) } } +exprt conjunction(exprt a, exprt b) +{ + PRECONDITION(a.is_boolean() && b.is_boolean()); + if(b.is_constant()) + { + if(to_constant_expr(b).is_false()) + return false_exprt{}; + return a; + } + if(a.is_constant()) + { + if(to_constant_expr(a).is_false()) + return false_exprt{}; + return b; + } + if(b.id() == ID_and) + { + b.add_to_operands(std::move(a)); + return b; + } + return and_exprt{std::move(a), std::move(b)}; +} + exprt conjunction(const exprt::operandst &op) { if(op.empty()) return true_exprt(); else if(op.size()==1) return op.front(); + else if(op.size() == 2) + return conjunction(op[0], op[1]); else { return and_exprt(exprt::operandst(op)); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 431de0bfa00..65e8e1722d1 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2152,6 +2152,11 @@ class and_exprt:public multi_ary_exprt exprt conjunction(const exprt::operandst &); +/// Conjunction of two expressions. If the second is already an `and_exprt` +/// add to its operands instead of creating a new expression. If one is `true`, +/// return the other expression. If one is `false` returns `false`. +exprt conjunction(exprt a, exprt b); + template <> inline bool can_cast_expr(const exprt &base) {