From fc92f47ce17c320a1596958e9f0db31fde6c9728 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sat, 23 Dec 2023 19:08:08 +0000
Subject: [PATCH] remove dead code in FunctionExpr

---
 smt/exprs.cpp | 24 +-----------------------
 smt/exprs.h   |  7 ++-----
 2 files changed, 3 insertions(+), 28 deletions(-)

diff --git a/smt/exprs.cpp b/smt/exprs.cpp
index e48b37d70..8e2be974c 100644
--- a/smt/exprs.cpp
+++ b/smt/exprs.cpp
@@ -189,12 +189,8 @@ void FunctionExpr::add(const FunctionExpr &other) {
   fn.insert(other.fn.begin(), other.fn.end());
 }
 
-void FunctionExpr::del(const expr &key) {
-  fn.erase(key);
-}
-
 optional<expr> FunctionExpr::operator()(const expr &key) const {
-  DisjointExpr disj(default_val);
+  DisjointExpr<expr> disj;
   for (auto &[k, v] : fn) {
     disj.add(v, k == key);
   }
@@ -208,35 +204,17 @@ const expr* FunctionExpr::lookup(const expr &key) const {
 
 FunctionExpr FunctionExpr::simplify() const {
   FunctionExpr newfn;
-  if (default_val)
-    newfn.default_val = default_val->simplify();
-
   for (auto &[k, v] : fn) {
     newfn.add(k.simplify(), v.simplify());
   }
   return newfn;
 }
 
-weak_ordering FunctionExpr::operator<=>(const FunctionExpr &rhs) const {
-  if (auto cmp = fn <=> rhs.fn;
-      is_neq(cmp))
-    return cmp;
-
-  // libstdc++'s optional::operator<=> is buggy
-  // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=98842
-  if (default_val && rhs.default_val)
-    return *default_val <=> *rhs.default_val;
-
-  return (bool)default_val <=> (bool)rhs.default_val;
-}
-
 ostream& operator<<(ostream &os, const FunctionExpr &f) {
   os << "{\n";
   for (auto &[k, v] : f) {
     os << k << ": " << v << '\n';
   }
-  if (f.default_val)
-    os << "default: " << *f.default_val << '\n';
   return os << '}';
 }
 
diff --git a/smt/exprs.h b/smt/exprs.h
index 3ff2b63b5..c94aecc21 100644
--- a/smt/exprs.h
+++ b/smt/exprs.h
@@ -189,14 +189,11 @@ class ChoiceExpr {
 
 class FunctionExpr {
   std::map<expr, expr> fn; // key -> val
-  std::optional<expr> default_val;
 
 public:
   FunctionExpr() = default;
-  FunctionExpr(expr &&default_val) : default_val(std::move(default_val)) {}
   void add(const expr &key, expr &&val);
   void add(const FunctionExpr &other);
-  void del(const expr &key);
 
   std::optional<expr> operator()(const expr &key) const;
   const expr* lookup(const expr &key) const;
@@ -205,9 +202,9 @@ class FunctionExpr {
 
   auto begin() const { return fn.begin(); }
   auto end() const { return fn.end(); }
-  bool empty() const { return fn.empty() && !default_val; }
+  bool empty() const { return fn.empty(); }
 
-  std::weak_ordering operator<=>(const FunctionExpr &rhs) const;
+  auto operator<=>(const FunctionExpr &rhs) const = default;
 
   friend std::ostream& operator<<(std::ostream &os, const FunctionExpr &e);
 };