Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/approx_simplex.h	Lines:	0	3	0.0 %
Date:	2021-09-17	Branches:	0	0	0.0 %


/******************************************************************************
 * 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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
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