* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.
%typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
%typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
-%typemap(throws) CVC4::RationalFromDoubleException = Exception;
-
// Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
%typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
#error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
d_explanation.clear();
}
};
+
ApproximateStatistics::ApproximateStatistics()
- // : d_relaxCalls("z::approx::relaxCalls",0)
- // , d_relaxUnknowns("z::approx::relaxUnknowns",0)
- // , d_relaxFeasible("z::approx::relaxFeasible",0)
- // , d_relaxInfeasible("z::approx::relaxInfeasible",0)
- // , d_relaxPivotsExhausted("z::approx::relaxPivotsExhausted",0)
- // , d_mipCalls("z::approx::mipCalls",0)
- // , d_mipUnknowns("z::approx::mipUnknowns",0)
- // , d_mipBingo("z::approx::mipBingo",0)
- // , d_mipClosed("z::approx::mipClosed",0)
- // , d_mipBranchesExhausted("z::approx::mipBranchesExhausted",0)
- // , d_mipPivotsExhausted("z::approx::mipPivotsExhausted",0)
- // , d_mipExecExhausted("z::approx::mipExecExhausted",0)
- // , d_gmiGen("z::approx::gmiGen",0)
- // , d_gmiReplay("z::approx::gmiReplay",0)
- // , d_mipGen("z::approx::mipGen",0)
- // , d_mipReplay("z::approx::mipReplay",0)
: d_branchMaxDepth("z::approx::branchMaxDepth",0)
, d_branchesMaxOnAVar("z::approx::branchesMaxOnAVar",0)
- //, d_branchTotal("z::approx::branchTotal",0)
- //, d_branchCuts("z::approx::branchCuts",0)
-
, d_gaussianElimConstructTime("z::approx::gaussianElimConstruct::time")
, d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
, d_averageGuesses("z::approx::averageGuesses")
{
- // smtStatisticsRegistry()->registerStat(&d_relaxCalls);
- // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns);
- // smtStatisticsRegistry()->registerStat(&d_relaxFeasible);
- // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible);
- // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted);
-
- // smtStatisticsRegistry()->registerStat(&d_mipCalls);
- // smtStatisticsRegistry()->registerStat(&d_mipUnknowns);
- // smtStatisticsRegistry()->registerStat(&d_mipBingo);
- // smtStatisticsRegistry()->registerStat(&d_mipClosed);
- // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted);
- // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted);
- // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted);
-
-
- // smtStatisticsRegistry()->registerStat(&d_gmiGen);
- // smtStatisticsRegistry()->registerStat(&d_gmiReplay);
- // smtStatisticsRegistry()->registerStat(&d_mipGen);
- // smtStatisticsRegistry()->registerStat(&d_mipReplay);
-
smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
- //smtStatisticsRegistry()->registerStat(&d_branchTotal);
- //smtStatisticsRegistry()->registerStat(&d_branchCuts);
smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
}
ApproximateStatistics::~ApproximateStatistics(){
- // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
- // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns);
- // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible);
- // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible);
- // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted);
-
- // smtStatisticsRegistry()->unregisterStat(&d_mipCalls);
- // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns);
- // smtStatisticsRegistry()->unregisterStat(&d_mipBingo);
- // smtStatisticsRegistry()->unregisterStat(&d_mipClosed);
- // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted);
- // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted);
- // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted);
-
-
- // smtStatisticsRegistry()->unregisterStat(&d_gmiGen);
- // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay);
- // smtStatisticsRegistry()->unregisterStat(&d_mipGen);
- // smtStatisticsRegistry()->unregisterStat(&d_mipReplay);
-
smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
- //smtStatisticsRegistry()->unregisterStat(&d_branchTotal);
- //smtStatisticsRegistry()->unregisterStat(&d_branchCuts);
smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar);
smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime);
}
}
-Rational ApproximateSimplex::estimateWithCFE(double d, const Integer& D) throw (RationalFromDoubleException){
- return estimateWithCFE(Rational::fromDouble(d), D);
+Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d, const Integer& D)
+{
+ if (Maybe<Rational> from_double = Rational::fromDouble(d))
+ {
+ return estimateWithCFE(from_double.value(), D);
+ }
+ return Maybe<Rational>();
}
-Rational ApproximateSimplex::estimateWithCFE(double d) throw (RationalFromDoubleException){
+Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d)
+{
return estimateWithCFE(d, s_defaultMaxDenom);
}
{}
~ApproxNoOp(){}
- virtual LinResult solveRelaxation(){
- return LinUnknown;
- }
- virtual Solution extractRelaxation() const throw (RationalFromDoubleException){
- return Solution();
- }
+ LinResult solveRelaxation() override { return LinUnknown; }
+ Solution extractRelaxation() const override { return Solution(); }
- virtual ArithRatPairVec heuristicOptCoeffs() const{
+ ArithRatPairVec heuristicOptCoeffs() const override
+ {
return ArithRatPairVec();
}
- virtual MipResult solveMIP(bool al){
- return MipUnknown;
- }
- virtual Solution extractMIP() const throw (RationalFromDoubleException){
- return Solution();
- }
+ MipResult solveMIP(bool al) override { return MipUnknown; }
+ Solution extractMIP() const override { return Solution(); }
- virtual void setOptCoeffs(const ArithRatPairVec& ref){}
- virtual std::vector<const CutInfo*> getValidCuts(const std::set<const NodeLog*>& nodes){
- return std::vector<const CutInfo*>();
- }
+ void setOptCoeffs(const ArithRatPairVec& ref) override {}
- virtual void tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException){}
+ void tryCut(int nid, CutInfo& cut) override {}
- virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) throw(RationalFromDoubleException){
+ std::vector<const CutInfo*> getValidCuts(const NodeLog& node) override
+ {
return std::vector<const CutInfo*>();
}
- virtual ArithVar getBranchVar(const NodeLog& nl) const{
+ ArithVar getBranchVar(const NodeLog& nl) const override
+ {
return ARITHVAR_SENTINEL;
}
- virtual double sumInfeasibilities(bool mip) const{
- return 0.0;
- }
+ double sumInfeasibilities(bool mip) const override { return 0.0; }
};
}/* CVC4::theory::arith namespace */
ApproxGLPK(const ArithVariables& v, TreeLog& l, ApproximateStatistics& s);
~ApproxGLPK();
- virtual LinResult solveRelaxation();
- virtual Solution extractRelaxation() const throw (RationalFromDoubleException){
- return extractSolution(false);
- }
+ LinResult solveRelaxation();
+ Solution extractRelaxation() const override { return extractSolution(false); }
- virtual ArithRatPairVec heuristicOptCoeffs() const;
+ ArithRatPairVec heuristicOptCoeffs() const override;
- virtual MipResult solveMIP(bool al);
- virtual Solution extractMIP() const throw (RationalFromDoubleException){
- return extractSolution(true);
- }
- virtual void setOptCoeffs(const ArithRatPairVec& ref);
- //void getValidCuts(const NodeLog& con, std::vector<const CutInfo*>& out);
- virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& nodes) throw (RationalFromDoubleException);
- //virtual std::vector<const NodeLog*> getBranches();
-
- //Node downBranchLiteral(const NodeLog& con) const;
+ MipResult solveMIP(bool al) override;
+ Solution extractMIP() const override { return extractSolution(true); }
+ void setOptCoeffs(const ArithRatPairVec& ref) override;
+ std::vector<const CutInfo*> getValidCuts(const NodeLog& nodes) override;
ArithVar getBranchVar(const NodeLog& con) const;
static void printGLPKStatus(int status, std::ostream& out);
private:
- Solution extractSolution(bool mip) const throw (RationalFromDoubleException);
- int guessDir(ArithVar v) const;
+ Solution extractSolution(bool mip) const;
+ int guessDir(ArithVar v) const;
- // get this stuff out of here
- void tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException);
+ // get this stuff out of here
+ void tryCut(int nid, CutInfo& cut) override;
- ArithVar _getArithVar(int nid, int M, int ind) const;
- ArithVar getArithVarFromRow(int nid, int ind) const {
- if(ind >= 0){
- const NodeLog& nl = d_log.getNode(nid);
- return nl.lookupRowId(ind);
- }
- return ARITHVAR_SENTINEL;
+ ArithVar _getArithVar(int nid, int M, int ind) const;
+ ArithVar getArithVarFromRow(int nid, int ind) const
+ {
+ if (ind >= 0)
+ {
+ const NodeLog& nl = d_log.getNode(nid);
+ return nl.lookupRowId(ind);
+ }
+ return ARITHVAR_SENTINEL;
}
// virtual void mapRowId(int nid, int ind, ArithVar v){
}
-
-ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const throw (RationalFromDoubleException){
+ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
+{
Assert(d_solvedRelaxation);
Assert(!mip || d_solvedMIP);
// Message() << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
}
- DeltaRational proposal = estimateWithCFE(newAssign);
-
+ DeltaRational proposal;
+ if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign))
+ {
+ proposal = maybe_new.value();
+ }
+ else
+ {
+ // failed to estimate the old value. defaulting to the current.
+ proposal = d_vars.getAssignment(vi);
+ }
if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
// Message() << " to prev value" << newAssign << " " << oldAssign << endl;
}
}
-std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const NodeLog& con) throw (RationalFromDoubleException){
+std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const NodeLog& con)
+{
std::vector<const CutInfo*> proven;
int nid = con.getNodeId();
for(NodeLog::const_iterator j = con.begin(), jend=con.end(); j!=jend; ++j){
return proven;
}
-// std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const std::set<const NodeLog*>& nodes){
-// // assume selected has been applied
-// std::vector<const CutInfo*> proven;
-// std::set<const NodeLog*>::const_iterator i, iend;
-// for(i = nodes.begin(), iend=nodes.end(); i!=iend; ++i){
-// const NodeLog* nl = *i;
-// getValidCuts(*nl, proven);
-// }
-
-// return proven;
-// }
-
ArithVar ApproxGLPK::getBranchVar(const NodeLog& con) const{
int br_var = con.branchVariable();
return getArithVarFromStructural(br_var);
}
-// Node ApproxGLPK::downBranchLiteral(const NodeLog& con) const{
-// int br_var = con.branchVariable();
-// ArithVar v = getArithVarFromStructural(br_var);
-// if(v != ARITHVAR_SENTINEL){
-// if(d_vars.isIntegerInput(v) && d_vars.hasNode(v)){
-// Node var = d_vars.asNode(v);
-// double br_val = con.branchValue();
-// Rational val = estimateWithCFE(br_val);
-// if(!val.isIntegral()){
-// NodeManager* nm = NodeManager::currentNM();
-// Node ineq = nm->mkNode(kind::LEQ, var, mkRationalNode(val));
-// return Rewriter::rewrite(ineq);
-// }
-// }
-// }
-// return Node::null();
-// }
-
-// std::vector<const NodeLog*> ApproxGLPK::getBranches(){
-// std::vector<const NodeLog*> branches;
-// for(TreeLog::const_iterator i = d_log.begin(), iend=d_log.end(); i!=iend;++i){
-// const NodeLog& con = (*i).second;
-// if(con.isBranch()){
-// branches.push_back(&con);
-// }
-// }
-// return branches;
-// }
MipResult ApproxGLPK::solveMIP(bool activelyLog){
Assert(d_solvedRelaxation);
d_pad.d_cut.lhs.set(x, Rational(1));
Rational& rhs = d_pad.d_cut.rhs;
- rhs = estimateWithCFE(Rational::fromDouble(br_cut.getRhs()), Integer(1));
+ Maybe<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
+ if (!br_cut_rhs)
+ {
+ return true;
+ }
+
+ rhs = estimateWithCFE(br_cut_rhs.value(), 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;
- Rational delta = estimateWithCFE(mir.delta);
- d_pad.d_failure = (delta.sgn() <= 0);
+ Maybe<Rational> delta = estimateWithCFE(mir.delta);
+ if (!delta)
+ {
+ return true;
+ }
+
+ d_pad.d_failure = (delta.value().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;
+ Rational next = curr / delta.value();
if(compRanges.isKey(v)){
b -= curr * compRanges[v];
alpha.set(v, - next);
alpha.set(v, next);
}
}
- b = b / delta;
+ b = b / delta.value();
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; }
- Rational c = estimateWithCFE(coeff);
- if(lhs.isKey(x)){
- lhs.get(x) -= c;
- }else{
- lhs.set(x, -c);
+ Maybe<Rational> c = estimateWithCFE(coeff);
+ if (!c)
+ {
+ return true;
+ }
+
+ if (lhs.isKey(x))
+ {
+ lhs.get(x) -= c.value();
+ }
+ else
+ {
+ lhs.set(x, -c.value());
}
}
double coeff = row_sum.coeffs[i];
ArithVar x = _getArithVar(nid, M, aux_ind);
Assert(x != ARITHVAR_SENTINEL);
- Rational c = estimateWithCFE(coeff);
+ Maybe<Rational> c = estimateWithCFE(coeff);
+ if (!c)
+ {
+ return true;
+ }
Assert(!lhs.isKey(x));
- lhs.set(x, c);
+ lhs.set(x, c.value());
}
if(Debug.isOn("approx::mir")){
}
Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("<<d_vars.asNode(var)<<")"<<endl;
- Rational cfe = estimateWithCFE(coeff, D);
- tab.set(var, cfe);
+ Maybe<Rational> cfe = estimateWithCFE(coeff, D);
+ if (!cfe)
+ {
+ return true;
+ }
+ tab.set(var, cfe.value());
Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl;
}
if(!guessIsConstructable(tab)){
return false;
}
-void ApproxGLPK::tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException){
+void ApproxGLPK::tryCut(int nid, CutInfo& cut)
+{
Assert(!cut.reconstructed());
Assert(cut.getKlass() != RowsDeletedKlass);
bool failure = false;
#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_registry.h"
std::ostream& operator<<(std::ostream& out, MipResult res);
class ApproximateStatistics {
-public:
- // IntStat d_relaxCalls;
- // IntStat d_relaxUnknowns;
- // IntStat d_relaxFeasible;
- // IntStat d_relaxInfeasible;
- // IntStat d_relaxPivotsExhausted;
-
- // IntStat d_mipCalls;
- // IntStat d_mipUnknowns;
- // IntStat d_mipBingo;
- // IntStat d_mipClosed;
- // IntStat d_mipBranchesExhausted;
- // IntStat d_mipPivotsExhausted;
- // IntStat d_mipExecExhausted;
-
-
- // IntStat d_gmiGen;
- // IntStat d_gmiReplay;
- // IntStat d_mipGen;
- // IntStat d_mipReplay;
+ public:
+ ApproximateStatistics();
+ ~ApproximateStatistics();
IntStat d_branchMaxDepth;
IntStat d_branchesMaxOnAVar;
TimerStat d_gaussianElimConstructTime;
IntStat d_gaussianElimConstruct;
AverageStat d_averageGuesses;
-
- ApproximateStatistics();
- ~ApproximateStatistics();
};
class RowsDeleted;
class ApproximateSimplex{
-protected:
- const ArithVariables& d_vars;
- TreeLog& d_log;
- ApproximateStatistics& d_stats;
-
- int d_pivotLimit;
- /* the maximum pivots allowed in a query. */
-
- int d_branchLimit;
- /* maximum branches allowed on a variable */
-
- int d_maxDepth;
- /* maxmimum branching depth allowed.*/
-
- static Integer s_defaultMaxDenom;
- /* Default denominator for diophatine approximation.
- * 2^{26}*/
-
-public:
-
+ public:
static bool enabled();
/**
void setBranchingDepth(int bd);
/** A result is either sat, unsat or unknown.*/
- //enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat};
struct Solution {
DenseSet newBasis;
DenseMap<DeltaRational> newValues;
};
virtual ArithVar getBranchVar(const NodeLog& nl) const = 0;
- //virtual void mapRowId(int nid, int ind, ArithVar v) = 0;
- //virtual void applyRowsDeleted(int nid, const RowsDeleted& rd) = 0;
/** Sets a maximization criteria for the approximate solver.*/
virtual void setOptCoeffs(const ArithRatPairVec& ref) = 0;
virtual ArithRatPairVec heuristicOptCoeffs() const = 0;
virtual LinResult solveRelaxation() = 0;
- virtual Solution extractRelaxation() const throw(RationalFromDoubleException) = 0;
+ virtual Solution extractRelaxation() const = 0;
virtual MipResult solveMIP(bool activelyLog) = 0;
- virtual Solution extractMIP() const throw(RationalFromDoubleException) = 0;
- virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) throw(RationalFromDoubleException) = 0;
- //virtual std::vector<const NodeLog*> getBranches() = 0;
+ virtual Solution extractMIP() const = 0;
- //virtual Node downBranchLiteral(const NodeLog& con) const = 0;
+ virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) = 0;
- virtual void tryCut(int nid, CutInfo& cut) throw(RationalFromDoubleException) = 0;
+ virtual void tryCut(int nid, CutInfo& cut) = 0;
/** UTILITIES FOR DEALING WITH ESTIMATES */
* cuts off the estimate once the value is approximately zero.
* This is designed for removing rounding artifacts.
*/
- static Rational estimateWithCFE(double d) throw(RationalFromDoubleException);
- static Rational estimateWithCFE(double d, const Integer& D) throw(RationalFromDoubleException);
+ static Maybe<Rational> estimateWithCFE(double d);
+ static Maybe<Rational> estimateWithCFE(double d, const Integer& D);
/**
* Converts a rational to a continued fraction expansion representation
static Rational cfeToRational(const std::vector<Integer>& exp);
/** Estimates a rational as a continued fraction expansion.*/
- //static Rational estimateWithCFE(const Rational& q, int depth);
static Rational estimateWithCFE(const Rational& q, const Integer& K);
virtual double sumInfeasibilities(bool mip) const = 0;
+
+ protected:
+ const ArithVariables& d_vars;
+ TreeLog& d_log;
+ ApproximateStatistics& d_stats;
+
+ /* the maximum pivots allowed in a query. */
+ int d_pivotLimit;
+
+ /* maximum branches allowed on a variable */
+ int d_branchLimit;
+
+ /* maxmimum branching depth allowed.*/
+ int d_maxDepth;
+
+ /* Default denominator for diophatine approximation, 2^{26} .*/
+ static Integer s_defaultMaxDenom;
};/* class ApproximateSimplex */
Assert(nbSgn != 0);
if(nbSgn > 0){
- if(d_upperBoundDifference.nothing() || nbDiff <= d_upperBoundDifference){
+ if (d_upperBoundDifference.nothing()
+ || nbDiff <= d_upperBoundDifference.value())
+ {
return false;
}
}else{
- if(d_lowerBoundDifference.nothing() || nbDiff >= d_lowerBoundDifference){
+ if (d_lowerBoundDifference.nothing()
+ || nbDiff >= d_lowerBoundDifference.value())
+ {
return false;
}
}
if(d_variables.hasUpperBound(nb)){
ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
- Border border(ub, d_upperBoundDifference, false, NULL, true);
+ Border border(ub, d_upperBoundDifference.value(), 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, false, NULL, false);
+ Border border(lb, d_lowerBoundDifference.value(), false, NULL, false);
Debug("handleBorders") << "push back decreasing " << border << endl;
d_decreasing.push_back(border);
}
** \todo document this file
**/
+#include "theory/arith/pseudoboolean_proc.h"
+
#include "base/output.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
-#include "theory/arith/pseudoboolean_proc.h"
#include "theory/rewriter.h"
namespace CVC4 {
Polynomial p = Polynomial::parsePolynomial(l);
clear();
- if(negated){
+ if (negated)
+ {
// (not (>= p r))
// (< p r)
// (> (-p) (-r))
// (>= (-p) (-r +1))
d_off = (-r.getConst<Rational>());
- if(d_off.constValue().isIntegral()){
- d_off = d_off.constValue() + Rational(1) ;
- }else{
- d_off = Rational(d_off.constValue().ceiling());
+ if (d_off.value().isIntegral())
+ {
+ d_off = d_off.value() + Rational(1);
}
- }else{
+ else
+ {
+ d_off = Rational(d_off.value().ceiling());
+ }
+ }
+ else
+ {
// (>= p r)
d_off = r.getConst<Rational>();
- d_off = Rational(d_off.constValue().ceiling());
+ d_off = Rational(d_off.value().ceiling());
}
- Assert(d_off.constValue().isIntegral());
+ Assert(d_off.value().isIntegral());
int adj = negated ? -1 : 1;
for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){
Debug("pbs::rewrites") << "failed " << std::endl;
return;
}
- Assert(d_off.constValue().isIntegral());
- Integer off = d_off.constValue().ceiling();
+ Assert(d_off.value().isIntegral());
+ Integer off = d_off.value().ceiling();
// \sum pos >= \sum neg + off
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
* d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
*/
bool debugSgnAgreement() const {
- int deltaSgn = d_nonbasicDelta.constValue().sgn();
+ int deltaSgn = d_nonbasicDelta.value().sgn();
return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
}
inline int nonbasicDirection() const{ return d_nonbasicDirection; }
/** Requires errorsChange to be set through setErrorsChange or updateProposal. */
- inline int errorsChange() const { return d_errorsChange; }
+ inline int errorsChange() const { return d_errorsChange.value(); }
/**
* If errorsChange has been set, return errorsChange().
* Otherwise, return def.
*/
inline int errorsChangeSafe(int def) const {
- if(d_errorsChange.just()){
- return d_errorsChange;
- }else{
+ if (d_errorsChange)
+ {
+ return d_errorsChange.value();
+ }
+ else
+ {
return def;
}
}
/** Requires errorsChange to be set through setErrorsChange or updateProposal. */
- inline int focusDirection() const{ return d_focusDirection; }
+ inline int focusDirection() const { return d_focusDirection.value(); }
/** Sets the focusDirection. */
void setFocusDirection(int fd){
* The burden for this being safe is on the user!
*/
void determineFocusDirection(){
- int deltaSgn = d_nonbasicDelta.constValue().sgn();
+ const int deltaSgn = d_nonbasicDelta.value().sgn();
setFocusDirection(deltaSgn * d_nonbasicDirection);
}
/** Requires nonbasicDelta to be set through updateProposal(...). */
- const DeltaRational& nonbasicDelta() const {
- return d_nonbasicDelta;
- }
+ const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
const Rational& getCoefficient() const {
Assert(describesPivot());
- Assert(d_tableauCoefficient.constValue() != NULL);
- return *(d_tableauCoefficient.constValue());
+ Assert(d_tableauCoefficient.value() != NULL);
+ return *(d_tableauCoefficient.value());
}
int basicDirection() const {
return nonbasicDirection() * (getCoefficient().sgn());
}
}
- const DeltaRational& focusChange() const {
- return d_focusChange;
- }
+ const DeltaRational& focusChange() const { return d_focusChange.value(); }
void setFocusChange(const DeltaRational& fc) {
d_focusChange = fc;
}
WitnessImprovement computeWitness() const {
if(d_foundConflict){
return ConflictFound;
- }else if(d_errorsChange.just() && d_errorsChange < 0){
+ }
+ else if (d_errorsChange.just() && d_errorsChange.value() < 0)
+ {
return ErrorDropped;
- }else if(d_errorsChange.nothing() || d_errorsChange == 0){
+ }
+ else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
+ {
if(d_focusDirection.just()){
- if(d_focusDirection > 0){
+ if (d_focusDirection.value() > 0)
+ {
return FocusImproved;
- }else if(d_focusDirection == 0){
+ }
+ else if (d_focusDirection.value() == 0)
+ {
return Degenerate;
}
}
d_replayedLemmas = false;
- std::vector<ConstraintCPVec> res;
- try{
- /* use the try block for the purpose of pushing the sat context */
- context::Context::ScopedPush speculativePush(getSatContext());
- d_cmEnabled = false;
- res = replayLogRec(approx, tl.getRootId(), NullConstraint, 1);
- }catch(RationalFromDoubleException& rfde){
- turnOffApproxFor(options::replayNumericFailurePenalty());
- }
-
+ /* use the try block for the purpose of pushing the sat context */
+ context::Context::ScopedPush speculativePush(getSatContext());
+ d_cmEnabled = false;
+ std::vector<ConstraintCPVec> res =
+ replayLogRec(approx, tl.getRootId(), NullConstraint, 1);
-
if(res.empty()){
++d_statistics.d_replayAttemptFailed;
}else{
return make_pair(newc, added);
}
-std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException){
+std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(
+ ApproximateSimplex* approx, const NodeLog& nl)
+{
Assert(nl.isBranch());
Assert(d_lhsTmp.empty());
if(d_partialModel.hasNode(v)){
d_lhsTmp.set(v, Rational(1));
double dval = nl.branchValue();
- Rational val = ApproximateSimplex::estimateWithCFE(dval);
- Rational fl(val.floor());
+ Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+ if (!maybe_value)
+ {
+ return make_pair(NullConstraint, ARITHVAR_SENTINEL);
+ }
+ Rational fl(maybe_value.value().floor());
pair<ConstraintP, ArithVar> p;
p = replayGetConstraint(d_lhsTmp, kind::LEQ, fl, true);
d_lhsTmp.purge();
return *d_approxStats;
}
-Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx, const NodeLog& bn) const throw(RationalFromDoubleException) {
+Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
+ const NodeLog& bn) const
+{
Assert(bn.isBranch());
ArithVar v = approx->getBranchVar(bn);
if(v != ARITHVAR_SENTINEL && d_partialModel.isIntegerInput(v)){
if(d_partialModel.hasNode(v)){
Node n = d_partialModel.asNode(v);
double dval = bn.branchValue();
- Rational val = ApproximateSimplex::estimateWithCFE(dval);
- Rational fl(val.floor());
+ Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+ if (!maybe_value)
+ {
+ return Node::null();
+ }
+ Rational fl(maybe_value.value().floor());
NodeManager* nm = NodeManager::currentNM();
Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl));
Node norm = Rewriter::rewrite(leq);
}
bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
- try{
++(d_statistics.d_mipReplayLemmaCalls);
bool anythingnew = false;
}
}
return anythingnew;
- }catch(RationalFromDoubleException& rfde){
- turnOffApproxFor(options::replayNumericFailurePenalty());
- return false;
- }
}
void TheoryArithPrivate::turnOffApproxFor(int32_t rounds){
ApproximateSimplex* approx =
ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, tl, stats);
- try{
approx->setPivotLimit(mipLimit);
if(!d_guessedCoeffSet){
d_guessedCoeffs = approx->heuristicOptCoeffs();
break;
}
}
- }catch(RationalFromDoubleException& rfde){
- turnOffApproxFor(options::replayNumericFailurePenalty());
- }
delete approx;
if(!Theory::fullEffort(effortLevel)){
TimerStat::CodeTimer codeTimer(d_statistics.d_lpTimer);
relaxRes = approxSolver->solveRelaxation();
}
- try{
Debug("solveRealRelaxation") << "solve relaxation? " << endl;
switch(relaxRes){
case LinFeasible:
++d_statistics.d_relaxOthers;
break;
}
- }catch(RationalFromDoubleException& rfde){
- turnOffApproxFor(options::replayNumericFailurePenalty());
- }
delete approxSolver;
}
enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
ResultState finalState = Unset;
- int maxRounds = param.getSimplexRounds().just()
- ? param.getSimplexRounds().constValue()
- : -1;
+ const int maxRounds =
+ param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1;
Maybe<DeltaRational> threshold;
// TODO: get this from the parameters
}
if(threshold.just()){
- if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){
+ if (d_partialModel.getAssignment(optVar) >= threshold.value())
+ {
finalState = ReachedThreshold;
break;
}
void subsumption(std::vector<ConstraintCPVec>& confs) const;
Node cutToLiteral(ApproximateSimplex* approx, const CutInfo& cut) const;
- Node branchToNode(ApproximateSimplex* approx, const NodeLog& cut) const throw(RationalFromDoubleException);
-
+ Node branchToNode(ApproximateSimplex* approx, const NodeLog& cut) const;
void propagateCandidates();
void propagateCandidate(ArithVar basic);
std::vector<ConstraintCPVec> replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth);
std::pair<ConstraintP, ArithVar> replayGetConstraint(const CutInfo& info);
- std::pair<ConstraintP, ArithVar> replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException);
+ std::pair<ConstraintP, ArithVar> replayGetConstraint(
+ ApproximateSimplex* approx, const NodeLog& nl);
std::pair<ConstraintP, ArithVar> replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch);
void replayAssert(ConstraintP c);
** Nothing using a value of T
** - High level of assurance that a value is not used before it is set.
**/
-#include "cvc4_private.h"
+#include "cvc4_public.h"
-#pragma once
+#ifndef __CVC4__UTIL__MAYBE_H
+#define __CVC4__UTIL__MAYBE_H
#include <ostream>
namespace CVC4 {
template <class T>
-class Maybe {
-private:
- bool d_just;
- T d_value;
-
-public:
+class CVC4_PUBLIC Maybe
+{
+ public:
Maybe() : d_just(false), d_value(){}
Maybe(const T& val): d_just(true), d_value(val){}
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()){
}
}
- T& value() {
- Assert(just(), "Maybe::value() requires the maybe to be set.");
- return d_value;
- }
- const T& constValue() const {
- Assert(just(), "Maybe::constValue() requires the maybe to be set.");
+ const T& value() const
+ {
+ if (nothing())
+ {
+ throw Exception("Maybe::value() requires the maybe to be set.");
+ }
return d_value;
}
- operator const T&() const { return constValue(); }
+ private:
+ bool d_just;
+ T d_value;
};
template <class T>
out << "Nothing";
}else{
out << "Just ";
- out << m.constValue();
+ out << m.value();
}
out << "}";
return out;
}
}/* CVC4 namespace */
+
+#endif /* __CVC4__UTIL__MAYBE_H */
#include "util/rational.h"
%}
-%ignore CVC4::RationalFromDoubleException::RationalFromDoubleException(double);
-
%ignore CVC4::Rational::Rational(int);
%ignore CVC4::Rational::Rational(unsigned int);
%ignore CVC4::Rational::Rational(int, int);
}
}
-Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){
+Maybe<Rational> Rational::fromDouble(double d)
+{
try{
cln::cl_DF fromD = d;
Rational q;
q.d_value = cln::rationalize(fromD);
return q;
}catch(cln::floating_point_underflow_exception& fpue){
- throw RationalFromDoubleException(d);
+ return Maybe<Rational>();
}catch(cln::floating_point_nan_exception& fpne){
- throw RationalFromDoubleException(d);
+ return Maybe<Rational>();
}catch(cln::floating_point_overflow_exception& fpoe){
- throw RationalFromDoubleException(d);
+ return Maybe<Rational>();
}
-}
-
-RationalFromDoubleException::RationalFromDoubleException(double d) throw()
- : Exception()
-{
- std::stringstream ss;
- ss << "RationalFromDoubleException(";
- ss << d;
- ss << ")";
- setMessage(ss.str());
+ Unreachable();
}
} /* namespace CVC4 */
#include "base/exception.h"
#include "util/integer.h"
+#include "util/maybe.h"
namespace CVC4 {
-class CVC4_PUBLIC RationalFromDoubleException : public Exception {
-public:
- RationalFromDoubleException(double d) throw();
-};
-
/**
** A multi-precision rational constant.
** This stores the rational as a pair of multi-precision integers,
}
/** Return an exact rational for a double d. */
- static Rational fromDouble(double d) throw(RationalFromDoubleException);
+ static Maybe<Rational> fromDouble(double d);
/**
* Get a double representation of this Rational, which is
/** Return an exact rational for a double d. */
-Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){
+Maybe<Rational> Rational::fromDouble(double d)
+{
using namespace std;
if(isfinite(d)){
Rational q;
mpq_set_d(q.d_value.get_mpq_t(), d);
return q;
}
-
- throw RationalFromDoubleException(d);
-}
-
-RationalFromDoubleException::RationalFromDoubleException(double d) throw()
- : Exception()
-{
- std::stringstream ss;
- ss << "RationalFromDoubleException(";
- ss << d;
- ss << ")";
- setMessage(ss.str());
+ return Maybe<Rational>();
}
} /* namespace CVC4 */
#include "base/exception.h"
#include "util/integer.h"
+#include "util/maybe.h"
namespace CVC4 {
-class CVC4_PUBLIC RationalFromDoubleException : public Exception {
-public:
- RationalFromDoubleException(double d) throw();
-};
-
/**
** A multi-precision rational constant.
** This stores the rational as a pair of multi-precision integers,
return Integer(d_value.get_den());
}
- static Rational fromDouble(double d) throw(RationalFromDoubleException);
+ static Maybe<Rational> fromDouble(double d);
/**
* Get a double representation of this Rational, which is
projects / cvc5.git / commitdiff