diff options
-rw-r--r-- | .lvimrc | 2 | ||||
-rwxr-xr-x | matthew_conf.sh | 2 | ||||
-rwxr-xr-x | sdev.sh | 2 | ||||
-rw-r--r-- | src/theory/arith/idl/idl_extension.cpp | 165 | ||||
-rw-r--r-- | src/theory/arith/idl/idl_extension.h | 4 | ||||
-rw-r--r-- | test/regress/regress0/idl/matthew-many-syntax.smt2 | 66 |
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) |