2 #include "cvc4_private.h"
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"
17 class ApproximateSimplex
{
23 static bool enabled();
26 * If glpk is enabled, return a subclass that can do something.
27 * If glpk is disabled, return a sublass that does nothing.
29 static ApproximateSimplex
* mkApproximateSimplexSolver(const ArithVariables
& vars
);
31 virtual ~ApproximateSimplex(){}
33 /** A result is either sat, unsat or unknown.*/
34 enum ApproxResult
{ApproxError
, ApproxSat
, ApproxUnsat
};
37 DenseMap
<DeltaRational
> newValues
;
38 Solution() : newBasis(), newValues(){}
41 /** Sets a deterministic effort limit. */
42 void setPivotLimit(int pivotLimit
);
44 /** Sets a maximization criteria for the approximate solver.*/
45 virtual void setOptCoeffs(const ArithRatPairVec
& ref
) = 0;
47 virtual ArithRatPairVec
heuristicOptCoeffs() const = 0;
49 virtual ApproxResult
solveRelaxation() = 0;
50 virtual Solution
extractRelaxation() const = 0;
52 virtual ApproxResult
solveMIP() = 0;
53 virtual Solution
extractMIP() const = 0;
55 /** UTILIES FOR DEALING WITH ESTIMATES */
57 static const double SMALL_FIXED_DELTA
;
58 static const double TOLERENCE
;
60 /** Returns true if two doubles are roughly equal based on TOLERENCE and SMALL_FIXED_DELTA.*/
61 static bool roughlyEqual(double a
, double b
);
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.
68 static Rational
estimateWithCFE(double d
);
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.
75 static std::vector
<Integer
> rationalToCfe(const Rational
& q
, int depth
);
77 /** Converts a continued fraction expansion representation to a rational. */
78 static Rational
cfeToRational(const std::vector
<Integer
>& exp
);
80 /** Estimates a rational as a continued fraction expansion.*/
81 static Rational
estimateWithCFE(const Rational
& q
, int depth
);
82 };/* class ApproximateSimplex */
85 }/* CVC4::theory::arith namespace */
86 }/* CVC4::theory namespace */