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

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_bounds.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andrew Reynolds
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
22
#include <ostream>
23
24
#include "expr/node.h"
25
#include "theory/arith/delta_rational.h"
26
#include "util/integer.h"
27
#include "util/maybe.h"
28
#include "util/rational.h"
29
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
namespace inferbounds {
36
  enum Algorithms {None = 0, Lookup, RowSum, Simplex};
37
  enum SimplexParamKind { Unbounded, NumVars, Direct};
38
39
class InferBoundAlgorithm {
40
private:
41
  Algorithms d_alg;
42
  Maybe<int> d_simplexRounds;
43
  InferBoundAlgorithm(Algorithms a);
44
  InferBoundAlgorithm(const Maybe<int>& simplexRounds);
45
46
public:
47
  InferBoundAlgorithm();
48
49
  Algorithms getAlgorithm() const;
50
  const Maybe<int>& getSimplexRounds() const;
51
52
  static InferBoundAlgorithm mkLookup();
53
  static InferBoundAlgorithm mkRowSum();
54
  static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
55
};
56
57
std::ostream& operator<<(std::ostream& os, const Algorithms a);
58
} /* namespace inferbounds */
59
60
class ArithEntailmentCheckParameters
61
{
62
 private:
63
  typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
64
  VecInferBoundAlg d_algorithms;
65
66
public:
67
  typedef VecInferBoundAlg::const_iterator const_iterator;
68
69
  ArithEntailmentCheckParameters();
70
  ~ArithEntailmentCheckParameters();
71
72
  void addLookupRowSumAlgorithms();
73
  void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
74
75
  const_iterator begin() const;
76
  const_iterator end() const;
77
};
78
79
80
81
class InferBoundsResult {
82
public:
83
  InferBoundsResult();
84
  InferBoundsResult(Node term, bool ub);
85
86
  void setBound(const DeltaRational& dr, Node exp);
87
  bool foundBound() const;
88
89
  void setIsOptimal();
90
  bool boundIsOptimal() const;
91
92
  void setInconsistent();
93
  bool inconsistentState() const;
94
95
  const DeltaRational& getValue() const;
96
  bool boundIsRational() const;
97
  const Rational& valueAsRational() const;
98
  bool boundIsInteger() const;
99
  Integer valueAsInteger() const;
100
101
  Node getTerm() const;
102
  Node getLiteral() const;
103
  void setTerm(Node t){ d_term = t; }
104
105
  /* If there is a bound, this is a node that explains the bound. */
106
  Node getExplanation() const;
107
108
  bool budgetIsExhausted() const;
109
  void setBudgetExhausted();
110
111
  bool thresholdWasReached() const;
112
  void setReachedThreshold();
113
114
  bool findUpperBound() const { return d_upperBound; }
115
116
  void setFindLowerBound() { d_upperBound = false; }
117
  void setFindUpperBound() { d_upperBound = true; }
118
private:
119
  /* was a bound found */
120
  bool d_foundBound;
121
122
  /* was the budget exhausted */
123
  bool d_budgetExhausted;
124
125
  /* does the bound have to be optimal*/
126
  bool d_boundIsProvenOpt;
127
128
  /* was this started on an inconsistent state. */
129
  bool d_inconsistentState;
130
131
  /* reached the threshold. */
132
  bool d_reachedThreshold;
133
134
  /* the value of the bound */
135
  DeltaRational d_value;
136
137
  /* The input term. */
138
  Node d_term;
139
140
  /* Was the bound found an upper or lower bound.*/
141
  bool d_upperBound;
142
143
  /* Explanation of the bound. */
144
  Node d_explanation;
145
};
146
147
std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
148
149
class ArithEntailmentCheckSideEffects
150
{
151
 public:
152
  ArithEntailmentCheckSideEffects();
153
  ~ArithEntailmentCheckSideEffects();
154
155
  InferBoundsResult& getSimplexSideEffects();
156
157
private:
158
  InferBoundsResult* d_simplexSideEffects;
159
};
160
161
162
} /* namespace arith */
163
} /* namespace theory */
164
} /* namespace CVC4 */