summaryrefslogtreecommitdiff
path: root/src/theory/arith/partial_model.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-02-15 21:52:16 +0000
committerTim King <taking@cs.nyu.edu>2012-02-15 21:52:16 +0000
commit9a0a59d5c85c4a1d2469f43e9d2b433e156810ba (patch)
treeba66b1c5cdeec062ce4144a463ec0b61a83e3cc6 /src/theory/arith/partial_model.h
parent093fa1757392e7bfc18493f2daa87ff540aeea86 (diff)
This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.
- This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r--src/theory/arith/partial_model.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 6e85f7e80..cf0fc7d4e 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -116,7 +116,7 @@ private:
void zeroDifferenceDetected(ArithVar x);
public:
-
+ bool boundsAreEqual(ArithVar x);
void setUpperBound(ArithVar x, const DeltaRational& r);
void setLowerBound(ArithVar x, const DeltaRational& r);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback