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