2 #include "cvc4_private.h"
7 #include "util/statistics_registry.h"
8 #include "theory/arith/arithvar.h"
9 #include "theory/arith/constraint_forward.h"
10 #include "util/dense_map.h"
14 #include <ext/hash_map>
20 /** A low level vector of indexed doubles. */
27 bool initialized() const;
30 void print(std::ostream
& out
) const;
32 std::ostream
& operator<<(std::ostream
& os
, const PrimitiveVec
& pv
);
35 DenseMap
<Rational
> lhs
;
38 void print(std::ostream
& os
) const;
40 static void print(std::ostream
& os
, const DenseMap
<Rational
>& lhs
);
43 /** The different kinds of cuts. */
44 enum CutInfoKlass
{ MirCutKlass
, GmiCutKlass
, BranchCutKlass
,
47 std::ostream
& operator<<(std::ostream
& os
, CutInfoKlass kl
);
49 /** A general class for describing a cut. */
55 int d_poolOrd
; /* cut's ordinal in the current node pool */
56 Kind d_cutType
; /* Lowerbound, upperbound or undefined. */
57 double d_cutRhs
; /* right hand side of the cut */
58 PrimitiveVec d_cutVec
; /* vector of the cut */
61 * The number of rows at the time the cut was made.
62 * This is required to descramble indices after the fact!
66 /** This is the number of structural variables. */
69 /** if selected, make this non-zero */
72 /* If the cut has been successfully created,
73 * the cut is stored in exact precision in d_exactPrecision.
74 * If the cut has not yet been proven, this is null.
76 DenseVector
* d_exactPrecision
;
78 ConstraintCPVec
* d_explanation
;
81 CutInfo(CutInfoKlass kl
, int cutid
, int ordinal
);
88 void setRowId(int rid
);
90 void print(std::ostream
& out
) const;
91 //void init_cut(int l);
92 PrimitiveVec
& getCutVector();
93 const PrimitiveVec
& getCutVector() const;
99 void setRhs(double r
);
100 double getRhs() const;
102 CutInfoKlass
getKlass() const;
103 int poolOrdinal() const;
105 void setDimensions(int N
, int M
);
107 int getMAtCreation() const;
109 bool operator<(const CutInfo
& o
) const;
111 /* Returns true if the cut was successfully made in exact precision.*/
112 bool reconstructed() const;
114 /* Returns true if the cut has an explanation. */
117 void setReconstruction(const DenseVector
& ep
);
118 void setExplanation(const ConstraintCPVec
& ex
);
119 void swapExplanation(ConstraintCPVec
& ex
);
121 const DenseVector
& getReconstruction() const;
122 const ConstraintCPVec
& getExplanation() const;
124 void clearReconstruction();
126 std::ostream
& operator<<(std::ostream
& os
, const CutInfo
& ci
);
128 struct BranchCutInfo
: public CutInfo
{
129 BranchCutInfo(int execOrd
, int br
, Kind dir
, double val
);
132 struct RowsDeleted
: public CutInfo
{
133 RowsDeleted(int execOrd
, int nrows
, const int num
[]);
141 NodeLog
* d_parent
; /* If null this is the root */
142 TreeLog
* d_tl
; /* TreeLog containing the node. */
144 struct CmpCutPointer
{
145 int operator()(const CutInfo
* a
, const CutInfo
* b
) const{
149 typedef std::set
<CutInfo
*, CmpCutPointer
> CutSet
;
151 std::map
<int, int> d_rowIdsSelected
;
153 enum Status
{Open
, Closed
, Branched
};
156 int d_brVar
; // branching variable
162 typedef __gnu_cxx::hash_map
<int, ArithVar
> RowIdMap
;
164 RowIdMap d_rowId2ArithVar
;
167 NodeLog(); /* default constructor. */
168 NodeLog(TreeLog
* tl
, int node
, const RowIdMap
& m
); /* makes a root node. */
169 NodeLog(TreeLog
* tl
, NodeLog
* parent
, int node
);/* makes a non-root node. */
173 int getNodeId() const;
174 void addSelected(int ord
, int sel
);
175 void applySelected();
176 void addCut(CutInfo
* ci
);
177 void print(std::ostream
& o
) const;
180 const NodeLog
& getParent() const;
182 void copyParentRowIds();
184 bool isBranch() const;
185 int branchVariable() const;
186 double branchValue() const;
188 typedef CutSet::const_iterator const_iterator
;
189 const_iterator
begin() const;
190 const_iterator
end() const;
192 void setBranch(int br
, double val
, int dn
, int up
);
195 int getDownId() const;
199 * Looks up a row id to the appropraite arith variable.
200 * Be careful these are deleted in context during replay!
201 * failure returns ARITHVAR_SENTINEL */
202 ArithVar
lookupRowId(int rowId
) const;
205 * Maps a row id to an arithvar.
206 * Be careful these are deleted in context during replay!
208 void mapRowId(int rowid
, ArithVar v
);
209 void applyRowsDeleted(const RowsDeleted
& rd
);
212 std::ostream
& operator<<(std::ostream
& os
, const NodeLog
& nl
);
214 class ApproximateSimplex
;
217 ApproximateSimplex
* d_generator
;
220 typedef std::map
<int, NodeLog
> ToNodeMap
;
222 DenseMultiset d_branches
;
231 NodeLog
& getNode(int nid
);
232 void branch(int nid
, int br
, double val
, int dn
, int up
);
235 //void applySelected();
236 void print(std::ostream
& o
) const;
238 typedef ToNodeMap::const_iterator const_iterator
;
239 const_iterator
begin() const;
240 const_iterator
end() const;
242 int getExecutionOrd();
244 void reset(const NodeLog::RowIdMap
& m
);
246 // Applies rd tp to the node with id nid
247 void applyRowsDeleted(int nid
, const RowsDeleted
& rd
);
249 // Synonym for getNode(nid).mapRowId(ind, v)
250 void mapRowId(int nid
, int ind
, ArithVar v
);
259 bool isActivelyLogging() const;
262 uint32_t cutCount() const;
264 void logBranch(uint32_t x
);
265 uint32_t numBranches(uint32_t x
);
267 int getRootId() const;
269 uint32_t numNodes() const{
270 return d_toNode
.size();
273 NodeLog
& getRootNode();
274 void printBranchInfo(std::ostream
& os
) const;
279 }/* CVC4::theory::arith namespace */
280 }/* CVC4::theory namespace */
281 }/* CVC4 namespace */