mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

refactor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-04-19 11:58:57 -07:00
parent 5ead06bcef
commit 032e2618f6
3 changed files with 166 additions and 165 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/opt/opt_sls_solver.h
View file

@ -21,6 +21,7 @@ Notes:
#define _OPT_SLS_SOLVER_H_
#include "solver_na2as.h"
#include "card2bv_tactic.h"
namespace opt {
@ -28,15 +29,17 @@ namespace opt {
ast_manager& m;
ref<solver> m_solver;
bvsls_opt_engine m_sls;
pb::card_pb_rewriter m_pb2bv;
model_ref m_model;
expr_ref m_objective;
expr_ref m_objective;
public:
sls_solver(ast_manager & m, solver* s, expr* to_maximize, params_ref const& p):
solver_na2as(m),
m(m),
m_solver(s),
m_sls(m, p),
m_objective(to_maximize,m)
m_pb2bv(m),
m_objective(to_maximize, m)
{
}
virtual ~sls_solver() {}
@ -52,8 +55,10 @@ namespace opt {
// TBD: m_sls.get_stats();
}
virtual void assert_expr(expr * t) {
expr_ref tmp(m);
m_solver->assert_expr(t);
m_sls.assert_expr(t);
m_pb2bv(t, tmp);
m_sls.assert_expr(tmp);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
m_solver->get_unsat_core(r);
@ -89,15 +94,16 @@ namespace opt {
}
protected:
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
typedef bvsls_opt_engine::optimization_result opt_result;
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
lbool r = m_solver->check_sat(num_assumptions, assumptions);
if (r == l_true) {
m_solver->get_model(m_model);
bvsls_opt_engine::optimization_result or(m);
or = m_sls.optimize(m_objective, m_model, true);
SASSERT(or.is_sat == l_true);
assertions2sls();
opt_result or = m_sls.optimize(m_objective, m_model, true);
SASSERT(or.is_sat == l_true || or.is_sat == l_undef);
m_sls.get_model(m_model);
or.optimum;
}
return r;
}
@ -107,6 +113,26 @@ namespace opt {
virtual void pop_core(unsigned n) {
m_solver->pop(n);
}
private:
void assertions2sls() {
expr_ref tmp(m);
goal_ref g(alloc(goal, m, true, false));
for (unsigned i = 0; i < m_solver->get_num_assertions(); ++i) {
m_pb2bv(m_solver->get_assertion(i), tmp);
g->assert_expr(tmp);
}
tactic_ref simplify = mk_nnf_tactic(m);
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
model_converter_ref model_converter;
(*simplify)(g, result, model_converter, pc, core);
SASSERT(result.size() == 1);
goal* r = result[0];
for (unsigned i = 0; i < r->size(); ++i) {
m_sls.assert_expr(r->form(i));
}
}
};
}