diff options
| -rw-r--r-- | INCREMENTAL.md | 14 | ||||
| -rwxr-xr-x | matthew_test.sh | 2 | ||||
| -rw-r--r-- | src/theory/arith/idl/idl_extension.cpp | 307 | ||||
| -rw-r--r-- | src/theory/arith/idl/idl_extension.h | 34 |
4 files changed, 192 insertions, 165 deletions
diff --git a/INCREMENTAL.md b/INCREMENTAL.md deleted file mode 100644 index ebea125d5..000000000 --- a/INCREMENTAL.md +++ /dev/null @@ -1,14 +0,0 @@ -Some options for incremental solving - -The biggest issue is that we dont have an incremental matrix data structure. - -1. Just have a CDList<std::vector<std::vector<Rational>>> and push/pop the - entire state at each step. Should be fast, but is it too much memory usage? -2. Use a CDHashMap<std::pair<size_t, size_t>, Rational> instead -3. Use a CDHashMap<std::pair<size_t, size_t>, Rational> but do updates in a - local copy first so we dont overload it with updates -4. Can we do something like std::vector<CDHashMap>? Since the dimensions dont - change. -5. Something else entirely, like - -For now I will just do #4 since that seems simplest and not too horrible. diff --git a/matthew_test.sh b/matthew_test.sh index 066fe0fdb..9f9eb3460 100755 --- a/matthew_test.sh +++ b/matthew_test.sh @@ -3,7 +3,7 @@ set -e RUN_SIMPLE=false -GET_STATS=false +GET_STATS=true RUN_SMTLIB=500 TIMEOUT_SMTLIB=5m diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp index 044c7bb67..ee92c41ff 100644 --- a/src/theory/arith/idl/idl_extension.cpp +++ b/src/theory/arith/idl/idl_extension.cpp @@ -35,7 +35,7 @@ IdlExtension::IdlExtension(Env& env, TheoryArith& parent) d_parent(parent), d_varMap(context()), d_varList(context()), - conflict_cycle(context()), + d_facts(context()), d_numVars(0) { // Thanks to Andres and Aina for clarifying how to get an internal variable! @@ -69,9 +69,9 @@ void IdlExtension::presolve() // Initialize adjacency matrix. for (size_t i = 0; i < d_numVars; ++i) { - d_matrix.push_back(context::CDHashMap(context())); - // d_next.emplace_back(context()); - // d_facts.emplace_back(context()); + d_matrix.emplace_back(d_numVars); + d_matrix_facts.emplace_back(d_numVars); + d_valid.emplace_back(d_numVars, false); } } @@ -80,93 +80,7 @@ void IdlExtension::notifyFact( { Trace("theory::arith::idl") << "IdlExtension::notifyFact(): processing " << fact << std::endl; - - if (!conflict_cycle.empty()) return; - - // TODO: Check that atom, pol, fact, are correct as assumed by this code - // copied from processAssertion... - Assert(atom.getKind() == kind::LEQ); - Assert(atom[0].getKind() == kind::MINUS); - TNode var1 = atom[0][0]; - TNode var2 = atom[0][1]; - - Rational value = (atom[1].getKind() == kind::UMINUS) - ? -atom[1][0].getConst<Rational>() - : atom[1].getConst<Rational>(); - - if (!pol) - { - std::swap(var1, var2); - value = -value - Rational(1); - } - - size_t index1 = d_varMap[var1]; - size_t index2 = d_varMap[var2]; - - if (d_matrix[index1].count(index2) && d_matrix[index1][index2].get() < value) { - // This does not tighten it at all. - return; - } - Rational zero = Rational(); - if (index1 == index2) { - if (value < zero) { - // This is already a conflict. - conflict_cycle.push_back(fact); - } - // In either case, don't do anything else (we have an implicit zero in that - // cell). - return; - } - // Otherwise, update that cell. - d_matrix[index1].insert(index2, value); - d_next[index1].insert(index2, index2); - d_facts[index1].insert(index2, fact); - // Do the incremental update. - std::vector<size_t> touched(d_numVars); - std::vector<size_t> worklist{index1, index2}; - while (worklist.size()) { - size_t k = worklist.back(); - worklist.pop_back(); - for (size_t i = 0; i < d_numVars; i++) { - if (!(d_matrix[i].count(k))) continue; // TODO replace this with an iter over keys - const Rational &i_to_k = d_matrix[i][k].get(); - for (size_t j = 0; i < d_numVars; i++) { - if (!(d_matrix[k].count(j))) continue; - const Rational &k_to_j = d_matrix[k][j].get(); - if (i == j) { - if (i_to_k + k_to_j < zero) { - // Trace back a cycle from i to i - size_t last = i, - next = d_next[i][k].get(); - while (next != i) { - // Update the cycle with the edge last->next - Assert(d_facts[last].count(next)); - conflict_cycle.push_back(d_facts[last][next].get()); - // Update last/next - last = next; - Assert(d_next[last].count(i)); - next = d_next[last][i].get(); - } - return; - } - } else { // i != j - if (!(d_matrix[i].count(j)) - || d_matrix[i][j].get() > i_to_k + k_to_j) { - d_matrix[i].insert(j, i_to_k + k_to_j); - d_next[i].insert(j, d_next[i][k].get()); - if (!(touched[i])) { - touched[i] = true; - worklist.push_back(i); - } - if (!(touched[j])) { - touched[j] = true; - worklist.push_back(j); - } - } - } - } - } - } + d_facts.push_back(fact); } Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) @@ -315,22 +229,46 @@ void IdlExtension::postCheck(Theory::Effort level) << "IdlExtension::postCheck(): number of facts = " << d_facts.size() << std::endl; - if (conflict_cycle.empty()) return; + // Reset the graph + for (size_t i = 0; i < d_numVars; i++) + { + for (size_t j = 0; j < d_numVars; j++) + { + d_valid[i][j] = false; + } + } + + for (Node fact : d_facts) + { + // For simplicity, we reprocess all the literals that have been asserted to + // this theory solver. A better implementation would process facts in + // notifyFact(). + Trace("theory::arith::idl") + << "IdlExtension::check(): processing " << fact << std::endl; + processAssertion(fact); + } - // Return a conflict that includes all the literals that have been asserted - // to this theory solver. A better implementation would only include the - // literals involved in the conflict here. - NodeBuilder conjunction(kind::AND); - for (Node fact : conflict_cycle) + std::vector<std::vector<TNode>> negative_cycles = negativeCycles(); + if (negative_cycles.size()) { - conjunction << fact; + for (const auto &negative_cycle : negative_cycles) { + // Return a conflict that includes all the literals that have been asserted + // to this theory solver. A better implementation would only include the + // literals involved in the conflict here. + NodeBuilder conjunction(kind::AND); + for (Node fact : negative_cycle) + { + conjunction << fact; + } + Node conflict = conjunction; + // Send the conflict using the inference manager. Each conflict is assigned + // an ID. Here, we use ARITH_CONF_IDL_EXT, which indicates a generic + // conflict detected by this extension + d_parent.getInferenceManager().conflict(conflict, + InferenceId::ARITH_CONF_IDL_EXT); + } + return; } - Node conflict = conjunction; - // Send the conflict using the inference manager. Each conflict is assigned - // an ID. Here, we use ARITH_CONF_IDL_EXT, which indicates a generic - // conflict detected by this extension - d_parent.getInferenceManager().conflict(conflict, - InferenceId::ARITH_CONF_IDL_EXT); } // Idea is to assign each node its shortest distance from any other given node @@ -343,38 +281,143 @@ void IdlExtension::postCheck(Theory::Effort level) bool IdlExtension::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) { - // TODO: With incremental... - // std::vector<Rational> distance(d_numVars, Rational(0)); - - // 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; - // } - - // Rational offset = Rational(); - // if (d_varMap.count(zero_node)) { - // offset = distance[d_varMap[zero_node]]; - // } - - // NodeManager* nm = NodeManager::currentNM(); - // for (size_t i = 0; i < d_numVars; i++) - // { - // // Assert that the variable's value is equal to its distance in the model - // m->assertEquality(d_varList[i], nm->mkConstInt(distance[i] - offset), true); - // } + std::vector<Rational> distance(d_numVars, Rational(0)); + + 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; + } + + Rational offset = Rational(); + if (d_varMap.count(zero_node)) { + offset = distance[d_varMap[zero_node]]; + } + + NodeManager* nm = NodeManager::currentNM(); + for (size_t i = 0; i < d_numVars; i++) + { + // Assert that the variable's value is equal to its distance in the model + m->assertEquality(d_varList[i], nm->mkConstInt(distance[i] - offset), true); + } return true; } +void IdlExtension::processAssertion(TNode assertion) +{ + bool polarity = assertion.getKind() != kind::NOT; + TNode atom = polarity ? assertion : assertion[0]; + Assert(atom.getKind() == kind::LEQ); + Assert(atom[0].getKind() == kind::MINUS); + TNode var1 = atom[0][0]; + TNode var2 = atom[0][1]; + + Rational value = (atom[1].getKind() == kind::UMINUS) + ? -atom[1][0].getConst<Rational>() + : atom[1].getConst<Rational>(); + + if (!polarity) + { + std::swap(var1, var2); + value = -value - Rational(1); + } + + 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; + d_matrix_facts[index1][index2] = assertion; +} + + +// From different attempts: +// 1. Reporting more cycles here doesn't necessarily help (and can often hurt). +// Hence moving to Floyd-Warshall where we only return one. +// 2. Bellman-Ford stops early on sat, but has worst-case on unsat. +// Floyd-Warshall is the opposite. It seems to be more important to stop +// early on unsat, because (roughly) all but the last theory propagation is +// going to be unsat. +// Bellman-Ford time on smallest 75 benchmarks: ~2m34s +// Floyd-Warshall: 48s +std::vector<std::vector<TNode>> IdlExtension::negativeCycles() +{ + std::vector<std::vector<TNode>> cycles; + Rational zero = Rational(); + + // Setup + std::vector<std::vector<Rational>> distance; + std::vector<std::vector<bool>> reachable; + std::vector<std::vector<size_t>> next; + for (size_t i = 0; i < d_numVars; i++) { + distance.emplace_back(d_numVars, zero); + reachable.emplace_back(d_numVars, false); + next.emplace_back(d_numVars, 0); + for (size_t j = 0; j < d_numVars; j++) { + if (i == j) { + if (d_valid[i][j] && d_matrix[i][i] < zero) { + cycles.push_back(std::vector<TNode>{d_matrix_facts[i][i]}); + return cycles; + } + reachable[i][i] = true; + // already: distance[i][i] = zero; + next[i][i] = i; + } else if (d_valid[i][j]) { + reachable[i][j] = true; + distance[i][j] = d_matrix[i][j]; + next[i][j] = j; + } else { + // already: reachable[i][j] = false; + } + } + } + + // Floyd-Warshall + for (size_t k = 0; k < d_numVars; k++) { + for (size_t i = 0; i < d_numVars; i++) { + if (!reachable[i][k]) continue; + for (size_t j = 0; j < d_numVars; j++) { + if (!reachable[k][j]) continue; + if (!reachable[i][j] + || distance[i][j] > distance[i][k] + distance[k][j]) { + reachable[i][j] = true; + distance[i][j] = distance[i][k] + distance[k][j]; + next[i][j] = next[i][k]; + if (i == j && distance[i][j] < zero) { + // Trace back the cycle and return. + std::vector<size_t> idx_cycle{i}; + do { + idx_cycle.push_back(next[idx_cycle.back()][i]); + } while (idx_cycle.back() != i); + Assert(idx_cycle.size() > 1); + std::vector<TNode> cycle; + for (size_t c = 0; c < idx_cycle.size() - 1; c++) { + cycle.emplace_back(d_matrix_facts[idx_cycle[c]][idx_cycle[c+1]]); + } + cycles.emplace_back(cycle); + return cycles; + } + } + } + } + } + Assert(cycles.empty()); + return cycles; +} + void IdlExtension::printMatrix(const std::vector<std::vector<Rational>>& matrix, const std::vector<std::vector<bool>>& valid) { diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h index 2ba08b86f..06ec78130 100644 --- a/src/theory/arith/idl/idl_extension.h +++ b/src/theory/arith/idl/idl_extension.h @@ -19,7 +19,6 @@ #define CVC5__THEORY__ARITH__IDL__IDL_EXTENSION_H #include "context/cdlist.h" -#include "context/cdhashmap.h" #include "smt/env_obj.h" #include "theory/skolem_lemma.h" #include "theory/theory.h" @@ -49,7 +48,7 @@ class IdlExtension : protected EnvObj /** Called for each asserted literal */ void notifyFact( - TNode atom, bool pol, TNode assertion, bool isPrereg, bool isInternal); + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom, std::vector<SkolemLemma>& lems); @@ -61,6 +60,9 @@ class IdlExtension : protected EnvObj bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet); private: + /** Process a new assertion */ + void processAssertion(TNode assertion); + /** Returns a vector containing paths (vector of sequential edges/assertions) * corresponding to negative cycles in the graph. Returns the empty vector * iff there are no negative cycles. @@ -82,25 +84,21 @@ class IdlExtension : protected EnvObj /** Context-dependent vector of variables */ context::CDList<TNode> d_varList; - /*** NOTE: The below four data structures are *only* added to if there is no - * negative cycle --- as soon as a negative cycle is found, conflict_cycle - * is updated and they are 'frozen' until a pop happens to clear - * conflict_cycle. */ - /*** NOTE: I would like to do std::vector<CDHashMap<size_t, Rational>>, but I - * guess std::vector requires a copy constructor, which CDHashMap doesn't - * have...We could make that work, probably, with vector<ptr<CDHashMap>>, - * but that just seems more trouble than it's worth. */ - /** d_matrix[i][j] = tightest edge weight from i to j (if exists). */ - std::vector<context::CDHashMap<size_t, Rational>> d_matrix; - /** d_next[i][j] = the first node along the shortest path from i->j (if exists). */ - std::vector<context::CDHashMap<size_t, size_t>> d_next; - /** d_facts[i][j] stores the literal that is responsible for edge i->j. */ - std::vector<context::CDHashMap<size_t, TNode>> d_facts; - /** If a conflict (negative cycle) is found, it is stored here. */ - context::CDList<TNode> conflict_cycle; + /** Context-dependent list of asserted theory literals */ + context::CDList<TNode> d_facts; + + /** i,jth entry is true iff there is an edge from i to j. */ + std::vector<std::vector<bool>> d_valid; + + /** i,jth entry stores weight for edge from i to j. */ + std::vector<std::vector<Rational>> d_matrix; + + /** i,jth entry stores the literal that is responsible for this edge. */ + std::vector<std::vector<TNode>> d_matrix_facts; /** Shifted to zero always in the model. */ Node zero_node; + /** Number of variables in the graph */ size_t d_numVars; }; /* class IdlExtension */ |