IDL example theory (to be used with --use-theory=idl).

15 files changed, 718 insertions, 5 deletions

diff --git a/.project b/.project
index 252288336..b1fd9f133 100644
--- a/.project
+++ b/.project
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
-	<name>cvc4-bvprop</name>
+	<name>cvc4-idl</name>
 	<comment></comment>
 	<projects>
 	</projects>
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 21988df56..670718e4e 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -36,7 +36,9 @@ OPTIONS_FILES_SRCS = \
 	../main/options.cpp \
 	../main/options.h \
 	../parser/options.cpp \
-	../parser/options.h
+	../parser/options.h \
+	../theory/idl/options.cpp \
+	../theory/idl/options.h
 
 OPTIONS_FILES = \
 	$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
@@ -93,7 +95,9 @@ nodist_liboptions_la_SOURCES = \
 	../main/options.cpp \
 	../main/options.h \
 	../parser/options.cpp \
-	../parser/options.h
+	../parser/options.h \
+	../theory/idl/options.cpp \
+	../theory/idl/options.h
 
 BUILT_SOURCES = \
 	exprs-builts \
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 70962e6ed..2df698da4 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -3,7 +3,7 @@ AM_CPPFLAGS = \
 	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules
+SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl
 DIST_SUBDIRS = $(SUBDIRS) example
 
 noinst_LTLIBRARIES = libtheory.la
@@ -60,7 +60,8 @@ libtheory_la_LIBADD = \
 	@builddir@/bv/libbv.la \
 	@builddir@/datatypes/libdatatypes.la \
 	@builddir@/quantifiers/libquantifiers.la \
-	@builddir@/rewriterules/librewriterules.la
+	@builddir@/rewriterules/librewriterules.la \
+	@builddir@/idl/libidl.la
 
 EXTRA_DIST = \
 	logic_info.i \
diff --git a/src/theory/idl/Makefile b/src/theory/idl/Makefile
new file mode 100644
index 000000000..7c57f81ef
--- /dev/null
+++ b/src/theory/idl/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/rdl
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/idl/Makefile.am b/src/theory/idl/Makefile.am
new file mode 100644
index 000000000..4297e3bdb
--- /dev/null
+++ b/src/theory/idl/Makefile.am
@@ -0,0 +1,19 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libidl.la
+
+libidl_la_SOURCES = \
+	idl_model.h \
+	idl_model.cpp \
+	idl_assertion.h \
+	idl_assertion.cpp \
+	idl_assertion_db.h \
+	idl_assertion_db.cpp \
+	theory_idl.h \
+	theory_idl.cpp
+
+EXTRA_DIST = \
+	kinds 
diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
new file mode 100644
index 000000000..c84989d4f
--- /dev/null
+++ b/src/theory/idl/idl_assertion.cpp
@@ -0,0 +1,196 @@
+#include "theory/idl/idl_assertion.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLAssertion::IDLAssertion()
+: d_op(kind::LAST_KIND)
+{}
+
+IDLAssertion::IDLAssertion(TNode node) {
+  bool ok = parse(node, 1, false);
+  if (!ok) {
+    d_x = d_y = TNode::null();
+  } else {
+    if (d_op == kind::GT) {
+      // Turn GT into LT x - y > c is the same as y - x < -c
+      std::swap(d_x, d_y);
+      d_c = -d_c;
+      d_op = kind::LT;
+    }
+    if (d_op == kind::GEQ) {
+      // Turn GT into LT x - y >= c is the same as y - x <= -c
+      std::swap(d_x, d_y);
+      d_c = -d_c;
+      d_op = kind::LEQ;
+    }
+    if (d_op == kind::LT) {
+      // Turn strict into non-strict x - y < c is the same as x - y <= c-1
+      d_c = d_c - 1;
+      d_op = kind::LEQ;
+    }
+  }
+  d_original = node;
+}
+
+IDLAssertion::IDLAssertion(const IDLAssertion& other)
+: d_x(other.d_x)
+, d_y(other.d_y)
+, d_op(other.d_op)
+, d_c(other.d_c)
+, d_original(other.d_original)
+{}
+
+bool IDLAssertion::propagate(IDLModel& model) const {
+  Debug("theory::idl::model") << model << std::endl;
+  Assert(ok());
+  // Should be d_x - d_y <= d_c, or d_x - d_c <= d_y
+  Integer x_value = model.getValue(d_x);
+  Integer y_value = model.getValue(d_y);
+  if (x_value - y_value > d_c) {
+    model.setValue(d_y, x_value - d_c, IDLReason(d_x, d_original));
+    Debug("theory::idl::model") << model << std::endl;
+    return true;
+  } else {
+    return false;
+  }
+}
+
+void IDLAssertion::toStream(std::ostream& out) const {
+  out << "IDL[" << d_x << " - " << d_y << " " << d_op << " " << d_c << "]";
+}
+
+/** Negates the given arithmetic kind */
+static Kind negateOp(Kind op) {
+  switch (op) {
+  case kind::LT:
+    // not (a < b) = (a >= b)
+    return kind::GEQ;
+  case kind::LEQ:
+    // not (a <= b) = (a > b)
+    return kind::GT;
+  case kind::GT:
+    // not (a > b) = (a <= b)
+    return kind::LEQ;
+  case kind::GEQ:
+    // not (a >= b) = (a < b)
+    return kind::LT;
+  case kind::EQUAL:
+    // not (a = b) = (a != b)
+    return kind::DISTINCT;
+  case kind::DISTINCT:
+    // not (a != b) = (a = b)
+    return kind::EQUAL;
+  default:
+    Unreachable();
+    break;
+  }
+  return kind::LAST_KIND;
+}
+
+bool IDLAssertion::parse(TNode node, int c, bool negated) {
+
+  // Only unit coefficients allowed
+  if (c != 1 && c != -1) {
+    return false;
+  }
+
+  // Assume we're ok
+  bool ok = true;
+
+  // The kind of the node
+  switch(node.getKind()) {
+
+  case kind::NOT:
+    // We parse the negation
+    ok = parse(node[0], c, true);
+    // Setup the kind
+    if(ok) {
+      d_op = negateOp(d_op);
+    }
+    break;
+
+  case kind::EQUAL:
+  case kind::LT:
+  case kind::LEQ:
+  case kind::GT:
+  case kind::GEQ: {
+    // All relation operators are parsed on both sides
+    d_op = node.getKind();
+    ok = parse(node[0], c, negated);
+    if(ok) {
+      ok = parse(node[1],-c, negated);
+    }
+    break;
+  }
+
+  case kind::CONST_RATIONAL: {
+    // Constants
+    Rational m = node.getConst<Rational>();
+    if (m.isIntegral()) {
+      d_c +=  m.getNumerator() * (-c);
+    } else {
+      ok = false;
+    }
+    break;
+  }
+  case kind::MULT: {
+    // Only unit multiplication of variables
+    if(node.getNumChildren() == 2 && node[0].isConst()) {
+      Rational a = node[0].getConst<Rational>();
+      if(a == 1 || a == -1) {
+        return parse(node[1], c * a.sgn(), negated);
+      } else {
+        ok = false;
+      }
+    } else {
+      ok = false;
+    }
+    break;
+  }
+
+  case kind::PLUS: {
+    for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+      bool ok = parse(node[i], c, negated);
+      if(!ok) {
+        break;
+      }
+    }
+    break;
+  }
+
+  case kind::MINUS: {
+    ok = parse(node[0], c, negated);
+    if(ok) {
+      ok = parse(node[1], -c, negated);
+    }
+    break;
+  }
+
+  case kind::UMINUS: {
+    ok = parse(node[0], -c, negated);
+    break;
+  }
+
+  default: {
+    if(c > 0) {
+      if(d_x.isNull()) {
+        d_x = node;
+      } else {
+        ok = false;
+      }
+    } else {
+      if(d_y.isNull()) {
+        d_y = node;
+      } else {
+        ok = false;
+      }
+    }
+    break;
+  }
+  } // End case
+
+  // Difference logic OK
+  return ok;
+}
diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
new file mode 100644
index 000000000..2ed5a6bef
--- /dev/null
+++ b/src/theory/idl/idl_assertion.h
@@ -0,0 +1,74 @@
+#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;
+}
+
+}
+}
+}
diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
new file mode 100644
index 000000000..7c27e9d0d
--- /dev/null
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -0,0 +1,42 @@
+#include "theory/idl/idl_assertion_db.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLAssertionDB::IDLAssertionDB(context::Context* c)
+: d_assertions(c)
+, d_variableLists(c)
+{}
+
+void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) {
+  // Is there a list for the variable already?
+  unsigned previous = -1;
+  var_to_unsigned_map::iterator find = d_variableLists.find(var);
+  if (find != d_variableLists.end()) {
+    previous = (*find).second;
+  }
+  // Add to the DB
+  d_variableLists[var] = d_assertions.size();
+  d_assertions.push_back(IDLAssertionListElement(assertion, previous));
+}
+
+IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var)
+: d_db(db)
+, d_current(-1)
+{
+  var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var);
+  if (find != d_db.d_variableLists.end()) {
+    d_current = (*find).second;
+  }
+}
+
+void IDLAssertionDB::iterator::next() {
+  if (d_current != (unsigned)(-1)) {
+    d_current = d_db.d_assertions[d_current].d_previous;
+  }
+}
+
+IDLAssertion IDLAssertionDB::iterator::get() const {
+  return d_db.d_assertions[d_current].d_assertion;
+}
diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
new file mode 100644
index 000000000..3972819da
--- /dev/null
+++ b/src/theory/idl/idl_assertion_db.h
@@ -0,0 +1,69 @@
+#pragma once
+
+#include "theory/idl/idl_assertion.h"
+#include "context/cdlist.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * Context-dependent database assertions, organized by variable. Each variable
+ * can be associated a list of IDL assertions. The list of assertions can
+ * be iterated over using the provided iterator class.
+ */
+class IDLAssertionDB {
+
+  /** Elements of the assertion lists */
+  struct IDLAssertionListElement {
+    /** The assertion itself */
+    IDLAssertion d_assertion;
+    /** The inndex of the previous element (-1 for null) */
+    unsigned d_previous;
+
+    IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
+    : d_assertion(assertion), d_previous(previous)
+    {}
+  };
+
+  /** All assertions in a context dependent stack */
+  context::CDList<IDLAssertionListElement> d_assertions;
+
+  typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map;
+
+  /** Map from variables to the first element of their list */
+  var_to_unsigned_map d_variableLists;
+
+public:
+
+  /** Create a new assertion database */
+  IDLAssertionDB(context::Context* c);
+
+  /** Add a new assertion, attach to the list of the given variable */
+  void add(const IDLAssertion& assertion, TNode var);
+
+  /** Iteration over the constraints of a variable */
+  class iterator {
+    /** The database */
+    const IDLAssertionDB& d_db;
+    /** Index of the current constraint */
+    unsigned d_current;
+  public:
+    /** Construct the iterator for the variable */
+    iterator(IDLAssertionDB& db, TNode var);
+    /** Is this iterator done */
+    bool done() const { return d_current == (unsigned)(-1); }
+    /** Next element */
+    void next();
+    /** Get the assertion */
+    IDLAssertion get() const;
+  };
+};
+
+}
+}
+}
+
+
+
+
diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
new file mode 100644
index 000000000..2feabd700
--- /dev/null
+++ b/src/theory/idl/idl_model.cpp
@@ -0,0 +1,47 @@
+#include "theory/idl/idl_model.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLModel::IDLModel(context::Context* context)
+: d_model(context)
+, d_reason(context)
+{}
+
+Integer IDLModel::getValue(TNode var) const {
+  model_value_map::const_iterator find = d_model.find(var);
+  if (find != d_model.end()) {
+    return (*find).second;
+  } else {
+    return 0;
+  }
+}
+
+void IDLModel::setValue(TNode var, Integer value, IDLReason reason) {
+  Assert(!reason.constraint.isNull());
+  d_model[var] = value;
+  d_reason[var] = reason;
+}
+
+void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) {
+  TNode current = var;
+  do {
+    Debug("theory::idl::model") << "processing: " << var << std::endl;
+    Assert(d_reason.find(current) != d_reason.end());
+    IDLReason reason = d_reason[current];
+    Debug("theory::idl::model") << "adding reason: " << reason.constraint << std::endl;
+    reasons.push_back(reason.constraint);
+    current = reason.x;
+  } while (current != var);
+}
+
+void IDLModel::toStream(std::ostream& out) const {
+  model_value_map::const_iterator it = d_model.begin();
+  model_value_map::const_iterator it_end = d_model.end();
+  out << "Model[" << std::endl;
+  for (; it != it_end; ++ it) {
+    out << (*it).first << " -> " << (*it).second << std::endl;
+  }
+  out << "]";
+}
diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
new file mode 100644
index 000000000..a1840a35a
--- /dev/null
+++ b/src/theory/idl/idl_model.h
@@ -0,0 +1,67 @@
+#pragma once
+
+#include "expr/node.h"
+#include "context/cdhashmap.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * A reason for a value of a variable in the model is a constraint that implies
+ * this value by means of the value of another variable. For example, if the
+ * value of x is 0, then the variable x and the constraint (y > 0) are a reason
+ * for the y taking the value 1.
+ */
+struct IDLReason {
+  /** The variable of the reason */
+  TNode x;
+  /** The constraint of the reaason */
+  TNode constraint;
+
+  IDLReason(TNode x, TNode constraint)
+  : x(x), constraint(constraint) {}
+  IDLReason() {}
+};
+
+/**
+ * A model maps variables to integer values and backs them up with reasons.
+ * Default values (if not set with setValue) for all variables are 0.
+ */
+class IDLModel {
+
+  typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map;
+  typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> model_reason_map;
+
+  /** Values assigned to individual variables */
+  model_value_map d_model;
+
+  /** Reasons constraining the individual variables */
+  model_reason_map d_reason;
+
+public:
+
+  IDLModel(context::Context* context);
+
+  /** Get the model value of the variable */
+  Integer getValue(TNode var) const;
+
+  /** Set the value of the variable */
+  void setValue(TNode var, Integer value, IDLReason reason);
+
+  /** Get the cycle of reasons behind the variable var */
+  void getReasonCycle(TNode var, std::vector<TNode>& reasons);
+
+  /** Output to the given stream */
+  void toStream(std::ostream& out) const;
+
+};
+
+inline std::ostream& operator << (std::ostream& out, const IDLModel& model) {
+  model.toStream(out);
+  return out;
+}
+
+}
+}
+}
diff --git a/src/theory/idl/kinds b/src/theory/idl/kinds
new file mode 100644
index 000000000..6bf0218b0
--- /dev/null
+++ b/src/theory/idl/kinds
@@ -0,0 +1,8 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+alternate THEORY_ARITH "idl" ::CVC4::theory::idl::TheoryIdl "theory/idl/theory_idl.h"
+
diff --git a/src/theory/idl/options b/src/theory/idl/options
new file mode 100644
index 000000000..0048353b9
--- /dev/null
+++ b/src/theory/idl/options
@@ -0,0 +1,10 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module IDL "theory/idl/options.h" Idl
+
+option idlRewriteEq --enable-idl-rewrite-equalities/--disable-idl-rewrite-equalities bool :default false :read-write
+
+endmodule
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
new file mode 100644
index 000000000..bf2297d3d
--- /dev/null
+++ b/src/theory/idl/theory_idl.cpp
@@ -0,0 +1,126 @@
+#include "theory/idl/theory_idl.h"
+#include "theory/idl/options.h"
+#include "theory/rewriter.h"
+
+#include <set>
+#include <queue>
+
+using namespace std;
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
+                     Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
+: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
+, d_model(c)
+, d_assertionsDB(c)
+{}
+
+Node TheoryIdl::ppRewrite(TNode atom) {
+  if (atom.getKind() == kind::EQUAL  && options::idlRewriteEq()) {
+    // If the option is turned on, each equality into two inequalities. This in
+    // effect removes equalities, and theorefore dis-equalities too.
+    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+    return rewritten;
+  } else {
+    return atom;
+  }
+}
+
+void TheoryIdl::check(Effort level) {
+
+  while(!done()) {
+
+    // Get the next assertion
+    Assertion assertion = get();
+    Debug("theory::idl") << "TheoryIdl::check(): processing " << assertion.assertion << std::endl;
+
+    // Convert the assertion into the internal representation
+    IDLAssertion idlAssertion(assertion.assertion);
+    Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl;
+
+    if (idlAssertion.ok()) {
+      if (idlAssertion.getOp() == kind::DISTINCT) {
+        // We don't handle dis-equalities
+        d_out->setIncomplete();
+      } else {
+        // Process the convex assertions immediately
+        bool ok = processAssertion(idlAssertion);
+        if (!ok) {
+          // In conflict, we're done
+          return;
+        }
+      }
+    } else {
+      // Not an IDL assertion, set incomplete
+      d_out->setIncomplete();
+    }
+  }
+
+}
+
+bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
+
+  Debug("theory::idl") << "TheoryIdl::processAssertion(" << assertion << ")" << std::endl;
+
+  // Add the constraint (x - y op c) to the list assertions of x
+  d_assertionsDB.add(assertion, assertion.getX());
+
+  // Update the model, if forced by the assertion
+  bool y_updated = assertion.propagate(d_model);
+
+  // If the value of y was updated, we might need to update further
+  if (y_updated) {
+
+    std::queue<TNode> queue; // Queue of variables to consider
+    std::set<TNode> inQueue; // Current elements of the queue
+
+    // Add the first updated variable to the queue
+    queue.push(assertion.getY());
+    inQueue.insert(assertion.getY());
+
+    while (!queue.empty()) {
+      // Pop a new variable x off the queue
+      TNode x = queue.front();
+      queue.pop();
+      inQueue.erase(x);
+
+      // Go through the constraint (x - y op c), and update values of y
+      IDLAssertionDB::iterator it(d_assertionsDB, x);
+      while (!it.done()) {
+        // Get the assertion and update y
+        IDLAssertion x_y_assertion = it.get();
+        y_updated = x_y_assertion.propagate(d_model);
+        // If updated add to the queue
+        if (y_updated) {
+          // If the variable that we updated is the same as the first
+          // variable that we updated, it's a cycle of updates => conflict
+          if (x_y_assertion.getY() == assertion.getX()) {
+            std::vector<TNode> reasons;
+            d_model.getReasonCycle(x_y_assertion.getY(), reasons);
+            // Construct the reason of the conflict
+            Node conflict = NodeManager::currentNM()->mkNode(kind::AND, reasons);
+            d_out->conflict(conflict);
+            return false;
+          } else {
+            // No cycle, just a model update, so we add to the queue
+            TNode y = x_y_assertion.getY();
+            if (inQueue.count(y) == 0) {
+              queue.push(y);
+              inQueue.insert(x_y_assertion.getY());
+            }
+          }
+        }
+        // Go to the next constraint
+        it.next();
+      }
+    }
+  }
+
+  // Everything fine, no conflict
+  return true;
+}
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
new file mode 100644
index 000000000..25b992981
--- /dev/null
+++ b/src/theory/idl/theory_idl.h
@@ -0,0 +1,46 @@
+#pragma once
+
+#include "cvc4_private.h"
+
+#include "theory/theory.h"
+#include "theory/idl/idl_model.h"
+#include "theory/idl/idl_assertion_db.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * Handles integer difference logic (IDL) constraints.
+ */
+class TheoryIdl : public Theory {
+
+  /** The current model */
+  IDLModel d_model;
+
+  /** The asserted constraints, organized by variable */
+  IDLAssertionDB d_assertionsDB;
+
+  /** Process a new assertion, returns false if in conflict */
+  bool processAssertion(const IDLAssertion& assertion);
+
+public:
+
+  /** Theory constructor. */
+  TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
+            Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+
+  /** Pre-processing of input atoms */
+  Node ppRewrite(TNode atom);
+
+  /** Check the assertions for satisfiability */
+  void check(Effort effort);
+
+  /** Identity string */
+  std::string identify() const { return "THEORY_IDL"; }
+
+};/* class TheoryIdl */
+
+}/* CVC4::theory::idl namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */