summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_utilities.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r--src/theory/arith/arith_utilities.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c764d0d2e..d50c48552 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -25,6 +25,7 @@
#include "util/rational.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include <vector>
#include <stdint.h>
#include <limits>
@@ -55,6 +56,9 @@ inline void setArithVar(TNode x, ArithVar a){
return x.setAttribute(ArithVarAttr(), (uint64_t)a);
}
+typedef std::vector<uint64_t> ActivityMonitor;
+
+
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback