blob: fa606188a09bb1985d37f513c0a081643c8761bb (
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
|
#include <set>
#include "expr/kind.h"
#include "expr/node.h"
#include "util/Assert.h"
namespace CVC4 {
namespace theory {
namespace arith {
struct RightHandRationalLT
{
bool operator()(TNode s1, TNode s2) const
{
TNode rh1 = s1[1];
TNode rh2 = s2[1];
const Rational& c1 = rh1.getConst<Rational>();
const Rational& c2 = rh2.getConst<Rational>();
int cmpRes = c1.cmp(c2);
return cmpRes < 0;
}
};
typedef std::set<Node, RightHandRationalLT> OrderedSet;
struct SetCleanupStrategy{
static void cleanup(OrderedSet* l){
Debug("arithgc") << "cleaning up " << l << "\n";
delete l;
}
};
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
