diff options
Diffstat (limited to 'src/theory/arith/approx_simplex.h')
-rw-r--r-- | src/theory/arith/approx_simplex.h | 118 |
1 files changed, 106 insertions, 12 deletions
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index b32fdef2d..15996fef8 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -22,7 +22,9 @@ #include "util/statistics_registry.h" #include "theory/arith/arithvar.h" -#include "theory/arith/linear_equality.h" +#include "util/rational.h" +#include "theory/arith/delta_rational.h" +//#include "theory/arith/linear_equality.h" #include "util/dense_map.h" #include <vector> @@ -30,10 +32,81 @@ namespace CVC4 { namespace theory { namespace arith { +enum LinResult { + LinUnknown, /* Unknown error */ + LinFeasible, /* Relaxation is feasible */ + LinInfeasible, /* Relaxation is infeasible/all integer branches closed */ + LinExhausted +}; + +enum MipResult { + MipUnknown, /* Unknown error */ + MipBingo, /* Integer feasible */ + MipClosed, /* All integer branches closed */ + BranchesExhausted, /* Exhausted number of branches */ + PivotsExhauasted, /* Exhausted number of pivots */ + ExecExhausted /* Exhausted total operations */ +}; +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; + + IntStat d_branchMaxDepth; + IntStat d_branchesMaxOnAVar; + + TimerStat d_gaussianElimConstructTime; + IntStat d_gaussianElimConstruct; + AverageStat d_averageGuesses; + + ApproximateStatistics(); + ~ApproximateStatistics(); +}; + + +class NodeLog; +class TreeLog; +class ArithVariables; +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: @@ -43,31 +116,48 @@ public: * If glpk is enabled, return a subclass that can do something. * If glpk is disabled, return a subclass that does nothing. */ - static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars); - ApproximateSimplex(); + static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s); + ApproximateSimplex(const ArithVariables& v, TreeLog& l, ApproximateStatistics& s); virtual ~ApproximateSimplex(){} + /* the maximum pivots allowed in a query. */ + void setPivotLimit(int pl); + + /* maximum branches allowed on a variable */ + void setBranchOnVariableLimit(int bl); + + /* maximum branches allowed on a variable */ + void setBranchingDepth(int bd); + /** A result is either sat, unsat or unknown.*/ - enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat}; + //enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat}; struct Solution { DenseSet newBasis; DenseMap<DeltaRational> newValues; Solution() : newBasis(), newValues(){} }; - /** Sets a deterministic effort limit. */ - void setPivotLimit(int pivotLimit); + 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 ApproxResult solveRelaxation() = 0; - virtual Solution extractRelaxation() const = 0; + virtual LinResult solveRelaxation() = 0; + virtual Solution extractRelaxation() const throw(RationalFromDoubleException) = 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 ApproxResult solveMIP() = 0; - virtual Solution extractMIP() const = 0; + //virtual Node downBranchLiteral(const NodeLog& con) const = 0; + + virtual void tryCut(int nid, CutInfo& cut) throw(RationalFromDoubleException) = 0; /** UTILITIES FOR DEALING WITH ESTIMATES */ @@ -82,7 +172,8 @@ public: * cuts off the estimate once the value is approximately zero. * This is designed for removing rounding artifacts. */ - static Rational estimateWithCFE(double d); + static Rational estimateWithCFE(double d) throw(RationalFromDoubleException); + static Rational estimateWithCFE(double d, const Integer& D) throw(RationalFromDoubleException); /** * Converts a rational to a continued fraction expansion representation @@ -95,7 +186,10 @@ public: 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, int depth); + static Rational estimateWithCFE(const Rational& q, const Integer& K); + + virtual double sumInfeasibilities(bool mip) const = 0; };/* class ApproximateSimplex */ |