1 files changed, 91 insertions, 0 deletions
diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
new file mode 100644
index 000000000..8ce0e93b2
--- /dev/null
+++ b/src/theory/idl/idl_assertion.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file idl_assertion.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#pragma once
+
+#include "theory/idl/idl_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * An internal representation of the IDL assertions. Each IDL assertions is
+ * of the form (x - y op c) where op is one of (<=, =, !=). IDL assertion
+ * can be constructed from an expression.
+ */
+class IDLAssertion {
+
+  /** The positive variable */
+  TNode d_x;
+  /** The negative variable */
+  TNode d_y;
+  /** The relation */
+  Kind d_op;
+  /** The RHS constant */
+  Integer d_c;
+
+  /** Original assertion we got this one from */
+  TNode d_original;
+
+  /** Parses the given node into an assertion, and return true if OK. */
+  bool parse(TNode node, int c = 1, bool negated = false);
+
+public:
+
+  /** Null assertion */
+  IDLAssertion();
+  /** Create the assertion from given node */
+  IDLAssertion(TNode node);
+  /** Copy constructor */
+  IDLAssertion(const IDLAssertion& other);
+
+  TNode getX() const { return d_x; }
+  TNode getY() const { return d_y; }
+  Kind getOp() const { return d_op;}
+  Integer getC() const { return d_c; }
+
+  /**
+   * Propagate the constraint using the model. For example, if the constraint
+   * is of the form x - y <= -1, and the value of x in the model is 0, then
+   *
+   *   (x - y <= -1) and (x = 0) implies y >= x + 1 = 1
+   *
+   * If the value of y is less then 1, is is set to 1 and true is returned. If
+   * the value of y is 1 or more, than false is return.
+   *
+   * @return true if value of y was updated
+   */
+  bool propagate(IDLModel& model) const;
+
+  /** Is this constraint proper */
+  bool ok() const {
+    return !d_x.isNull() || !d_y.isNull();
+  }
+
+  /** Output to the stream */
+  void toStream(std::ostream& out) const;
+};
+
+inline std::ostream& operator << (std::ostream& out, const IDLAssertion& assertion) {
+  assertion.toStream(out);
+  return out;
+}
+
+}
+}
+}