diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh deleted file mode 100644 index 9be53967f..000000000 --- a/scripts/vsts-mac.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/sh - -cd .. -mkdir build -CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py --java --python -cd build -make -make test-z3 -make cpp_example -make c_example -# make java_example -# make python_example -./cpp_example -./test_capi - -git clone https://github.com/z3prover/z3test.git z3test -ls -python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2 - diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 35d594b34..a6e036408 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -245,14 +245,14 @@ namespace sat { m_pos.push_back(l); m_neg.push_back(~l); } -#if 1 compare_left cmp(big); std::sort(m_pos.begin(), m_pos.end(), cmp); std::sort(m_neg.begin(), m_neg.end(), cmp); -#else - radix_sort(big, m_pos); - radix_sort(big, m_neg); -#endif + + // alternative: worse + // radix_sort(big, m_pos); + // radix_sort(big, m_neg); + IF_VERBOSE(100, for (literal l : m_pos) verbose_stream() << big.get_left(l) << " "; verbose_stream() << "\n"; diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 3443625cf..2f1a3727f 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -164,8 +164,19 @@ namespace sat { DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);}); } - unsigned big::reduce_tr(solver& s) { + // svector> big::s_del_bin; + bool big::in_del(literal u, literal v) const { + if (u.index() > v.index()) std::swap(u, v); + return m_del_bin.contains(std::make_pair(u, v)); + } + + void big::add_del(literal u, literal v) { + if (u.index() > v.index()) std::swap(u, v); + m_del_bin.push_back(std::make_pair(u, v)); + } + + unsigned big::reduce_tr(solver& s) { unsigned num_lits = s.num_vars() * 2; unsigned idx = 0; unsigned elim = 0; @@ -182,7 +193,8 @@ namespace sat { literal v = w.get_literal(); if (u != get_parent(v) && safe_reach(u, v)) { ++elim; - m_del_bin.push_back(std::make_pair(~u, v)); + add_del(~u, v); + // IF_VERBOSE(1, verbose_stream() << "remove " << u << " -> " << v << "\n"); if (find_binary_watch(wlist, ~v)) { IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n"); s.assign(~u, justification()); @@ -197,6 +209,23 @@ namespace sat { } wlist.set_end(itprev); } + +#if 0 + s_del_bin.append(m_del_bin); + IF_VERBOSE(1, + display(verbose_stream() << "Learned: " << learned() << ":"); + verbose_stream() << "del-bin\n"; + for (auto p : m_del_bin) { + verbose_stream() << p.first << " " << p.second << "\n"; + if (safe_reach(~p.first, p.second)) { + display_path(verbose_stream(), ~p.first, p.second) << " " << "\n"; + } + else { + display_path(verbose_stream(), ~p.second, p.first) << " " << "\n"; + } + } + ); +#endif s.propagate(false); return elim; } @@ -205,8 +234,7 @@ namespace sat { if (!reaches(u, v)) return false; while (u != v) { literal w = next(u, v); - if (m_del_bin.contains(std::make_pair(~u, w)) || - m_del_bin.contains(std::make_pair(~w, u))) { + if (in_del(~u, w)) { return false; } u = w; @@ -216,11 +244,27 @@ namespace sat { literal big::next(literal u, literal v) const { SASSERT(reaches(u, v)); + literal result = null_literal; + int left = m_right[u.index()]; + // identify the path from the reachability graph for (literal w : m_dag[u.index()]) { - if (reaches(u, w) && (w == v || reaches(w, v))) return w; + if (reaches(u, w) && + (w == v || reaches(w, v)) && + m_left[w.index()] < left) { + left = m_left[w.index()]; + result = w; + } } - UNREACHABLE(); - return null_literal; + SASSERT(result != null_literal); + return result; + } + + std::ostream& big::display_path(std::ostream& out, literal u, literal v) const { + while (u != v) { + out << u << " -> "; + u = next(u, v); + } + return out << v; } void big::display(std::ostream& out) const { @@ -228,6 +272,12 @@ namespace sat { for (auto& next : m_dag) { if (!next.empty()) { out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n"; +#if 0 + for (literal n : next) { + out << n << "[" << m_left[n.index()] << ":" << m_right[n.index()] << "] "; + } + out << "\n"; +#endif } ++idx; } diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index c9d47f82c..f2adf9ad8 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -45,8 +45,15 @@ namespace sat { bool safe_reach(literal u, literal v); literal next(literal u, literal v) const; + std::ostream& display_path(std::ostream& out, literal u, literal v) const; + + void add_del(literal u, literal v); + bool in_del(literal u, literal v) const; + public: + // static svector> s_del_bin; + big(random_gen& rand); /** \brief initialize a BIG from a solver. diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 3d0899692..c0c6fabe4 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -117,19 +117,13 @@ namespace sat { else { unsigned new_sz = j; CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n"; - if (c.size() > 0) tout << "unit: " << c[0] << "\n";); - SASSERT(c.frozen() || new_sz >= 2); + if (c.size() > 0) tout << "unit: " << c[0] << "\n"; + s.display_watches(tout);); if (new_sz == 0) { - // It can only happen with frozen clauses. - // active clauses would have signed the conflict. - SASSERT(c.frozen()); s.set_conflict(justification()); s.del_clause(c); } else if (new_sz == 1) { - // It can only happen with frozen clauses. - // active clauses would have propagated the literal - SASSERT(c.frozen()); s.assign(c[0], justification()); s.del_clause(c); } @@ -188,6 +182,7 @@ namespace sat { CASSERT("cleaner_bug", s.check_invariant()); unsigned trail_sz = s.m_trail.size(); s.propagate(false); // make sure that everything was propagated. + TRACE("sat_cleaner_bug", s.display(tout); s.display_watches(tout);); if (s.m_inconsistent) return false; if (m_last_num_units == trail_sz) diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 850a33cef..56a5b6e6c 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -33,8 +33,8 @@ def_module_params('sat', ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.check_unsat', BOOL, False, 'build up internal proof and check'), ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'), - ('cardinality.solver', BOOL, False, 'use cardinality solver'), - ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'), + ('cardinality.solver', BOOL, True, 'use cardinality solver'), + ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'), ('xor.solver', BOOL, False, 'use xor solver'), ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search', BOOL, False, 'use local search instead of CDCL'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 47a456b24..a2ef176a1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1634,6 +1634,15 @@ namespace sat { } TRACE("sat_mc_bug", m_mc.display(tout);); +#if 0 + IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + for (auto p : big::s_del_bin) { + if (value(p.first) != l_true && value(p.second) != l_true) { + IF_VERBOSE(0, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n"); + } + } +#endif + IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";); if (!check_clauses(m_model)) { throw solver_exception("check model failed");