GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/cut_log.h Lines: 0 7 0.0 %
Date: 2021-03-22 Branches: 0 6 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cut_log.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Kshitij Bansal
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 <unordered_map>
23
#include <map>
24
#include <set>
25
26
#include "expr/kind.h"
27
#include "theory/arith/arithvar.h"
28
#include "theory/arith/constraint_forward.h"
29
#include "util/dense_map.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
/** A low level vector of indexed doubles. */
36
struct PrimitiveVec {
37
  int len;
38
  int* inds;
39
  double* coeffs;
40
  PrimitiveVec();
41
  ~PrimitiveVec();
42
  bool initialized() const;
43
  void clear();
44
  void setup(int l);
45
  void print(std::ostream& out) const;
46
};
47
std::ostream& operator<<(std::ostream& os, const PrimitiveVec& pv);
48
49
struct DenseVector {
50
  DenseMap<Rational> lhs;
51
  Rational rhs;
52
  void purge();
53
  void print(std::ostream& os) const;
54
55
  static void print(std::ostream& os, const DenseMap<Rational>& lhs);
56
};
57
58
/** The different kinds of cuts. */
59
enum CutInfoKlass{ MirCutKlass, GmiCutKlass, BranchCutKlass,
60
                   RowsDeletedKlass,
61
                   UnknownKlass};
62
std::ostream& operator<<(std::ostream& os, CutInfoKlass kl);
63
64
/** A general class for describing a cut. */
65
class CutInfo {
66
protected:
67
  CutInfoKlass d_klass;
68
  int d_execOrd;
69
70
  int d_poolOrd;    /* cut's ordinal in the current node pool */
71
  Kind d_cutType;   /* Lowerbound, upperbound or undefined. */
72
  double d_cutRhs; /* right hand side of the cut */
73
  PrimitiveVec d_cutVec; /* vector of the cut */
74
75
  /**
76
   * The number of rows at the time the cut was made.
77
   * This is required to descramble indices after the fact!
78
   */
79
  int d_mAtCreation;
80
81
  /** This is the number of structural variables. */
82
  int d_N;
83
84
  /** if selected, make this non-zero */
85
  int d_rowId;
86
87
  /* If the cut has been successfully created,
88
   * the cut is stored in exact precision in d_exactPrecision.
89
   * If the cut has not yet been proven, this is null.
90
   */
91
  std::unique_ptr<DenseVector> d_exactPrecision;
92
93
  std::unique_ptr<ConstraintCPVec> d_explanation;
94
95
 public:
96
  CutInfo(CutInfoKlass kl, int cutid, int ordinal);
97
98
  virtual ~CutInfo();
99
100
  int getId() const;
101
102
  int getRowId() const;
103
  void setRowId(int rid);
104
105
  void print(std::ostream& out) const;
106
  //void init_cut(int l);
107
  PrimitiveVec& getCutVector();
108
  const PrimitiveVec& getCutVector() const;
109
110
  Kind getKind() const;
111
  void setKind(Kind k);
112
113
114
  void setRhs(double r);
115
  double getRhs() const;
116
117
  CutInfoKlass getKlass() const;
118
  int poolOrdinal() const;
119
120
  void setDimensions(int N, int M);
121
  int getN() const;
122
  int getMAtCreation() const;
123
124
  bool operator<(const CutInfo& o) const;
125
126
  /* Returns true if the cut was successfully made in exact precision.*/
127
  bool reconstructed() const;
128
129
  /* Returns true if the cut has an explanation. */
130
  bool proven() const;
131
132
  void setReconstruction(const DenseVector& ep);
133
  void setExplanation(const ConstraintCPVec& ex);
134
  void swapExplanation(ConstraintCPVec& ex);
135
136
  const DenseVector& getReconstruction() const;
137
  const ConstraintCPVec& getExplanation() const;
138
139
  void clearReconstruction();
140
};
141
std::ostream& operator<<(std::ostream& os, const CutInfo& ci);
142
143
class BranchCutInfo : public CutInfo {
144
public:
145
  BranchCutInfo(int execOrd, int br,  Kind dir, double val);
146
};
147
148
class RowsDeleted : public CutInfo {
149
public:
150
  RowsDeleted(int execOrd, int nrows, const int num[]);
151
};
152
153
class TreeLog;
154
155
class NodeLog {
156
private:
157
  int d_nid;
158
  NodeLog* d_parent; /* If null this is the root */
159
  TreeLog* d_tl;     /* TreeLog containing the node. */
160
161
  struct CmpCutPointer{
162
    int operator()(const CutInfo* a, const CutInfo* b) const{
163
      return *a < *b;
164
    }
165
  };
166
  typedef std::set<CutInfo*, CmpCutPointer> CutSet;
167
  CutSet d_cuts;
168
  std::map<int, int> d_rowIdsSelected;
169
170
  enum Status {Open, Closed, Branched};
171
  Status d_stat;
172
173
  int d_brVar; // branching variable
174
  double d_brVal;
175
  int d_downId;
176
  int d_upId;
177
178
public:
179
  typedef std::unordered_map<int, ArithVar> RowIdMap;
180
private:
181
  RowIdMap d_rowId2ArithVar;
182
183
public:
184
  NodeLog(); /* default constructor. */
185
  NodeLog(TreeLog* tl, int node, const RowIdMap& m); /* makes a root node. */
186
  NodeLog(TreeLog* tl, NodeLog* parent, int node);/* makes a non-root node. */
187
188
  ~NodeLog();
189
190
  int getNodeId() const;
191
  void addSelected(int ord, int sel);
192
  void applySelected();
193
  void addCut(CutInfo* ci);
194
  void print(std::ostream& o) const;
195
196
  bool isRoot() const;
197
  const NodeLog& getParent() const;
198
199
  void copyParentRowIds();
200
201
  bool isBranch() const;
202
  int branchVariable() const;
203
  double branchValue() const;
204
205
  typedef CutSet::const_iterator const_iterator;
206
  const_iterator begin() const;
207
  const_iterator end() const;
208
209
  void setBranch(int br, double val, int dn, int up);
210
  void closeNode();
211
212
  int getDownId() const;
213
  int getUpId() const;
214
215
  /**
216
   * Looks up a row id to the appropriate arith variable.
217
   * Be careful these are deleted in context during replay!
218
   * failure returns ARITHVAR_SENTINEL */
219
  ArithVar lookupRowId(int rowId) const;
220
221
  /**
222
   * Maps a row id to an arithvar.
223
   * Be careful these are deleted in context during replay!
224
   */
225
  void mapRowId(int rowid, ArithVar v);
226
  void applyRowsDeleted(const RowsDeleted& rd);
227
228
};
229
std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
230
231
class TreeLog {
232
private:
233
  int next_exec_ord;
234
  typedef std::map<int, NodeLog> ToNodeMap;
235
  ToNodeMap d_toNode;
236
  DenseMultiset d_branches;
237
238
  uint32_t d_numCuts;
239
240
  bool d_active;
241
242
public:
243
  TreeLog();
244
245
  NodeLog& getNode(int nid);
246
  void branch(int nid, int br, double val, int dn, int up);
247
  void close(int nid);
248
249
  //void applySelected();
250
  void print(std::ostream& o) const;
251
252
  typedef ToNodeMap::const_iterator const_iterator;
253
  const_iterator begin() const;
254
  const_iterator end() const;
255
256
  int getExecutionOrd();
257
258
  void reset(const NodeLog::RowIdMap& m);
259
260
  // Applies rd tp to the node with id nid
261
  void applyRowsDeleted(int nid, const RowsDeleted& rd);
262
263
  // Synonym for getNode(nid).mapRowId(ind, v)
264
  void mapRowId(int nid, int ind, ArithVar v);
265
266
private:
267
  void clear();
268
269
public:
270
  void makeInactive();
271
  void makeActive();
272
273
  bool isActivelyLogging() const;
274
275
  void addCut();
276
  uint32_t cutCount() const;
277
278
  void logBranch(uint32_t x);
279
  uint32_t numBranches(uint32_t x);
280
281
  int getRootId() const;
282
283
  uint32_t numNodes() const{
284
    return d_toNode.size();
285
  }
286
287
  NodeLog& getRootNode();
288
  void printBranchInfo(std::ostream& os) const;
289
};
290
291
292
293
}/* CVC4::theory::arith namespace */
294
}/* CVC4::theory namespace */
295
}/* CVC4 namespace */