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

1 files changed, 196 insertions, 0 deletions

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