From 074e851d4972ff3f2b45ec3e8f53a83575ab6eeb Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 15 Nov 2013 12:58:11 -0800 Subject: [PATCH 1/6] Display Fu Malik statistics --- src/opt/fu_malik.cpp | 89 ++++++++++++++++++++++++---- src/opt/opt_solver.cpp | 12 +++- src/opt/opt_solver.h | 6 +- src/sat/sat_solver.cpp | 3 +- src/smt/tactic/smt_tactic.cpp | 1 + src/solver/tactic2solver.cpp | 8 ++- src/tactic/smtlogics/qfbv_tactic.cpp | 14 ++--- 7 files changed, 104 insertions(+), 29 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 77eb108a9..235fa4205 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -22,6 +22,7 @@ Notes: #include "tactic2solver.h" #include "goal.h" #include "probe.h" +#include "tactic.h" #include "smt_context.h" /** @@ -41,16 +42,16 @@ Notes: namespace opt { struct fu_malik::imp { - ast_manager& m; - ref m_s; + ast_manager& m; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; expr_ref_vector m_assignment; unsigned m_upper_size; + ref m_s; solver & m_original_solver; - bool m_use_new_bv_solver; + bool m_use_new_bv_solver; imp(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), @@ -82,6 +83,63 @@ namespace opt { * add at-most-one constraint with blocking */ + typedef obj_hashtable expr_set; + + void set2vector(expr_set const& set, expr_ref_vector & es) const { + es.reset(); + expr_set::iterator it = set.begin(), end = set.end(); + for (; it != end; ++it) { + es.push_back(*it); + } + } + + void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const { + set.reset(); + expr_set::iterator it = set1.begin(), end = set1.end(); + for (; it != end; ++it) { + set.insert(*it); + } + it = set2.begin(); + end = set2.end(); + for (; it != end; ++it) { + set.insert(*it); + } + } + + void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) { + if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { + core.reset(); + return; + } + + SASSERT(!literals.empty()); + if (literals.size() == 1) { + core.reset(); + core.insert(literals[0].get()); + return; + } + + unsigned mid = literals.size()/2; + expr_ref_vector ls1(m), ls2(m); + ls1.append(mid, literals.c_ptr()); + ls2.append(literals.size()-mid, literals.c_ptr() + mid); + + expr_ref_vector as1(m); + as1.append(assumptions); + as1.append(ls1); + expr_set core2; + quick_explain(as1, ls2, !ls1.empty(), core2); + + expr_ref_vector as2(m), cs2(m); + as2.append(assumptions); + set2vector(core2, cs2); + as2.append(cs2); + expr_set core1; + quick_explain(as2, ls1, !core2.empty(), core1); + + set_union(core1, core2, core); + } + lbool step() { IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";); expr_ref_vector assumptions(m), block_vars(m); @@ -95,12 +153,14 @@ namespace opt { ptr_vector core; if (m_use_new_bv_solver) { - unsigned i = 0; - while (s().check_sat(core.size(), core.c_ptr()) != l_false) { - IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";); - core.push_back(assumptions[i].get()); - ++i; + expr_set core_set; + expr_ref_vector empty(m); + quick_explain(empty, assumptions, true, core_set); + expr_set::iterator it = core_set.begin(), end = core_set.end(); + for (; it != end; ++it) { + core.push_back(*it); } + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";); } else { s().get_unsat_core(core); @@ -164,11 +224,11 @@ namespace opt { probe *p = mk_is_qfbv_probe(); bool all_bv = (*p)(g).is_true(); if (all_bv) { - opt_solver & os = opt_solver::to_opt(m_original_solver); - smt::context & ctx = os.get_context(); - tactic* t = mk_qfbv_tactic(m, ctx.get_params()); + opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + smt::context & ctx = opt_s.get_context(); + tactic_ref t = mk_qfbv_tactic(m, ctx.get_params()); // The new SAT solver hasn't supported unsat core yet - m_s = mk_tactic2solver(m, t); + m_s = mk_tactic2solver(m, t.get()); SASSERT(m_s != &m_original_solver); for (unsigned i = 0; i < num_assertions; ++i) { m_s->assert_expr(current_solver.get_assertion(i)); @@ -211,6 +271,11 @@ namespace opt { } } } + statistics st; + s().collect_statistics(st); + SASSERT(st.size() > 0); + opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + opt_s.set_interim_stats(st); // We are done and soft_constraints has // been updated with the max-sat assignment. return is_sat; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index fee4a8663..a8e7d8535 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -55,7 +55,13 @@ namespace opt { } void opt_solver::collect_statistics(statistics & st) const { - m_context.collect_statistics(st); + // Hack to display fu_malik statistics + if (m_stats.size() > 0) { + st.copy(m_stats); + } + else { + m_context.collect_statistics(st); + } } void opt_solver::assert_expr(expr * t) { @@ -213,6 +219,10 @@ namespace opt { } return dynamic_cast(s); } + + void opt_solver::set_interim_stats(statistics & st) { + m_stats.copy(st); + } void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, char const * status, char const * attributes) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index de7ef0b1d..e5af48a5c 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -46,7 +46,8 @@ namespace opt { bool m_objective_enabled; svector m_objective_vars; vector m_objective_values; - bool m_is_dump; + bool m_is_dump; + statistics m_stats; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -77,7 +78,8 @@ namespace opt { expr_ref block_upper_bound(unsigned obj_index, inf_eps const& val); static opt_solver& to_opt(solver& s); - + void set_interim_stats(statistics & st); + class toggle_objective { opt_solver& s; bool m_old_value; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3e9b60260..ec00be897 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -671,6 +671,7 @@ namespace sat { // // ----------------------- lbool solver::check() { + IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";); SASSERT(scope_lvl() == 0); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { @@ -1970,7 +1971,7 @@ namespace sat { m_cancel = f; } - void solver::collect_statistics(statistics & st) { + void solver::collect_statistics(statistics & st) { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); m_simplifier.collect_statistics(st); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 95b150a8c..0fdde612d 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -135,6 +135,7 @@ public: proof_converter_ref & pc, expr_dependency_ref & core) { try { + IF_VERBOSE(0, verbose_stream() << "(smt.smt-tactic using the old SAT solver)\n";); SASSERT(in->is_well_sorted()); ast_manager & m = in->m(); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 1268fbcea..dde03f962 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -40,6 +40,7 @@ class tactic2solver : public solver_na2as { bool m_produce_models; bool m_produce_proofs; bool m_produce_unsat_cores; + statistics m_stats; public: tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic); virtual ~tactic2solver(); @@ -161,6 +162,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass m_result->m_unknown = ex.msg(); } m_tactic->collect_statistics(m_result->m_stats); + m_tactic->collect_statistics(m_stats); m_result->m_model = md; m_result->m_proof = pr; if (m_produce_unsat_cores) { @@ -177,9 +179,9 @@ void tactic2solver::set_cancel(bool f) { m_tactic->set_cancel(f); } -void tactic2solver::collect_statistics(statistics & st) const { - if (m_result.get()) - m_result->collect_statistics(st); +void tactic2solver::collect_statistics(statistics & st) const { + st.copy(m_stats); + SASSERT(m_stats.size() > 0); } void tactic2solver::get_unsat_core(ptr_vector & r) { diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index cdbc6927e..51b040332 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -31,15 +31,6 @@ Notes: #define MEMLIMIT 300 -tactic * mk_new_sat_tactic(ast_manager & m) { - IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;); - tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - and_then(mk_simplify_tactic(m), - mk_smt_tactic()), - mk_sat_tactic(m)); - return new_sat; -} - tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); @@ -94,7 +85,10 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = and_then(mk_simplify_tactic(m), mk_smt_tactic()); #else - tactic * new_sat = mk_new_sat_tactic(m); + tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + and_then(mk_simplify_tactic(m), + mk_smt_tactic()), + mk_sat_tactic(m)); #endif tactic * st = using_params(and_then(preamble_st, From 314f03c12ca7730d00315d2bf42b8aa5ac4e73ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Nov 2013 16:44:08 -0800 Subject: [PATCH 2/6] started new PB solver Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/opt/fu_malik.cpp | 2 +- src/smt/theory_pb.cpp | 703 ++++++++++++++++++++++++++++++++++++++++++ src/smt/theory_pb.h | 117 +++++++ 4 files changed, 822 insertions(+), 2 deletions(-) create mode 100644 src/smt/theory_pb.cpp create mode 100644 src/smt/theory_pb.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e92899436..b52934dfe 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -63,11 +63,11 @@ def init_project_def(): add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc'], 'muz/fp') - add_lib('opt', ['smt'], 'opt') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') + add_lib('opt', ['smt', 'smtlogic_tactics'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 77eb108a9..db4cb93d2 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "fu_malik.h" -#include "smtlogics/qfbv_tactic.h" +#include "qfbv_tactic.h" #include "tactic2solver.h" #include "goal.h" #include "probe.h" diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp new file mode 100644 index 000000000..171615c95 --- /dev/null +++ b/src/smt/theory_pb.cpp @@ -0,0 +1,703 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_pb.cpp + +Abstract: + + Pseudo-Boolean theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + + +--*/ + +#include "theory_pb.h" +#include "smt_context.h" +#include "ast_pp.h" +#include "sorting_network.h" + +namespace smt { + + theory_pb::theory_pb(ast_manager& m): + theory(m.mk_family_id("card")), + m_util(m) + {} + + theory_pb::~theory_pb() { + reset_eh(); + } + + theory * theory_pb::mk_fresh(context * new_ctx) { + return alloc(theory_pb, new_ctx->get_manager()); + } + + bool theory_pb::internalize_atom(app * atom, bool gate_ctx) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + unsigned num_args = atom->get_num_args(); + SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom)); + + if (ctx.b_internalized(atom)) { + return false; + } + + m_stats.m_num_predicates++; + + SASSERT(!ctx.b_internalized(atom)); + bool_var abv = ctx.mk_bool_var(atom); + + ineq* c = alloc(ineq, atom, literal(abv)); + c->m_k = m_util.get_k(atom); + int& k = c->m_k; + arg_t& args = c->m_args; + + // extract literals and coefficients. + for (unsigned i = 0; i < num_args; ++i) { + expr* arg = atom->get_arg(i); + literal l = compile_arg(arg); + int c = m_util.get_le_coeff(atom, i); + args.push_back(std::make_pair(l, c)); + } + // turn W <= k into -W >= -k + for (unsigned i = 0; i < args.size(); ++i) { + args[i].second = -args[i].second; + } + k = -k; + lbool is_true = normalize_ineq(args, k); + + literal lit(abv); + switch(is_true) { + case l_false: + lit = ~lit; + // fall-through + case l_true: + ctx.mk_th_axiom(get_id(), 1, &lit); + TRACE("card", tout << mk_pp(atom, m) << " := " << lit << "\n";); + dealloc(c); + return true; + case l_undef: + break; + } + + // TBD: special cases: args.size() == 1 + + // maximal coefficient: + int& max_coeff = c->m_max_coeff; + max_coeff = 0; + for (unsigned i = 0; i < args.size(); ++i) { + max_coeff = std::max(max_coeff, args[i].second); + } + + // compute watch literals: + int sum = 0; + unsigned& wsz = c->m_watch_sz; + wsz = 0; + while (sum < k + max_coeff && wsz < args.size()) { + sum += args[wsz].second; + wsz++; + } + + for (unsigned i = 0; i < wsz; ++i) { + add_watch(args[i].first, c); + } + + // pre-compile threshold for cardinality + bool is_cardinality = true; + for (unsigned i = 0; is_cardinality && i < args.size(); ++i) { + is_cardinality = (args[i].second == 1); + } + if (is_cardinality) { + unsigned log = 1, n = 1; + while (n <= args.size()) { + ++log; + n *= 2; + } + c->m_compilation_threshold = args.size()*log; + TRACE("card", tout << "threshold:" << (args.size()*log) << "\n";); + } + else { + c->m_compilation_threshold = UINT_MAX; + } + m_ineqs.insert(abv, c); + m_ineqs_trail.push_back(abv); + + TRACE("card", display(tout, *c);); + + return true; + } + + literal theory_pb::compile_arg(expr* arg) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + if (!ctx.b_internalized(arg)) { + ctx.internalize(arg, false); + } + bool_var bv; + bool has_bv = false; + bool negate = m.is_not(arg, arg); + if (ctx.b_internalized(arg)) { + bv = ctx.get_bool_var(arg); + if (null_theory_var == ctx.get_var_theory(bv)) { + ctx.set_var_theory(bv, get_id()); + } + has_bv = (ctx.get_var_theory(bv) == get_id()); + } + + // pre-processing should better remove negations under cardinality. + // assumes relevancy level = 2 or 0. + if (!has_bv) { + expr_ref tmp(m), fml(m); + tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort()); + fml = m.mk_iff(tmp, arg); + ctx.internalize(fml, false); + SASSERT(ctx.b_internalized(tmp)); + bv = ctx.get_bool_var(tmp); + SASSERT(null_theory_var == ctx.get_var_theory(bv)); + ctx.set_var_theory(bv, get_id()); + literal lit(ctx.get_bool_var(fml)); + ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.mark_as_relevant(tmp); + } + return negate?~literal(bv):literal(bv); + } + + void theory_pb::add_watch(literal l, ineq* c) { + unsigned idx = l.index(); + ptr_vector* ineqs; + if (!m_watch.find(idx, ineqs)) { + ineqs = alloc(ptr_vector); + m_watch.insert(idx, ineqs); + } + ineqs->push_back(c); + } + + static unsigned gcd(unsigned a, unsigned b) { + while (a != b) { + if (a == 0) return b; + if (b == 0) return a; + SASSERT(a != 0 && b != 0); + if (a < b) { + b %= a; + } + else { + a %= b; + } + } + return a; + } + + lbool theory_pb::normalize_ineq(arg_t& args, int& k) { + + // normalize first all literals to be positive: + // then we can can compare them more easily. + for (unsigned i = 0; i < args.size(); ++i) { + if (args[i].first.sign()) { + args[i].first.neg(); + k -= args[i].second; + args[i].second = -args[i].second; + } + } + // sort and coalesce arguments: + std::sort(args.begin(), args.end()); + for (unsigned i = 0; i + 1 < args.size(); ++i) { + if (args[i].first == args[i+1].first) { + args[i].second += args[i+1].second; + for (unsigned j = i+1; j + 1 < args.size(); ++j) { + args[j] = args[j+1]; + } + args.resize(args.size()-1); + } + if (args[i].second == 0) { + for (unsigned j = i; j + 1 < args.size(); ++j) { + args[j] = args[j+1]; + } + args.resize(args.size()-1); + } + } + // + // Ensure all coefficients are positive: + // c*l + y >= k + // <=> + // c*(1-~l) + y >= k + // <=> + // c - c*~l + y >= k + // <=> + // -c*~l + y >= k - c + // + unsigned sum = 0; + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c < 0) { + args[i].second = -c; + args[i].first = ~args[i].first; + k -= c; + } + sum += args[i].second; + } + // detect tautologies: + if (k <= 0) { + args.reset(); + return l_true; + } + // detect infeasible constraints: + if (static_cast(sum) < k) { + args.reset(); + return l_false; + } + // Ensure the largest coefficient is not larger than k: + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c > k) { + args[i].second = k; + } + } + SASSERT(!args.empty()); + + // apply cutting plane reduction: + unsigned g = 0; + for (unsigned i = 0; g != 1 && i < args.size(); ++i) { + int c = args[i].second; + if (c != k) { + g = gcd(g, c); + } + } + if (g == 0) { + // all coefficients are equal to k. + for (unsigned i = 0; i < args.size(); ++i) { + SASSERT(args[i].second == k); + args[i].second = 1; + } + k = 1; + } + else if (g > 1) { + // + // Example 5x + 5y + 2z + 2u >= 5 + // becomes 3x + 3y + z + u >= 3 + // + int k_new = k / g; // k_new is the ceiling of k / g. + if (gcd(k, g) != g) { + k_new++; + } + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c == k) { + c = k_new; + } + else { + c = c / g; + } + args[i].second = c; + } + k = k_new; + } + + return l_undef; + } + + void theory_pb::collect_statistics(::statistics& st) const { + st.update("pb axioms", m_stats.m_num_axioms); + st.update("pb propagations", m_stats.m_num_propagations); + st.update("pb predicates", m_stats.m_num_predicates); + st.update("pb compilations", m_stats.m_num_compiles); + } + + void theory_pb::reset_eh() { + + // m_watch; + u_map*>::iterator it = m_watch.begin(), end = m_watch.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); + for (; itc != endc; ++itc) { + dealloc(itc->m_value); + } + m_watch.reset(); + m_ineqs.reset(); + m_ineqs_trail.reset(); + m_ineqs_lim.reset(); + m_stats.reset(); + } + + +#if 0 + void theory_pb::propagate_assignment(ineq& c) { + if (c.m_compiled) { + return; + } + if (should_compile(c)) { + compile_ineq(c); + return; + } + context& ctx = get_context(); + ast_manager& m = get_manager(); + arg_t const& args = c.m_args; + bool_var abv = c.m_bv; + int min = c.m_current_min; + int max = c.m_current_max; + int k = c.m_k; + + TRACE("card", + tout << mk_pp(c.m_app, m) << " min: " + << min << " max: " << max << "\n";); + + // + // if min > k && abv != l_false -> force abv false + // if max <= k && abv != l_true -> force abv true + // if min == k && abv == l_true -> force positive + // unassigned literals false + // if max == k + 1 && abv == l_false -> force negative + // unassigned literals false + // + lbool aval = ctx.get_assignment(abv); + if (min > k && aval != l_false) { + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + SASSERT(curr_min > k); + add_assign(c, lits, ~literal(abv)); + } + else if (max <= k && aval != l_true) { + literal_vector& lits = get_lits(); + int curr_max = accumulate_max(lits, c); + SASSERT(curr_max <= k); + add_assign(c, lits, literal(abv)); + } + else if (min <= k && k < min + get_max_delta(c) && aval == l_true) { + literal_vector& lits = get_lits(); + lits.push_back(~literal(abv)); + int curr_min = accumulate_min(lits, c); + if (curr_min > k) { + add_clause(c, lits); + } + else { + for (unsigned i = 0; i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc > 0)); + } + } + } + } + else if (max - get_max_delta(c) <= k && k < max && aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + if (curr_max <= k) { + add_clause(c, lits); + } + else { + for (unsigned i = 0; i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc < 0)); + } + } + } + } + else if (aval == l_true) { + SASSERT(min < k); + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + bool all_inc = curr_min == k; + unsigned num_incs = 0; + for (unsigned i = 0; all_inc && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + all_inc = inc + min > k; + num_incs++; + } + } + if (num_incs > 0) { + std::cout << "missed T propgations " << num_incs << "\n"; + } + } + else if (aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + bool all_dec = curr_max > k; + unsigned num_decs = 0; + for (unsigned i = 0; all_dec && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + all_dec = inc + max <= k; + num_decs++; + } + } + if (num_decs > 0) { + std::cout << "missed F propgations " << num_decs << "\n"; + } + } + } +#endif + + void theory_pb::assign_eh(bool_var v, bool is_true) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + ptr_vector* ineqs = 0; + ineq* c = 0; + TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";); + + if (m_watch.find(v, ineqs)) { + for (unsigned i = 0; i < ineqs->size(); ++i) { + // TBD: assign_use(v, is_true, *(*ineqs)[i]); + } + } + if (m_ineqs.find(v, c)) { + // TBD: propagate_assignment(*c); + } + } + + struct theory_pb::sort_expr { + theory_pb& th; + context& ctx; + ast_manager& m; + expr_ref_vector m_trail; + sort_expr(theory_pb& th): + th(th), + ctx(th.get_context()), + m(th.get_manager()), + m_trail(m) {} + typedef expr* T; + typedef expr_ref_vector vector; + + T mk_ite(T a, T b, T c) { + if (m.is_true(a)) { + return b; + } + if (m.is_false(a)) { + return c; + } + if (b == c) { + return b; + } + m_trail.push_back(m.mk_ite(a, b, c)); + return m_trail.back(); + } + + T mk_le(T a, T b) { + return mk_ite(b, a, m.mk_true()); + } + + T mk_default() { + return m.mk_false(); + } + + literal internalize(ineq& ca, expr* e) { + obj_map cache; + for (unsigned i = 0; i < ca.m_args.size(); ++i) { + cache.insert(ca.m_app->get_arg(i), literal(ca.m_args[i].first)); + } + cache.insert(m.mk_false(), false_literal); + cache.insert(m.mk_true(), true_literal); + ptr_vector todo; + todo.push_back(e); + expr *a, *b, *c; + literal la, lb, lc; + while (!todo.empty()) { + expr* t = todo.back(); + if (cache.contains(t)) { + todo.pop_back(); + continue; + } + VERIFY(m.is_ite(t, a, b, c)); + unsigned sz = todo.size(); + if (!cache.find(a, la)) { + todo.push_back(a); + } + if (!cache.find(b, lb)) { + todo.push_back(b); + } + if (!cache.find(c, lc)) { + todo.push_back(c); + } + if (sz != todo.size()) { + continue; + } + todo.pop_back(); + cache.insert(t, mk_ite(ca, t, la, lb, lc)); + } + return cache.find(e); + } + + literal mk_ite(ineq& ca, expr* t, literal a, literal b, literal c) { + if (a == true_literal) { + return b; + } + else if (a == false_literal) { + return c; + } + else if (b == true_literal && c == false_literal) { + return a; + } + else if (b == false_literal && c == true_literal) { + return ~a; + } + else if (b == c) { + return b; + } + else { + literal l; + if (ctx.b_internalized(t)) { + l = literal(ctx.get_bool_var(t)); + } + else { + l = literal(ctx.mk_bool_var(t)); + } + add_clause(~l, ~a, b); + add_clause(~l, a, c); + add_clause(l, ~a, ~b); + add_clause(l, a, ~c); + TRACE("card", tout << mk_pp(t, m) << " ::= (if "; + ctx.display_detailed_literal(tout, a); + ctx.display_detailed_literal(tout << " ", b); + ctx.display_detailed_literal(tout << " ", c); + tout << ")\n";); + return l; + } + } + + + // auxiliary clauses don't get garbage collected. + void add_clause(literal a, literal b, literal c) { + literal_vector& lits = th.get_lits(); + if (a != null_literal) lits.push_back(a); + if (b != null_literal) lits.push_back(b); + if (c != null_literal) lits.push_back(c); + justification* js = 0; + TRACE("card", + ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0); + } + + void add_clause(literal l1, literal l2) { + add_clause(l1, l2, null_literal); + } + + }; + + + bool theory_pb::should_compile(ineq& c) { +#if 1 + return false; +#else + return c.m_num_propagations > c.m_compilation_threshold; +#endif + } + + void theory_pb::compile_ineq(ineq& c) { + ++m_stats.m_num_compiles; + ast_manager& m = get_manager(); + context& ctx = get_context(); + app* a = c.m_app; + SASSERT(m_util.is_at_most_k(a)); + literal atmostk; + int k = m_util.get_k(a); + unsigned num_args = a->get_num_args(); + + sort_expr se(*this); + if (k >= static_cast(num_args)) { + atmostk = true_literal; + } + else if (k < 0) { + atmostk = false_literal; + } + else { + sorting_network sn(se); + expr_ref_vector in(m), out(m); + for (unsigned i = 0; i < num_args; ++i) { + in.push_back(c.m_app->get_arg(i)); + } + sn(in, out); + atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0. + TRACE("card", tout << "~atmost: " << mk_pp(out[k].get(), m) << "\n";); + } + literal thl = c.m_lit; + se.add_clause(~thl, atmostk); + se.add_clause(thl, ~atmostk); + TRACE("card", tout << mk_pp(a, m) << "\n";); + // auxiliary clauses get removed when popping scopes. + // we have to recompile the circuit after back-tracking. + ctx.push_trail(value_trail(c.m_compiled)); + c.m_compiled = true; + } + + + void theory_pb::init_search_eh() { + + } + + void theory_pb::push_scope_eh() { + m_ineqs_lim.push_back(m_ineqs_trail.size()); + } + + void theory_pb::pop_scope_eh(unsigned num_scopes) { + unsigned sz = m_ineqs_lim[m_ineqs_lim.size()-num_scopes]; + while (m_ineqs_trail.size() > sz) { + SASSERT(m_ineqs.contains(m_ineqs_trail.back())); + m_ineqs.remove(m_ineqs_trail.back()); + m_ineqs_trail.pop_back(); + } + m_ineqs_lim.resize(m_ineqs_lim.size()-num_scopes); + } + + std::ostream& theory_pb::display(std::ostream& out, ineq& c) const { + ast_manager& m = get_manager(); + out << mk_pp(c.m_app, m) << "\n"; + for (unsigned i = 0; i < c.m_args.size(); ++i) { + out << c.m_args[i].second << "*" << c.m_args[i].first; + if (i + 1 < c.m_args.size()) { + out << " + "; + } + } + out << " >= " << c.m_k << "\n" + << "propagations: " << c.m_num_propagations + << " max_coeff: " << c.m_max_coeff + << " watch size: " << c.m_watch_sz + << "\n"; + return out; + } + + + literal_vector& theory_pb::get_lits() { + m_literals.reset(); + return m_literals; + } + + void theory_pb::add_assign(ineq& c, literal_vector const& lits, literal l) { + literal_vector ls; + ++c.m_num_propagations; + m_stats.m_num_propagations++; + context& ctx = get_context(); + for (unsigned i = 0; i < lits.size(); ++i) { + ls.push_back(~lits[i]); + } + ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l))); + } + + + + void theory_pb::add_clause(ineq& c, literal_vector const& lits) { + ++c.m_num_propagations; + m_stats.m_num_axioms++; + context& ctx = get_context(); + TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + justification* js = 0; + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), + lits.size(), lits.c_ptr()); + verbose_stream() << "\n";); + // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + } +} diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h new file mode 100644 index 000000000..432d4e497 --- /dev/null +++ b/src/smt/theory_pb.h @@ -0,0 +1,117 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_pb.h + +Abstract: + + Cardinality theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + + This custom theory handles cardinality constraints + It performs unit propagation and switches to creating + sorting circuits if it keeps having to propagate (create new clauses). +--*/ + +#include "smt_theory.h" +#include "card_decl_plugin.h" +#include "smt_clause.h" + +namespace smt { + class theory_pb : public theory { + + struct sort_expr; + typedef svector > arg_t; + + struct stats { + unsigned m_num_axioms; + unsigned m_num_propagations; + unsigned m_num_predicates; + unsigned m_num_compiles; + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; + + + struct ineq { + app* m_app; + literal m_lit; // literal repesenting predicate + arg_t m_args; // encode args[0]*coeffs[0]+...+args[n-1]*coeffs[n-1] >= m_k; + int m_k; // invariants: m_k > 0, coeffs[i] > 0 + + // Watch the first few positions until the sum satisfies: + // sum coeffs[i] >= m_lower + max_coeff + + int m_max_coeff; // maximal coefficient. + unsigned m_watch_sz; // number of literals being watched. + unsigned m_num_propagations; + unsigned m_compilation_threshold; + bool m_compiled; + + ineq(app* a, literal l): + m_app(a), + m_lit(l), + m_num_propagations(0), + m_compilation_threshold(UINT_MAX), + m_compiled(false) + {} + }; + + typedef ptr_vector watch_list; + + u_map m_watch; // per literal. + u_map m_ineqs; // per inequality. + unsigned_vector m_ineqs_trail; + unsigned_vector m_ineqs_lim; + literal_vector m_literals; // temporary vector + card_util m_util; + stats m_stats; + + // internalize_atom: + lbool normalize_ineq(arg_t& args, int& k); + literal compile_arg(expr* arg); + void add_watch(literal l, ineq* c); + + std::ostream& display(std::ostream& out, ineq& c) const; + + void add_clause(ineq& c, literal_vector const& lits); + void add_assign(ineq& c, literal_vector const& lits, literal l); + literal_vector& get_lits(); + + // + // Utilities to compile cardinality + // constraints into a sorting network. + // + void compile_ineq(ineq& c); + bool should_compile(ineq& c); + unsigned get_compilation_threshold(ineq& c); + public: + theory_pb(ast_manager& m); + + virtual ~theory_pb(); + + virtual theory * mk_fresh(context * new_ctx); + virtual bool internalize_atom(app * atom, bool gate_ctx); + virtual bool internalize_term(app * term) { UNREACHABLE(); return false; } + virtual void new_eq_eh(theory_var v1, theory_var v2) { } + virtual void new_diseq_eh(theory_var v1, theory_var v2) { } + virtual bool use_diseqs() const { return false; } + virtual bool build_models() const { return false; } + virtual final_check_status final_check_eh() { return FC_DONE; } + + virtual void reset_eh(); + virtual void assign_eh(bool_var v, bool is_true); + virtual void init_search_eh(); + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual void collect_statistics(::statistics & st) const; + + }; +}; From c837f62863330e7eb908308d45449eda84cb6219 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 15 Nov 2013 16:58:42 -0800 Subject: [PATCH 3/6] Use quick explain for unsat core in Fu Malik algorithm by default --- src/opt/fu_malik.cpp | 38 ++++++++++++++++++++++++++++++++++---- src/opt/opt_solver.cpp | 4 ++++ src/opt/opt_solver.h | 1 + 3 files changed, 39 insertions(+), 4 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 235fa4205..a0946dc9f 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -123,7 +123,15 @@ namespace opt { expr_ref_vector ls1(m), ls2(m); ls1.append(mid, literals.c_ptr()); ls2.append(literals.size()-mid, literals.c_ptr() + mid); - +#if Z3DEBUG + expr_ref_vector ls(m); + ls.append(ls1); + ls.append(ls2); + SASSERT(ls.size() == literals.size()); + for (unsigned i = 0; i < literals.size(); ++i) { + SASSERT(ls[i].get() == literals[i].get()); + } +#endif expr_ref_vector as1(m); as1.append(assumptions); as1.append(ls1); @@ -153,6 +161,7 @@ namespace opt { ptr_vector core; if (m_use_new_bv_solver) { + // Binary search for minimal unsat core expr_set core_set; expr_ref_vector empty(m); quick_explain(empty, assumptions, true, core_set); @@ -160,6 +169,24 @@ namespace opt { for (; it != end; ++it) { core.push_back(*it); } + + //// Forward linear search for unsat core + //unsigned i = 0; + //while (s().check_sat(core.size(), core.c_ptr()) != l_false) { + // IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";); + // core.push_back(assumptions[i].get()); + // ++i; + //} + + //// Backward linear search for unsat core + //unsigned i = 0; + //core.append(assumptions.size(), assumptions.c_ptr()); + //while (!core.empty() && s().check_sat(core.size()-1, core.c_ptr()) == l_false) { + // IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";); + // core.pop_back(); + // ++i; + //} + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";); } else { @@ -214,7 +241,11 @@ namespace opt { } } - void set_solver() { + void set_solver() { + opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + if (opt_s.is_dumping_benchmark()) + return; + solver& current_solver = s(); goal g(m, true, false); unsigned num_assertions = current_solver.get_num_assertions(); @@ -223,8 +254,7 @@ namespace opt { } probe *p = mk_is_qfbv_probe(); bool all_bv = (*p)(g).is_true(); - if (all_bv) { - opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + if (all_bv) { smt::context & ctx = opt_s.get_context(); tactic_ref t = mk_qfbv_tactic(m, ctx.get_params()); // The new SAT solver hasn't supported unsat core yet diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index a8e7d8535..88d1cab1f 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -105,6 +105,10 @@ namespace opt { static unsigned g_checksat_count = 0; + bool opt_solver::is_dumping_benchmark() { + return m_is_dump; + } + lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { TRACE("opt_solver_na2as", { tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n"; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e5af48a5c..e946d2131 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -79,6 +79,7 @@ namespace opt { static opt_solver& to_opt(solver& s); void set_interim_stats(statistics & st); + bool is_dumping_benchmark(); class toggle_objective { opt_solver& s; From af8da013b59ce33309b08a33c3f3f9d5b8709e36 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 15 Nov 2013 17:17:20 -0800 Subject: [PATCH 4/6] Fix a few issues related to thread spanning tree --- src/smt/network_flow.h | 2 +- src/smt/network_flow_def.h | 20 ++--- src/smt/spanning_tree.h | 2 +- src/smt/spanning_tree_base.h | 12 +-- src/smt/spanning_tree_def.h | 146 +++++++++++++++++------------------ 5 files changed, 90 insertions(+), 92 deletions(-) diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 461312985..d845c671a 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -244,7 +244,7 @@ namespace smt { }; graph m_graph; - thread_spanning_tree m_tree; + spanning_tree_base * m_tree; // Denote supply/demand b_i on node i vector m_balances; diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 515d49933..0ec7fe0c0 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -27,8 +27,7 @@ namespace smt { template network_flow::network_flow(graph & g, vector const & balances) : - m_balances(balances), - m_tree(m_graph) { + m_balances(balances) { // Network flow graph has the edges in the reversed order compared to constraint graph // We only take enabled edges from the original graph for (unsigned i = 0; i < g.get_num_nodes(); ++i) { @@ -42,6 +41,7 @@ namespace smt { } } m_step = 0; + m_tree = alloc(thread_spanning_tree, m_graph); } template @@ -82,7 +82,7 @@ namespace smt { tree.push_back(m_graph.add_edge(src, tgt, numeral::one(), explanation())); } - m_tree.initialize(tree); + m_tree->initialize(tree); TRACE("network_flow", { tout << pp_vector("Potentials", m_potentials, true) << pp_vector("Flows", m_flows); @@ -96,14 +96,14 @@ namespace smt { node src = m_graph.get_source(m_enter_id); node tgt = m_graph.get_target(m_enter_id); numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(m_enter_id); - numeral change = m_tree.in_subtree_t2(tgt) ? cost : -cost; + numeral change = m_tree->in_subtree_t2(tgt) ? cost : -cost; node start = m_graph.get_source(m_leave_id); - if (!m_tree.in_subtree_t2(start)) { + if (!m_tree->in_subtree_t2(start)) { start = m_graph.get_target(m_leave_id);; } TRACE("network_flow", tout << "update_potentials of T_" << start << " with change = " << change << "...\n";); svector descendants; - m_tree.get_descendants(start, descendants); + m_tree->get_descendants(start, descendants); SASSERT(descendants.size() >= 1); for (unsigned i = 0; i < descendants.size(); ++i) { node u = descendants[i]; @@ -120,7 +120,7 @@ namespace smt { node tgt = m_graph.get_target(m_enter_id); svector path; svector against; - m_tree.get_path(src, tgt, path, against); + m_tree->get_path(src, tgt, path, against); SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { edge_id e_id = path[i]; @@ -138,7 +138,7 @@ namespace smt { edge_id leave_id; svector path; svector against; - m_tree.get_path(src, tgt, path, against); + m_tree->get_path(src, tgt, path, against); SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { edge_id e_id = path[i]; @@ -164,7 +164,7 @@ namespace smt { template void network_flow::update_spanning_tree() { - m_tree.update(m_enter_id, m_leave_id); + m_tree->update(m_enter_id, m_leave_id); } // FIXME: should declare pivot as a pivot_rule_impl and refactor @@ -240,7 +240,7 @@ namespace smt { template bool network_flow::check_well_formed() { - SASSERT(m_tree.check_well_formed()); + SASSERT(m_tree->check_well_formed()); SASSERT(!m_delta || !(*m_delta).is_neg()); // m_flows are zero on non-basic edges diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index c591f5485..f5f6b624f 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -49,7 +49,7 @@ namespace smt { void swap_order(node q, node v); node find_rev_thread(node n) const; - void fix_depth(node start, node end); + void fix_depth(node start, node after_end); node get_final(int start); bool is_preorder_traversal(node start, node end); node get_common_ancestor(node u, node v); diff --git a/src/smt/spanning_tree_base.h b/src/smt/spanning_tree_base.h index e492f80fa..25384d52e 100644 --- a/src/smt/spanning_tree_base.h +++ b/src/smt/spanning_tree_base.h @@ -47,14 +47,14 @@ namespace smt { typedef int node; public: - virtual void initialize(svector const & tree) {}; - virtual void get_descendants(node start, svector & descendants) {}; + virtual void initialize(svector const & tree) = 0; + virtual void get_descendants(node start, svector & descendants) = 0; - virtual void update(edge_id enter_id, edge_id leave_id) {}; - virtual void get_path(node start, node end, svector & path, svector & against) {}; - virtual bool in_subtree_t2(node child) {UNREACHABLE(); return false;}; + virtual void update(edge_id enter_id, edge_id leave_id) = 0; + virtual void get_path(node start, node end, svector & path, svector & against) = 0; + virtual bool in_subtree_t2(node child) = 0; - virtual bool check_well_formed() {UNREACHABLE(); return false;}; + virtual bool check_well_formed() = 0; }; } diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index c1e05ba3b..281a2cf45 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -162,11 +162,26 @@ namespace smt { tout << u << ", " << v << ") leaves\n"; }); + // Old threads: alpha -> v -*-> f(v) -> beta | p -*-> f(p) -> gamma + // New threads: alpha -> beta | p -*-> f(p) -> v -*-> f(v) -> gamma + + node f_p = get_final(p); + node f_v = get_final(v); + node alpha = find_rev_thread(v); + node beta = m_thread[f_v]; + node gamma = m_thread[f_p]; + + if (v != gamma) { + m_thread[alpha] = beta; + m_thread[f_p] = v; + m_thread[f_v] = gamma; + } + node old_pred = m_pred[q]; // Update stem nodes from q to v if (q != v) { - for (node n = q; n != u; ) { - SASSERT(old_pred != u || n == v); // the last processed node is v + for (node n = q; n != v; ) { + SASSERT(old_pred != u); // the last processed node is v SASSERT(-1 != m_pred[old_pred]); int next_old_pred = m_pred[old_pred]; swap_order(n, old_pred); @@ -175,34 +190,18 @@ namespace smt { old_pred = next_old_pred; } } - - // Old threads: alpha -> q -*-> f(q) -> beta | p -*-> f(p) -> gamma - // New threads: alpha -> beta | p -*-> f(p) -> q -*-> f(q) -> gamma - - node f_p = get_final(p); - node f_q = get_final(q); - node alpha = find_rev_thread(q); - node beta = m_thread[f_q]; - node gamma = m_thread[f_p]; - - if (q != gamma) { - m_thread[alpha] = beta; - m_thread[f_p] = q; - m_thread[f_q] = gamma; - } - + m_pred[q] = p; m_tree[q] = enter_id; m_root_t2 = q; + node after_final_q = (v == gamma) ? beta : gamma; + fix_depth(q, after_final_q); + SASSERT(!in_subtree_t2(p)); SASSERT(in_subtree_t2(q)); SASSERT(!in_subtree_t2(u)); SASSERT(in_subtree_t2(v)); - - // Update the depth. - - fix_depth(q, get_final(q)); TRACE("network_flow", { tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); @@ -210,6 +209,53 @@ namespace smt { }); } + /** + swap v and q in tree. + - fixup m_thread + - fixup m_pred + + Case 1: final(q) == final(v) + ------- + Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next + New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next + + Case 2: final(q) != final(v) + ------- + Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next + New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next + + */ + template + void thread_spanning_tree::swap_order(node q, node v) { + SASSERT(q != v); + SASSERT(m_pred[q] == v); + SASSERT(is_preorder_traversal(v, get_final(v))); + node prev = find_rev_thread(v); + node f_q = get_final(q); + node f_v = get_final(v); + node next = m_thread[f_v]; + node alpha = find_rev_thread(q); + + if (f_q == f_v) { + SASSERT(f_q != v && alpha != next); + m_thread[f_q] = v; + m_thread[alpha] = next; + f_q = alpha; + } + else { + node beta = m_thread[f_q]; + SASSERT(f_q != v && alpha != beta); + m_thread[f_q] = v; + m_thread[alpha] = beta; + f_q = f_v; + } + SASSERT(prev != q); + m_thread[prev] = q; + m_pred[v] = q; + // Notes: f_q has to be used since m_depth hasn't been updated yet. + SASSERT(is_preorder_traversal(q, f_q)); + } + /** \brief Check invariants of main data-structures. @@ -311,53 +357,6 @@ namespace smt { roots[y] = x; } - /** - swap v and q in tree. - - fixup m_thread - - fixup m_pred - - Case 1: final(q) == final(v) - ------- - Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next - New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next - - Case 2: final(q) != final(v) - ------- - Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next - New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next - - */ - template - void thread_spanning_tree::swap_order(node q, node v) { - SASSERT(q != v); - SASSERT(m_pred[q] == v); - SASSERT(is_preorder_traversal(v, get_final(v))); - node prev = find_rev_thread(v); - node f_q = get_final(q); - node f_v = get_final(v); - node next = m_thread[f_v]; - node alpha = find_rev_thread(q); - - if (f_q == f_v) { - SASSERT(f_q != v && alpha != next); - m_thread[f_q] = v; - m_thread[alpha] = next; - f_q = alpha; - } - else { - node beta = m_thread[f_q]; - SASSERT(f_q != v && alpha != beta); - m_thread[f_q] = v; - m_thread[alpha] = beta; - f_q = f_v; - } - SASSERT(prev != q); - m_thread[prev] = q; - m_pred[v] = q; - // Notes: f_q has to be used since m_depth hasn't been updated yet. - SASSERT(is_preorder_traversal(q, f_q)); - } - /** \brief find node that points to 'n' in m_thread */ @@ -372,12 +371,11 @@ namespace smt { } template - void thread_spanning_tree::fix_depth(node start, node end) { - SASSERT(m_pred[start] != -1); - m_depth[start] = m_depth[m_pred[start]]+1; - while (start != end) { - start = m_thread[start]; + void thread_spanning_tree::fix_depth(node start, node after_end) { + while (start != after_end) { + SASSERT(m_pred[start] != -1); m_depth[start] = m_depth[m_pred[start]]+1; + start = m_thread[start]; } } From 13c97d12a8f4302a924acf5708ce4f485738f76b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Nov 2013 17:31:31 -0800 Subject: [PATCH 5/6] snapshot Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 34 ++++++++++++++++++++++++++++++++-- src/smt/theory_pb.h | 1 + 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 171615c95..52d525bde 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -196,7 +196,7 @@ namespace smt { lbool theory_pb::normalize_ineq(arg_t& args, int& k) { // normalize first all literals to be positive: - // then we can can compare them more easily. + // then we can compare them more easily. for (unsigned i = 0; i < args.size(); ++i) { if (args[i].first.sign()) { args[i].first.neg(); @@ -451,7 +451,7 @@ namespace smt { if (m_watch.find(v, ineqs)) { for (unsigned i = 0; i < ineqs->size(); ++i) { - // TBD: assign_use(v, is_true, *(*ineqs)[i]); + assign_watch(v, is_true, *ineqs, i); } } if (m_ineqs.find(v, c)) { @@ -459,6 +459,36 @@ namespace smt { } } + void theory_pb::assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index) { +#if 0 + TBD + ineq& c = *watch[i]; + c.m_sum; + unsigned w; + for (w = 0; w < c.m_watch_sz; ++i) { + if (c.m_args[w].first.var() == v) { + break; + } + } + SASSERT(w < c.m_watch_sz); + literal l = c.m_args[w].first; + int coeff = c.m_args[w].second; + if (is_true == !l.sign()) { + ctx.push_trail(value_trail(c.m_sum)); + c.m_sum += coeff; + // optional propagate + } + else { + unsigned deficit = c.m_max_sum - coeff; + for (unsigned i = c.m_watch_sz; i < c.m_args.size(); ++i) { + if + } + // find a different literal to watch. + ctx.push_trail(value_trail(c.m_watch_sz)); + } +#endif + } + struct theory_pb::sort_expr { theory_pb& th; context& ctx; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 432d4e497..5fb66f3f4 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -78,6 +78,7 @@ namespace smt { lbool normalize_ineq(arg_t& args, int& k); literal compile_arg(expr* arg); void add_watch(literal l, ineq* c); + void assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index); std::ostream& display(std::ostream& out, ineq& c) const; From 6ddc8386285cd9c1eff50640cb09b1112e25db0f Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 15 Nov 2013 18:34:05 -0800 Subject: [PATCH 6/6] Add a basic spanning tree --- src/smt/diff_logic.h | 82 +++++++++++++++++++++++++++++++++++++ src/smt/network_flow_def.h | 2 +- src/smt/spanning_tree.h | 21 +++++++--- src/smt/spanning_tree_def.h | 57 ++++++++++++++++++++++++++ 4 files changed, 155 insertions(+), 7 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index ff01a4792..fcd4f6309 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -25,6 +25,7 @@ Revision History: #include"trace.h" #include"warning.h" #include"uint_set.h" +#include typedef int dl_var; @@ -953,6 +954,87 @@ public: return m_edges; } + void get_neighbours_undirected(dl_var current, svector & neighbours) { + neighbours.reset(); + edge_id_vector & edges = m_out_edges[current]; + typename edge_id_vector::iterator it = edges.begin(), end = edges.end(); + for (; it != end; ++it) { + edge_id e_id = *it; + edge & e = m_edges[e_id]; + if (!e.is_enabled()) continue; + SASSERT(e.get_source() == current); + dl_var neighbour = e.get_target(); + neighbours.push_back(neighbour); + } + edges = m_in_edges[current]; + it = edges.begin(); + end = edges.end(); + for (; it != end; ++it) { + edge_id e_id = *it; + edge & e = m_edges[e_id]; + if (!e.is_enabled()) continue; + SASSERT(e.get_target() == current); + dl_var neighbour = e.get_source(); + neighbours.push_back(neighbour); + } + } + + void dfs_undirected(dl_var start, svector & threads) { + threads.reset(); + threads.resize(get_num_nodes()); + uint_set visited; + svector nodes; + nodes.push_back(start); + dl_var prev = -1; + while(!nodes.empty()) { + dl_var current = nodes.back(); + nodes.pop_back(); + visited.insert(current); + if (prev != -1) + threads[prev] = current; + prev = current; + svector neighbours; + get_neighbours_undirected(current, neighbours); + for (unsigned i = 0; i < neighbours.size(); ++i) { + edge_id id; + SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id)); + if (!visited.contains(neighbours[i])) { + nodes.push_back(neighbours[i]); + } + } + } + threads[prev] = start; + } + + void bfs_undirected(dl_var start, svector & parents, svector & depths) { + parents.reset(); + parents.resize(get_num_nodes()); + depths.reset(); + depths.resize(get_num_nodes()); + uint_set visited; + std::deque nodes; + visited.insert(start); + nodes.push_front(start); + while(!nodes.empty()) { + dl_var current = nodes.back(); + nodes.pop_back(); + SASSERT(visited.contains(current)); + svector neighbours; + get_neighbours_undirected(current, neighbours); + for (unsigned i = 0; i < neighbours.size(); ++i) { + dl_var & next = neighbours[i]; + edge_id id; + SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)); + if (!visited.contains(next)) { + parents[next] = current; + depths[next] = depths[current] + 1; + visited.insert(next); + nodes.push_front(next); + } + } + } + } + template void enumerate_edges(dl_var source, dl_var target, Functor& f) { edge_id_vector & edges = m_out_edges[source]; diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 0ec7fe0c0..7af1a87ff 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -41,7 +41,7 @@ namespace smt { } } m_step = 0; - m_tree = alloc(thread_spanning_tree, m_graph); + m_tree = alloc(basic_spanning_tree, m_graph); } template diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index f5f6b624f..bce910b87 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -25,8 +25,8 @@ Notes: namespace smt { template - class thread_spanning_tree : public spanning_tree_base, private Ext { - private: + class thread_spanning_tree : public spanning_tree_base, protected Ext { + protected: typedef dl_var node; typedef dl_edge edge; typedef dl_graph graph; @@ -57,20 +57,29 @@ namespace smt { bool is_ancestor_of(node ancestor, node child); public: - thread_spanning_tree() {}; thread_spanning_tree(graph & g); - ~thread_spanning_tree() {}; - void initialize(svector const & tree); + virtual void initialize(svector const & tree); void get_descendants(node start, svector & descendants); - void update(edge_id enter_id, edge_id leave_id); + virtual void update(edge_id enter_id, edge_id leave_id); void get_path(node start, node end, svector & path, svector & against); bool in_subtree_t2(node child); bool check_well_formed(); }; + template + class basic_spanning_tree : public thread_spanning_tree { + private: + graph * m_tree_graph; + + public: + basic_spanning_tree(graph & g); + void initialize(svector const & tree); + void update(edge_id enter_id, edge_id leave_id); + }; + } #endif diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index 281a2cf45..32b971c45 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -412,6 +412,63 @@ namespace smt { SASSERT(children.empty()); return true; } + + // Basic spanning tree + template + basic_spanning_tree::basic_spanning_tree(graph & g) : thread_spanning_tree(g) { + } + + template + void basic_spanning_tree::initialize(svector const & tree) { + unsigned num_nodes = m_graph.get_num_nodes(); + m_tree_graph = alloc(graph); + for (unsigned i = 0; i < num_nodes; ++i) { + m_tree_graph->init_var(i); + } + + vector const & es = m_graph.get_all_edges(); + svector::const_iterator it = tree.begin(), end = tree.end(); + for(; it != end; ++it) { + edge const & e = es[*it]; + m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); + } + + node root = num_nodes - 1; + m_tree_graph->bfs_undirected(root, m_pred, m_depth); + m_tree_graph->dfs_undirected(root, m_thread); + } + + template + void basic_spanning_tree::update(edge_id enter_id, edge_id leave_id) { + if (m_tree_graph) + dealloc(m_tree_graph); + m_tree_graph = alloc(graph); + unsigned num_nodes = m_graph.get_num_nodes(); + for (unsigned i = 0; i < num_nodes; ++i) { + m_tree_graph->init_var(i); + } + + vector const & es = m_graph.get_all_edges(); + svector::const_iterator it = m_tree.begin(), end = m_tree.end(); + for(; it != end; ++it) { + edge const & e = es[*it]; + if (leave_id != *it) { + m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); + } + } + m_tree_graph->add_edge(m_graph.get_source(enter_id), m_graph.get_target(enter_id), m_graph.get_weight(enter_id), explanation()); + + node root = num_nodes - 1; + m_tree_graph->bfs_undirected(root, m_pred, m_depth); + m_tree_graph->dfs_undirected(root, m_thread); + + for (node x = m_thread[root]; x != root; x = m_thread[x]) { + edge_id id; + VERIFY(m_graph.get_edge_id(x, m_pred[x], id)); + m_tree[x] = id; + } + } + } #endif \ No newline at end of file