src/theory/arith/approx_simplex.h

   1
   2 #include "cvc4_private.h"
   3
   4 #pragma once
   5
   6 #include "util/statistics_registry.h"
   7 #include "theory/arith/arithvar.h"
   8 #include "theory/arith/linear_equality.h"
   9 #include "util/dense_map.h"
  10 #include <vector>
  11
  12 namespace CVC4 {
  13 namespace theory {
  14 namespace arith {
  15
  16
  17 class ApproximateSimplex{
  18 protected:
  19   int d_pivotLimit;
  20
  21 public:
  22
  23   static bool enabled();
  24
  25   /**
  26    * If glpk is enabled, return a subclass that can do something.
  27    * If glpk is disabled, return a sublass that does nothing.
  28    */
  29   static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars);
  30   ApproximateSimplex();
  31   virtual ~ApproximateSimplex(){}
  32
  33   /** A result is either sat, unsat or unknown.*/
  34   enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat};
  35   struct Solution {
  36     DenseSet newBasis;
  37     DenseMap<DeltaRational> newValues;
  38     Solution() : newBasis(), newValues(){}
  39   };
  40
  41   /** Sets a deterministic effort limit. */
  42   void setPivotLimit(int pivotLimit);
  43
  44   /** Sets a maximization criteria for the approximate solver.*/
  45   virtual void setOptCoeffs(const ArithRatPairVec& ref) = 0;
  46
  47   virtual ArithRatPairVec heuristicOptCoeffs() const = 0;
  48
  49   virtual ApproxResult solveRelaxation() = 0;
  50   virtual Solution extractRelaxation() const = 0;
  51
  52   virtual ApproxResult solveMIP() = 0;
  53   virtual Solution extractMIP() const = 0;
  54
  55   /** UTILIES FOR DEALING WITH ESTIMATES */
  56
  57   static const double SMALL_FIXED_DELTA;
  58   static const double TOLERENCE;
  59
  60   /** Returns true if two doubles are roughly equal based on TOLERENCE and SMALL_FIXED_DELTA.*/
  61   static bool roughlyEqual(double a, double b);
  62
  63   /**
  64    * Estimates a double as a Rational using continued fraction expansion that
  65    * cuts off the estimate once the value is approximately zero.
  66    * This is designed for removing rounding artifacts.
  67    */
  68   static Rational estimateWithCFE(double d);
  69
  70   /**
  71    * Converts a rational to a continued fraction expansion representation
  72    * using a maximum number of expansions equal to depth as long as the expression
  73    * is not roughlyEqual() to 0.
  74    */
  75   static std::vector<Integer> rationalToCfe(const Rational& q, int depth);
  76
  77   /** Converts a continued fraction expansion representation to a rational. */
  78   static Rational cfeToRational(const std::vector<Integer>& exp);
  79
  80   /** Estimates a rational as a continued fraction expansion.*/
  81   static Rational estimateWithCFE(const Rational& q, int depth);
  82 };/* class ApproximateSimplex */
  83
  84
  85 }/* CVC4::theory::arith namespace */
  86 }/* CVC4::theory namespace */
  87 }/* CVC4 namespace */