diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-14 04:39:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-14 04:39:43 +0000 |
commit | a8f1f0e2cef69acd278f859fe32a2df7852256e0 (patch) | |
tree | 70f590c29e7224ca8c34a53fb44c456baa5baa9c /src/theory/arith/simplex.h | |
parent | d192b7f7aed685e89053bd0f0a4c3e42f1136b80 (diff) |
Brings the tuning branch into trunk. This includes the changes from restricted-simplex.
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 8450afb06..d260ff9b4 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -62,6 +62,7 @@ #include "util/dense_map.h" #include "util/options.h" #include "util/stats.h" +#include "util/result.h" #include <queue> @@ -130,7 +131,7 @@ public: * * Corresponds to the "check()" procedure in [Cav06]. */ - bool findModel(); + Result::Sat findModel(bool exactResult); private: @@ -218,6 +219,11 @@ private: public: void increaseMax() {d_numVariables++;} + + void clearQueue() { + d_queue.clear(); + } + private: /** Reports a conflict to on the output channel. */ |