Deprecate make_and in favour of conjunction(expr, expr)

`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.

Author: tautschnig

regression/cbmc-cover/mcdc8/test.desc

@@ -3,10 +3,10 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$
-^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$
-^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
-^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'a != FALSE && !\(b != FALSE\) && c != FALSE: SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'a != FALSE && !\(b != FALSE\) && !\(c != FALSE\):  SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition '!\(a != FALSE\) && b != FALSE && c != FALSE: SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(a != FALSE\) && !\(b != FALSE\) && c != FALSE: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

src/goto-symex/symex_assign.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "symex_assign.h"
 
 #include <util/byte_operators.h>
-#include <util/expr_util.h>
 #include <util/pointer_expr.h>
 #include <util/range.h>
 
@@ -238,7 +237,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),

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);

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)

src/util/expr_util.h

@@ -112,6 +112,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

src/util/std_expr.cpp

@@ -80,12 +80,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));

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<and_exprt>(const exprt &base)
 {