z3/src/tactic/arith/lia2card_tactic.cpp

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    lia2card_tactic.cpp

Abstract:

    Convert 0-1 integer variables cardinality constraints to built-in cardinality operator.

Author:

    Nikolaj Bjorner (nbjorner) 2013-11-5

Notes:

--*/
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/pb_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/ast_util.h"
#include "ast/ast_pp_util.h"
#include "tactic/tactical.h"
#include "ast/simplifiers/bound_manager.h"
#include "ast/converters/generic_model_converter.h"

class lia2card_tactic : public tactic {

    struct bound {
        unsigned m_lo;
        unsigned m_hi;
        expr*    m_expr;
        bound(unsigned lo, unsigned hi, expr* b):
            m_lo(lo), m_hi(hi), m_expr(b) {}
        bound(): m_lo(0), m_hi(0), m_expr(nullptr) {}
    };

    struct lia_rewriter_cfg : public default_rewriter_cfg {
        ast_manager&     m;
        lia2card_tactic& t;
        arith_util       a;
        expr_ref_vector  args;
        vector<rational> coeffs;
        rational         coeff;

        bool is_pb(expr* x, expr* y, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
            args.reset();
            coeffs.reset();
            coeff.reset();
            return
                t.get_pb_sum(x,  rational::one(), args, coeffs, coeff) &&
                t.get_pb_sum(y, -rational::one(), args, coeffs, coeff);
        }

        bool is_le(expr* x, expr* y, expr_ref& result) {
            if (is_pb(x, y, args, coeffs, coeff)) {
                result = t.mk_le(coeffs.size(), coeffs.data(), args.data(), -coeff);
                return true;
            }
            else {
                return false;
            }
        }

        br_status mk_app_core(func_decl* f, unsigned sz, expr*const* es, expr_ref& result) {
            if (is_decl_of(f, a.get_family_id(), OP_LE) && is_le(es[0], es[1], result)) {
            }
            else if (is_decl_of(f, a.get_family_id(), OP_GE) && is_le(es[1], es[0], result)) {
            }
            else if (is_decl_of(f, a.get_family_id(), OP_LT) && is_le(es[1], es[0], result)) {
                result = m.mk_not(result);
            }
            else if (is_decl_of(f, a.get_family_id(), OP_GT) && is_le(es[0], es[1], result)) {
                result = m.mk_not(result);
            }
            else if (m.is_eq(f) && is_pb(es[0], es[1], args, coeffs, coeff)) {
                result = t.mk_eq(coeffs.size(), coeffs.data(), args.data(), -coeff);
            }
            else {
                return BR_FAILED;
            }
            TRACE("pbsum", tout << expr_ref(m.mk_app(f, sz, es), m) << " ==>\n" <<  result << "\n";);

            return BR_DONE;
        }

        bool rewrite_patterns() const { return false; }
        bool flat_assoc(func_decl * f) const { return false; }
        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
            result_pr = nullptr;
            return mk_app_core(f, num, args, result);
        }
        lia_rewriter_cfg(lia2card_tactic& t):m(t.m), t(t), a(m), args(m) {}
    };

    class lia_rewriter : public rewriter_tpl<lia_rewriter_cfg> {
        lia_rewriter_cfg m_cfg;
    public:
        lia_rewriter(lia2card_tactic& t):
            rewriter_tpl<lia_rewriter_cfg>(t.m, false, m_cfg),
            m_cfg(t)
        {}
    };

public:
    typedef obj_map<expr, bound> bounds_map;
    ast_manager &                    m;
    arith_util                       a;
    lia_rewriter                     m_rw;
    params_ref                       m_params;
    pb_util                          m_pb;
    mutable ptr_vector<expr>*        m_todo;
    bounds_map                       m_bounds;
    bool                             m_compile_equality;
    unsigned                         m_max_ub;
    ref<generic_model_converter>     m_mc;

    lia2card_tactic(ast_manager & _m, params_ref const & p):
        m(_m),
        a(m),
        m_rw(*this),
        m_pb(m),
        m_todo(alloc(ptr_vector<expr>)),
        m_compile_equality(true) {
        m_max_ub = 100;
    }

    ~lia2card_tactic() override {
        dealloc(m_todo);
    }

    char const* name() const override { return "lia2card"; }

    void updt_params(params_ref const & p) override {
        m_params.append(p);
        m_compile_equality = m_params.get_bool("compile_equality", true);
    }

    expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) {
        expr_ref_vector xs(m);
        expr_ref last_v(m);
        if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card");
        if (hi == 0) {
            expr* r = a.mk_int(0);
            m_mc->add(x->get_decl(), r);
            return expr_ref(r, m);
        }
        if (lo > 0) {
            xs.push_back(a.mk_int(lo));
        }
        verbose_stream() << "bounded " << lo << " " << hi << "\n";
        for (unsigned i = lo; i < hi; ++i) {
            checkpoint();

            expr_ref v(m.mk_fresh_const(x->get_decl()->get_name(), m.mk_bool_sort()), m);
            if (last_v) axioms.push_back(m.mk_implies(v, last_v));
            xs.push_back(m.mk_ite(v, a.mk_int(1), a.mk_int(0)));
            m_mc->hide(v);
            last_v = v;
        }
        expr* r = a.mk_add(xs.size(), xs.data());
        m_mc->add(x->get_decl(), r);
        return expr_ref(r, m);
    }

    void checkpoint() {
        if (!m.inc()) {
            throw tactic_exception(m.limit().get_cancel_msg());
        }
    }

    void operator()(goal_ref const & g, goal_ref_buffer & result) override {
        m_bounds.reset();
        m_mc.reset();
        expr_ref_vector axioms(m);
        expr_safe_replace rep(m);

        tactic_report report("lia2card", *g);

        bound_manager bounds(m);
        for (unsigned i = 0; i < g->size(); ++i)
            bounds(g->form(i), g->dep(i), g->pr(i));

        for (expr* x : bounds) {
            checkpoint();

            bool s1 = false, s2 = false;
            rational lo, hi;
            if (a.is_int(x) &&
                is_uninterp_const(x) &&
                bounds.has_lower(x, lo, s1) && !s1 && lo.is_unsigned() &&
                bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() - lo.get_unsigned() <= m_max_ub) {
                expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned());
                rep.insert(x, b);
                m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), b));
                TRACE("pb", tout << "add bound " << lo << " " << hi << ": " << mk_pp(x, m) << "\n";);
            }
        }
        for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {
            checkpoint();

            expr_ref   new_curr(m), tmp(m);
            proof_ref  pr1(m), pr2(m), new_pr(m);
            rep(g->form(i), tmp);
            if (g->form(i) != tmp && m.proofs_enabled()) {
                pr1 = m.mk_rewrite(g->form(i), tmp);
            }
            m_rw(tmp, new_curr, pr2);
            if (m.proofs_enabled() && tmp != new_curr && !pr2) {
                pr2 = m.mk_rewrite(tmp, new_curr);
            }
            if (m.proofs_enabled() && g->pr(i)) {
                new_pr = m.mk_transitivity(pr1, pr2);
                new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
            }
            // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";);
            g->update(i, new_curr, new_pr, g->dep(i));
        }
        for (expr* a : axioms) 
            g->assert_expr(a);

        if (m_mc) g->add(m_mc.get());
        g->inc_depth();
        result.push_back(g.get());
        m_bounds.reset();
    }

    expr* mk_le(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
        if (sz == 0) {
            return w.is_neg()?m.mk_false():m.mk_true();
        }
        if (sz == 1 && weights[0].is_one() && w >= rational::one()) {
            return m.mk_true();
        }
        if (sz == 1 && weights[0].is_one() && w.is_zero()) {
            return m.mk_not(args[0]);
        }
        if (w.is_neg()) {
            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
            return m.mk_false();
        }
        return m_pb.mk_le(sz, weights, args, w);
    }

    expr* mk_eq(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
        if (w.is_neg()) {
            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
            return m.mk_false();
        }
        if (m_compile_equality) {
            return m_pb.mk_eq(sz, weights, args, w);
        }
        else {
            return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w));
        }
    }

    expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
        if (sz == 0) {
            return w.is_pos()?m.mk_false():m.mk_true();
            return w.is_pos() ? m.mk_false() : m.mk_true();
        }
        if (sz == 1 && weights[0].is_one() && w.is_one()) {
            return args[0];
        }
        if (sz == 1 && weights[0].is_one() && w.is_zero()) {
            return m.mk_not(args[0]);
        }
        if (w.is_neg()) {
            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
            return m.mk_true();
        }
        return m_pb.mk_ge(sz, weights, args, w);
    }

    bool get_pb_sum(expr* x, rational const& mul, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
        expr_ref_vector conds(m);
        return get_sum(0, x, mul, conds, args, coeffs, coeff);
    }

    bool get_sum(unsigned nesting, expr* x, rational const& mul, expr_ref_vector& conds, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
        checkpoint();

        expr *y, *z, *u;
        rational r, q;
        if (!is_app(x)) 
            return false;
        if (nesting > 8)
            return false;
        app* f = to_app(x);
        bool ok = true;
        if (a.is_add(x)) {
            for (unsigned i = 0; ok && i < f->get_num_args(); ++i) {
                ok = get_sum(nesting, f->get_arg(i), mul, conds, args, coeffs, coeff);
            }
        }
        else if (a.is_sub(x, y, z)) {
            ok = get_sum(nesting, y, mul, conds, args, coeffs, coeff);
            ok = ok && get_sum(nesting, z, -mul, conds, args, coeffs, coeff);
        }
        else if (a.is_uminus(x, y)) {
            ok = get_sum(nesting, y, -mul, conds, args, coeffs, coeff);
        }
        else if (a.is_mul(x, y, z) && is_numeral(y, r)) {
            ok = get_sum(nesting, z, r*mul, conds, args, coeffs, coeff);
        }
        else if (a.is_mul(x, z, y) && is_numeral(y, r)) {
            ok = get_sum(nesting, z, r*mul, conds, args, coeffs, coeff);
        }
        else if (a.is_to_real(x, y)) {
            ok = get_sum(nesting, y, mul, conds, args, coeffs, coeff);
        }
        else if (m.is_ite(x, y, z, u)) {
            conds.push_back(y);
            ok = get_sum(nesting + 1, z, mul, conds, args, coeffs, coeff);
            conds.pop_back();
            conds.push_back(m.mk_not(y));
            ok &= get_sum(nesting + 1, u, mul, conds, args, coeffs, coeff);
            conds.pop_back();
        }
        else if (is_numeral(x, r)) {
            insert_arg(mul*r, conds, m.mk_true(), args, coeffs, coeff);
        }
        else {
            TRACE("pb", tout << "Can't handle " << mk_pp(x, m) << "\n";);
            ok = false;
        }
        return ok;
    }

    expr_ref add_conds(expr_ref_vector& es, expr* e) {
        expr_ref result(m);
        if (!m.is_true(e)) {
            es.push_back(e);
        }
        result = mk_and(m, es.size(), es.data());
        if (!m.is_true(e)) {
            es.pop_back();
        }
        return result;
    }

    bool is_numeral(expr* e, rational& r) {
        if (a.is_uminus(e, e) && is_numeral(e, r)) {
            r.neg();
            return true;
        }
        if (a.is_to_real(e, e)) {
            return is_numeral(e, r);
        }
        return a.is_numeral(e, r);
    }

    void insert_arg(
        rational const& p,
        expr_ref_vector& conds,
        expr* x,
        expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
        expr_ref cond = add_conds(conds, x);
        if (m.is_true(cond)) {
            coeff += p;
        }
        else if (p.is_neg()) {
            // -p*x = p*(1-x) - p
            args.push_back(m.mk_not(cond));
            coeffs.push_back(-p);
            coeff += p;
        }
        else if (p.is_pos()) {
            args.push_back(cond);
            coeffs.push_back(p);
        }
    }

    tactic * translate(ast_manager & m) override {
        return alloc(lia2card_tactic, m, m_params);
    }

    void collect_param_descrs(param_descrs & r) override {
        r.insert("compile_equality", CPK_BOOL,
                 "(default:false) compile equalities into pseudo-Boolean equality");
    }

    void cleanup() override {
        ptr_vector<expr>* todo = alloc(ptr_vector<expr>);
        std::swap(m_todo, todo);
        dealloc(todo);
        m_bounds.reset();
    }
};

tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) {
    return clean(alloc(lia2card_tactic, m, p));
}

bool get_pb_sum(expr* term, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
    params_ref p;
    ast_manager& m = args.get_manager();
    lia2card_tactic tac(m, p);
    return tac.get_pb_sum(term, rational::one(), args, coeffs, coeff);
}