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
164
165
166
167
168
169
|
/********************* */
/*! \file linear_equality.h
** \verbatim
** Original author: Tim King <taking@cs.nyu.edu>
** Major contributors: none
** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu>
** 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 This module maintains the relationship between a Tableau and PartialModel.
**
** This shares with the theory a Tableau, and a PartialModel that:
** - satisfies the equalities in the Tableau, and
** - the assignment for the non-basic variables satisfies their bounds.
** This maintains the relationship needed by the SimplexDecisionProcedure.
**
** In the language of Simplex for DPLL(T), this provides:
** - update()
** - pivotAndUpdate()
**
** This class also provides utility functions that require
** using both the Tableau and PartialModel.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
#define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
#include "theory/arith/delta_rational.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/matrix.h"
#include "theory/arith/constraint.h"
#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace arith {
class LinearEqualityModule {
private:
/**
* Manages information about the assignment and upper and lower bounds on the
* variables.
*/
ArithPartialModel& d_partialModel;
/**
* Reference to the Tableau to operate upon.
*/
Tableau& d_tableau;
/** Called whenever the value of a basic variable is updated. */
ArithVarCallBack& d_basicVariableUpdates;
public:
/**
* Initializes a LinearEqualityModule with a partial model, a tableau,
* and a callback function for when basic variables update their values.
*/
LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f):
d_partialModel(pm), d_tableau(t), d_basicVariableUpdates(f)
{}
/**
* Updates the assignment of a nonbasic variable x_i to v.
* Also updates the assignment of basic variables accordingly.
*/
void update(ArithVar x_i, const DeltaRational& v);
/**
* Updates the value of a basic variable x_i to v,
* and then pivots x_i with the nonbasic variable in its row x_j.
* Updates the assignment of the other basic variables accordingly.
*/
void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
ArithPartialModel& getPartialModel() const{ return d_partialModel; }
Tableau& getTableau() const{ return d_tableau; }
bool hasBounds(ArithVar basic, bool upperBound);
bool hasLowerBounds(ArithVar basic){
return hasBounds(basic, false);
}
bool hasUpperBounds(ArithVar basic){
return hasBounds(basic, true);
}
private:
/**
* Exports either the explanation of an upperbound or a lower bound
* of the basic variable basic, using the non-basic variables in the row.
*/
template <bool upperBound>
void propagateNonbasics(ArithVar basic, Constraint c);
public:
void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){
Assert(c->isLowerBound());
propagateNonbasics<false>(basic, c);
}
void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
Assert(c->isUpperBound());
propagateNonbasics<true>(basic, c);
}
/**
* Computes the value of a basic variable using the assignments
* of the values of the variables in the basic variable's row tableau.
* This can compute the value using either:
* - the the current assignment (useSafe=false) or
* - the safe assignment (useSafe = true).
*/
DeltaRational computeRowValue(ArithVar x, bool useSafe);
inline DeltaRational computeLowerBound(ArithVar basic){
return computeBound(basic, false);
}
inline DeltaRational computeUpperBound(ArithVar basic){
return computeBound(basic, true);
}
private:
DeltaRational computeBound(ArithVar basic, bool upperBound);
public:
/**
* Checks to make sure the assignment is consistent with the tableau.
* This code is for debugging.
*/
void debugCheckTableau();
/** Debugging information for a pivot. */
void debugPivot(ArithVar x_i, ArithVar x_j);
/**
*
*/
bool debugEntireLinEqIsConsistent(const std::string& s);
private:
/** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
IntStat d_statPivots, d_statUpdates;
TimerStat d_pivotTime;
Statistics();
~Statistics();
};
Statistics d_statistics;
};/* class LinearEqualityModule */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H */
|
