mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Switch spacer_prop_solver to check_sat_cc

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-29 13:18:02 -07:00
parent 1343b272e7
commit f7d015de8d
2 changed files with 14 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -224,7 +224,8 @@ lbool prop_solver::mss(expr_ref_vector &hard, expr_ref_vector &soft) {
/// Poor man's maxsat. No guarantees of maximum solution /// Poor man's maxsat. No guarantees of maximum solution
/// Runs maxsat loop on m_ctx Returns l_false if hard is unsat, /// Runs maxsat loop on m_ctx Returns l_false if hard is unsat,
/// otherwise reduces soft such that hard & soft is sat. /// otherwise reduces soft such that hard & soft is sat.
lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft) lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
const expr_ref_vector &clause)
{ {
// replace expressions by assumption literals // replace expressions by assumption literals
iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard); iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard);
@ -232,7 +233,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft)
// assume soft constraints are propositional literals (no need to proxy) // assume soft constraints are propositional literals (no need to proxy)
hard.append(soft); hard.append(soft);
lbool res = m_ctx->check_sat(hard.size(), hard.c_ptr()); lbool res = m_ctx->check_sat_cc(hard, clause);
// if hard constraints alone are unsat or there are no soft // if hard constraints alone are unsat or there are no soft
// constraints, we are done // constraints, we are done
if (res != l_false || soft.empty()) { return res; } if (res != l_false || soft.empty()) { return res; }
@ -266,7 +267,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft)
} }
// check that the NEW constraints became sat // check that the NEW constraints became sat
res = m_ctx->check_sat(hard.size(), hard.c_ptr()); res = m_ctx->check_sat_cc(hard, clause);
if (res != l_false) { break; } if (res != l_false) { break; }
// still unsat, update the core and repeat // still unsat, update the core and repeat
core.reset(); core.reset();
@ -284,9 +285,9 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft)
return res; return res;
} }
lbool prop_solver::internal_check_assumptions( lbool prop_solver::internal_check_assumptions(expr_ref_vector &hard_atoms,
expr_ref_vector& hard_atoms, expr_ref_vector &soft_atoms,
expr_ref_vector& soft_atoms) const expr_ref_vector &clause)
{ {
// XXX Turn model generation if m_model != 0 // XXX Turn model generation if m_model != 0
SASSERT(m_ctx); SASSERT(m_ctx);
@ -298,7 +299,7 @@ lbool prop_solver::internal_check_assumptions(
} }
if (m_in_level) { assert_level_atoms(m_current_level); } if (m_in_level) { assert_level_atoms(m_current_level); }
lbool result = maxsmt(hard_atoms, soft_atoms); lbool result = maxsmt(hard_atoms, soft_atoms, clause);
if (result != l_false && m_model) { m_ctx->get_model(*m_model); } if (result != l_false && m_model) { m_ctx->get_model(*m_model); }
SASSERT(result != l_false || soft_atoms.empty()); SASSERT(result != l_false || soft_atoms.empty());
@ -352,8 +353,6 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
unsigned solver_id) unsigned solver_id)
{ {
expr_ref cls(m); expr_ref cls(m);
// XXX now clause is only supported when pushing is enabled
SASSERT(clause.empty() || !m_use_push_bg);
// current clients expect that flattening of HARD is // current clients expect that flattening of HARD is
// done implicitly during check_assumptions // done implicitly during check_assumptions
expr_ref_vector hard(m); expr_ref_vector hard(m);
@ -364,13 +363,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
// can be disabled if use_push_bg == true // can be disabled if use_push_bg == true
// solver::scoped_push _s_(*m_ctx); // solver::scoped_push _s_(*m_ctx);
if (!m_use_push_bg) { if (!m_use_push_bg) {m_ctx->push();}
m_ctx->push();
if (!clause.empty()) {
cls = mk_or(clause);
m_ctx->assert_expr(cls);
}
}
iuc_solver::scoped_bg _b_(*m_ctx); iuc_solver::scoped_bg _b_(*m_ctx);
for (unsigned i = 0; i < num_bg; ++i) for (unsigned i = 0; i < num_bg; ++i)
@ -379,7 +372,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
unsigned soft_sz = soft.size(); unsigned soft_sz = soft.size();
(void) soft_sz; (void) soft_sz;
lbool res = internal_check_assumptions(hard, soft); lbool res = internal_check_assumptions(hard, soft, clause);
if (!m_use_push_bg) { m_ctx->pop(1); } if (!m_use_push_bg) { m_ctx->pop(1); }
TRACE("psolve_verbose", TRACE("psolve_verbose",

6
src/muz/spacer/spacer_prop_solver.h
View file

@ -64,9 +64,11 @@ private:
void ensure_level(unsigned lvl); void ensure_level(unsigned lvl);
lbool internal_check_assumptions(expr_ref_vector &hard, lbool internal_check_assumptions(expr_ref_vector &hard,
expr_ref_vector &soft); expr_ref_vector &soft,
const expr_ref_vector &clause);
lbool maxsmt(expr_ref_vector &hard, expr_ref_vector &soft); lbool maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
const expr_ref_vector &clause);
lbool mss(expr_ref_vector &hard, expr_ref_vector &soft); lbool mss(expr_ref_vector &hard, expr_ref_vector &soft);