Replace `Maybe` with `std::optional` (#7005)

Because we are now using C++17, we can get rid of Maybe and instead
use std::optional, which offers the same functionality.

21 files changed, 156 insertions, 198 deletions

diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index dc48bc2a6..c60e636bd 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -411,7 +411,7 @@ void PseudoBooleanProcessor::applyReplacements(
 
 void PseudoBooleanProcessor::clear()
 {
-  d_off.clear();
+  d_off.reset();
   d_pos.clear();
   d_neg.clear();
 }
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 74ee67fa4..b5bb05138 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -21,6 +21,7 @@
 #ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
 #define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
 
+#include <optional>
 #include <unordered_set>
 #include <vector>
 
@@ -29,7 +30,6 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "theory/substitutions.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -100,7 +100,7 @@ class PseudoBooleanProcessor : public PreprocessingPass
   context::CDO<unsigned> d_pbs;
 
   // decompose into \sum pos >= neg + off
-  Maybe<Rational> d_off;
+  std::optional<Rational> d_off;
   std::vector<Node> d_pos;
   std::vector<Node> d_neg;
 
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 33860d2d9..89d7619cf 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -308,16 +308,17 @@ Rational ApproximateSimplex::estimateWithCFE(const Rational& r, const Integer& K
   }
 }
 
-Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d, const Integer& D)
+std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d,
+                                                            const Integer& D)
 {
-  if (Maybe<Rational> from_double = Rational::fromDouble(d))
+  if (std::optional<Rational> from_double = Rational::fromDouble(d))
   {
-    return estimateWithCFE(from_double.value(), D);
+    return estimateWithCFE(*from_double, D);
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
-Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d)
+std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d)
 {
   return estimateWithCFE(d, s_defaultMaxDenom);
 }
@@ -1106,9 +1107,9 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
         }
 
         DeltaRational proposal;
-        if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign))
+        if (std::optional maybe_new = estimateWithCFE(newAssign))
         {
-          proposal = maybe_new.value();
+          proposal = *maybe_new;
         }
         else
         {
@@ -2055,13 +2056,13 @@ bool ApproxGLPK::attemptBranchCut(int nid, const BranchCutInfo& br_cut){
   d_pad.d_cut.lhs.set(x, Rational(1));
 
   Rational& rhs = d_pad.d_cut.rhs;
-  Maybe<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
+  std::optional<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
   if (!br_cut_rhs)
   {
     return true;
   }
 
-  rhs = estimateWithCFE(br_cut_rhs.value(), Integer(1));
+  rhs = estimateWithCFE(*br_cut_rhs, Integer(1));
   d_pad.d_failure = !rhs.isIntegral();
   if(d_pad.d_failure) { return true; }
 
@@ -2112,13 +2113,13 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   DenseMap<Rational>& alpha = d_pad.d_alpha.lhs;
   Rational& b = d_pad.d_alpha.rhs;
 
-  Maybe<Rational> delta = estimateWithCFE(mir.delta);
+  std::optional<Rational> delta = estimateWithCFE(mir.delta);
   if (!delta)
   {
     return true;
   }
 
-  d_pad.d_failure = (delta.value().sgn() <= 0);
+  d_pad.d_failure = (delta->sgn() <= 0);
   if(d_pad.d_failure){ return true; }
 
   Debug("approx::mir") << "applyCMIRRule() " << delta << " " << mir.delta << endl;
@@ -2128,7 +2129,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   for(; iter != iend; ++iter){
     ArithVar v = *iter;
     const Rational& curr = alpha[v];
-    Rational next = curr / delta.value();
+    Rational next = curr / *delta;
     if(compRanges.isKey(v)){
       b -= curr * compRanges[v];
       alpha.set(v, - next);
@@ -2136,7 +2137,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
       alpha.set(v, next);
     }
   }
-  b = b / delta.value();
+  b = b / *delta;
 
   Rational roundB = (b + Rational(1,2)).floor();
   d_pad.d_failure = (b - roundB).abs() < Rational(1,90);
@@ -2554,7 +2555,7 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     if(x == ARITHVAR_SENTINEL){ return true; }
-    Maybe<Rational> c = estimateWithCFE(coeff);
+    std::optional<Rational> c = estimateWithCFE(coeff);
     if (!c)
     {
       return true;
@@ -2562,11 +2563,11 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
 
     if (lhs.isKey(x))
     {
-      lhs.get(x) -= c.value();
+      lhs.get(x) -= *c;
     }
     else
     {
-      lhs.set(x, -c.value());
+      lhs.set(x, -(*c));
     }
   }
 
@@ -2586,13 +2587,13 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     Assert(x != ARITHVAR_SENTINEL);
-    Maybe<Rational> c = estimateWithCFE(coeff);
+    std::optional<Rational> c = estimateWithCFE(coeff);
     if (!c)
     {
       return true;
     }
     Assert(!lhs.isKey(x));
-    lhs.set(x, c.value());
+    lhs.set(x, *c);
   }
 
   if(Debug.isOn("approx::mir")){
@@ -3023,12 +3024,12 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit
     }
     Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("<<d_vars.asNode(var)<<")"<<endl;
 
-    Maybe<Rational> cfe = estimateWithCFE(coeff, D);
+    std::optional<Rational> cfe = estimateWithCFE(coeff, D);
     if (!cfe)
     {
       return true;
     }
-    tab.set(var, cfe.value());
+    tab.set(var, *cfe);
     Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl;
   }
   if(!guessIsConstructable(tab)){
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index aeced6f10..c0d6990a4 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -19,12 +19,13 @@
 #include "cvc5_private.h"
 
 #pragma once
+
+#include <optional>
 #include <vector>
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 #include "util/statistics_stats.h"
 
@@ -126,8 +127,8 @@ class ApproximateSimplex{
    * cuts off the estimate once the value is approximately zero.
    * This is designed for removing rounding artifacts.
    */
-  static Maybe<Rational> estimateWithCFE(double d);
-  static Maybe<Rational> estimateWithCFE(double d, const Integer& D);
+  static std::optional<Rational> estimateWithCFE(double d);
+  static std::optional<Rational> estimateWithCFE(double d, const Integer& D);
 
   /**
    * Converts a rational to a continued fraction expansion representation
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 07f24f0f0..4cbb8211d 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.cpp
@@ -35,20 +35,21 @@ InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
   Assert(a != Simplex);
 }
 
-InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
-  : d_alg(Simplex)
+InferBoundAlgorithm::InferBoundAlgorithm(
+    const std::optional<int>& simplexRounds)
+    : d_alg(Simplex)
 {}
 
 Algorithms InferBoundAlgorithm::getAlgorithm() const{
   return d_alg;
 }
 
-const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
+const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const
+{
   Assert(getAlgorithm() == Simplex);
   return d_simplexRounds;
 }
 
-
 InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
   return InferBoundAlgorithm(Lookup);
 }
@@ -57,7 +58,9 @@ InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
   return InferBoundAlgorithm(RowSum);
 }
 
-InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
+InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
+    const std::optional<int>& rounds)
+{
   return InferBoundAlgorithm(rounds);
 }
 
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index 8a65c7c66..22b0b5d54 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -20,12 +20,12 @@
 
 #pragma once
 
+#include <optional>
 #include <ostream>
 
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
 #include "util/integer.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -39,19 +39,19 @@ namespace inferbounds {
 class InferBoundAlgorithm {
 private:
   Algorithms d_alg;
-  Maybe<int> d_simplexRounds;
+  std::optional<int> d_simplexRounds;
   InferBoundAlgorithm(Algorithms a);
-  InferBoundAlgorithm(const Maybe<int>& simplexRounds);
+  InferBoundAlgorithm(const std::optional<int>& simplexRounds);
 
-public:
+ public:
   InferBoundAlgorithm();
 
   Algorithms getAlgorithm() const;
-  const Maybe<int>& getSimplexRounds() const;
+  const std::optional<int>& getSimplexRounds() const;
 
   static InferBoundAlgorithm mkLookup();
   static InferBoundAlgorithm mkRowSum();
-  static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
+  static InferBoundAlgorithm mkSimplex(const std::optional<int>& rounds);
 };
 
 std::ostream& operator<<(std::ostream& os, const Algorithms a);
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 82cc02815..47dd208c1 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -1054,14 +1054,12 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   Assert(nbSgn != 0);
 
   if(nbSgn > 0){
-    if (d_upperBoundDifference.nothing()
-        || nbDiff <= d_upperBoundDifference.value())
+    if (!d_upperBoundDifference || nbDiff <= *d_upperBoundDifference)
     {
       return false;
     }
   }else{
-    if (d_lowerBoundDifference.nothing()
-        || nbDiff >= d_lowerBoundDifference.value())
+    if (!d_lowerBoundDifference || nbDiff >= *d_lowerBoundDifference)
     {
       return false;
     }
@@ -1132,8 +1130,8 @@ UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry, b
 UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref){
   Assert(d_increasing.empty());
   Assert(d_decreasing.empty());
-  Assert(d_lowerBoundDifference.nothing());
-  Assert(d_upperBoundDifference.nothing());
+  Assert(!d_lowerBoundDifference);
+  Assert(!d_upperBoundDifference);
 
   int focusCoeffSgn = focusCoeff.sgn();
 
@@ -1146,14 +1144,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational&
   if(d_variables.hasUpperBound(nb)){
     ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
     d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
-    Border border(ub, d_upperBoundDifference.value(), false, NULL, true);
+    Border border(ub, *d_upperBoundDifference, false, NULL, true);
     Debug("handleBorders") << "push back increasing " << border << endl;
     d_increasing.push_back(border);
   }
   if(d_variables.hasLowerBound(nb)){
     ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
     d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
-    Border border(lb, d_lowerBoundDifference.value(), false, NULL, false);
+    Border border(lb, *d_lowerBoundDifference, false, NULL, false);
     Debug("handleBorders") << "push back decreasing " << border << endl;
     d_decreasing.push_back(border);
   }
@@ -1189,8 +1187,8 @@ void LinearEqualityModule::clearSpeculative(){
   // clear everything away
   d_increasing.clear();
   d_decreasing.clear();
-  d_lowerBoundDifference.clear();
-  d_upperBoundDifference.clear();
+  d_lowerBoundDifference.reset();
+  d_upperBoundDifference.reset();
 }
 
 void LinearEqualityModule::handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref){
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 276c8e63e..7195a6583 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -37,7 +37,6 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/simplex_update.h"
 #include "theory/arith/tableau.h"
-#include "util/maybe.h"
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
@@ -216,8 +215,8 @@ private:
 
   BorderHeap d_increasing;
   BorderHeap d_decreasing;
-  Maybe<DeltaRational> d_upperBoundDifference;
-  Maybe<DeltaRational> d_lowerBoundDifference;
+  std::optional<DeltaRational> d_upperBoundDifference;
+  std::optional<DeltaRational> d_lowerBoundDifference;
 
   Rational d_one;
   Rational d_negOne;
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index e5fa31aad..2b1ef0a2e 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -603,39 +603,39 @@ Node excluding_interval_to_lemma(const Node& variable,
   return nm->mkNode(Kind::OR, lb, ub);
 }
 
-Maybe<Rational> get_lower_bound(const Node& n)
+std::optional<Rational> get_lower_bound(const Node& n)
 {
-  if (n.getNumChildren() != 2) return Maybe<Rational>();
+  if (n.getNumChildren() != 2) return std::optional<Rational>();
   if (n.getKind() == Kind::LT)
   {
-    if (!n[0].isConst()) return Maybe<Rational>();
-    if (!n[1].isVar()) return Maybe<Rational>();
+    if (!n[0].isConst()) return std::optional<Rational>();
+    if (!n[1].isVar()) return std::optional<Rational>();
     return n[0].getConst<Rational>();
   }
   else if (n.getKind() == Kind::GT)
   {
-    if (!n[0].isVar()) return Maybe<Rational>();
-    if (!n[1].isConst()) return Maybe<Rational>();
+    if (!n[0].isVar()) return std::optional<Rational>();
+    if (!n[1].isConst()) return std::optional<Rational>();
     return n[1].getConst<Rational>();
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
-Maybe<Rational> get_upper_bound(const Node& n)
+std::optional<Rational> get_upper_bound(const Node& n)
 {
-  if (n.getNumChildren() != 2) return Maybe<Rational>();
+  if (n.getNumChildren() != 2) return std::optional<Rational>();
   if (n.getKind() == Kind::LT)
   {
-    if (!n[0].isVar()) return Maybe<Rational>();
-    if (!n[1].isConst()) return Maybe<Rational>();
+    if (!n[0].isVar()) return std::optional<Rational>();
+    if (!n[1].isConst()) return std::optional<Rational>();
     return n[1].getConst<Rational>();
   }
   else if (n.getKind() == Kind::GT)
   {
-    if (!n[0].isConst()) return Maybe<Rational>();
-    if (!n[1].isVar()) return Maybe<Rational>();
+    if (!n[0].isConst()) return std::optional<Rational>();
+    if (!n[1].isVar()) return std::optional<Rational>();
     return n[0].getConst<Rational>();
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
 /** Returns indices of appropriate parts of ran encoding.
@@ -675,12 +675,12 @@ std::tuple<Node, Rational, Rational> detect_ran_encoding(const Node& n)
     Assert(false) << "Invalid polynomial equation.";
   }
 
-  Maybe<Rational> lower = get_lower_bound(n[0]);
+  std::optional<Rational> lower = get_lower_bound(n[0]);
   if (!lower) lower = get_lower_bound(n[1]);
   if (!lower) lower = get_lower_bound(n[2]);
   Assert(lower) << "Could not identify lower bound.";
 
-  Maybe<Rational> upper = get_upper_bound(n[0]);
+  std::optional<Rational> upper = get_upper_bound(n[0]);
   if (!upper) upper = get_upper_bound(n[1]);
   if (!upper) upper = get_upper_bound(n[2]);
   Assert(upper) << "Could not identify upper bound.";
diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index dc01a9b42..78e58000e 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -14,6 +14,7 @@
  */
 
 #include "theory/arith/simplex_update.h"
+
 #include "theory/arith/constraint.h"
 
 using namespace std;
@@ -22,6 +23,22 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
+/*
+ * Generates a string representation of std::optional and inserts it into a
+ * stream.
+ *
+ * Note: We define this function here in the cvc5::theory::arith namespace,
+ * because it would otherwise not be found for std::optional<int>. This is due
+ * to the argument-dependent lookup rules.
+ *
+ * @param out The stream
+ * @param m The value
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, const std::optional<int>& m)
+{
+  return cvc5::operator<<(out, m);
+}
 
 UpdateInfo::UpdateInfo():
   d_nonbasic(ARITHVAR_SENTINEL),
@@ -72,7 +89,7 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
   d_focusDirection = f;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(unbounded());
   Assert(improvement(d_witness));
@@ -82,9 +99,9 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
 void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
   d_limiting = c;
   d_nonbasicDelta = delta;
-  d_errorsChange.clear();
+  d_errorsChange.reset();
   d_focusDirection = 1;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(!describesPivot());
   Assert(improvement(d_witness));
@@ -94,8 +111,8 @@ void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
 void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
   d_limiting = c;
   d_nonbasicDelta = delta;
-  d_errorsChange.clear();
-  d_focusDirection.clear();
+  d_errorsChange.reset();
+  d_focusDirection.reset();
   updateWitness();
   Assert(describesPivot());
   Assert(debugSgnAgreement());
@@ -105,7 +122,7 @@ void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, Cons
   d_limiting = c;
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
-  d_focusDirection.clear();
+  d_focusDirection.reset();
   d_tableauCoefficient = &r;
   updateWitness();
   Assert(describesPivot());
@@ -117,7 +134,7 @@ void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
   d_focusDirection = fd;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(describesPivot() || improvement(d_witness));
   Assert(debugSgnAgreement());
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 6216f53f6..7efa51acb 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -29,10 +29,11 @@
 
 #pragma once
 
-#include "theory/arith/delta_rational.h"
+#include <optional>
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
-#include "util/maybe.h"
+#include "theory/arith/delta_rational.h"
 
 namespace cvc5 {
 namespace theory {
@@ -109,7 +110,7 @@ private:
    * This is changed via the updateProposal(...) methods.
    * The value needs to satisfy debugSgnAgreement() or it is in conflict.
    */
-  Maybe<DeltaRational> d_nonbasicDelta;
+  std::optional<DeltaRational> d_nonbasicDelta;
 
   /**
    * This is true if the pivot-and-update is *known* to cause a conflict.
@@ -118,16 +119,16 @@ private:
   bool d_foundConflict;
 
   /** This is the change in the size of the error set. */
-  Maybe<int> d_errorsChange;
+  std::optional<int> d_errorsChange;
 
   /** This is the sgn of the change in the value of the focus set.*/
-  Maybe<int> d_focusDirection;
+  std::optional<int> d_focusDirection;
 
   /** This is the sgn of the change in the value of the focus set.*/
-  Maybe<DeltaRational> d_focusChange;
+  std::optional<DeltaRational> d_focusChange;
 
   /** This is the coefficient in the tableau for the entry.*/
-  Maybe<const Rational*> d_tableauCoefficient;
+  std::optional<const Rational*> d_tableauCoefficient;
 
   /**
    * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
@@ -329,18 +330,19 @@ private:
     if(d_foundConflict){
       return ConflictFound;
     }
-    else if (d_errorsChange.just() && d_errorsChange.value() < 0)
+    else if (d_errorsChange && d_errorsChange.value() < 0)
     {
       return ErrorDropped;
     }
-    else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
+    else if (d_errorsChange.value_or(0) == 0)
     {
-      if(d_focusDirection.just()){
-        if (d_focusDirection.value() > 0)
+      if (d_focusDirection)
+      {
+        if (*d_focusDirection > 0)
         {
           return FocusImproved;
         }
-        else if (d_focusDirection.value() == 0)
+        else if (*d_focusDirection == 0)
         {
           return Degenerate;
         }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c85376e6b..3102dc7b8 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/theory_arith_private.h"
 
 #include <map>
+#include <optional>
 #include <queue>
 #include <vector>
 
@@ -2066,7 +2067,8 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(
     if(d_partialModel.hasNode(v)){
       d_lhsTmp.set(v, Rational(1));
       double dval = nl.branchValue();
-      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      std::optional<Rational> maybe_value =
+          ApproximateSimplex::estimateWithCFE(dval);
       if (!maybe_value)
       {
         return make_pair(NullConstraint, ARITHVAR_SENTINEL);
@@ -2609,7 +2611,8 @@ Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
     if(d_partialModel.hasNode(v)){
       Node n = d_partialModel.asNode(v);
       double dval = bn.branchValue();
-      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      std::optional<Rational> maybe_value =
+          ApproximateSimplex::estimateWithCFE(dval);
       if (!maybe_value)
       {
         return Node::null();
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 71742dfce..ad277cbb6 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -42,7 +42,6 @@ libcvc5_add_sources(
   iand.h
   index.cpp
   index.h
-  maybe.h
   ostream_util.cpp
   ostream_util.h
   poly_util.cpp
diff --git a/src/util/maybe.h b/src/util/maybe.h
deleted file mode 100644
index 838caa39e..000000000
--- a/src/util/maybe.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * This provides a templated Maybe construct.
- *
- * This class provides a templated Maybe<T> construct.
- * This follows the rough pattern of the Maybe monad in haskell.
- * A Maybe is an algebraic type that is either Nothing | Just T
- *
- * T must support T() and operator=.
- *
- * This has a couple of uses:
- * - There is no reasonable value or particularly clean way to represent
- *   Nothing using a value of T
- * - High level of assurance that a value is not used before it is set.
- */
-#include "cvc5_public.h"
-
-#ifndef CVC5__UTIL__MAYBE_H
-#define CVC5__UTIL__MAYBE_H
-
-#include <ostream>
-
-#include "base/exception.h"
-
-namespace cvc5 {
-
-template <class T>
-class Maybe
-{
- public:
-  Maybe() : d_just(false), d_value(){}
-  Maybe(const T& val): d_just(true), d_value(val){}
-
-  Maybe& operator=(const T& v){
-    d_just = true;
-    d_value = v;
-    return *this;
-  }
-
-  inline bool nothing() const { return !d_just; }
-  inline bool just() const { return d_just; }
-  explicit operator bool() const noexcept { return just(); }
-
-  void clear() {
-    if(just()){
-      d_just = false;
-      d_value = T();
-    }
-  }
-
-  const T& value() const
-  {
-    if (nothing())
-    {
-      throw Exception("Maybe::value() requires the maybe to be set.");
-    }
-    return d_value;
-  }
-
- private:
-  bool d_just;
-  T d_value;
-};
-
-template <class T>
-inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
-  out << "{";
-  if(m.nothing()){
-    out << "Nothing";
-  }else{
-    out << "Just ";
-    out << m.value();
-  }
-  out << "}";
-  return out;
-}
-
-}  // namespace cvc5
-
-#endif /* CVC5__UTIL__MAYBE_H */
diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
index 133cd00a3..7a5ae714e 100644
--- a/src/util/poly_util.cpp
+++ b/src/util/poly_util.cpp
@@ -23,7 +23,6 @@
 #include <sstream>
 
 #include "base/check.h"
-#include "maybe.h"
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/real_algebraic_number.h"
@@ -157,7 +156,7 @@ poly::Rational toRational(const Rational& r)
 #endif
 }
 
-Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
+std::optional<poly::DyadicRational> toDyadicRational(const Rational& r)
 {
   Integer den = r.getDenominator();
   if (den.isOne())
@@ -170,10 +169,10 @@ Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
     // It's a dyadic rational.
     return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1);
   }
-  return Maybe<poly::DyadicRational>();
+  return std::optional<poly::DyadicRational>();
 }
 
-Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
+std::optional<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
 {
   poly::Integer den = denominator(r);
   if (den == poly::Integer(1))
@@ -187,7 +186,7 @@ Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
     // It's a dyadic rational.
     return div_2exp(poly::DyadicRational(numerator(r)), size);
   }
-  return Maybe<poly::DyadicRational>();
+  return std::optional<poly::DyadicRational>();
 }
 
 poly::Rational approximateToDyadic(const poly::Rational& r,
@@ -212,8 +211,8 @@ poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
                                               const Rational& lower,
                                               const Rational& upper)
 {
-  Maybe<poly::DyadicRational> ml = toDyadicRational(lower);
-  Maybe<poly::DyadicRational> mu = toDyadicRational(upper);
+  std::optional<poly::DyadicRational> ml = toDyadicRational(lower);
+  std::optional<poly::DyadicRational> mu = toDyadicRational(upper);
   if (ml && mu)
   {
     return poly::AlgebraicNumber(std::move(p),
diff --git a/src/util/poly_util.h b/src/util/poly_util.h
index b33710fce..f8c430bc2 100644
--- a/src/util/poly_util.h
+++ b/src/util/poly_util.h
@@ -18,9 +18,9 @@
 #ifndef CVC5__POLY_UTIL_H
 #define CVC5__POLY_UTIL_H
 
+#include <optional>
 #include <vector>
 
-#include "maybe.h"
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/real_algebraic_number.h"
@@ -66,12 +66,12 @@ poly::Rational toRational(const Rational& r);
  * Converts a cvc5::Rational to a poly::DyadicRational. If the input is not
  * dyadic, no result is produced.
  */
-Maybe<poly::DyadicRational> toDyadicRational(const Rational& r);
+std::optional<poly::DyadicRational> toDyadicRational(const Rational& r);
 /**
  * Converts a poly::Rational to a poly::DyadicRational. If the input is not
  * dyadic, no result is produced.
  */
-Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r);
+std::optional<poly::DyadicRational> toDyadicRational(const poly::Rational& r);
 
 /**
  * Iteratively approximates a poly::Rational by a dyadic poly::Rational.
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 728b2d97e..033e53e95 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -99,7 +99,7 @@ int Rational::absCmp(const Rational& q) const{
   }
 }
 
-Maybe<Rational> Rational::fromDouble(double d)
+std::optional<Rational> Rational::fromDouble(double d)
 {
   try{
     cln::cl_DF fromD = d;
@@ -107,11 +107,11 @@ Maybe<Rational> Rational::fromDouble(double d)
     q.d_value = cln::rationalize(fromD);
     return q;
   }catch(cln::floating_point_underflow_exception& fpue){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }catch(cln::floating_point_nan_exception& fpne){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }catch(cln::floating_point_overflow_exception& fpoe){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }
 }
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 67e73f7e9..f1b6022cf 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -27,13 +27,13 @@
 #include <cln/rational_io.h>
 #include <cln/real.h>
 
+#include <optional>
 #include <sstream>
 #include <string>
 
 #include "base/exception.h"
 #include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/integer.h"
-#include "util/maybe.h"
 
 namespace cvc5 {
 
@@ -190,7 +190,7 @@ class CVC5_EXPORT Rational
   Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
 
   /** Return an exact rational for a double d. */
-  static Maybe<Rational> fromDouble(double d);
+  static std::optional<Rational> fromDouble(double d);
 
   /**
    * Get a double representation of this Rational, which is
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 0997b8b09..c68e15e27 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -85,7 +85,7 @@ int Rational::absCmp(const Rational& q) const{
 
 
 /** Return an exact rational for a double d. */
-Maybe<Rational> Rational::fromDouble(double d)
+std::optional<Rational> Rational::fromDouble(double d)
 {
   using namespace std;
   if(isfinite(d)){
@@ -93,7 +93,7 @@ Maybe<Rational> Rational::fromDouble(double d)
     mpq_set_d(q.d_value.get_mpq_t(), d);
     return q;
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
 }  // namespace cvc5
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index fd7492a87..b3c876533 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -20,12 +20,12 @@
 
 #include <gmp.h>
 
+#include <optional>
 #include <string>
 
 #include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/gmp_util.h"
 #include "util/integer.h"
-#include "util/maybe.h"
 
 namespace cvc5 {
 
@@ -164,7 +164,7 @@ class CVC5_EXPORT Rational
    */
   Integer getDenominator() const { return Integer(d_value.get_den()); }
 
-  static Maybe<Rational> fromDouble(double d);
+  static std::optional<Rational> fromDouble(double d);
 
   /**
    * Get a double representation of this Rational, which is
diff --git a/src/util/utility.h b/src/util/utility.h
index 3958ff166..9126d3e25 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -21,6 +21,7 @@
 #include <algorithm>
 #include <fstream>
 #include <memory>
+#include <optional>
 #include <string>
 
 namespace cvc5 {
@@ -61,6 +62,31 @@ void container_to_stream(std::ostream& out,
 }
 
 /**
+ * Generates a string representation of std::optional and inserts it into a
+ * stream.
+ *
+ * @param out The stream
+ * @param m The value
+ * @return The stream
+ */
+template <class T>
+std::ostream& operator<<(std::ostream& out, const std::optional<T>& m)
+{
+  out << "{";
+  if (m)
+  {
+    out << "Just ";
+    out << *m;
+  }
+  else
+  {
+    out << "Nothing";
+  }
+  out << "}";
+  return out;
+}
+
+/**
  * Opens a new temporary file with a given filename pattern and returns an
  * fstream to it. The directory that the file is created in is either TMPDIR or
  * /tmp/ if TMPDIR is not set.