diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-24 23:32:04 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-24 23:32:04 +0000 |
commit | e0cf8fd2f61a34b65a0baf3585fd2bfdd0165b2b (patch) | |
tree | 4e5792db54495fca7da3f5db8e4a94aa283c1761 /src/theory | |
parent | 16b38e0965a9b16b7c1aa1cddb4bf243631159e4 (diff) |
Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way of doing getConstraint() if the user already has a ValueCollection&.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/constraint.h | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 7295b17e0..8bf5447e3 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -842,6 +842,21 @@ public: Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r); /** + * Returns a constraint of the given type for the value and variable + * for the given ValueCollection, vc. + * This is made if there is no such constraint. + * Weirdly enough vc may be altered despite this signature! + */ + Constraint ensureConstraint(ValueCollection& vc, ConstraintType t){ + if(vc.hasConstraintOfType(t)){ + return vc.getConstraintOfType(t); + }else{ + return getConstraint(vc.getVariable(), t, vc.getValue()); + } + } + + + /** * Outputs a minimal set of unate implications onto the vector for the variable. * This outputs lemmas of the general forms * (= p c) implies (<= p d) for c < d, or |