blob: bce9a07dbe14e5171fc250354013ac2b2e4fafa6 (
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
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
|
/********************* */
/*! \file infer_bounds.h
** \verbatim
** Top contributors (to current version):
** Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#pragma once
#include <ostream>
#include "expr/node.h"
#include "theory/arith/delta_rational.h"
#include "theory/theory.h"
#include "util/integer.h"
#include "util/maybe.h"
#include "util/rational.h"
namespace CVC4 {
namespace theory {
namespace arith {
namespace inferbounds {
enum Algorithms {None = 0, Lookup, RowSum, Simplex};
enum SimplexParamKind { Unbounded, NumVars, Direct};
class InferBoundAlgorithm {
private:
Algorithms d_alg;
Maybe<int> d_simplexRounds;
InferBoundAlgorithm(Algorithms a);
InferBoundAlgorithm(const Maybe<int>& simplexRounds);
public:
InferBoundAlgorithm();
Algorithms getAlgorithm() const;
const Maybe<int>& getSimplexRounds() const;
static InferBoundAlgorithm mkLookup();
static InferBoundAlgorithm mkRowSum();
static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
};
std::ostream& operator<<(std::ostream& os, const Algorithms a);
} /* namespace inferbounds */
class ArithEntailmentCheckParameters : public EntailmentCheckParameters {
private:
typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
VecInferBoundAlg d_algorithms;
public:
typedef VecInferBoundAlg::const_iterator const_iterator;
ArithEntailmentCheckParameters();
~ArithEntailmentCheckParameters();
void addLookupRowSumAlgorithms();
void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
const_iterator begin() const;
const_iterator end() const;
};
class InferBoundsResult {
public:
InferBoundsResult();
InferBoundsResult(Node term, bool ub);
void setBound(const DeltaRational& dr, Node exp);
bool foundBound() const;
void setIsOptimal();
bool boundIsOptimal() const;
void setInconsistent();
bool inconsistentState() const;
const DeltaRational& getValue() const;
bool boundIsRational() const;
const Rational& valueAsRational() const;
bool boundIsInteger() const;
Integer valueAsInteger() const;
Node getTerm() const;
Node getLiteral() const;
void setTerm(Node t){ d_term = t; }
/* If there is a bound, this is a node that explains the bound. */
Node getExplanation() const;
bool budgetIsExhausted() const;
void setBudgetExhausted();
bool thresholdWasReached() const;
void setReachedThreshold();
bool findUpperBound() const { return d_upperBound; }
void setFindLowerBound() { d_upperBound = false; }
void setFindUpperBound() { d_upperBound = true; }
private:
/* was a bound found */
bool d_foundBound;
/* was the budget exhausted */
bool d_budgetExhausted;
/* does the bound have to be optimal*/
bool d_boundIsProvenOpt;
/* was this started on an inconsistent state. */
bool d_inconsistentState;
/* reached the threshold. */
bool d_reachedThreshold;
/* the value of the bound */
DeltaRational d_value;
/* The input term. */
Node d_term;
/* Was the bound found an upper or lower bound.*/
bool d_upperBound;
/* Explanation of the bound. */
Node d_explanation;
};
std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{
public:
ArithEntailmentCheckSideEffects();
~ArithEntailmentCheckSideEffects();
InferBoundsResult& getSimplexSideEffects();
private:
InferBoundsResult* d_simplexSideEffects;
};
} /* namespace arith */
} /* namespace theory */
} /* namespace CVC4 */
|
