summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_static_learner.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/arith_static_learner.h')
-rw-r--r--src/theory/arith/arith_static_learner.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index f2405cd5c..0ed9cbe85 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -44,10 +44,19 @@ private:
VarToNodeSetMap d_miplibTrick;
std::list<TNode> d_miplibTrickKeys;
+ /**
+ * Map from a node to it's minimum and maximum.
+ */
+ typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
+ NodeToMinMaxMap d_minMap;
+ NodeToMinMaxMap d_maxMap;
+
public:
ArithStaticLearner();
void staticLearning(TNode n, NodeBuilder<>& learned);
+ void addBound(TNode n);
+
void clear();
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback