From c80f34102fa0a290b2798b256ca09c3b4cd56786 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Dec 2017 17:29:31 -0800 Subject: [PATCH] adding ad-hoc method for converting models Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 8 ++ src/api/dotnet/Solver.cs | 7 ++ src/api/z3_api.h | 7 ++ src/sat/ba_solver.cpp | 176 +++++++++++++++------------------------ src/sat/ba_solver.h | 28 +++++-- src/sat/sat_config.cpp | 2 + src/sat/sat_config.h | 1 + 7 files changed, 113 insertions(+), 116 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 97fa23a79..4e7719f56 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -128,6 +128,14 @@ extern "C" { Z3_CATCH_RETURN(0); } + void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) { + Z3_TRY; + LOG_Z3_solver_import_model_converter(c, src, dst); + model_converter_ref mc = to_solver_ref(src)->get_model_converter(); + to_solver_ref(dst)->set_model_converter(mc.get()); + Z3_CATCH; + } + void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) { scoped_ptr ctx = alloc(cmd_context, false, &(mk_c(c)->m())); ctx->set_ignore_check(true); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index f67a298bb..1a62aa8e3 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -446,6 +446,13 @@ namespace Microsoft.Z3 return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx)); } + /// + /// Import model converter from other solver. + /// + public void ImportModelConverter(Solver src) + { + Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject); + } /// /// Solver statistics. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 99d6021ef..02ca43910 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6035,6 +6035,13 @@ extern "C" { */ Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target); + /** + \brief Ad-hoc method for importing model convertion from solver. + + def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER))) + */ + void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst); + /** \brief Return a string describing all solver available parameters. diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index e5623c05f..be4498061 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1518,7 +1518,7 @@ namespace sat { return p; } - ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0) { + ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); } @@ -2436,119 +2436,54 @@ namespace sat { } } - // ---------------------------------- - // lp based relaxation - -#if 0 - void ba_solver::lp_add_var(int coeff, lp::var_index v, lhs_t& lhs, rational& rhs) { - if (coeff < 0) { - rhs += rational(coeff); - } - lhs.push_back(std::make_pair(rational(coeff), v)); + // ------------------------- + // sorting networks + literal ba_solver::ba_sort::mk_false() { + return ~mk_true(); } - void ba_solver::lp_add_clause(lp::lar_solver& s, svector const& vars, clause const& c) { - lhs_t lhs; - rational rhs; - if (c.frozen()) return; - rhs = rational::one(); - for (literal l : c) { - lp_add_var(l.sign() ? -1 : 1, vars[l.var()], lhs, rhs); + literal ba_solver::ba_sort::mk_true() { + if (m_true == null_literal) { + bool_var v = s.s().mk_var(false, false); + m_true = literal(v, false); + s.s().mk_clause(1,&m_true); } - s.add_constraint(lhs, lp::GE, rhs); + VERIFY(m_true != null_literal); + return m_true; } - void ba_solver::lp_lookahead_reduction() { - lp::lar_solver solver; - solver.settings().set_message_ostream(&std::cout); - solver.settings().set_debug_ostream(&std::cout); - solver.settings().print_statistics = true; - solver.settings().report_frequency = 1000; - // solver.settings().simplex_strategy() = lp::simplex_strategy_enum::lu; - runs out of memory - // TBD: set rlimit on the solver - svector vars; - for (unsigned i = 0; i < s().num_vars(); ++i) { - lp::var_index v = solver.add_var(i, false); - vars.push_back(v); - solver.add_var_bound(v, lp::GE, rational::zero()); - solver.add_var_bound(v, lp::LE, rational::one()); - switch (value(v)) { - case l_true: solver.add_var_bound(v, lp::GE, rational::one()); break; - case l_false: solver.add_var_bound(v, lp::LE, rational::zero()); break; - default: break; - } - } - lhs_t lhs; - rational rhs; - for (clause* c : s().m_clauses) { - lp_add_clause(solver, vars, *c); - } - for (clause* c : s().m_learned) { - lp_add_clause(solver, vars, *c); - } - for (constraint const* c : m_constraints) { - if (c->lit() != null_literal) continue; // ignore definitions for now. - switch (c->tag()) { - case card_t: - case pb_t: { - pb_base const& p = dynamic_cast(*c); - rhs = rational(p.k()); - lhs.reset(); - for (unsigned i = 0; i < p.size(); ++i) { - literal l = p.get_lit(i); - int co = p.get_coeff(i); - lp_add_var(l.sign() ? -co : co, vars[l.var()], lhs, rhs); - } - solver.add_constraint(lhs, lp::GE, rhs); - break; - } - default: - // ignore xor - break; - } - } - std::cout << "lp solve\n"; - std::cout.flush(); - - lp::lp_status st = solver.solve(); - if (st == lp::lp_status::INFEASIBLE) { - std::cout << "infeasible\n"; - s().set_conflict(justification()); - return; - } - std::cout << "feasible\n"; - std::cout.flush(); - for (unsigned i = 0; i < s().num_vars(); ++i) { - lp::var_index v = vars[i]; - if (value(v) != l_undef) continue; - // TBD: take initial model into account to limit queries. - std::cout << "solve v" << v << "\n"; - std::cout.flush(); - solver.push(); - solver.add_var_bound(v, lp::GE, rational::one()); - st = solver.solve(); - solver.pop(1); - if (st == lp::lp_status::INFEASIBLE) { - std::cout << "found unit: " << literal(v, true) << "\n"; - s().assign(literal(v, true), justification()); - solver.add_var_bound(v, lp::LE, rational::zero()); - continue; - } - - solver.push(); - solver.add_var_bound(v, lp::LE, rational::zero()); - st = solver.solve(); - solver.pop(1); - if (st == lp::lp_status::INFEASIBLE) { - std::cout << "found unit: " << literal(v, false) << "\n"; - s().assign(literal(v, false), justification()); - solver.add_var_bound(v, lp::GE, rational::zero()); - continue; - } - } + literal ba_solver::ba_sort::mk_not(literal l) { + return ~l; } -#endif + literal ba_solver::ba_sort::fresh(char const*) { + bool_var v = s.s().mk_var(false, true); + return literal(v, false); + } + + literal ba_solver::ba_sort::mk_max(literal l1, literal l2) { + VERIFY(l1 != null_literal); + VERIFY(l2 != null_literal); + if (l1 == m_true) return l1; + if (l2 == m_true) return l2; + if (l1 == ~m_true) return l2; + if (l2 == ~m_true) return l1; + literal max = fresh("max"); + s.s().mk_clause(~l1, max); + s.s().mk_clause(~l2, max); + s.s().mk_clause(~max, l1, l2); + return max; + } + + literal ba_solver::ba_sort::mk_min(literal l1, literal l2) { + return ~mk_max(~l1, ~l2); + } + + void ba_solver::ba_sort::mk_clause(unsigned n, literal const* lits) { + literal_vector _lits(n, lits); + s.s().mk_clause(n, _lits.c_ptr()); + } + // ------------------------------- // set literals equivalent @@ -2665,6 +2600,10 @@ namespace sat { c.set_size(sz); c.set_k(k); + if (clausify(c)) { + return; + } + if (!all_units) { TRACE("ba", tout << "replacing by pb: " << c << "\n";); m_wlits.reset(); @@ -2684,6 +2623,27 @@ namespace sat { } } + bool ba_solver::clausify(card& c) { +#if 0 + if (get_config().m_card_solver) + return false; + + // + // TBD: conditions for when to clausify are TBD and + // handling of conditional cardinality as well. + // + if (c.lit() == null_literal) { + if (!c.learned() && !std::any_of(c.begin(), c.end(), [&](literal l) { return s().was_eliminated(l.var()); })) { + IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n"; + m_sort.ge(false, c.k(), c.size(), c.begin()); + } + remove_constraint(c, "recompiled to clauses"); + return true; + } +#endif + return false; + } + void ba_solver::split_root(constraint& c) { switch (c.tag()) { @@ -2693,8 +2653,6 @@ namespace sat { } } - - void ba_solver::flush_roots(constraint& c) { if (c.lit() != null_literal && !is_watched(c.lit(), c)) { watch_literal(c.lit(), c); diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index e7a220f5c..f447be64c 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -26,8 +26,7 @@ Revision History: #include "sat/sat_lookahead.h" #include "sat/sat_unit_walk.h" #include "util/scoped_ptr_vector.h" -#include "util/lp/lar_solver.h" - +#include "util/sorting_network.h" namespace sat { @@ -232,6 +231,24 @@ namespace sat { unsigned_vector m_pb_undef; + struct ba_sort { + ba_solver& s; + literal m_true; + + typedef sat::literal literal; + typedef sat::literal_vector literal_vector; + ba_sort(ba_solver& s): s(s), m_true(null_literal) {} + literal mk_false(); + literal mk_true(); + literal mk_not(literal l); + literal fresh(char const*); + literal mk_max(literal l1, literal l2); + literal mk_min(literal l1, literal l2); + void mk_clause(unsigned n, literal const* lits); + }; + ba_sort m_ba; + psort_nw m_sort; + void ensure_parity_size(bool_var v); unsigned get_parity(bool_var v); void inc_parity(bool_var v); @@ -277,11 +294,6 @@ namespace sat { void update_psm(constraint& c) const; void mutex_reduction(); - typedef vector> lhs_t; - void lp_lookahead_reduction(); - void lp_add_var(int coeff, lp::var_index v, lhs_t& lhs, rational& rhs); - void lp_add_clause(lp::lar_solver& s, svector const& vars, clause const& c); - unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); } void cleanup_clauses(); @@ -330,6 +342,7 @@ namespace sat { void get_antecedents(literal l, card const& c, literal_vector & r); void flush_roots(card& c); void recompile(card& c); + bool clausify(card& c); lbool eval(card const& c) const; double get_reward(card const& c, literal_occs_fun& occs) const; @@ -482,6 +495,7 @@ namespace sat { virtual bool validate(); + }; }; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 4cf448394..b67666993 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -177,6 +177,8 @@ namespace sat { else throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting"); + m_card_solver = p.cardinality_solver(); + sat_simplifier_params sp(_p); m_elim_vars = sp.elim_vars(); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 2aa5a325b..e64c0c544 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -129,6 +129,7 @@ namespace sat { bool m_drat_check_sat; pb_solver m_pb_solver; + bool m_card_solver; // branching heuristic settings. branching_heuristic m_branching_heuristic;