GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/approx_simplex.h Lines: 0 3 0.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file approx_simplex.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
#include <vector>
22
23
#include "theory/arith/arithvar.h"
24
#include "theory/arith/delta_rational.h"
25
#include "util/dense_map.h"
26
#include "util/maybe.h"
27
#include "util/rational.h"
28
#include "util/statistics_registry.h"
29
#include "util/stats_timer.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
enum LinResult {
36
  LinUnknown,  /* Unknown error */
37
  LinFeasible, /* Relaxation is feasible */
38
  LinInfeasible,   /* Relaxation is infeasible/all integer branches closed */
39
  LinExhausted
40
};
41
42
enum MipResult {
43
  MipUnknown,  /* Unknown error */
44
  MipBingo,    /* Integer feasible */
45
  MipClosed,   /* All integer branches closed */
46
  BranchesExhausted, /* Exhausted number of branches */
47
  PivotsExhauasted,  /* Exhausted number of pivots */
48
  ExecExhausted      /* Exhausted total operations */
49
};
50
std::ostream& operator<<(std::ostream& out, MipResult res);
51
52
class ApproximateStatistics {
53
 public:
54
  ApproximateStatistics();
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 Maybe<Rational> estimateWithCFE(double d);
131
  static Maybe<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
167
}/* CVC4::theory::arith namespace */
168
}/* CVC4::theory namespace */
169
}/* CVC4 namespace */