From: Tim King <taking@cs.nyu.edu>
Date: Sat, 24 Nov 2012 23:32:04 +0000 (+0000)
Subject: Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way... 
X-Git-Tag: cvc5-1.0.0~7567
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0cf8fd2f61a34b65a0baf3585fd2bfdd0165b2b;p=cvc5.git

Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way of doing getConstraint() if the user already has a ValueCollection&.
---

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
@@ -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