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

integrating SLS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-28 14:30:36 -07:00
parent 3d7f208ce6
commit efe2a70f6f
2 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_context.cpp
View file

@ -381,7 +381,7 @@ namespace opt {
params_ref lia_p; params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality()); lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p); tac3->updt_params(lia_p);
m_simplify = and_then(tac0.get(), tac2.get(), tac3.get()); m_simplify = and_then(tac0.get(), tac2.get(), tac3.get(), mk_nnf_tactic(m));
} }
else { else {
m_simplify = tac0.get(); m_simplify = tac0.get();

18
src/opt/weighted_maxsat.cpp
View file

@ -34,6 +34,7 @@ Notes:
#include "card2bv_tactic.h" #include "card2bv_tactic.h"
#include "tactic2solver.h" #include "tactic2solver.h"
#include "bvsls_opt_engine.h" #include "bvsls_opt_engine.h"
#include "nnf_tactic.h"
namespace smt { namespace smt {
@ -702,9 +703,21 @@ namespace opt {
expr_ref tmp(m), objective(m), zero(m); expr_ref tmp(m), objective(m), zero(m);
expr_ref_vector es(m); expr_ref_vector es(m);
goal_ref g(alloc(goal, m, true, false));
for (unsigned i = 0; i < s.get_num_assertions(); ++i) { for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
pb_rewriter(s.get_assertion(i), tmp); pb_rewriter(s.get_assertion(i), tmp);
m_bvsls.assert_expr(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_bvsls.assert_expr(r->form(i));
} }
m_lower = m_upper = rational::zero(); m_lower = m_upper = rational::zero();
@ -718,7 +731,8 @@ namespace opt {
unsigned bv_size = maxval.get_num_bits(); unsigned bv_size = maxval.get_num_bits();
zero = bv.mk_numeral(rational(0), bv_size); zero = bv.mk_numeral(rational(0), bv_size);
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
es.push_back(m.mk_ite(m_soft[i].get(), bv.mk_numeral(den*m_weights[i], bv_size), zero)); pb_rewriter(m_soft[i].get(), tmp);
es.push_back(m.mk_ite(tmp, bv.mk_numeral(den*m_weights[i], bv_size), zero));
} }
if (es.empty()) { if (es.empty()) {
objective = bv.mk_numeral(0, bv_size); objective = bv.mk_numeral(0, bv_size);