blob: f0e314bfb1cd55c0aa1042efdf19b561c4d540aa (
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
|
/********************* */
/*! \file callbacks.h
** \verbatim
** Original author: Tim King
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** 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
**/
#pragma once
#include "expr/node.h"
#include "util/rational.h"
#include "theory/arith/theory_arith_private_forward.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/constraint_forward.h"
namespace CVC4 {
namespace theory {
namespace arith {
/**
* ArithVarCallBack provides a mechanism for agreeing on callbacks while
* breaking mutual recursion inclusion order problems.
*/
class ArithVarCallBack {
public:
virtual void operator()(ArithVar x) = 0;
};
/**
* Requests arithmetic variables for internal use,
* and releases arithmetic variables that are no longer being used.
*/
class ArithVarMalloc {
public:
virtual ArithVar request() = 0;
virtual void release(ArithVar v) = 0;
};
class TNodeCallBack {
public:
virtual void operator()(TNode n) = 0;
};
class NodeCallBack {
public:
virtual void operator()(Node n) = 0;
};
class RationalCallBack {
public:
virtual Rational operator()() const = 0;
};
class SetupLiteralCallBack : public TNodeCallBack {
private:
TheoryArithPrivate& d_arith;
public:
SetupLiteralCallBack(TheoryArithPrivate& ta);
void operator()(TNode lit);
};
class DeltaComputeCallback : public RationalCallBack {
private:
const TheoryArithPrivate& d_ta;
public:
DeltaComputeCallback(const TheoryArithPrivate& ta);
Rational operator()() const;
};
class BasicVarModelUpdateCallBack : public ArithVarCallBack{
private:
TheoryArithPrivate& d_ta;
public:
BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
void operator()(ArithVar x);
};
class TempVarMalloc : public ArithVarMalloc {
private:
TheoryArithPrivate& d_ta;
public:
TempVarMalloc(TheoryArithPrivate& ta);
ArithVar request();
void release(ArithVar v);
};
class RaiseConflict {
private:
TheoryArithPrivate& d_ta;
ConstraintCPVec& d_construction;
public:
RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& d_construction);
/* Adds a constraint to the constraint under construction. */
void addConstraint(ConstraintCP c);
/* Turns the vector under construction into a conflict */
void commitConflict();
void sendConflict(const ConstraintCPVec& vec);
/* If you are not an equality engine, don't use this! */
void blackBoxConflict(Node n);
};
class BoundCountingLookup {
private:
TheoryArithPrivate& d_ta;
public:
BoundCountingLookup(TheoryArithPrivate& ta);
const BoundsInfo& boundsInfo(ArithVar basic) const;
BoundCounts atBounds(ArithVar basic) const;
BoundCounts hasBounds(ArithVar basic) const;
};
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
