mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

revising pd-maxres

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-23 10:53:39 -07:00
parent da0c12cdba
commit 546a9b8f03
9 changed files with 65 additions and 82 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/maxres.cpp
View file

@ -171,7 +171,7 @@ public:
}
void new_assumption(expr* e, rational const& w) {
IF_VERBOSE(3, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";);
IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";);
TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";);
m_asm2weight.insert(e, w);
m_asms.push_back(e);

14
src/opt/maxsls.cpp
View file

@ -20,6 +20,8 @@ Notes:
#include "maxsls.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
#include "opt_context.h"
#include "inc_sat_solver.h"
namespace opt {
@ -34,7 +36,7 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
init();
enable_sls(true);
lbool is_sat = s().check_sat(0, 0);
lbool is_sat = check();
if (is_sat == l_true) {
s().get_model(m_model);
m_upper.reset();
@ -49,6 +51,16 @@ namespace opt {
}
return is_sat;
}
lbool check() {
if (m_c.sat_enabled()) {
return inc_sat_check_sat(
s(), m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr(), m_upper);
}
else {
return s().check_sat(0, 0);
}
}
};

1
src/sat/sat_sls.cpp
View file

@ -386,6 +386,7 @@ namespace sat {
m_best_value = val;
m_best_model.reset();
m_best_model.append(m_model);
s.set_model(m_best_model);
IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
if (i*2 > m_max_tries) {
m_max_tries *= 2;

1
src/sat/sat_sls.h
View file

@ -97,7 +97,6 @@ namespace sat {
void set_soft(unsigned sz, literal const* lits, double const* weights);
bool has_soft() const { return !m_soft.empty(); }
void opt(unsigned sz, literal const* tabu, bool reuse_model);
model const& get_model() { return m_best_model; }
virtual void display(std::ostream& out) const;
double evaluate_model(model& mdl);
private:

12
src/sat/sat_solver.cpp
View file

@ -1105,6 +1105,12 @@ namespace sat {
}
}
void solver::set_model(model const& mdl) {
m_model.reset();
m_model.append(mdl);
m_model_is_current = !m_model.empty();
}
void solver::mk_model() {
m_model.reset();
m_model_is_current = true;
@ -1117,8 +1123,6 @@ namespace sat {
TRACE("sat_mc_bug", m_mc.display(tout););
if (m_config.m_optimize_model) {
m_wsls.opt(0, 0, false);
m_model.reset();
m_model.append(m_wsls.get_model());
}
m_mc(m_model);
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
@ -1808,9 +1812,7 @@ namespace sat {
// apply optional clause minimization by detecting subsumed literals.
// initial experiment suggests it has no effect.
m_mus(); // ignore return value on cancelation.
m_model.reset();
m_model.append(m_mus.get_model());
m_model_is_current = !m_model.empty();
set_model(m_mus.get_model());
}
}

1
src/sat/sat_solver.h
View file

@ -280,6 +280,7 @@ namespace sat {
bool model_is_current() const { return m_model_is_current; }
literal_vector const& get_core() const { return m_core; }
model_converter const & get_model_converter() const { return m_mc; }
void set_model(model const& mdl);
protected:
unsigned m_conflicts;

110
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -56,7 +56,7 @@ class inc_sat_solver : public solver {
proof_converter_ref m_pc;
model_converter_ref m_mc2;
expr_dependency_ref m_dep_core;
svector<double> m_weights;
typedef obj_map<expr, sat::literal> dep2asm_t;
public:
@ -82,8 +82,6 @@ public:
simp2_p.set_bool("hoist_mul", false); // required by som
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
//mk_simplify_tactic(m),
//mk_propagate_values_tactic(m),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m),
@ -100,25 +98,32 @@ public:
}
void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
m_weights.reset();
if (weights != 0) {
for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
}
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
VERIFY(l_true == internalize_formulas());
VERIFY(l_true == internalize_assumptions(sz, assumptions, 0 != weights, dep2asm));
VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm));
m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights);
}
lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {
m_weights.reset();
if (weights != 0) {
m_weights.append(sz, weights);
}
SASSERT(m_weights.empty() == (m_weights.c_ptr() == 0));
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, 0 != weights, dep2asm);
r = internalize_assumptions(sz, assumptions, dep2asm);
if (r != l_true) return r;
//m_solver.display_dimacs(std::cout);
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), weights, max_weight);
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
switch (r) {
case l_true:
if (sz > 0 && !weights) {
@ -179,7 +184,7 @@ public:
}
}
virtual void assert_expr(expr * t) {
TRACE("opt", tout << mk_pp(t, m) << "\n";);
TRACE("sat", tout << mk_pp(t, m) << "\n";);
m_fmls.push_back(t);
}
virtual void set_produce_models(bool f) {}
@ -238,9 +243,10 @@ private:
m_pc.reset();
m_dep_core.reset();
m_subgoals.reset();
m_preprocess->reset();
SASSERT(g->models_enabled());
SASSERT(!g->proofs_enabled());
TRACE("opt", g->display(tout););
TRACE("sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core);
}
@ -254,61 +260,26 @@ private:
return l_undef;
}
g = m_subgoals[0];
TRACE("opt", g->display_with_dependencies(tout););
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
return l_true;
}
lbool internalize_assumptions(unsigned sz, expr* const* asms, bool is_weighted, dep2asm_t& dep2asm) {
lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
if (sz == 0) {
return l_true;
}
if (is_weighted) {
return internalize_weighted(sz, asms, dep2asm);
}
return internalize_unweighted(sz, asms, dep2asm);
}
lbool internalize_unweighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
lbool res = l_undef;
for (unsigned i = 0; i < sz; ++i) {
g->assert_expr(asms[i], m.mk_leaf(asms[i]));
}
res = internalize_goal(g, dep2asm);
lbool res = internalize_goal(g, dep2asm);
if (res == l_true) {
extract_assumptions(dep2asm);
extract_assumptions(sz, asms, dep2asm);
}
return res;
}
/*
\brief extract weighted assumption literals in the same order as the weights.
For this purpose we enforce tha assumptions are literals.
*/
lbool internalize_weighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
lbool res = l_undef;
m_asms.reset();
expr_ref_vector lits(m);
filter_model_converter_ref fmc = alloc(filter_model_converter, m);
for (unsigned i = 0; i < sz; ++i) {
expr_ref lit = ensure_literal(g, asms[i], fmc.get());
lits.push_back(lit);
g->assert_expr(lit, m.mk_leaf(lit));
}
m_mc = concat(m_mc.get(), fmc.get());
res = internalize_goal(g, dep2asm);
if (res == l_true) {
for (unsigned i = 0; i < lits.size(); ++i) {
sat::literal l;
VERIFY (dep2asm.find(lits[i].get(), l));
m_asms.push_back(l);
}
}
return res;
}
lbool internalize_formulas() {
if (m_fmls_head == m_fmls.size()) {
return l_true;
@ -321,39 +292,31 @@ private:
return internalize_goal(g, dep2asm);
}
expr_ref ensure_literal(goal_ref& g, expr* e, filter_model_converter* fmc) {
expr_ref result(m), fml(m);
expr* e1;
if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) {
result = e;
}
else {
// TBD: need a filter_model_converter to remove
result = m.mk_fresh_const("soft", m.mk_bool_sort());
fmc->insert(to_app(result)->get_decl());
fml = m.mk_implies(result, e);
g->assert_expr(fml);
}
return result;
}
void extract_assumptions(dep2asm_t& dep2asm) {
void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
m_asms.reset();
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
m_asms.push_back(it->m_value);
unsigned j = 0;
sat::literal lit;
for (unsigned i = 0; i < sz; ++i) {
if (dep2asm.find(asms[i], lit)) {
m_asms.push_back(lit);
if (i != j && !m_weights.empty()) {
m_weights[j] = m_weights[i];
}
++j;
}
}
//IF_VERBOSE(0, verbose_stream() << asms << "\n";);
SASSERT(dep2asm.size() == m_asms.size());
}
void extract_core(dep2asm_t& dep2asm) {
u_map<expr*> asm2dep;
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
asm2dep.insert(it->m_value.index(), it->m_key);
expr* e = it->m_key;
asm2dep.insert(it->m_value.index(), e);
}
sat::literal_vector const& core = m_solver.get_core();
TRACE("opt",
TRACE("sat",
dep2asm_t::iterator it2 = dep2asm.begin();
dep2asm_t::iterator end2 = dep2asm.end();
for (; it2 != end2; ++it2) {
@ -426,7 +389,7 @@ private:
for (unsigned i = 0; i < m_fmls.size(); ++i) {
expr_ref tmp(m);
VERIFY(m_model->eval(m_fmls[i].get(), tmp));
CTRACE("opt", !m.is_true(tmp),
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
@ -461,3 +424,4 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof
}
return s.display_weighted(out, sz, soft, weights.c_ptr());
}

1
src/tactic/arith/card2bv_tactic.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include"card2bv_tactic.h"
#include"pb_rewriter.h"
#include"ast_util.h"
#include"ast_pp.h"
namespace pb {
unsigned card2bv_rewriter::get_num_bits(func_decl* f) {

5
src/tactic/core/simplify_tactic.cpp
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include"simplify_tactic.h"
#include"th_rewriter.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
struct simplify_tactic::imp {
ast_manager & m_manager;
@ -65,6 +65,9 @@ struct simplify_tactic::imp {
proof * pr = g.pr(idx);
new_pr = m().mk_modus_ponens(pr, new_pr);
}
if (m_manager.is_false(new_curr)) {
std::cout << mk_pp(curr, m_manager) << " => " << new_curr << "\n";
}
g.update(idx, new_curr, new_pr, g.dep(idx));
}
TRACE("after_simplifier_bug", g.display(tout););