void PseudoBooleanProcessor::clear()
{
- d_off.clear();
+ d_off.reset();
d_pos.clear();
d_neg.clear();
}
#ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#include <optional>
#include <unordered_set>
#include <vector>
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
#include "theory/substitutions.h"
-#include "util/maybe.h"
#include "util/rational.h"
namespace cvc5 {
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;
}
}
-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);
}
}
DeltaRational proposal;
- if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign))
+ if (std::optional maybe_new = estimateWithCFE(newAssign))
{
- proposal = maybe_new.value();
+ proposal = *maybe_new;
}
else
{
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; }
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;
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);
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);
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;
if (lhs.isKey(x))
{
- lhs.get(x) -= c.value();
+ lhs.get(x) -= *c;
}
else
{
- lhs.set(x, -c.value());
+ lhs.set(x, -(*c));
}
}
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")){
}
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)){
#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"
* 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
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);
}
return InferBoundAlgorithm(RowSum);
}
-InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
+InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
+ const std::optional<int>& rounds)
+{
return InferBoundAlgorithm(rounds);
}
#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 {
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);
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;
}
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();
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);
}
// 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){
#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 {
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;
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.
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.";
*/
#include "theory/arith/simplex_update.h"
+
#include "theory/arith/constraint.h"
using namespace std;
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),
d_nonbasicDelta = delta;
d_errorsChange = ec;
d_focusDirection = f;
- d_tableauCoefficient.clear();
+ d_tableauCoefficient.reset();
updateWitness();
Assert(unbounded());
Assert(improvement(d_witness));
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));
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());
d_limiting = c;
d_nonbasicDelta = delta;
d_errorsChange = ec;
- d_focusDirection.clear();
+ d_focusDirection.reset();
d_tableauCoefficient = &r;
updateWitness();
Assert(describesPivot());
d_nonbasicDelta = delta;
d_errorsChange = ec;
d_focusDirection = fd;
- d_tableauCoefficient.clear();
+ d_tableauCoefficient.reset();
updateWitness();
Assert(describesPivot() || improvement(d_witness));
Assert(debugSgnAgreement());
#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 {
* 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.
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.
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;
}
#include "theory/arith/theory_arith_private.h"
#include <map>
+#include <optional>
#include <queue>
#include <vector>
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);
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();
iand.h
index.cpp
index.h
- maybe.h
ostream_util.cpp
ostream_util.h
poly_util.cpp
+++ /dev/null
-/******************************************************************************
- * 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 */
#include <sstream>
#include "base/check.h"
-#include "maybe.h"
#include "util/integer.h"
#include "util/rational.h"
#include "util/real_algebraic_number.h"
#endif
}
-
Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
+
std::optional<poly::DyadicRational> toDyadicRational(const Rational& r)
{
Integer den = r.getDenominator();
if (den.isOne())
// 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))
// 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,
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),
#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"
* 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.
}
}
-Maybe<Rational> Rational::fromDouble(double d)
+std::optional<Rational> Rational::fromDouble(double d)
{
try{
cln::cl_DF fromD = 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>();
}
}
#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 {
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
/** 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)){
mpq_set_d(q.d_value.get_mpq_t(), d);
return q;
}
- return Maybe<Rational>();
+ return std::optional<Rational>();
}
} // namespace cvc5
#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 {
*/
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
#include <algorithm>
#include <fstream>
#include <memory>
+#include <optional>
#include <string>
namespace cvc5 {
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 <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
projects / cvc5.git / commitdiff