mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-08-25 12:11:49 -07:00
commit 15734398d8
9 changed files with 212 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/inc_sat_solver.cpp
View file

@ -228,11 +228,25 @@ private:
r = internalize_assumptions(soft.size(), soft.c_ptr(), dep2asm);
sat::literal_vector lits;
svector<double> weights;
sat::literal lit;
if (r == l_true) {
for (unsigned i = 0; i < soft.size(); ++i) {
weights.push_back(m_weights[i].get_double());
lits.push_back(dep2asm.find(soft[i].get()));
expr* s = soft[i].get();
bool is_neg = m.is_not(s, s);
if (!dep2asm.find(s, lit)) {
std::cout << "not found: " << mk_pp(s, m) << "\n";
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
std::cout << mk_pp(it->m_key, m) << " " << it->m_value << "\n";
}
UNREACHABLE();
}
if (is_neg) {
lit.neg();
}
lits.push_back(lit);
}
m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr());
m_params.set_bool("optimize_model", true);

1
src/opt/maxsls.cpp
View file

@ -33,6 +33,7 @@ namespace opt {
lbool operator()() {
IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
init();
set_enable_sls(true);
enable_sls(m_soft, m_weights);
lbool is_sat = s().check_sat(0, 0);
if (is_sat == l_true) {

4
src/opt/maxsmt.cpp
View file

@ -98,6 +98,10 @@ namespace opt {
m_c.enable_sls(soft, ws);
}
void maxsmt_solver_base::set_enable_sls(bool f) {
m_c.set_enable_sls(f);
}
app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
app* result = m.mk_fresh_const(name, m.mk_bool_sort());
m_c.fm().insert(result->get_decl());

2
src/opt/maxsmt.h
View file

@ -84,6 +84,8 @@ namespace opt {
app* mk_fresh_bool(char const* name);
protected:
void enable_sls(expr_ref_vector const& soft, weights_t& ws);
void set_enable_sls(bool f);
};
/**

1
src/opt/opt_context.h
View file

@ -177,6 +177,7 @@ namespace opt {
ast_manager& get_manager() { return this->m; }
params_ref& params() { return m_params; }
void enable_sls(expr_ref_vector const& soft, weights_t& weights);
void set_enable_sls(bool f) { m_enable_sls = f; }
symbol const& maxsat_engine() const { return m_maxsat_engine; }