src/theory/arith/approx_simplex.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Morgan Deters
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * [[ Add one-line brief description here ]]
  14  *
  15  * [[ Add lengthier description here ]]
  16  * \todo document this file
  17  */
  18
  19 #include "cvc5_private.h"
  20
  21 #pragma once
  22
  23 #include <optional>
  24 #include <vector>
  25
  26 #include "theory/arith/arithvar.h"
  27 #include "theory/arith/delta_rational.h"
  28 #include "util/dense_map.h"
  29 #include "util/rational.h"
  30 #include "util/statistics_stats.h"
  31
  32 namespace cvc5 {
  33 namespace theory {
  34 namespace arith {
  35
  36 enum LinResult {
  37   LinUnknown,  /* Unknown error */
  38   LinFeasible, /* Relaxation is feasible */
  39   LinInfeasible,   /* Relaxation is infeasible/all integer branches closed */
  40   LinExhausted
  41 };
  42
  43 enum MipResult {
  44   MipUnknown,  /* Unknown error */
  45   MipBingo,    /* Integer feasible */
  46   MipClosed,   /* All integer branches closed */
  47   BranchesExhausted, /* Exhausted number of branches */
  48   PivotsExhauasted,  /* Exhausted number of pivots */
  49   ExecExhausted      /* Exhausted total operations */
  50 };
  51 std::ostream& operator<<(std::ostream& out, MipResult res);
  52
  53 class ApproximateStatistics {
  54  public:
  55   ApproximateStatistics();
  56
  57   IntStat d_branchMaxDepth;
  58   IntStat d_branchesMaxOnAVar;
  59
  60   TimerStat d_gaussianElimConstructTime;
  61   IntStat d_gaussianElimConstruct;
  62   AverageStat d_averageGuesses;
  63 };
  64
  65
  66 class NodeLog;
  67 class TreeLog;
  68 class ArithVariables;
  69 class CutInfo;
  70
  71 class ApproximateSimplex{
  72  public:
  73   static bool enabled();
  74
  75   /**
  76    * If glpk is enabled, return a subclass that can do something.
  77    * If glpk is disabled, return a subclass that does nothing.
  78    */
  79   static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s);
  80   ApproximateSimplex(const ArithVariables& v, TreeLog& l, ApproximateStatistics& s);
  81   virtual ~ApproximateSimplex(){}
  82
  83   /* the maximum pivots allowed in a query. */
  84   void setPivotLimit(int pl);
  85
  86   /* maximum branches allowed on a variable */
  87   void setBranchOnVariableLimit(int bl);
  88
  89   /* maximum branches allowed on a variable */
  90   void setBranchingDepth(int bd);
  91
  92   /** A result is either sat, unsat or unknown.*/
  93   struct Solution {
  94     DenseSet newBasis;
  95     DenseMap<DeltaRational> newValues;
  96     Solution() : newBasis(), newValues(){}
  97   };
  98
  99   virtual ArithVar getBranchVar(const NodeLog& nl) const = 0;
 100
 101   /** Sets a maximization criteria for the approximate solver.*/
 102   virtual void setOptCoeffs(const ArithRatPairVec& ref) = 0;
 103
 104   virtual ArithRatPairVec heuristicOptCoeffs() const = 0;
 105
 106   virtual LinResult solveRelaxation() = 0;
 107   virtual Solution extractRelaxation() const = 0;
 108
 109   virtual MipResult solveMIP(bool activelyLog) = 0;
 110
 111   virtual Solution extractMIP() const = 0;
 112
 113   virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) = 0;
 114
 115   virtual void tryCut(int nid, CutInfo& cut) = 0;
 116
 117   /** UTILITIES FOR DEALING WITH ESTIMATES */
 118
 119   static const double SMALL_FIXED_DELTA;
 120   static const double TOLERENCE;
 121
 122   /** Returns true if two doubles are roughly equal based on TOLERENCE and SMALL_FIXED_DELTA.*/
 123   static bool roughlyEqual(double a, double b);
 124
 125   /**
 126    * Estimates a double as a Rational using continued fraction expansion that
 127    * cuts off the estimate once the value is approximately zero.
 128    * This is designed for removing rounding artifacts.
 129    */
 130   static std::optional<Rational> estimateWithCFE(double d);
 131   static std::optional<Rational> estimateWithCFE(double d, const Integer& D);
 132
 133   /**
 134    * Converts a rational to a continued fraction expansion representation
 135    * using a maximum number of expansions equal to depth as long as the expression
 136    * is not roughlyEqual() to 0.
 137    */
 138   static std::vector<Integer> rationalToCfe(const Rational& q, int depth);
 139
 140   /** Converts a continued fraction expansion representation to a rational. */
 141   static Rational cfeToRational(const std::vector<Integer>& exp);
 142
 143   /** Estimates a rational as a continued fraction expansion.*/
 144   static Rational estimateWithCFE(const Rational& q, const Integer& K);
 145
 146   virtual double sumInfeasibilities(bool mip) const = 0;
 147
 148  protected:
 149   const ArithVariables& d_vars;
 150   TreeLog& d_log;
 151   ApproximateStatistics& d_stats;
 152
 153   /* the maximum pivots allowed in a query. */
 154   int d_pivotLimit;
 155
 156   /* maximum branches allowed on a variable */
 157   int d_branchLimit;
 158
 159   /* maxmimum branching depth allowed.*/
 160   int d_maxDepth;
 161
 162   /* Default denominator for diophatine approximation, 2^{26} .*/
 163   static Integer s_defaultMaxDenom;
 164 };/* class ApproximateSimplex */
 165
 166 }  // namespace arith
 167 }  // namespace theory
 168 }  // namespace cvc5