From 20957db27201d594a83e0e5abe77875ed4932faf Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 7 Jan 2018 16:46:16 -0800 Subject: [PATCH] =?utf8?q?Removes=20RationalFromDoubleException.=20Replace?= =?utf8?q?s=20this=20with=20an=20explicit=20M=E2=80=A6=20(#1476)?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit * Removes RationalFromDoubleException. Replaces this with an explicit Maybe datatype. Makes Maybe CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex. --- src/cvc4.i | 2 - src/theory/arith/approx_simplex.cpp | 275 ++++++++-------------- src/theory/arith/approx_simplex.h | 83 +++---- src/theory/arith/linear_equality.cpp | 12 +- src/theory/arith/pseudoboolean_proc.cpp | 30 ++- src/theory/arith/simplex_update.h | 44 ++-- src/theory/arith/theory_arith_private.cpp | 61 +++-- src/theory/arith/theory_arith_private.h | 6 +- src/util/maybe.h | 35 +-- src/util/rational.i | 2 - src/util/rational_cln_imp.cpp | 20 +- src/util/rational_cln_imp.h | 8 +- src/util/rational_gmp_imp.cpp | 16 +- src/util/rational_gmp_imp.h | 8 +- 14 files changed, 241 insertions(+), 361 deletions(-) diff --git a/src/cvc4.i b/src/cvc4.i index 2f7205b19..bc5f5fdfe 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -174,8 +174,6 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %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" diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 78b57d3f6..07cb6aca6 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -144,55 +144,15 @@ struct CutScratchPad { 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); @@ -202,29 +162,7 @@ ApproximateStatistics::ApproximateStatistics() } 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); @@ -373,11 +311,17 @@ Rational ApproximateSimplex::estimateWithCFE(const Rational& r, const Integer& K } } -Rational ApproximateSimplex::estimateWithCFE(double d, const Integer& D) throw (RationalFromDoubleException){ - return estimateWithCFE(Rational::fromDouble(d), D); +Maybe ApproximateSimplex::estimateWithCFE(double d, const Integer& D) +{ + if (Maybe from_double = Rational::fromDouble(d)) + { + return estimateWithCFE(from_double.value(), D); + } + return Maybe(); } -Rational ApproximateSimplex::estimateWithCFE(double d) throw (RationalFromDoubleException){ +Maybe ApproximateSimplex::estimateWithCFE(double d) +{ return estimateWithCFE(d, s_defaultMaxDenom); } @@ -388,42 +332,32 @@ public: {} ~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 getValidCuts(const std::set& nodes){ - return std::vector(); - } + 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 getValidCuts(const NodeLog& node) throw(RationalFromDoubleException){ + std::vector getValidCuts(const NodeLog& node) override + { return std::vector(); } - 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 */ @@ -483,42 +417,36 @@ public: 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& out); - virtual std::vector getValidCuts(const NodeLog& nodes) throw (RationalFromDoubleException); - //virtual std::vector 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 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){ @@ -1063,8 +991,8 @@ ApproxGLPK::~ApproxGLPK(){ } - -ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const throw (RationalFromDoubleException){ +ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const +{ Assert(d_solvedRelaxation); Assert(!mip || d_solvedMIP); @@ -1150,8 +1078,16 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const throw ( // Message() << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl; } - DeltaRational proposal = estimateWithCFE(newAssign); - + DeltaRational proposal; + if (Maybe 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; @@ -1705,7 +1641,8 @@ static void glpkCallback(glp_tree *tree, void *info){ } } -std::vector ApproxGLPK::getValidCuts(const NodeLog& con) throw (RationalFromDoubleException){ +std::vector ApproxGLPK::getValidCuts(const NodeLog& con) +{ std::vector proven; int nid = con.getNodeId(); for(NodeLog::const_iterator j = con.begin(), jend=con.end(); j!=jend; ++j){ @@ -1725,51 +1662,11 @@ std::vector ApproxGLPK::getValidCuts(const NodeLog& con) throw ( return proven; } -// std::vector ApproxGLPK::getValidCuts(const std::set& nodes){ -// // assume selected has been applied -// std::vector proven; -// std::set::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 ApproxGLPK::getBranches(){ -// std::vector 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); @@ -2124,7 +2021,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; - rhs = estimateWithCFE(Rational::fromDouble(br_cut.getRhs()), Integer(1)); + Maybe 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; } @@ -2175,8 +2078,13 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){ DenseMap& 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 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; @@ -2186,7 +2094,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; + Rational next = curr / delta.value(); if(compRanges.isKey(v)){ b -= curr * compRanges[v]; alpha.set(v, - next); @@ -2194,7 +2102,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){ 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); @@ -2612,11 +2520,19 @@ 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; } - Rational c = estimateWithCFE(coeff); - if(lhs.isKey(x)){ - lhs.get(x) -= c; - }else{ - lhs.set(x, -c); + Maybe c = estimateWithCFE(coeff); + if (!c) + { + return true; + } + + if (lhs.isKey(x)) + { + lhs.get(x) -= c.value(); + } + else + { + lhs.set(x, -c.value()); } } @@ -2636,9 +2552,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); - Rational c = estimateWithCFE(coeff); + Maybe 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")){ @@ -3070,8 +2990,12 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit } Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("< cfe = estimateWithCFE(coeff, D); + if (!cfe) + { + return true; + } + tab.set(var, cfe.value()); Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl; } if(!guessIsConstructable(tab)){ @@ -3173,7 +3097,8 @@ bool ApproxGLPK::constructGmiCut(){ 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; diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 234fd10c0..eb95190bf 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -24,6 +24,7 @@ #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" @@ -49,26 +50,9 @@ enum MipResult { 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; @@ -76,9 +60,6 @@ public: TimerStat d_gaussianElimConstructTime; IntStat d_gaussianElimConstruct; AverageStat d_averageGuesses; - - ApproximateStatistics(); - ~ApproximateStatistics(); }; @@ -89,26 +70,7 @@ class CutInfo; 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(); /** @@ -129,7 +91,6 @@ public: void setBranchingDepth(int bd); /** A result is either sat, unsat or unknown.*/ - //enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat}; struct Solution { DenseSet newBasis; DenseMap newValues; @@ -137,8 +98,6 @@ public: }; 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; @@ -146,17 +105,15 @@ public: 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 getValidCuts(const NodeLog& node) throw(RationalFromDoubleException) = 0; - //virtual std::vector getBranches() = 0; + virtual Solution extractMIP() const = 0; - //virtual Node downBranchLiteral(const NodeLog& con) const = 0; + virtual std::vector 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 */ @@ -171,8 +128,8 @@ public: * 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 estimateWithCFE(double d); + static Maybe estimateWithCFE(double d, const Integer& D); /** * Converts a rational to a continued fraction expansion representation @@ -185,10 +142,26 @@ public: static Rational cfeToRational(const std::vector& 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 */ diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 9d414fcd7..c97ed9714 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -1074,11 +1074,15 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr 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; } } @@ -1162,14 +1166,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, 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); } diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp index 230cfb7ca..1cdb90e20 100644 --- a/src/theory/arith/pseudoboolean_proc.cpp +++ b/src/theory/arith/pseudoboolean_proc.cpp @@ -15,10 +15,11 @@ ** \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 { @@ -58,24 +59,30 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){ Polynomial p = Polynomial::parsePolynomial(l); clear(); - if(negated){ + if (negated) + { // (not (>= p r)) // (< p r) // (> (-p) (-r)) // (>= (-p) (-r +1)) d_off = (-r.getConst()); - 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(); - 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){ @@ -247,8 +254,8 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){ 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 @@ -323,4 +330,3 @@ void PseudoBooleanProcessor::clear() { }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 7b487c8a3..70c9a5998 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -145,7 +145,7 @@ private: * 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; } @@ -228,16 +228,19 @@ public: 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; } } @@ -250,7 +253,7 @@ public: /** 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){ @@ -265,18 +268,16 @@ public: * 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()); @@ -301,9 +302,7 @@ public: } } - const DeltaRational& focusChange() const { - return d_focusChange; - } + const DeltaRational& focusChange() const { return d_focusChange.value(); } void setFocusChange(const DeltaRational& fc) { d_focusChange = fc; } @@ -329,13 +328,20 @@ private: 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; } } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0e1dc62e1..f281bdfcc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2228,18 +2228,12 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){ d_replayedLemmas = false; - std::vector 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 res = + replayLogRec(approx, tl.getRootId(), NullConstraint, 1); - if(res.empty()){ ++d_statistics.d_replayAttemptFailed; }else{ @@ -2359,7 +2353,9 @@ std::pair TheoryArithPrivate::replayGetConstraint(const D return make_pair(newc, added); } -std::pair TheoryArithPrivate::replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException){ +std::pair TheoryArithPrivate::replayGetConstraint( + ApproximateSimplex* approx, const NodeLog& nl) +{ Assert(nl.isBranch()); Assert(d_lhsTmp.empty()); @@ -2368,8 +2364,12 @@ std::pair TheoryArithPrivate::replayGetConstraint(Approxi 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 maybe_value = ApproximateSimplex::estimateWithCFE(dval); + if (!maybe_value) + { + return make_pair(NullConstraint, ARITHVAR_SENTINEL); + } + Rational fl(maybe_value.value().floor()); pair p; p = replayGetConstraint(d_lhsTmp, kind::LEQ, fl, true); d_lhsTmp.purge(); @@ -2899,15 +2899,21 @@ ApproximateStatistics& TheoryArithPrivate::getApproxStats(){ 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 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); @@ -2935,7 +2941,6 @@ Node TheoryArithPrivate::cutToLiteral(ApproximateSimplex* approx, const CutInfo& } bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){ - try{ ++(d_statistics.d_mipReplayLemmaCalls); bool anythingnew = false; @@ -2981,10 +2986,6 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){ } } return anythingnew; - }catch(RationalFromDoubleException& rfde){ - turnOffApproxFor(options::replayNumericFailurePenalty()); - return false; - } } void TheoryArithPrivate::turnOffApproxFor(int32_t rounds){ @@ -3047,7 +3048,6 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ ApproximateSimplex* approx = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, tl, stats); - try{ approx->setPivotLimit(mipLimit); if(!d_guessedCoeffSet){ d_guessedCoeffs = approx->heuristicOptCoeffs(); @@ -3143,9 +3143,6 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ break; } } - }catch(RationalFromDoubleException& rfde){ - turnOffApproxFor(options::replayNumericFailurePenalty()); - } delete approx; if(!Theory::fullEffort(effortLevel)){ @@ -3295,7 +3292,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ TimerStat::CodeTimer codeTimer(d_statistics.d_lpTimer); relaxRes = approxSolver->solveRelaxation(); } - try{ Debug("solveRealRelaxation") << "solve relaxation? " << endl; switch(relaxRes){ case LinFeasible: @@ -3326,9 +3322,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ ++d_statistics.d_relaxOthers; break; } - }catch(RationalFromDoubleException& rfde){ - turnOffApproxFor(options::replayNumericFailurePenalty()); - } delete approxSolver; } @@ -5464,9 +5457,8 @@ std::pair TheoryArithPrivate::entailmentCheckSimplex(int sg 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 threshold; // TODO: get this from the parameters @@ -5592,7 +5584,8 @@ std::pair TheoryArithPrivate::entailmentCheckSimplex(int sg } if(threshold.just()){ - if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){ + if (d_partialModel.getAssignment(optVar) >= threshold.value()) + { finalState = ReachedThreshold; break; } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 08b884a03..ff60e8436 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -590,8 +590,7 @@ private: void subsumption(std::vector& 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); @@ -705,7 +704,8 @@ private: std::vector replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth); std::pair replayGetConstraint(const CutInfo& info); - std::pair replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException); + std::pair replayGetConstraint( + ApproximateSimplex* approx, const NodeLog& nl); std::pair replayGetConstraint(const DenseMap& lhs, Kind k, const Rational& rhs, bool branch); void replayAssert(ConstraintP c); diff --git a/src/util/maybe.h b/src/util/maybe.h index b2c8b9797..f27f320ae 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -22,9 +22,10 @@ ** 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 @@ -33,12 +34,9 @@ namespace CVC4 { template -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){} @@ -50,6 +48,7 @@ public: 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()){ @@ -58,16 +57,18 @@ public: } } - 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 @@ -77,10 +78,12 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe& m){ out << "Nothing"; }else{ out << "Just "; - out << m.constValue(); + out << m.value(); } out << "}"; return out; } }/* CVC4 namespace */ + +#endif /* __CVC4__UTIL__MAYBE_H */ diff --git a/src/util/rational.i b/src/util/rational.i index a9e3e23f8..a65c78327 100644 --- a/src/util/rational.i +++ b/src/util/rational.i @@ -2,8 +2,6 @@ #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); diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 09e3c8168..6250cbccd 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -84,29 +84,21 @@ int Rational::absCmp(const Rational& q) const{ } } -Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){ +Maybe 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(); }catch(cln::floating_point_nan_exception& fpne){ - throw RationalFromDoubleException(d); + return Maybe(); }catch(cln::floating_point_overflow_exception& fpoe){ - throw RationalFromDoubleException(d); + return Maybe(); } -} - -RationalFromDoubleException::RationalFromDoubleException(double d) throw() - : Exception() -{ - std::stringstream ss; - ss << "RationalFromDoubleException("; - ss << d; - ss << ")"; - setMessage(ss.str()); + Unreachable(); } } /* namespace CVC4 */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index bdfff9875..0b09bf1fd 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -35,14 +35,10 @@ #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, @@ -201,7 +197,7 @@ public: } /** Return an exact rational for a double d. */ - static Rational fromDouble(double d) throw(RationalFromDoubleException); + static Maybe 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 527222f7a..40c9c35f3 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -87,25 +87,15 @@ int Rational::absCmp(const Rational& q) const{ /** Return an exact rational for a double d. */ -Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){ +Maybe 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(); } } /* namespace CVC4 */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 70146561d..7c17ead15 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -32,14 +32,10 @@ #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, @@ -192,7 +188,7 @@ public: return Integer(d_value.get_den()); } - static Rational fromDouble(double d) throw(RationalFromDoubleException); + static Maybe fromDouble(double d); /** * Get a double representation of this Rational, which is -- 2.30.2