mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

adding ad-hoc method for converting models

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-28 17:29:31 -08:00
parent b1724b2f62
commit c80f34102f
7 changed files with 113 additions and 116 deletions

8
src/api/api_solver.cpp
View file

@ -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<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx->set_ignore_check(true);

7
src/api/dotnet/Solver.cs
View file

@ -446,6 +446,13 @@ namespace Microsoft.Z3
return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/// <summary>
/// Import model converter from other solver.
/// </summary>
public void ImportModelConverter(Solver src)
{
Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
}
/// <summary>
/// Solver statistics.

7
src/api/z3_api.h
View file

@ -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.

176
src/sat/ba_solver.cpp
View file

@ -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<lp::var_index> 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<lp::var_index> 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<pb_base const&>(*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);

28
src/sat/ba_solver.h
View file

@ -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<ba_sort> 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<std::pair<rational, lp::var_index>> 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<lp::var_index> 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();
};
};

2
src/sat/sat_config.cpp
View file

@ -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();
}

1
src/sat/sat_config.h
View file

@ -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;