From 5e026b78979ef480364186f6f4f2c96bc391e5e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Aug 2014 23:34:43 -0700 Subject: [PATCH] mss and maxres tuning Signed-off-by: Nikolaj Bjorner --- src/opt/mss.cpp | 161 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/mss.h | 52 ++++++++++++++++ src/opt/mus.cpp | 2 - src/opt/mus.h | 2 +- 4 files changed, 214 insertions(+), 3 deletions(-) create mode 100644 src/opt/mss.cpp create mode 100644 src/opt/mss.h diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp new file mode 100644 index 000000000..d0780c916 --- /dev/null +++ b/src/opt/mss.cpp @@ -0,0 +1,161 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mss.cpp + +Abstract: + + MSS/MCS extraction. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-2-8 + +Notes: + + +--*/ + +#include "solver.h" +#include "smt_literal.h" +#include "mss.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + +namespace opt { + + + mss::mss(solver& s, ast_manager& m): s(s), m(m), m_cancel(false) { + } + + mss::~mss() { + } + + + void mss::check_parameters(vector const& cores, exprs& literals) { + expr* n; + for (unsigned i = 0; i < literals.size(); ++i) { + n = literals[i]; + m.is_not(n, n); + if (!is_uninterp_const(n)) { + throw default_exception("arguments have to be uninterpreted literals"); + } + } + // cores are disjoint + // cores are a subset of literals + // literals not in cores evaluate to true in current model + } + + /** + \brief Move literals satisfied in todo into mss. + Precondition: the solver state is satisfiable. + */ + void mss::update_model() { + expr_ref tmp(m); + s.get_model(m_model); + update_set(m_todo); + } + + void mss::update_set(exprs& lits) { + expr_ref tmp(m); + unsigned sz = lits.size(); + unsigned j = 0; + for (unsigned i = 0; i < lits.size(); ++i) { + expr* n = lits[i]; + if (m_mcs.contains(n)) { + // remove from todo. + continue; + } + VERIFY(m_model->eval(n, tmp)); + if (m.is_false(tmp)) { + if (j != i) { + lits[j] = lits[i]; + } + ++j; + } + else { + m_mss.push_back(n); + } + } + lits.resize(j); + } + + + lbool mss::operator()(vector const& cores, exprs& literals) { + m_mss.reset(); + m_mcs.reset(); + m_todo.reset(); + m_todo.append(literals); + check_parameters(cores, literals); + update_model(); + lbool is_sat = l_true; + for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { + is_sat = process_core(cores[i]); + } + if (is_sat == l_true) { + literals.reset(); + literals.append(m_mss); + } + return is_sat; + } + + lbool mss::process_core(exprs const& _core) { + // at least one literal in core is false in current model. + // pick literals in core that are not yet in mss. + exprs core(_core); + update_set(core); + return process_core(1, core); + } + + lbool mss::process_core(unsigned sz, exprs& core) { + TRACE("opt", tout << "process: " << sz << " out of " << core.size() << " literals\n";); + SASSERT(sz > 0); + if (core.empty()) { + return l_true; + } + if (m_cancel) { + return l_undef; + } + sz = std::min(sz, core.size()); + unsigned sz_save = m_mss.size(); + m_mss.append(sz, core.c_ptr()); + lbool is_sat = s.check_sat(m_mss.size(), m_mss.c_ptr()); + m_mss.resize(sz_save); + switch (is_sat) { + case l_true: + update_model(); + update_set(core); + return process_core(2*sz, core); + case l_false: + if (sz == 1) { + m_mcs.insert(core[0]); + core[0] = core.back(); + core.pop_back(); + } + else { + exprs core2; + core2.append(core.size()-sz, core.c_ptr()+sz); + core.resize(sz); + is_sat = process_core(sz, core2); + if (is_sat != l_true) { + return is_sat; + } + } + return process_core(1, core); + case l_undef: + return l_undef; + } + + return l_true; + } + + void mss::display(std::ostream& out) const { + + } +} + + + + diff --git a/src/opt/mss.h b/src/opt/mss.h new file mode 100644 index 000000000..2e5d82df2 --- /dev/null +++ b/src/opt/mss.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mss.h + +Abstract: + + Maximal satisfying subset/minimal correction sets: MSS/MCS + +Author: + + Nikolaj Bjorner (nbjorner) 2014-2-8 + +Notes: + +--*/ +#ifndef _MSS_H_ +#define _MSS_H_ + +namespace opt { + class mss { + solver& s; + ast_manager& m; + volatile bool m_cancel; + typedef ptr_vector exprs; + typedef obj_hashtable expr_set; + exprs m_mss; + expr_set m_mcs; + exprs m_todo; + model_ref m_model; + public: + mss(solver& s, ast_manager& m); + ~mss(); + + lbool operator()(vector > const& cores, ptr_vector& literals); + + void set_cancel(bool f) { m_cancel = f; } + + private: + void check_parameters(vector const& cores, exprs& literals); + void update_model(); + void update_set(exprs& lits); + lbool process_core(exprs const& _core); + lbool process_core(unsigned sz, exprs& core); + void display(std::ostream& out) const; + }; + +}; + +#endif diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 5fd246294..a8126e699 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -15,8 +15,6 @@ Author: Notes: - Model rotation needs fixes to ensure that hard constraints are satisfied - under pertubed model. Model rotation also has o be consistent with theories. --*/ diff --git a/src/opt/mus.h b/src/opt/mus.h index e9e3b80bd..3a96b4842 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + Basic MUS extraction Author: