GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/callbacks.h Lines: 13 13 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file callbacks.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Mathias Preiner, Clark Barrett
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
#pragma once
19
20
#include "expr/node.h"
21
#include "theory/arith/arithvar.h"
22
#include "theory/arith/bound_counts.h"
23
#include "theory/arith/constraint_forward.h"
24
#include "theory/inference_id.h"
25
#include "util/rational.h"
26
27
namespace CVC4 {
28
29
class ProofNode;
30
31
namespace theory {
32
namespace arith {
33
34
class TheoryArithPrivate;
35
36
/**
37
 * ArithVarCallBack provides a mechanism for agreeing on callbacks while
38
 * breaking mutual recursion inclusion order problems.
39
 */
40
17994
class ArithVarCallBack {
41
public:
42
17991
  virtual ~ArithVarCallBack() {}
43
  virtual void operator()(ArithVar x) = 0;
44
};
45
46
/**
47
 * Requests arithmetic variables for internal use,
48
 * and releases arithmetic variables that are no longer being used.
49
 */
50
107964
class ArithVarMalloc {
51
public:
52
107952
  virtual ~ArithVarMalloc() {}
53
  virtual ArithVar request() = 0;
54
  virtual void release(ArithVar v) = 0;
55
};
56
57
17994
class TNodeCallBack {
58
public:
59
17991
  virtual ~TNodeCallBack() {}
60
  virtual void operator()(TNode n) = 0;
61
};
62
63
class NodeCallBack {
64
public:
65
  virtual ~NodeCallBack() {}
66
  virtual void operator()(Node n) = 0;
67
};
68
69
17994
class RationalCallBack {
70
public:
71
17991
  virtual ~RationalCallBack() {}
72
  virtual Rational operator()() const = 0;
73
};
74
75
26988
class SetupLiteralCallBack : public TNodeCallBack {
76
private:
77
  TheoryArithPrivate& d_arith;
78
public:
79
  SetupLiteralCallBack(TheoryArithPrivate& ta);
80
  void operator()(TNode lit) override;
81
};
82
83
26988
class DeltaComputeCallback : public RationalCallBack {
84
private:
85
  const TheoryArithPrivate& d_ta;
86
public:
87
  DeltaComputeCallback(const TheoryArithPrivate& ta);
88
  Rational operator()() const override;
89
};
90
91
26988
class BasicVarModelUpdateCallBack : public ArithVarCallBack{
92
private:
93
  TheoryArithPrivate& d_ta;
94
public:
95
  BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
96
  void operator()(ArithVar x) override;
97
};
98
99
215916
class TempVarMalloc : public ArithVarMalloc {
100
private:
101
  TheoryArithPrivate& d_ta;
102
public:
103
  TempVarMalloc(TheoryArithPrivate& ta);
104
  ArithVar request() override;
105
  void release(ArithVar v) override;
106
};
107
108
class RaiseConflict {
109
private:
110
  TheoryArithPrivate& d_ta;
111
public:
112
  RaiseConflict(TheoryArithPrivate& ta);
113
114
  /** Calls d_ta.raiseConflict(c) */
115
  void raiseConflict(ConstraintCP c, InferenceId id) const;
116
};
117
118
35976
class FarkasConflictBuilder {
119
private:
120
  RationalVector d_farkas;
121
  ConstraintCPVec d_constraints;
122
  ConstraintCP d_consequent;
123
  bool d_consequentSet;
124
public:
125
126
  /**
127
   * Constructs a new FarkasConflictBuilder.
128
   */
129
  FarkasConflictBuilder();
130
131
  /**
132
   * Adds an antecedent constraint to the conflict under construction
133
   * with the farkas coefficient fc * mult.
134
   *
135
   * The value mult is either 1 or -1.
136
   */
137
  void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
138
139
  /**
140
   * Adds an antecedent constraint to the conflict under construction
141
   * with the farkas coefficient fc.
142
   */
143
  void addConstraint(ConstraintCP c, const Rational& fc);
144
145
  /**
146
   * Makes the last constraint added the consequent.
147
   * Can be done exactly once per reset().
148
   */
149
  void makeLastConsequent();
150
151
  /**
152
   * Turns the antecendents into a proof of the negation of one of the
153
   * antecedents.
154
   *
155
   * The buffer is no longer underConstruction afterwards.
156
   *
157
   * precondition:
158
   * - At least two constraints have been asserted.
159
   * - makeLastConsequent() has been called.
160
   *
161
   * postcondition: The returned constraint is in conflict.
162
   */
163
  ConstraintCP commitConflict();
164
165
  /** Returns true if a conflict has been pushed back since the last reset. */
166
  bool underConstruction() const;
167
168
  /** Returns true if the consequent has been set since the last reset. */
169
  bool consequentIsSet() const;
170
171
  /** Resets the state of the buffer. */
172
  void reset();
173
};
174
175
176
class RaiseEqualityEngineConflict {
177
private:
178
  TheoryArithPrivate& d_ta;
179
180
public:
181
  RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
182
183
  /* If you are not an equality engine, don't use this!
184
   *
185
   * The proof should prove that `n` is a conflict.
186
   * */
187
  void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
188
};
189
190
class BoundCountingLookup {
191
private:
192
  TheoryArithPrivate& d_ta;
193
public:
194
  BoundCountingLookup(TheoryArithPrivate& ta);
195
  const BoundsInfo& boundsInfo(ArithVar basic) const;
196
  BoundCounts atBounds(ArithVar basic) const;
197
  BoundCounts hasBounds(ArithVar basic) const;
198
};
199
200
}/* CVC4::theory::arith namespace */
201
}/* CVC4::theory namespace */
202
}/* CVC4 namespace */