Skip to content

Commit

Permalink
Deprecate make_and in favour of conjunction(expr, expr)
Browse files Browse the repository at this point in the history
`make_and` does not necessarily produce an `and_exprt`, so its name is
misleading. We already have `conjunction(exprt::operandst)`, and will
now have a variant thereof that takes exactly two operands.
  • Loading branch information
tautschnig committed Sep 10, 2024
1 parent 4ae54e6 commit eb098bb
Show file tree
Hide file tree
Showing 6 changed files with 35 additions and 22 deletions.
2 changes: 1 addition & 1 deletion src/goto-symex/symex_assign.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/prop/bdd_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down
20 changes: 1 addition & 19 deletions src/util/expr_util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions src/util/expr_util.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
25 changes: 25 additions & 0 deletions src/util/std_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
5 changes: 5 additions & 0 deletions src/util/std_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -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<and_exprt>(const exprt &base)
{
Expand Down

0 comments on commit eb098bb

Please sign in to comment.