mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

debug opt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-17 21:13:31 -07:00
parent af55088b78
commit 4effa7f0c0
5 changed files with 157 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast_smt2_pp.cpp
View file

@ -77,6 +77,8 @@ bool smt2_pp_environment::is_indexed_fdecl(func_decl * f) const {
for (i = 0; i < num; i++) {
if (f->get_parameter(i).is_int())
continue;
if (f->get_parameter(i).is_rational())
continue;
if (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast()))
continue;
break;
@ -105,9 +107,13 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) {
ptr_buffer<format> fs;
fs.push_back(fname);
for (unsigned i = 0; i < num; i++) {
SASSERT(f->get_parameter(i).is_int() || (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
SASSERT(f->get_parameter(i).is_int() ||
f->get_parameter(i).is_rational() ||
(f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
if (f->get_parameter(i).is_int())
fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int()));
else if (f->get_parameter(i).is_rational())
fs.push_back(mk_string(get_manager(), f->get_parameter(i).get_rational().to_string().c_str()));
else
fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast())));
}

126
src/ast/rewriter/pb_rewriter.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "pb_rewriter.h"
#include "pb_rewriter_def.h"
#include "ast_pp.h"
#include "ast_smt_pp.h"
class pb_ast_rewriter_util {
@ -72,6 +73,126 @@ public:
};
};
expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
pb_util util(m());
arith_util a(m());
expr_ref result(m()), tmp(m());
expr_ref_vector es(m());
expr*const* args = to_app(fml)->get_args();
unsigned sz = to_app(fml)->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr* e = args[i];
if (m().is_not(e, e)) {
es.push_back(a.mk_sub(a.mk_numeral(rational(1),true),vars.find(e)));
}
else {
es.push_back(vars.find(e));
}
}
if (util.is_at_most_k(fml) || util.is_at_least_k(fml)) {
if (es.empty()) {
tmp = a.mk_numeral(rational(0), true);
}
else {
tmp = a.mk_add(es.size(), es.c_ptr());
}
if (util.is_at_most_k(fml)) {
result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
}
else {
result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
}
}
else if (util.is_le(fml) || util.is_ge(fml) || util.is_eq(fml)) {
for (unsigned i = 0; i < sz; ++i) {
es[i] = a.mk_mul(a.mk_numeral(util.get_coeff(fml, i),false), es[i].get());
}
if (es.empty()) {
tmp = a.mk_numeral(rational(0), true);
}
else {
tmp = a.mk_add(es.size(), es.c_ptr());
}
if (util.is_le(fml)) {
result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
}
else if (util.is_ge(fml)) {
result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
}
else {
result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
}
}
else {
result = fml;
}
return result;
}
expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
ast_manager& m = e1.get_manager();
arith_util a(m);
symbol name;
obj_map<expr,expr*> vars;
expr_ref_vector trail(m), fmls(m);
unsigned sz = to_app(e1)->get_num_args();
expr*const*args = to_app(e1)->get_args();
for (unsigned i = 0; i < sz; ++i) {
expr* e = args[i];
if (m.is_true(e)) {
if (!vars.contains(e)) {
trail.push_back(a.mk_numeral(rational(1), true));
vars.insert(e, trail.back());
}
continue;
}
if (m.is_false(e)) {
if (!vars.contains(e)) {
trail.push_back(a.mk_numeral(rational(0), true));
vars.insert(e, trail.back());
}
continue;
}
std::ostringstream strm;
strm << "x" << i;
name = symbol(strm.str().c_str());
trail.push_back(m.mk_const(name, a.mk_int()));
expr* x = trail.back();
m.is_not(e,e);
vars.insert(e, x);
fmls.push_back(a.mk_le(a.mk_numeral(rational(0), true), x));
fmls.push_back(a.mk_le(x, a.mk_numeral(rational(1), true)));
}
expr_ref tmp(m);
expr_ref fml1 = translate_pb2lia(vars, e1);
expr_ref fml2 = translate_pb2lia(vars, e2);
tmp = m.mk_not(m.mk_eq(fml1, fml2));
fmls.push_back(tmp);
tmp = m.mk_and(fmls.size(), fmls.c_ptr());
return tmp;
}
static unsigned s_lemma = 0;
void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml) {
ast_manager& m = fml.get_manager();
app_ref tmp1(m), tmp2(m);
tmp1 = m.mk_app(f, sz, args);
tmp2 = to_app(fml);
expr_ref tmp = mk_validate_rewrite(tmp1, tmp2);
dump_pb_rewrite(tmp);
}
void pb_rewriter::dump_pb_rewrite(expr* fml) {
std::ostringstream strm;
strm << "pb_rewrite_" << (s_lemma++) << ".smt2";
std::ofstream out(strm.str().c_str());
ast_smt_pp pp(m());
pp.display_smt2(out, fml);
out.close();
}
br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
ast_manager& m = result.get_manager();
@ -143,7 +264,10 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
expr_ref tmp(m);
tmp = m.mk_app(f, num_args, args);
tout << tmp << "\n";
tout << result << "\n";);
tout << result << "\n";
);
TRACE("pb_validate",
validate_rewrite(f, num_args, args, result););
return BR_DONE;
}

