blob: b32fdef2d95434cae50075d3a4a9ed4a1c3c9291 (
plain)
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
|
/********************* */
/*! \file approx_simplex.h
** \verbatim
** Original author: Tim King
** Major contributors: none
** Minor contributors (to current version): Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#pragma once
#include "util/statistics_registry.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/linear_equality.h"
#include "util/dense_map.h"
#include <vector>
namespace CVC4 {
namespace theory {
namespace arith {
class ApproximateSimplex{
protected:
int d_pivotLimit;
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);
ApproximateSimplex();
virtual ~ApproximateSimplex(){}
/** A result is either sat, unsat or unknown.*/
enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat};
struct Solution {
DenseSet newBasis;
DenseMap<DeltaRational> newValues;
Solution() : newBasis(), newValues(){}
};
/** Sets a deterministic effort limit. */
void setPivotLimit(int pivotLimit);
/** 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 ApproxResult solveMIP() = 0;
virtual Solution extractMIP() const = 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 Rational estimateWithCFE(double 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, int depth);
};/* class ApproximateSimplex */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
