mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

experimenting with inc_sat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-14 09:27:47 -07:00
parent 6821d61ac4
commit 6d6abb4dde
1 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/opt/weighted_maxsat.cpp
View file

@ -51,7 +51,9 @@ namespace opt {
expr_ref_vector m_fmls; expr_ref_vector m_fmls;
atom2bool_var m_map; atom2bool_var m_map;
model_ref m_model; model_ref m_model;
model_converter_ref m_mc;
tactic_ref m_preprocess; tactic_ref m_preprocess;
statistics m_stats;
public: public:
inc_sat_solver(ast_manager& m, params_ref const& p): inc_sat_solver(ast_manager& m, params_ref const& p):
m(m), m_solver(p,0), m_params(p), m(m), m_solver(p,0), m_params(p),
@ -68,9 +70,10 @@ namespace opt {
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(num_assumptions == 0); SASSERT(num_assumptions == 0);
m_solver.pop(m_solver.scope_lvl());
goal_ref_buffer result; goal_ref_buffer result;
model_converter_ref mc; // TODO make model convertion work between checks
proof_converter_ref pc; proof_converter_ref pc;
model_converter_ref mc;
expr_dependency_ref core(m); expr_dependency_ref core(m);
if (!m_fmls.empty()) { if (!m_fmls.empty()) {
@ -84,8 +87,10 @@ namespace opt {
} }
catch (tactic_exception &) { catch (tactic_exception &) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic\n";); IF_VERBOSE(0, verbose_stream() << "exception in tactic\n";);
m_preprocess->collect_statistics(m_stats);
return l_undef; return l_undef;
} }
m_mc = concat(m_mc.get(), mc.get());
// TODO: check that result is a singleton. // TODO: check that result is a singleton.
if (result.size() != 1) { if (result.size() != 1) {
IF_VERBOSE(0, verbose_stream() << "size of result is not 1, it is: " << result.size() << "\n";); IF_VERBOSE(0, verbose_stream() << "size of result is not 1, it is: " << result.size() << "\n";);
@ -114,13 +119,13 @@ namespace opt {
break; break;
} }
} }
TRACE("sat_tactic", model_v2_pp(tout, *md););
m_model = md; m_model = md;
if (mc) { if (m_mc) {
(*mc)(m_model); (*m_mc)(m_model);
} }
// IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *(m_model.get()), 0););
} }
m_solver.pop(m_solver.scope_lvl()); m_solver.collect_statistics(m_stats);
return r; return r;
} }
virtual void set_cancel(bool f) { virtual void set_cancel(bool f) {
@ -157,7 +162,9 @@ namespace opt {
m_params = p; m_params = p;
} }
virtual void collect_statistics(statistics & st) const {} virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void get_unsat_core(ptr_vector<expr> & r) { virtual void get_unsat_core(ptr_vector<expr> & r) {
UNREACHABLE(); UNREACHABLE();
} }