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

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

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 \

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 \

src/theory/idl/Makefile

@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/rdl
+
+include $(topdir)/Makefile.subdir

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 

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;
+}

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;
+}
+
+}
+}
+}

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;
+}