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 */