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