mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

inc sat experiment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-15 08:46:20 -07:00
parent d849b5c637
commit 33e2f2012d
1 changed files with 32 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/opt/weighted_maxsat.cpp
View file

@ -45,6 +45,9 @@ Notes:
#include "sat_solver.h" #include "sat_solver.h"
#include "goal2sat.h" #include "goal2sat.h"
#define _INC_SAT 0
namespace opt { namespace opt {
static app_ref mk_bv_vec(ast_manager& m, sort* s) { static app_ref mk_bv_vec(ast_manager& m, sort* s) {
@ -76,7 +79,7 @@ namespace opt {
inc_sat_solver(ast_manager& m, params_ref const& p, expr_ref_vector const& soft, vector<rational> const& weights): inc_sat_solver(ast_manager& m, params_ref const& p, expr_ref_vector const& soft, vector<rational> const& weights):
m(m), m_solver(p,0), m_params(p), m(m), m_solver(p,0), m_params(p),
m_fmls(m), m_map(m), m_soft(m) { m_fmls(m), m_map(m), m_soft(m) {
// m_params.set_bool("elim_vars", false); m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params); m_solver.updt_params(m_params);
params_ref simp2_p = p; params_ref simp2_p = p;
simp2_p.set_bool("som", true); simp2_p.set_bool("som", true);
@ -116,7 +119,6 @@ namespace opt {
for (unsigned i = 0; i < m_fmls.size(); ++i) { for (unsigned i = 0; i < m_fmls.size(); ++i) {
g->assert_expr(m_fmls[i].get()); g->assert_expr(m_fmls[i].get());
} }
//g->assert_expr(m_soft);
TRACE("opt", g->display(tout);); TRACE("opt", g->display(tout););
m_fmls.reset(); m_fmls.reset();
try { try {
@ -146,23 +148,29 @@ namespace opt {
atom2bool_var::iterator end = m_map.end(); atom2bool_var::iterator end = m_map.end();
for (; it != end; ++it) { for (; it != end; ++it) {
expr * n = it->m_key; expr * n = it->m_key;
if (is_app(n) && to_app(n)->get_num_args() > 0) continue; if (is_app(n) && to_app(n)->get_num_args() > 0) {
IF_VERBOSE(0, verbose_stream() << "skip: " << mk_pp(n, m) << "\n";);
continue;
}
sat::bool_var v = it->m_value; sat::bool_var v = it->m_value;
switch (sat::value_at(v, ll_m)) { switch (sat::value_at(v, ll_m)) {
case l_true: case l_true:
IF_VERBOSE(0, verbose_stream() << "true: " << mk_pp(n, m) << "\n";);
md->register_decl(to_app(n)->get_decl(), m.mk_true()); md->register_decl(to_app(n)->get_decl(), m.mk_true());
break; break;
case l_false: case l_false:
IF_VERBOSE(0, verbose_stream() << "false: " << mk_pp(n, m) << "\n";);
md->register_decl(to_app(n)->get_decl(), m.mk_false()); md->register_decl(to_app(n)->get_decl(), m.mk_false());
break; break;
default: default:
IF_VERBOSE(0, verbose_stream() << "undef: " << mk_pp(n, m) << "\n";);
break; break;
} }
} }
m_model = md; m_model = md;
if (m_mc) { //if (m_mc) {
(*m_mc)(m_model); // (*m_mc)(m_model);
} //}
// IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *(m_model.get()), 0);); // IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *(m_model.get()), 0););
} }
m_solver.collect_statistics(m_stats); m_solver.collect_statistics(m_stats);
@ -200,7 +208,7 @@ namespace opt {
} }
virtual void updt_params(params_ref const & p) { virtual void updt_params(params_ref const & p) {
m_params = p; m_params = p;
//m_params.set_bool("elim_vars", false); m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params); m_solver.updt_params(m_params);
} }
@ -348,13 +356,13 @@ namespace opt {
void enable_bvsat() { void enable_bvsat() {
if (m_enable_sat && !m_sat_enabled && probe_bv()) { if (m_enable_sat && !m_sat_enabled && probe_bv()) {
#if 0 #if _INC_SAT
solver* sat_solver = alloc(inc_sat_solver, m, m_params, m_soft, m_weights);
#else
tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); tactic_ref pb2bv = mk_card2bv_tactic(m, m_params);
tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); tactic_ref bv2sat = mk_qfbv_tactic(m, m_params);
tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); tactic_ref tac = and_then(pb2bv.get(), bv2sat.get());
solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params);
#else
solver* sat_solver = alloc(inc_sat_solver, m, m_params, m_soft, m_weights);
#endif #endif
unsigned sz = s().get_num_assertions(); unsigned sz = s().get_num_assertions();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
@ -772,6 +780,7 @@ namespace opt {
virtual ~pbmax() {} virtual ~pbmax() {}
#if _INC_SAT
lbool operator()() { lbool operator()() {
enable_bvsat(); enable_bvsat();
enable_sls(); enable_sls();
@ -806,10 +815,13 @@ namespace opt {
lbool is_sat = s().check_sat(0,0); lbool is_sat = s().check_sat(0,0);
while (l_true == is_sat) { while (l_true == is_sat) {
TRACE("opt", s().display(tout<<"looping\n");); s().get_model(m_model);
TRACE("opt", s().display(tout<<"looping\n");
model_smt2_pp(tout, m, *(m_model.get()), 0););
m_model->eval(var, val); m_model->eval(var, val);
unsigned bv_size; unsigned bv_size;
if (bv.is_numeral(val, m_upper, bv_size)) { VERIFY(bv.is_numeral(val, m_upper, bv_size));
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";); IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";);
TRACE("opt", tout << "new upper: " << m_upper << "\n";); TRACE("opt", tout << "new upper: " << m_upper << "\n";);
@ -817,7 +829,7 @@ namespace opt {
// fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); // fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
// solver::scoped_push _scope2(s()); // solver::scoped_push _scope2(s());
s().assert_expr(fml); s().assert_expr(fml);
}
is_sat = s().check_sat(0,0); is_sat = s().check_sat(0,0);
if (m_cancel) { if (m_cancel) {
is_sat = l_undef; is_sat = l_undef;
@ -834,7 +846,7 @@ namespace opt {
return is_sat; return is_sat;
} }
#if 0 #else
lbool operator()() { lbool operator()() {
enable_bvsat(); enable_bvsat();
enable_sls(); enable_sls();