summaryrefslogtreecommitdiff
path: root/src/theory/arith/partial_model.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2013-05-07 14:35:22 -0400
committerTim King <taking@cs.nyu.edu>2013-05-07 14:35:22 -0400
commitd5638ce2fc70625c2b0bbc013b37d96fb5306568 (patch)
treee42102a8e2c46893a82f29ae71bb9613d9b327c9 /src/theory/arith/partial_model.h
parente7519f8b5020259bd02f01c24bed74cf0e0c8be2 (diff)
Improving arithmetic debugging output.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r--src/theory/arith/partial_model.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 953c8c0d3..deafb559a 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -204,6 +204,11 @@ private:
bool isSlack(ArithVar x) const {
return d_vars[x].d_slack;
}
+
+ bool integralAssignment(ArithVar x) const {
+ return getAssignment(x).isIntegral();
+ }
+
private:
typedef std::pair<ArithVar, Constraint> AVCPair;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback