Initial working

6 files changed, 222 insertions, 19 deletions

diff --git a/.lvimrc b/.lvimrc
new file mode 100644
index 000000000..c9f7e9149
--- /dev/null
+++ b/.lvimrc
@@ -0,0 +1,2 @@
+set shiftwidth=2
+set softtabstop=2
diff --git a/matthew_conf.sh b/matthew_conf.sh
new file mode 100755
index 000000000..c047f3a2f
--- /dev/null
+++ b/matthew_conf.sh
@@ -0,0 +1,2 @@
+#!/bin/bash
+./configure.sh debug --ubsan --asan --auto-download
diff --git a/sdev.sh b/sdev.sh
new file mode 100755
index 000000000..c4354625c
--- /dev/null
+++ b/sdev.sh
@@ -0,0 +1,2 @@
+#!/bin/bash
+srun --time 24:00:00 --ntasks=1 --cpus-per-task=16 --pty bash
diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 0149dde20..246e420ec 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -64,6 +64,8 @@ void IdlExtension::presolve()
   for (size_t i = 0; i < d_numVars; ++i)
   {
     d_matrix.emplace_back(d_numVars);
+    n_matrix.emplace_back(d_numVars);
+    n_reachable.emplace_back(d_numVars, false);
     d_valid.emplace_back(d_numVars, false);
   }
 }
@@ -95,16 +97,27 @@ Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     switch (atom.getKind())
     {
       // -------------------------------------------------------------------------
-      // TODO: Handle these cases.
+      // DONE: Handle these cases.
       // -------------------------------------------------------------------------
-      case kind::EQUAL:
-      case kind::LT:
-      case kind::LEQ:
-      case kind::GT:
-      case kind::GEQ:
+      case kind::EQUAL: // c == x == x == c
+        k = kind::EQUAL;
+        break;
+      case kind::LT: // c < x == x > c
+        k = kind::GT;
+        break;
+      case kind::LEQ: // c <= x == x >= c
+        k = kind::GEQ;
+        break;
+      case kind::GT: // c > x == x < c
+        k = kind::LT;
+        break;
+      case kind::GEQ: // c >= x == x <= c
+        k = kind::LEQ;
+        break;
       default: break;
     }
 
+    Assert(!(atom[1].getKind() == kind::CONST_RATIONAL));
     return ppRewrite(nm->mkNode(k, atom[1], atom[0]), lems);
   }
   else if (atom[1].getKind() == kind::VARIABLE)
@@ -113,11 +126,44 @@ Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     // x and y are variables
     Node ret = atom;
     // -------------------------------------------------------------------------
-    // TODO: Handle this case.
+    // DONE: Handle this case.
     // -------------------------------------------------------------------------
+    switch (atom.getKind())
+    {
+      case kind::EQUAL: // x == y == x - y <= 0 ^ y - x <= 0
+      {
+        Node left_1 = nm->mkNode(kind::MINUS, atom[0], atom[1]);
+        Node left_2 = nm->mkNode(kind::MINUS, atom[1], atom[0]);
+        return nm->mkNode(kind::AND,
+            nm->mkNode(kind::LEQ, left_1, nm->mkConstInt(0)),
+            nm->mkNode(kind::LEQ, left_2, nm->mkConstInt(0)));
+      }
+      case kind::LT: // x < y == x - y < 0 == x - y <= -1
+      {
+        Node lhs = nm->mkNode(kind::MINUS, atom[0], atom[1]);
+        return nm->mkNode(kind::LEQ, lhs, nm->mkConstInt(-1));
+      }
+      case kind::LEQ: // x <= y == x - y <= 0
+      {
+        Node lhs = nm->mkNode(kind::MINUS, atom[0], atom[1]);
+        return nm->mkNode(kind::LEQ, lhs, nm->mkConstInt(0));
+      }
+      case kind::GT: // x > y == x - y > 0 == y - x < 0 == y - x <= -1
+      {
+        Node lhs = nm->mkNode(kind::MINUS, atom[1], atom[0]);
+        return nm->mkNode(kind::LEQ, lhs, nm->mkConstInt(-1));
+      }
+      case kind::GEQ: // x >= y == x - y >= 0 == y - x <= 0
+      {
+        Node lhs = nm->mkNode(kind::MINUS, atom[1], atom[0]);
+        return nm->mkNode(kind::LEQ, lhs, nm->mkConstInt(0));
+      }
+      default: break;
+    }
     return ppRewrite(ret, lems);
   }
 
+  // NOTE: Does *NOT* handle cases like x = 5.
   switch (atom.getKind())
   {
     case kind::EQUAL:
@@ -132,12 +178,30 @@ Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     }
 
     // -------------------------------------------------------------------------
-    // TODO: Handle these cases.
+    // DONE: Handle these cases.
     // -------------------------------------------------------------------------
-    case kind::LT:
-    case kind::LEQ:
-    case kind::GT:
-    case kind::GEQ:
+    case kind::LT: // a - b < c == a - b <= c - 1 (integers)
+    {
+      Assert(atom[0].getKind() == kind::MINUS);
+      const Rational& right = atom[1].getConst<Rational>();
+      Node tight_right = nm->mkConstInt(right - 1);
+      return nm->mkNode(kind::LEQ, atom[0], tight_right);
+    }
+    case kind::LEQ: return atom;
+    case kind::GT: // a - b > c == -(a - b) < -c == b - a <= -c - 1
+    {
+      Node negated_left = nm->mkNode(kind::MINUS, atom[0][1], atom[0][0]);
+      const Rational& right = atom[1].getConst<Rational>();
+      Node updated_right = nm->mkConstInt(-right - 1);
+      return nm->mkNode(kind::LEQ, negated_left, updated_right);
+    }
+    case kind::GEQ: // a - b >= c == b - a <= -c
+    {
+      Node negated_left = nm->mkNode(kind::MINUS, atom[0][1], atom[0][0]);
+      const Rational& right = atom[1].getConst<Rational>();
+      Node negated_right = nm->mkConstInt(-right);
+      return nm->mkNode(kind::LEQ, negated_left, negated_right);
+    }
       // -------------------------------------------------------------------------
 
     default: break;
@@ -195,15 +259,31 @@ void IdlExtension::postCheck(Theory::Effort level)
   }
 }
 
+// Idea is to assign each node its shortest distance from any other given node
+// (including itself). Flip the directions of the edges, so x->y is the upper
+// bound of y-x. Then for an edge x->y, we want to guarantee that y-x is _at
+// most_ the value e of that edge.  Suppose y - x > e, then we could take the
+// path x->y which would have weight x+e. But then from the supposition we get
+// y > x + e, contradicting the claim about the value at y being the weight of
+// the shortest path.
 bool IdlExtension::collectModelInfo(TheoryModel* m,
                                     const std::set<Node>& termSet)
 {
   std::vector<Rational> distance(d_numVars, Rational(0));
 
-  // ---------------------------------------------------------------------------
-  // TODO: implement model generation by computing the single-source shortest
-  // path from a node that has distance zero to all other nodes
-  // ---------------------------------------------------------------------------
+  Rational zero = Rational(); // 0 constructor
+  for (size_t k = 0; k < d_numVars; k++) {
+    bool changed_anything = false;
+    for (size_t i = 0; i < d_numVars; i++) {
+      for (size_t j = 0; j < d_numVars; j++) {
+        if (d_valid[i][j] && distance[j] + d_matrix[i][j] < distance[i]) {
+          distance[i] = distance[j] + d_matrix[i][j];
+          changed_anything = true;
+        }
+      }
+    }
+    if (!changed_anything) break;
+  }
 
   NodeManager* nm = NodeManager::currentNM();
   for (size_t i = 0; i < d_numVars; i++)
@@ -237,15 +317,62 @@ void IdlExtension::processAssertion(TNode assertion)
   size_t index1 = d_varMap[var1];
   size_t index2 = d_varMap[var2];
 
+  // Don't update in the case of (assert (<= X 5)), (assert (<= X 6)).
+  if (d_valid[index1][index2] && d_matrix[index1][index2] < value) {
+    return;
+  }
   d_valid[index1][index2] = true;
   d_matrix[index1][index2] = value;
 }
 
+// Improvements:
+// (1) Better algorithm. This one is roughly Floyd-Warshall. Bellman-Ford lets
+//     us do O(VE), but right now I'm not explicitly constructing E so it ends
+//     up being O(V^3) anyways, with the downside that we can't do
+//     early-stopping.
+// (2) Don't use Fraction. Either multiply through by the common denominators
+//     or use intervals or something. Or do a fast first pass through that
+//     over-approximates, followed by a verification round of that proposed
+//     negative cycle.
+// (3) Better initialization of n_matrix; maybe just copy d_matrix and modify
+//     that or something else.
+// (4) Parallelize, or just try sampling random cycles according to some
+//     heuristic.
 bool IdlExtension::negativeCycle()
 {
-  // --------------------------------------------------------------------------
-  // TODO: write the code to detect a negative cycle.
-  // --------------------------------------------------------------------------
+  // Initialize the n matrix. i -> i starts at 0, otherwise is just whatever
+  // the value of the edge weight is.
+  for (size_t i = 0; i < d_numVars; i++) {
+    for (size_t j = 0; j < d_numVars; j++) {
+      if (i == j) {
+        n_matrix[i][j] = Rational(); // 0 constructor
+        n_reachable[i][j] = true;
+      } else if (d_valid[i][j]) {
+        n_matrix[i][j] = d_matrix[i][j];
+        n_reachable[i][j] = true;
+      } else {
+        // 'inf'
+        n_reachable[i][j] = false;
+      }
+    }
+  }
+
+  Rational zero = Rational(); // 0 constructor
+  for (size_t k = 0; k < d_numVars; k++) {
+    for (size_t i = 0; i < d_numVars; i++) {
+      if (!n_reachable[i][k]) continue;
+      for (size_t j = 0; j < d_numVars; j++) {
+        if (!n_reachable[k][j]) continue;
+        if (!n_reachable[i][j] || n_matrix[i][k] + n_matrix[k][j] < n_matrix[i][j]) {
+          n_matrix[i][j] = n_matrix[i][k] + n_matrix[k][j];
+          n_reachable[i][j] = true;
+          if (i == j && n_matrix[i][j] < zero) {
+            return true;
+          }
+        }
+      }
+    }
+  }
 
   return false;
 }
diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h
index 8d854484d..9cd972c03 100644
--- a/src/theory/arith/idl/idl_extension.h
+++ b/src/theory/arith/idl/idl_extension.h
@@ -90,6 +90,10 @@ class IdlExtension : protected EnvObj
   /** i,jth entry stores weight for edge from i to j. */
   std::vector<std::vector<Rational>> d_matrix;
 
+  /** Essentially a normalized form of d_matrix. */
+  std::vector<std::vector<Rational>> n_matrix;
+  std::vector<std::vector<bool>> n_reachable;
+
   /** Number of variables in the graph */
   size_t d_numVars;
 }; /* class IdlExtension */
diff --git a/test/regress/regress0/idl/matthew-many-syntax.smt2 b/test/regress/regress0/idl/matthew-many-syntax.smt2
new file mode 100644
index 000000000..5d364b577
--- /dev/null
+++ b/test/regress/regress0/idl/matthew-many-syntax.smt2
@@ -0,0 +1,66 @@
+; COMMAND-LINE: --arith-idl-ext
+(set-option :produce-models true)
+(set-logic QF_IDL)
+(set-info :source |Tests out a variety of syntaxes that the rewriter should support
+Matthew Sotoudeh
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+; Should support:
+; - [const] [op] [var]
+; - [var] [op] [var]
+; - [var] [op] [const]
+; Where op \in { =, <, <=, >=, > }
+; =
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= 5 (- x z)))
+(assert (= y z))
+(assert (= (- x y) 5))
+; (assert (= x 0))
+; (assert (= y -5))
+; (assert (= z -5))
+; <
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+(assert (< 5 (- a b)))
+(assert (< b a))
+(assert (< (- a c) 5))
+; (assert (= a 0))
+; (assert (= b -6))
+; (assert (= c 0))
+; <=
+(declare-const d Int)
+(declare-const e Int)
+(declare-const f Int)
+(assert (<= 5 (- d e)))
+(assert (<= e d))
+(assert (<= (- d f) 5))
+; (assert (= d 0))
+; (assert (= e -5))
+; (assert (= f -5))
+; >=
+(declare-const g Int)
+(declare-const h Int)
+(declare-const i Int)
+(assert (>= 5 (- g h)))
+(assert (>= g h))
+(assert (>= (- g i) 5))
+; (assert (= g 0))
+; (assert (= h 0))
+; (assert (= i -5))
+; >
+(declare-const j Int)
+(declare-const k Int)
+(declare-const l Int)
+(assert (> 5 (- j k)))
+(assert (> j k))
+(assert (> (- j l) 5))
+; (assert (= j 0))
+; (assert (= k -1))
+; (assert (= l -6))
+(check-sat)
+(get-model)