5
src/ast/rewriter/pb_rewriter.h
View file

@ -43,6 +43,8 @@ class pb_rewriter {
pb_util m_util;
vector<rational> m_coeffs;
ptr_vector<expr> m_args;
void validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml);
public:
pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {
@ -55,6 +57,9 @@ public:
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
expr_ref translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml);
expr_ref mk_validate_rewrite(app_ref& e1, app_ref& e2);
void dump_pb_rewrite(expr* fml);
};
#endif

26
src/opt/weighted_maxsat.cpp
View file

@ -716,6 +716,7 @@ namespace opt {
bool was_sat = false;
fml = m.mk_true();
while (l_true == is_sat) {
TRACE("opt", s.display(tout<<"looping\n"););
solver::scoped_push _s2(s);
s.assert_expr(fml);
is_sat = simplify_and_check_sat(0,0);
@ -841,11 +842,14 @@ namespace opt {
return l_false;
}
uint_set B;
rational k(0);
rational old_lower(m_lower);
for (unsigned i = 0; i < sc.size(); ++i) {
uint_set t(sc[i]);
t &= A;
if (!t.empty()) {
B |= sc[i];
k += amk[i];
m_lower -= amk[i];
sc[i] = sc.back();
sc.pop_back();
@ -864,13 +868,14 @@ namespace opt {
bs.push_back(block[i].get());
}
}
rational k;
TRACE("opt", tout << "at most bound: " << k << "\n";);
is_sat = new_bound(al, ws, bs, k);
if (is_sat != l_true) {
return is_sat;
}
TRACE("opt", tout << "new bound: " << k << " lower: " << m_lower << "\n";);
m_lower += k;
SASSERT(m_lower > old_lower);
TRACE("opt", tout << "new bound: " << m_lower << "\n";);
expr_ref B_le_k(m), B_ge_k(m);
B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k);
B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k);
@ -980,12 +985,14 @@ namespace opt {
return l_false;
}
uint_set B;
rational k;
for (unsigned i = 0; i < sc.size(); ++i) {
uint_set t(sc[i]);
t &= A;
if (!t.empty()) {
B |= sc[i];
m_lower -= amk[i];
k += amk[i];
sc[i] = sc.back();
sc.pop_back();
am[i] = am.back();
@ -1003,7 +1010,6 @@ namespace opt {
bs.push_back(block[i].get());
}
}
rational k;
expr_ref_vector al2(al);
for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
@ -1058,22 +1064,17 @@ namespace opt {
s.assert_expr(soft[i].get());
}
}
}
}
lbool new_bound(expr_ref_vector const& al,
vector<rational> const& ws,
expr_ref_vector const& bs,
rational& k) {
pb_util u(m);
lbool is_sat = bound(al, ws, bs, k);
if (is_sat != l_true || !k.is_zero()) {
return is_sat;
}
expr_ref_vector al2(m);
al2.append(al);
// w_j*b_j > k
al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k)));
al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k)));
return bound(al2, ws, bs, k);
}
@ -1102,6 +1103,7 @@ namespace opt {
});
m_imp->re_init(nbs, ws);
lbool is_sat = m_imp->pb_simplify_solve();
SASSERT(m_imp->m_lower > k);
k = m_imp->m_lower;
return is_sat;
}
@ -1129,8 +1131,8 @@ namespace opt {
lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) {
lbool is_sat = l_true;
tactic_ref tac1 = mk_simplify_tactic(m);
tactic_ref tac2 = mk_pb_preprocess_tactic(m);
tactic_ref tac = and_then(tac1.get(), tac2.get()); // TBD: make attribute for cancelation.
// tactic_ref tac2 = mk_pb_preprocess_tactic(m);
tactic_ref tac = tac1; // and_then(tac1.get(), tac2.get()); // TBD: make attribute for cancelation.
proof_converter_ref pc;
expr_dependency_ref core(m);
model_converter_ref mc;

6
src/smt/theory_pb.cpp
View file

@ -444,13 +444,19 @@ namespace smt {
SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom) || m_util.is_eq(atom));
}
TRACE("pb", display(tout, *c););
//app_ref fml1(m), fml2(m);
//fml1 = c->to_expr(ctx, m);
c->unique();
lbool is_true = c->normalize();
c->prune();
c->post_prune();
//fml2 = c->to_expr(ctx, m);
//expr_ref validate_pb = pb_rewriter(m).mk_validate_rewrite(fml1, fml2);
//pb_rewriter(m).dump_pb_rewrite(validate_pb);
literal lit(abv);
TRACE("pb", display(tout, *c); tout << " := " << lit << "\n";);
switch(is_true) {
case l_false: