From 42b8e0a4fc5b23dfce79cbadc08a8aa8542997e0 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 17 Aug 2021 11:18:16 -0700 Subject: [PATCH] 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. --- .../passes/pseudo_boolean_processor.cpp | 2 +- .../passes/pseudo_boolean_processor.h | 4 +- src/theory/arith/approx_simplex.cpp | 41 ++++----- src/theory/arith/approx_simplex.h | 7 +- src/theory/arith/infer_bounds.cpp | 13 +-- src/theory/arith/infer_bounds.h | 12 +-- src/theory/arith/linear_equality.cpp | 18 ++-- src/theory/arith/linear_equality.h | 5 +- src/theory/arith/nl/poly_conversion.cpp | 32 +++---- src/theory/arith/simplex_update.cpp | 31 +++++-- src/theory/arith/simplex_update.h | 26 +++--- src/theory/arith/theory_arith_private.cpp | 7 +- src/util/CMakeLists.txt | 1 - src/util/maybe.h | 90 ------------------- src/util/poly_util.cpp | 13 ++- src/util/poly_util.h | 6 +- src/util/rational_cln_imp.cpp | 8 +- src/util/rational_cln_imp.h | 4 +- src/util/rational_gmp_imp.cpp | 4 +- src/util/rational_gmp_imp.h | 4 +- src/util/utility.h | 26 ++++++ 21 files changed, 156 insertions(+), 198 deletions(-) delete mode 100644 src/util/maybe.h 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 #include #include @@ -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 d_pbs; // decompose into \sum pos >= neg + off - Maybe d_off; + std::optional d_off; std::vector d_pos; std::vector 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 ApproximateSimplex::estimateWithCFE(double d, const Integer& D) +std::optional ApproximateSimplex::estimateWithCFE(double d, + const Integer& D) { - if (Maybe from_double = Rational::fromDouble(d)) + if (std::optional from_double = Rational::fromDouble(d)) { - return estimateWithCFE(from_double.value(), D); + return estimateWithCFE(*from_double, D); } - return Maybe(); + return std::optional(); } -Maybe ApproximateSimplex::estimateWithCFE(double d) +std::optional ApproximateSimplex::estimateWithCFE(double d) { return estimateWithCFE(d, s_defaultMaxDenom); } @@ -1106,9 +1107,9 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const } DeltaRational proposal; - if (Maybe 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 br_cut_rhs = Rational::fromDouble(br_cut.getRhs()); + std::optional 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& alpha = d_pad.d_alpha.lhs; Rational& b = d_pad.d_alpha.rhs; - Maybe delta = estimateWithCFE(mir.delta); + std::optional 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 c = estimateWithCFE(coeff); + std::optional 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 c = estimateWithCFE(coeff); + std::optional 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 << "("< cfe = estimateWithCFE(coeff, D); + std::optional 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 #include #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 estimateWithCFE(double d); - static Maybe estimateWithCFE(double d, const Integer& D); + static std::optional estimateWithCFE(double d); + static std::optional 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& simplexRounds) - : d_alg(Simplex) +InferBoundAlgorithm::InferBoundAlgorithm( + const std::optional& simplexRounds) + : d_alg(Simplex) {} Algorithms InferBoundAlgorithm::getAlgorithm() const{ return d_alg; } -const Maybe& InferBoundAlgorithm::getSimplexRounds() const{ +const std::optional& 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& rounds){ +InferBoundAlgorithm InferBoundAlgorithm::mkSimplex( + const std::optional& 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 #include #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 d_simplexRounds; + std::optional d_simplexRounds; InferBoundAlgorithm(Algorithms a); - InferBoundAlgorithm(const Maybe& simplexRounds); + InferBoundAlgorithm(const std::optional& simplexRounds); -public: + public: InferBoundAlgorithm(); Algorithms getAlgorithm() const; - const Maybe& getSimplexRounds() const; + const std::optional& getSimplexRounds() const; static InferBoundAlgorithm mkLookup(); static InferBoundAlgorithm mkRowSum(); - static InferBoundAlgorithm mkSimplex(const Maybe& rounds); + static InferBoundAlgorithm mkSimplex(const std::optional& 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 d_upperBoundDifference; - Maybe d_lowerBoundDifference; + std::optional d_upperBoundDifference; + std::optional 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 get_lower_bound(const Node& n) +std::optional get_lower_bound(const Node& n) { - if (n.getNumChildren() != 2) return Maybe(); + if (n.getNumChildren() != 2) return std::optional(); if (n.getKind() == Kind::LT) { - if (!n[0].isConst()) return Maybe(); - if (!n[1].isVar()) return Maybe(); + if (!n[0].isConst()) return std::optional(); + if (!n[1].isVar()) return std::optional(); return n[0].getConst(); } else if (n.getKind() == Kind::GT) { - if (!n[0].isVar()) return Maybe(); - if (!n[1].isConst()) return Maybe(); + if (!n[0].isVar()) return std::optional(); + if (!n[1].isConst()) return std::optional(); return n[1].getConst(); } - return Maybe(); + return std::optional(); } -Maybe get_upper_bound(const Node& n) +std::optional get_upper_bound(const Node& n) { - if (n.getNumChildren() != 2) return Maybe(); + if (n.getNumChildren() != 2) return std::optional(); if (n.getKind() == Kind::LT) { - if (!n[0].isVar()) return Maybe(); - if (!n[1].isConst()) return Maybe(); + if (!n[0].isVar()) return std::optional(); + if (!n[1].isConst()) return std::optional(); return n[1].getConst(); } else if (n.getKind() == Kind::GT) { - if (!n[0].isConst()) return Maybe(); - if (!n[1].isVar()) return Maybe(); + if (!n[0].isConst()) return std::optional(); + if (!n[1].isVar()) return std::optional(); return n[0].getConst(); } - return Maybe(); + return std::optional(); } /** Returns indices of appropriate parts of ran encoding. @@ -675,12 +675,12 @@ std::tuple detect_ran_encoding(const Node& n) Assert(false) << "Invalid polynomial equation."; } - Maybe lower = get_lower_bound(n[0]); + std::optional 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 upper = get_upper_bound(n[0]); + std::optional 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. 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& 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 + #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 d_nonbasicDelta; + std::optional 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 d_errorsChange; + std::optional d_errorsChange; /** This is the sgn of the change in the value of the focus set.*/ - Maybe d_focusDirection; + std::optional d_focusDirection; /** This is the sgn of the change in the value of the focus set.*/ - Maybe d_focusChange; + std::optional d_focusChange; /** This is the coefficient in the tableau for the entry.*/ - Maybe d_tableauCoefficient; + std::optional 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 +#include #include #include @@ -2066,7 +2067,8 @@ std::pair TheoryArithPrivate::replayGetConstraint( if(d_partialModel.hasNode(v)){ d_lhsTmp.set(v, Rational(1)); double dval = nl.branchValue(); - Maybe maybe_value = ApproximateSimplex::estimateWithCFE(dval); + std::optional 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 maybe_value = ApproximateSimplex::estimateWithCFE(dval); + std::optional 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 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 - -#include "base/exception.h" - -namespace cvc5 { - -template -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 -inline std::ostream& operator<<(std::ostream& out, const Maybe& 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 #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 toDyadicRational(const Rational& r) +std::optional toDyadicRational(const Rational& r) { Integer den = r.getDenominator(); if (den.isOne()) @@ -170,10 +169,10 @@ Maybe toDyadicRational(const Rational& r) // It's a dyadic rational. return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1); } - return Maybe(); + return std::optional(); } -Maybe toDyadicRational(const poly::Rational& r) +std::optional toDyadicRational(const poly::Rational& r) { poly::Integer den = denominator(r); if (den == poly::Integer(1)) @@ -187,7 +186,7 @@ Maybe toDyadicRational(const poly::Rational& r) // It's a dyadic rational. return div_2exp(poly::DyadicRational(numerator(r)), size); } - return Maybe(); + return std::optional(); } poly::Rational approximateToDyadic(const poly::Rational& r, @@ -212,8 +211,8 @@ poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p, const Rational& lower, const Rational& upper) { - Maybe ml = toDyadicRational(lower); - Maybe mu = toDyadicRational(upper); + std::optional ml = toDyadicRational(lower); + std::optional 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 #include -#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 toDyadicRational(const Rational& r); +std::optional toDyadicRational(const Rational& r); /** * Converts a poly::Rational to a poly::DyadicRational. If the input is not * dyadic, no result is produced. */ -Maybe toDyadicRational(const poly::Rational& r); +std::optional 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::fromDouble(double d) +std::optional Rational::fromDouble(double d) { try{ cln::cl_DF fromD = d; @@ -107,11 +107,11 @@ Maybe Rational::fromDouble(double d) q.d_value = cln::rationalize(fromD); return q; }catch(cln::floating_point_underflow_exception& fpue){ - return Maybe(); + return std::optional(); }catch(cln::floating_point_nan_exception& fpne){ - return Maybe(); + return std::optional(); }catch(cln::floating_point_overflow_exception& fpoe){ - return Maybe(); + return std::optional(); } } 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 #include +#include #include #include #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 fromDouble(double d); + static std::optional 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::fromDouble(double d) +std::optional Rational::fromDouble(double d) { using namespace std; if(isfinite(d)){ @@ -93,7 +93,7 @@ Maybe Rational::fromDouble(double d) mpq_set_d(q.d_value.get_mpq_t(), d); return q; } - return Maybe(); + return std::optional(); } } // 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 +#include #include #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 fromDouble(double d); + static std::optional 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 #include #include +#include #include namespace cvc5 { @@ -60,6 +61,31 @@ void container_to_stream(std::ostream& out, out << postfix; } +/** + * 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 +std::ostream& operator<<(std::ostream& out, const std::optional& 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 -- 2.30.2