From 0641c4f69447c7c4f123bf76e22015eb0f81082c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Dec 2013 09:53:33 -0800 Subject: [PATCH] working on pre-processing Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.h | 4 +- src/ast/rewriter/pb_rewriter_def.h | 28 +- src/opt/opt_context.cpp | 2 +- src/opt/opt_solver.cpp | 19 +- src/opt/opt_solver.h | 4 +- src/opt/weighted_maxsat.cpp | 98 ++++- src/smt/theory_pb.cpp | 22 +- src/tactic/core/pb_preprocess_tactic.cpp | 441 +++++++++++++++++------ 8 files changed, 467 insertions(+), 151 deletions(-) diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index c590f8320..9ee74dfaf 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -89,14 +89,14 @@ public: bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); } bool is_at_least_k(app *a, rational& k) const; rational get_k(func_decl *a) const; - rational get_k(app *a) const { return get_k(a->get_decl()); } + rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); } bool is_le(func_decl *a) const; bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); } bool is_le(app* a, rational& k) const; bool is_ge(func_decl* a) const; bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); } bool is_ge(app* a, rational& k) const; - rational get_coeff(app* a, unsigned index) const { return get_coeff(a->get_decl(), index); } + rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); } rational get_coeff(func_decl* a, unsigned index) const; private: rational to_rational(parameter const& p) const; diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h index 3ffedb020..c6e21b6ce 100644 --- a/src/ast/rewriter/pb_rewriter_def.h +++ b/src/ast/rewriter/pb_rewriter_def.h @@ -36,7 +36,7 @@ void pb_rewriter_util::display(std::ostream& out, typename PBU::args_t& arg template void pb_rewriter_util::unique(typename PBU::args_t& args, typename PBU::numeral& k) { - TRACE("pb", display(tout << "pre-unique:", args, k);); + TRACE("pb_verbose", display(tout << "pre-unique:", args, k);); for (unsigned i = 0; i < args.size(); ++i) { if (m_util.is_negated(args[i].first)) { args[i].first = m_util.negate(args[i].first); @@ -73,9 +73,7 @@ void pb_rewriter_util::unique(typename PBU::args_t& args, typename PBU::num args[i] = args[j]; } } - if (i + 1 < args.size()) { - args.resize(i+1); - } + args.resize(i+1); // remove 0s. for (i = 0, j = 0; j < args.size(); ++j) { @@ -86,22 +84,22 @@ void pb_rewriter_util::unique(typename PBU::args_t& args, typename PBU::num ++i; } } - if (i < args.size()) { - args.resize(i); - } - TRACE("pb", display(tout << "post-unique:", args, k);); + args.resize(i); + TRACE("pb_verbose", display(tout << "post-unique:", args, k);); } template lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU::numeral& k) { - TRACE("pb", display(tout << "pre-normalize:", args, k);); + TRACE("pb_verbose", display(tout << "pre-normalize:", args, k);); + + DEBUG_CODE( + bool found = false; + for (unsigned i = 0; !found && i < args.size(); ++i) { + found = args[i].second.is_zero(); + } + if (found) display(verbose_stream(), args, k); + SASSERT(!found);); - bool found = false; - for (unsigned i = 0; !found && i < args.size(); ++i) { - found = args[i].second.is_zero(); - } - if (found) display(std::cout, args, k); - SASSERT(!found); // // Ensure all coefficients are positive: // c*l + y >= k diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 87895b33b..0695abc6d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -116,8 +116,8 @@ namespace opt { mdl = m_model; if (m_model_converter) { (*m_model_converter)(mdl, 0); - get_solver().mc()(mdl, 0); } + get_solver().mc()(mdl, 0); } lbool context::execute_min_max(unsigned index, bool committed) { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index c437e48f1..18285d37b 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -124,11 +124,10 @@ namespace opt { std::stringstream file_name; file_name << "opt_solver" << ++m_dump_count << ".smt2"; std::ofstream buffer(file_name.str().c_str()); - to_smt2_benchmark(buffer, "opt_solver", ""); + to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver", ""); buffer.close(); } - lbool r = m_context.check(num_assumptions, assumptions); - return r; + return m_context.check(num_assumptions, assumptions); } void opt_solver::maximize_objectives() { @@ -257,7 +256,9 @@ namespace opt { } - void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, + void opt_solver::to_smt2_benchmark(std::ofstream & buffer, + unsigned num_assumptions, expr * const * assumptions, + char const * name, char const * logic, char const * status, char const * attributes) { ast_smt_pp pp(m); pp.set_benchmark_name(name); @@ -266,10 +267,14 @@ namespace opt { pp.add_attributes(attributes); pp_params params; pp.set_simplify_implies(params.simplify_implies()); - for (unsigned i = 0; i < get_num_assertions(); ++i) { - pp.add_assumption(to_expr(get_assertion(i))); + + for (unsigned i = 0; i < num_assumptions; ++i) { + pp.add_assumption(assumptions[i]); } - pp.display_smt2(buffer, to_expr(m.mk_true())); + for (unsigned i = 0; i < get_num_assertions(); ++i) { + pp.add_assumption(get_assertion(i)); + } + pp.display_smt2(buffer, m.mk_true()); } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index eb5812317..0f62642d4 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -92,7 +92,9 @@ namespace opt { smt::theory_opt& get_optimizer(); - void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks", + void to_smt2_benchmark(std::ofstream & buffer, + unsigned num_assumptions, expr * const * assumptions, + char const * name = "benchmarks", char const * logic = "", char const * status = "unknown", char const * attributes = ""); }; } diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 6fae39bad..863cab7ef 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -23,6 +23,11 @@ Notes: #include "opt_params.hpp" #include "pb_decl_plugin.h" #include "uint_set.h" +#include "pb_preprocess_tactic.h" +#include "simplify_tactic.h" +#include "tactical.h" +#include "tactic.h" +#include "model_smt2_pp.h" namespace smt { @@ -637,6 +642,53 @@ namespace opt { return is_sat; } + lbool pb_simplify_solve() { + pb_util u(m); + expr_ref fml(m), val(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + rational minw(0); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + if (m_weights[i] < minw || minw.is_zero()) { + minw = m_weights[i]; + } + nsoft.push_back(m.mk_not(m_soft[i].get())); + } + solver::scoped_push _s1(s); + lbool is_sat = l_true; + bool was_sat = false; + fml = m.mk_true(); + while (l_true == is_sat) { + solver::scoped_push _s2(s); + s.assert_expr(fml); + is_sat = simplify_and_check_sat(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + rational old_upper = m_upper; + m_upper = rational::zero(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(m_soft[i].get(), val)); + m_assignment[i] = !m.is_false(val); + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } + } + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); + fml = u.mk_le(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper - minw); + was_sat = true; + } + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + m_lower = m_upper; + } + return is_sat; + } + + lbool wpm2_solve() { solver::scoped_push _s(s); pb_util u(m); @@ -645,6 +697,7 @@ namespace opt { expr_ref_vector block(m), ans(m), al(m), am(m); m_lower = m_upper = rational::zero(); obj_map ans_index; + vector amk; vector sc; for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -804,7 +857,7 @@ namespace opt { } m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition. m_imp->updt_params(m_params); - lbool is_sat = m_imp->pb_solve(); + lbool is_sat = m_imp->pb_simplify_solve(); k = m_imp->m_lower; m_solver.pop_core(1); return is_sat; @@ -819,6 +872,49 @@ 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. + proof_converter_ref pc; + expr_dependency_ref core(m); + model_converter_ref mc; + goal_ref_buffer result; + goal_ref g(alloc(goal, m, true, false)); + for (unsigned i = 0; i < s.get_num_assertions(); ++i) { + g->assert_expr(s.get_assertion(i)); + } + for (unsigned i = 0; i < n; ++i) { + NOT_IMPLEMENTED_YET(); + // add assumption in a wrapper. + } + (*tac)(g, result, mc, pc, core); + if (result.empty()) { + is_sat = l_false; + } + else { + SASSERT(result.size() == 1); + goal* r = result[0]; + solver::scoped_push _s(m_solver); + // TBD ptr_vector asms; + for (unsigned i = 0; i < r->size(); ++i) { + // TBD collect assumptions from r + m_solver.assert_expr(r->form(i)); + } + is_sat = m_solver.check_sat_core(0, 0); + if (l_true == is_sat) { + m_solver.get_model(m_model); + if (mc) (*mc)(m_model, 0); + IF_VERBOSE(2, + g->display(verbose_stream() << "goal:\n"); + r->display(verbose_stream() << "reduced:\n"); + model_smt2_pp(verbose_stream(), m, *m_model, 0);); + } + } + return is_sat; + } + }; wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 8c9be4659..c04390ea8 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -168,8 +168,6 @@ namespace smt { bool_var abv = ctx.mk_bool_var(atom); ctx.set_var_theory(abv, get_id()); - IF_VERBOSE(3, verbose_stream() << mk_pp(atom, m) << "\n";); - ineq* c = alloc(ineq, literal(abv)); c->m_k = m_util.get_k(atom); numeral& k = c->m_k; @@ -192,21 +190,19 @@ namespace smt { else { SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom)); } - TRACE("pb", display(tout, *c);); c->unique(); lbool is_true = c->normalize(); c->prune(); - TRACE("pb", display(tout, *c);); literal lit(abv); - + + TRACE("pb", display(tout << mk_pp(atom, m), *c); tout << " := " << lit << "\n";); switch(is_true) { case l_false: lit = ~lit; // fall-through case l_true: ctx.mk_th_axiom(get_id(), 1, &lit); - TRACE("pb", tout << mk_pp(atom, m) << " := " << lit << "\n";); dealloc(c); return true; case l_undef: @@ -1246,14 +1242,12 @@ namespace smt { sum += c.coeff(i); } } - if (sum >= c.k()) { - IF_VERBOSE(0, - display(verbose_stream(), c, true); - for (unsigned i = 0; i < lits.size(); ++i) { - verbose_stream() << lits[i] << " "; - } - verbose_stream() << " => " << l << "\n";); - } + CTRACE("pb", (sum >= c.k()), + display(tout << "invalid assign" , c, true); + for (unsigned i = 0; i < lits.size(); ++i) { + tout << lits[i] << " "; + } + tout << " => " << l << "\n";); SASSERT(sum < c.k()); } diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index dd1033d54..28aa96e56 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -16,6 +16,20 @@ Author: Notes: + Resolution for PB constraints require the implicit + inequalities that each variable ranges over [0,1] + so not all resolvents produce smaller sets of clauses. + + We here implement subsumption resolution. + + x + y >= 1 + A~x + B~y + Cz >= k + --------------------- + Cz >= k - B + + where A <= B, x, y do not occur elsewhere. + + --*/ #include "pb_preprocess_tactic.h" #include "tactical.h" @@ -25,30 +39,100 @@ Notes: #include "expr_substitution.h" #include "ast_pp.h" +class pb_preproc_model_converter : public model_converter { + ast_manager& m; + pb_util pb; + expr_ref_vector m_refs; + svector > m_const; + +public: + pb_preproc_model_converter(ast_manager& m):m(m), pb(m), m_refs(m) {} + + virtual void operator()(model_ref & mdl, unsigned goal_idx) { + SASSERT(goal_idx == 0); + for (unsigned i = 0; i < m_const.size(); ++i) { + mdl->register_decl(m_const[i].first->get_decl(), m_const[i].second); + } + } + + void set_value(app* e, expr* v) { + SASSERT(e->get_num_args() == 0); + SASSERT(is_uninterp_const(e)); + m_const.push_back(std::make_pair(e, v)); + m_refs.push_back(e); + m_refs.push_back(v); + } + + void set_value(expr* e, bool p) { + if (m.is_not(e, e)) { + set_value(e, !p); + } + else { + SASSERT(is_app(e)); + set_value(to_app(e), p?m.mk_true():m.mk_false()); + } + } + + virtual model_converter * translate(ast_translation & translator) { + pb_preproc_model_converter* mc = alloc(pb_preproc_model_converter, translator.to()); + for (unsigned i = 0; i < m_const.size(); ++i) { + mc->set_value(translator(m_const[i].first), translator(m_const[i].second)); + } + return mc; + } + +}; + class pb_preprocess_tactic : public tactic { struct rec { unsigned_vector pos, neg; rec() { } }; - typedef obj_map var_map; + typedef obj_map var_map; ast_manager& m; pb_util pb; var_map m_vars; unsigned_vector m_ge; unsigned_vector m_other; + bool m_progress; th_rewriter m_r; struct declassifier { - obj_map& m_vars; - declassifier(obj_map& v): m_vars(v) {} + var_map& m_vars; + declassifier(var_map& v): m_vars(v) {} void operator()(app* e) { if (m_vars.contains(e)) { m_vars.remove(e); } } - void operator()(var* e) {} - void operator()(quantifier* q) {} + void operator()(var*) {} + void operator()(quantifier*) {} }; + void display_annotation(std::ostream& out, goal_ref const& g) { + for (unsigned i = 0; i < m_ge.size(); ++i) { + out << "ge " << m_ge[i] << ": " << mk_pp(g->form(m_ge[i]), m) << "\n"; + } + for (unsigned i = 0; i < m_other.size(); ++i) { + out << "ot " << m_other[i] << ": " << mk_pp(g->form(m_other[i]), m) << "\n"; + } + + var_map::iterator it = m_vars.begin(); + var_map::iterator end = m_vars.end(); + for (; it != end; ++it) { + app* e = it->m_key; + unsigned_vector const& pos = it->m_value.pos; + unsigned_vector const& neg = it->m_value.neg; + out << mk_pp(e, m) << ": "; + for (unsigned i = 0; i < pos.size(); ++i) { + out << "p: " << pos[i] << " "; + } + for (unsigned i = 0; i < neg.size(); ++i) { + out << "n: " << neg[i] << " "; + } + out << "\n"; + } + } + public: pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): m(m), pb(m), m_r(m) {} @@ -68,65 +152,84 @@ public: SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; + // TBD: bail out if cores are enabled. + // TBD: bail out if proofs are enabled/add proofs. + // TBD: model construction by back-filling solutions. + + pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m); + mc = pp; + + g->inc_depth(); + result.push_back(g.get()); + while (simplify(g, *pp)); + + } + + bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) { reset(); + normalize(g); + if (g->inconsistent()) { + return false; + } for (unsigned i = 0; i < g->size(); ++i) { - process_vars(i, g->form(i)); + process_vars(i, g); } - + if (m_ge.empty()) { - result.push_back(g.get()); - return; + return false; } - + for (unsigned i = 0; i < m_ge.size(); ++i) { classify_vars(i, to_app(g->form(m_ge[i]))); } - + declassifier dcl(m_vars); expr_mark visited; for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) { for_each_expr(dcl, visited, g->form(m_other[i])); } - + if (m_vars.empty()) { - result.push_back(g.get()); - return; + return false; } - - g->inc_depth(); + + // display_annotation(tout, g); + m_progress = false; // first eliminate variables var_map::iterator it = next_resolvent(m_vars.begin()); - while (it != m_vars.end()) { - expr * e = it->m_key; + while (it != m_vars.end()) { + app * e = it->m_key; rec const& r = it->m_value; if (r.pos.empty()) { replace(r.neg, e, m.mk_false(), g); + mc.set_value(e, m.mk_false()); } else if (r.neg.empty()) { replace(r.pos, e, m.mk_true(), g); + mc.set_value(e, m.mk_true()); } + if (g->inconsistent()) return false; ++it; it = next_resolvent(it); } // now resolve clauses. it = next_resolvent(m_vars.begin()); while (it != m_vars.end()) { - expr * e = it->m_key; + + app * e = it->m_key; rec const& r = it->m_value; - if (r.pos.size() == 1) { - resolve(r.pos[0], r.neg, e, true, g); + if (r.pos.size() == 1 && !r.neg.empty()) { + resolve(mc, r.pos[0], r.neg, e, true, g); } - else if (r.neg.size() == 1) { - resolve(r.neg[0], r.pos, e, false, g); + else if (r.neg.size() == 1 && !r.pos.empty()) { + resolve(mc, r.neg[0], r.pos, e, false, g); } + if (g->inconsistent()) return false; ++it; it = next_resolvent(it); } - - g->elim_true(); - - result.push_back(g.get()); + return m_progress; } virtual void set_cancel(bool f) { @@ -146,9 +249,37 @@ private: m_vars.reset(); } + expr* negate(expr* e) { + if (m.is_not(e, e)) return e; + return m.mk_not(e); + } - void process_vars(unsigned i, expr* e) { + void normalize(goal_ref const& g) { expr* r; + expr_ref tmp(m); + for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) { + expr* e = g->form(i); + if (m.is_not(e, r) && pb.is_ge(r)) { + rational k = pb.get_k(r); + rational sum(0); + expr_ref_vector args(m); + vector coeffs; + for (unsigned j = 0; j < to_app(r)->get_num_args(); ++j) { + sum += pb.get_coeff(r, j); + coeffs.push_back(pb.get_coeff(r, j)); + args.push_back(negate(to_app(r)->get_arg(j))); + } + tmp = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), sum - k + rational::one()); + g->update(i, tmp); + } + } + } + + + void process_vars(unsigned i, goal_ref const& g) { + expr* r, *e; + e = g->form(i); + if (is_uninterp_const(e)) { m_ge.push_back(i); } @@ -168,8 +299,8 @@ private: void classify_vars(unsigned idx, app* e) { expr* r; - if (m.is_not(e, r)) { - insert(idx, r, false); + if (m.is_not(e, r) && is_uninterp_const(r)) { + insert(idx, e, false); return; } if (is_uninterp_const(e)) { @@ -182,15 +313,17 @@ private: // no-op } else if (m.is_not(arg, r)) { - insert(idx, r, false); + SASSERT(is_uninterp_const(r)); + insert(idx, to_app(r), false); } else { - insert(idx, arg, true); + SASSERT(is_uninterp_const(arg)); + insert(idx, to_app(arg), true); } } } - void insert(unsigned i, expr* e, bool pos) { + void insert(unsigned i, app* e, bool pos) { if (!m_vars.contains(e)) { m_vars.insert(e, rec()); } @@ -252,82 +385,86 @@ private: return true; } - void resolve(unsigned idx1, unsigned_vector const& positions, expr* e, bool pos, goal_ref const& g) { - if (!is_app(g->form(idx1))) { - return; - } - app* fml = to_app(g->form(idx1)); - if (m.is_true(fml)) { - return; - } - if (!is_valid(positions, g)) { - return; - } - if (positions.size() > 1 && !is_reduction(positions, fml, g)) { - return; - } - IF_VERBOSE(1, verbose_stream() << "resolving: " << mk_pp(fml, m) << "\n";); - m_r.set_substitution(0); - expr_ref tmp1(m), tmp2(m), e1(m), e2(m); - ptr_vector args; - vector coeffs; - rational k1, k2, c1, c2; - if (pos) { - e1 = e; - e2 = m.mk_not(e); - } - else { - e1 = m.mk_not(e); - e2 = e; - } - VERIFY(to_ge(fml, args, coeffs, k1)); - c1 = get_coeff(args.size(), args.c_ptr(), coeffs.c_ptr(), e1); - if (c1.is_zero()) { - return; - } - unsigned sz = coeffs.size(); - for (unsigned i = 0; i < positions.size(); ++i) { - unsigned idx2 = positions[i]; - if (idx2 == idx1) { - continue; + // Implement very special case of resolution. + + void resolve(pb_preproc_model_converter& mc, unsigned idx1, + unsigned_vector const& positions, app* e, bool pos, goal_ref const& g) { + if (positions.size() != 1) return; + unsigned idx2 = positions[0]; + expr_ref tmp1(m), tmp2(m); + expr* fml1 = g->form(idx1); + expr* fml2 = g->form(idx2); + expr_ref_vector args1(m), args2(m); + vector coeffs1, coeffs2; + rational k1, k2; + if (!to_ge(fml1, args1, coeffs1, k1)) return; + if (!k1.is_one()) return; + if (!to_ge(g->form(idx2), args2, coeffs2, k2)) return; + // check that each variable in idx1 occurs only in idx2 + unsigned min_index = 0; + rational min_coeff(0); + unsigned_vector indices; + for (unsigned i = 0; i < args1.size(); ++i) { + expr* x = args1[i].get(); + m.is_not(x, x); + if (!is_app(x)) return; + if (!m_vars.contains(to_app(x))) return; + rec const& r = m_vars.find(to_app(x)); + if (r.pos.size() != 1 || r.neg.size() != 1) return; + if (r.pos[0] != idx2 && r.neg[0] != idx2) return; + for (unsigned j = 0; j < args2.size(); ++j) { + if (is_complement(args1[i].get(), args2[j].get())) { + if (i == 0) { + min_coeff = coeffs2[j]; + } + else if (min_coeff > coeffs2[j]) { + min_coeff = coeffs2[j]; + min_index = j; + } + indices.push_back(j); + } } - app* fml2 = to_app(g->form(idx2)); - if (m.is_true(fml2)) continue; - VERIFY(to_ge(fml2, args, coeffs, k2)); - c2 = get_coeff(args.size()-sz, args.c_ptr()+sz, coeffs.c_ptr()+sz, e2); - if (!c2.is_zero()) { - rational m1(1), m2(1); - if (c1 != c2) { - rational lc = lcm(c1, c2); - m1 = lc/c1; - m2 = lc/c2; - for (unsigned j = 0; j < sz; ++j) { - coeffs[j] *= m1; - } - for (unsigned j = sz; j < args.size(); ++j) { - coeffs[j] *= m2; - } - } - tmp1 = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), m1*k1 + m2*k2); - m_r(tmp1, tmp2); - TRACE("pb", tout << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";); - IF_VERBOSE(1, verbose_stream() << mk_pp(fml2, m) << " -> " << tmp2 << "\n";); - - g->update(idx2, tmp2); // proof & dependencies - - if (!m1.is_one()) { - for (unsigned j = 0; j < sz; ++j) { - coeffs[j] /= m1; - } - } - } - args.resize(sz); - coeffs.resize(sz); } + for (unsigned i = 0; i < indices.size(); ++i) { + unsigned j = indices[i]; + expr* arg = args2[j].get(); + if (j == min_index) { + args2[j] = m.mk_false(); + } + else { + args2[j] = m.mk_true(); + } + mc.set_value(arg, j != min_index); + } + + tmp1 = pb.mk_ge(args2.size(), coeffs2.c_ptr(), args2.c_ptr(), k2); + IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n"; + for (unsigned i = 0; i < args2.size(); ++i) { + verbose_stream() << mk_pp(args2[i].get(), m) << " "; + } + verbose_stream() << "\n"; + ); + m_r(tmp1, tmp2); + if (pb.is_ge(tmp2) && pb.get_k(to_app(tmp2)).is_one()) { + tmp2 = m.mk_or(to_app(tmp2)->get_num_args(), to_app(tmp2)->get_args()); + } + IF_VERBOSE(3, + verbose_stream() << "resolve: " << mk_pp(fml1, m) << "\n" << mk_pp(fml2, m) << "\n" << tmp1 << "\n"; + verbose_stream() << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";); + g->update(idx1, m.mk_true()); // proof & dependencies + g->update(idx2, tmp2); // proof & dependencies + m_progress = true; + //IF_VERBOSE(0, if (!g->inconsistent()) display_annotation(verbose_stream(), g);); } - bool to_ge(app* e, ptr_vector& args, vector& coeffs, rational& k) { + bool is_complement(expr* x, expr* y) const { + if (m.is_not(x,x)) return x == y; + if (m.is_not(y,y)) return x == y; + return false; + } + + bool to_ge(expr* e, expr_ref_vector& args, vector& coeffs, rational& k) { expr* r; if (is_uninterp_const(e)) { args.push_back(e); @@ -340,17 +477,19 @@ private: k = rational::one(); } else if (pb.is_ge(e)) { - SASSERT(pure_args(e)); - for (unsigned i = 0; i < e->get_num_args(); ++i) { - args.push_back(e->get_arg(i)); - coeffs.push_back(pb.get_coeff(e, i)); + app* a = to_app(e); + SASSERT(pure_args(a)); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + args.push_back(a->get_arg(i)); + coeffs.push_back(pb.get_coeff(a, i)); } k = pb.get_k(e); } else if (m.is_or(e)) { + app* a = to_app(e); SASSERT(pure_args(e)); - for (unsigned i = 0; i < e->get_num_args(); ++i) { - args.push_back(e->get_arg(i)); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + args.push_back(a->get_arg(i)); coeffs.push_back(rational::one()); } k = rational::one(); @@ -375,8 +514,10 @@ private: TRACE("pb", tout << mk_pp(f, m) << " -> " << tmp << " by " << mk_pp(e, m) << " |-> " << mk_pp(v, m) << "\n";); g->update(idx, tmp); // proof & dependencies. + m_progress = true; } } + m_r.set_substitution(0); } }; @@ -384,3 +525,83 @@ private: tactic * mk_pb_preprocess_tactic(ast_manager & m, params_ref const & p) { return alloc(pb_preprocess_tactic, m); } + +#if 0 + + struct resolve_t { + app* e; + expr* lhs; + expr* rhs; + expr* res; + resolve_t(app* e, expr* lhs, expr* rhs, expr* res): + e(e), lhs(lhs), rhs(rhs), res(res) + {} + }; + + svector m_resolve; + + void satisfy(model_ref& mdl, expr* e) { + if (m.is_true(e)) { + return; + } + if (pb.is_ge(e)) { + rational k = pb.get_k(e); + rational c(0); + app* a = to_app(e); + for (unsigned i = 0; c < k && i < a->get_num_args(); ++i) { + expr* arg = a->get_arg(i); + if (is_uninterp_const(arg)) { + mdl->register_decl(to_app(arg)->get_decl(), m.mk_true()); + std::cout << mk_pp(arg, m) << " |-> true\n"; + c += pb.get_coeff(a, i); + } + else if (m.is_not(arg, arg) && is_uninterp_const(arg)) { + mdl->register_decl(to_app(arg)->get_decl(), m.mk_false()); + std::cout << mk_pp(arg, m) << " |-> false\n"; + c += pb.get_coeff(a, i); + } + } + SASSERT(c >= k); + return; + } + UNREACHABLE(); + } + + for (unsigned i = m_resolve.size(); i > 0; ) { + --i; + resolve_t const& r = m_resolve[i]; + expr_ref tmp1(m), tmp2(m), tmp3(m), tmp4(m); + VERIFY(mdl->eval(r.rhs, tmp2)); + satisfy(mdl, tmp2); + + VERIFY(mdl->eval(r.lhs, tmp1)); + satisfy(mdl, tmp1); + + if (m.is_false(tmp2) || m.is_false(tmp1)) { + VERIFY(mdl->eval(r.res, tmp3)); + th_rewriter rw(m); + rw(r.res, tmp4); + std::cout << "L:" << mk_pp(r.lhs,m) << " " << tmp1 << "\n"; + std::cout << "R:" << mk_pp(r.rhs,m) << " " << tmp2 << "\n"; + std::cout << "LR:" << mk_pp(r.res,m) << "\n" << tmp4 << "\n" << tmp3 << "\n"; + exit(0); + } + VERIFY(mdl->eval(r.e, tmp3)); + if (r.e == tmp3) { + mdl->register_decl(r.e->get_decl(), m.mk_true()); + } + // evaluate lhs, rhs + // determine how to + // assign e based on residue. + } + + void resolve(app* e, expr* lhs, expr* rhs, expr* res) { + m_refs.push_back(e); + m_refs.push_back(lhs); + m_refs.push_back(rhs); + m_refs.push_back(res); + m_resolve.push_back(resolve_t(e, lhs, rhs, res)); + } + + +#endif