blob: 7b578c934f09acad26095576036700fceb10bbd5 (
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
|
#ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
#include "util/rational.h"
#include "expr/node.h"
namespace CVC4 {
namespace theory {
namespace arith {
inline Node mkRationalNode(Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
inline Node mkBoolNode(bool b){
return NodeManager::currentNM()->mkConst<bool>(b);
}
inline Rational coerceToRational(TNode constant){
switch(constant.getKind()){
case kind::CONST_INTEGER:
{
Rational q(constant.getConst<Integer>());
return q;
}
case kind::CONST_RATIONAL:
return constant.getConst<Rational>();
default:
Unreachable();
}
Rational unreachable(0,0);
return unreachable;
}
inline Node coerceToRationalNode(TNode constant){
switch(constant.getKind()){
case kind::CONST_INTEGER:
{
Rational q(constant.getConst<Integer>());
Node n = mkRationalNode(q);
return n;
}
case kind::CONST_RATIONAL:
return constant;
default:
Unreachable();
}
return Node::null();
}
/** is k \in {LT, LEQ, EQ, GEQ, GT} */
inline bool isRelationOperator(Kind k){
using namespace kind;
switch(k){
case LT:
case LEQ:
case EQUAL:
case GEQ:
case GT:
return true;
default:
return false;
}
}
inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
using namespace kind;
switch(k){
case LT: return left < right;
case LEQ: return left <= right;
case EQUAL: return left == right;
case GEQ: return left >= right;
case GT: return left > right;
default:
Unreachable();
return true;
}
}
inline Node pushInNegation(Node assertion){
using namespace CVC4::kind;
Assert(assertion.getKind() == NOT);
Node p = assertion[0];
Kind k;
switch(p.getKind()){
case EQUAL:
return assertion;
case GT:
k = LT;
break;
case GEQ:
k = LEQ;
break;
case LEQ:
k = GEQ;
break;
case LT:
k = GT;
break;
default:
Unreachable();
}
return NodeManager::currentNM()->mkNode(k, p[0],p[1]);
}
}; /* namesapce arith */
}; /* namespace theory */
}; /* namespace CVC4 */
#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
|
