Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way...

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 7295b17e057e15d5c08ae98fb0ad157e170eaec5..8bf5447e38d46b5ac6ba163cccc51207eb84054d 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -841,6 +841,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