From eb098bb6c4be1044da353efc65810bb4c201d717 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 10 Sep 2024 12:50:56 +0000
Subject: [PATCH] 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.
---
 src/goto-symex/symex_assign.cpp |  2 +-
 src/solvers/prop/bdd_expr.cpp   |  4 ++--
 src/util/expr_util.cpp          | 20 +-------------------
 src/util/expr_util.h            |  1 +
 src/util/std_expr.cpp           | 25 +++++++++++++++++++++++++
 src/util/std_expr.h             |  5 +++++
 6 files changed, 35 insertions(+), 22 deletions(-)

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