diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index ce2c426ea..df884e442 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -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 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()))); } diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 76dcdd958..ce6e294c7 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -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& 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 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; } diff --git a/src/ast/rewriter/pb_rewriter.h b/src/ast/rewriter/pb_rewriter.h index 0e0986d1a..4c9aaaaf1 100644 --- a/src/ast/rewriter/pb_rewriter.h +++ b/src/ast/rewriter/pb_rewriter.h @@ -43,6 +43,8 @@ class pb_rewriter { pb_util m_util; vector m_coeffs; ptr_vector 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& vars, expr* fml); + expr_ref mk_validate_rewrite(app_ref& e1, app_ref& e2); + void dump_pb_rewrite(expr* fml); }; #endif diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index dde454941..330dc8df8 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -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 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; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index b5fadac7c..c610fe929 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -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: