3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

make card2bv a simplifier

This commit is contained in:
Nikolaj Bjorner 2022-11-25 11:07:31 +07:00
parent cb789f6ca8
commit db74e23de1
9 changed files with 120 additions and 191 deletions

View file

@ -1,6 +1,7 @@
z3_add_component(simplifiers
SOURCES
bv_slice.cpp
card2bv.cpp
elim_unconstrained.cpp
eliminate_predicates.cpp
euf_completion.cpp

View file

@ -0,0 +1,61 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
card2bv.cpp
Abstract:
convert cardinality constraints to bit-vectors
Author:
Nikolaj Bjorner (nbjorner) 2022-11-24
--*/
#include "ast/simplifiers/card2bv.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/pb2bv_rewriter.h"
card2bv::card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls) :
dependent_expr_simplifier(m, fmls), m_params(p) {}
void card2bv::reduce() {
th_rewriter rw1(m, m_params);
pb2bv_rewriter rw2(m, m_params);
expr_ref new_f1(m), new_f2(m);
proof_ref new_pr(m);
for (unsigned idx = 0; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
auto [f, d] = m_fmls[idx]();
rw1(f, new_f1);
rw2(false, new_f1, new_f2, new_pr);
if (new_f2 != f) {
TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_f2 << "\n");
m_fmls.update(idx, dependent_expr(m, new_f2, d));
++m_stats.m_num_rewrites;
}
}
expr_ref_vector fmls(m);
rw2.flush_side_constraints(fmls);
for (expr* e : fmls)
m_fmls.add(dependent_expr(m, e, nullptr));
func_decl_ref_vector const& fns = rw2.fresh_constants();
for (func_decl* f : fns)
m_fmls.model_trail().hide(f);
}
void card2bv::collect_statistics(statistics& st) const {
st.update("card2bv-rewrites", m_stats.m_num_rewrites);
}
void card2bv::collect_param_descrs(param_descrs& r) {
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver");
pb2bv_rewriter rw(m, m_params);
rw.collect_param_descrs(r);
}

View file

@ -0,0 +1,42 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
card2bv.h
Abstract:
convert cardinality constraints to bit-vectors
Author:
Nikolaj Bjorner (nbjorner) 2022-11-24
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/th_rewriter.h"
class card2bv : public dependent_expr_simplifier {
struct stats {
unsigned m_num_rewrites = 0;
void reset() { memset(this, 0, sizeof(*this)); }
};
stats m_stats;
params_ref m_params;
public:
card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls);
void reduce() override;
void collect_statistics(statistics& st) const override;
void reset_statistics() override { m_stats.reset(); }
void updt_params(params_ref const& p) override { m_params.append(p); }
void collect_param_descrs(param_descrs& r) override;
};

View file

@ -285,7 +285,7 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
for (auto const& entry : mc.entries()) {
switch (entry.m_instruction) {
case generic_model_converter::instruction::HIDE:
trail.push(entry.m_f);
trail.hide(entry.m_f);
break;
case generic_model_converter::instruction::ADD:
break;

View file

@ -327,7 +327,7 @@ void eliminate_predicates::try_find_macro(clause& cl) {
app_ref def(m), k(m), fml(m);
func_decl_ref fn(m);
fn = m.mk_fresh_func_decl(df->get_arity(), df->get_domain(), df->get_range());
m_fmls.model_trail().push(fn); // hide definition of fn
m_fmls.model_trail().hide(fn); // hide definition of fn
k = m.mk_app(fn, f->get_num_args(), f->get_args());
def = m.mk_ite(cond, t, k);
insert_macro(f, def, cl.m_dep);

View file

@ -102,7 +102,7 @@ public:
/**
* add declaration to hide
*/
void push(func_decl* f) {
void hide(func_decl* f) {
m_trail.push_back(alloc(entry, m, f));
m_trail_stack.push(push_back_vector(m_trail));
}

View file

@ -6,7 +6,6 @@ z3_add_component(arith_tactics
bound_propagator.cpp
bv2int_rewriter.cpp
bv2real_rewriter.cpp
card2bv_tactic.cpp
degree_shift_tactic.cpp
diff_neq_tactic.cpp
eq2bv_tactic.cpp

View file

@ -1,105 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
card2bv_tactic.cpp
Abstract:
Tactic for converting Pseudo-Boolean constraints to BV
Author:
Nikolaj Bjorner (nbjorner) 2014-03-20
Notes:
--*/
#include "tactic/tactical.h"
#include "ast/ast_smt2_pp.h"
#include "tactic/arith/card2bv_tactic.h"
#include "ast/rewriter/pb2bv_rewriter.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/converters/generic_model_converter.h"
class card2bv_tactic : public tactic {
ast_manager & m;
params_ref m_params;
public:
card2bv_tactic(ast_manager & m, params_ref const & p):
m(m),
m_params(p) {
}
tactic * translate(ast_manager & m) override {
return alloc(card2bv_tactic, m, m_params);
}
char const* name() const override { return "card2bv"; }
void updt_params(params_ref const & p) override {
m_params.append(p);
}
void collect_param_descrs(param_descrs & r) override {
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver");
pb2bv_rewriter rw(m, m_params);
rw.collect_param_descrs(r);
}
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
TRACE("card2bv-before", g->display(tout););
result.reset();
tactic_report report("card2bv", *g);
th_rewriter rw1(m, m_params);
pb2bv_rewriter rw2(m, m_params);
if (g->inconsistent()) {
result.push_back(g.get());
return;
}
expr_ref new_f1(m), new_f2(m);
for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
proof_ref new_pr1(m), new_pr2(m);
rw1(g->form(idx), new_f1, new_pr1);
TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;);
rw2(false, new_f1, new_f2, new_pr2);
TRACE("card2bv", tout << "Rewriting " << new_f2 << "\n" << new_pr2 << std::endl;);
if (m.proofs_enabled()) {
new_pr1 = m.mk_transitivity(new_pr1, new_pr2);
new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1);
}
g->update(idx, new_f2, new_pr1, g->dep(idx));
}
expr_ref_vector fmls(m);
rw2.flush_side_constraints(fmls);
for (expr* e : fmls) {
g->assert_expr(e);
}
func_decl_ref_vector const& fns = rw2.fresh_constants();
if (!fns.empty()) {
generic_model_converter* filter = alloc(generic_model_converter, m, "card2bv");
for (func_decl* f : fns) filter->hide(f);
g->add(filter);
}
g->inc_depth();
result.push_back(g.get());
}
void cleanup() override {
}
};
tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(card2bv_tactic, m, p));
}

View file

@ -13,95 +13,26 @@ Author:
Nikolaj Bjorner (nbjorner) 2014-03-20
Notes:
--*/
#pragma once
#include "util/params.h"
#include "ast/pb_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/rewriter.h"
#include<typeinfo>
#include "util/sorting_network.h"
#include "tactic/tactic.h"
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/card2bv.h"
class ast_manager;
class tactic;
namespace pb {
class card2bv_rewriter {
public:
typedef expr* pliteral;
typedef ptr_vector<expr> pliteral_vector;
private:
ast_manager& m;
arith_util au;
pb_util pb;
bv_util bv;
psort_nw<card2bv_rewriter> m_sort;
expr_ref_vector m_lemmas;
expr_ref_vector m_trail;
unsigned get_num_bits(func_decl* f);
void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
expr* negate(expr* e);
expr* mk_ite(expr* c, expr* hi, expr* lo);
bool is_or(func_decl* f);
bool is_and(func_decl* f);
bool is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result);
expr_ref mk_atmost1(unsigned sz, expr * const* args);
void mk_at_most_1_small(bool last, unsigned n, pliteral const* xs, expr_ref_vector& result, expr_ref_vector& ors);
public:
card2bv_rewriter(ast_manager& m);
br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
void mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas);
// definitions used for sorting network
pliteral mk_false() { return m.mk_false(); }
pliteral mk_true() { return m.mk_true(); }
pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); }
pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); }
pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
std::ostream& pp(std::ostream& out, pliteral lit);
pliteral fresh();
pliteral trail(pliteral l);
void mk_clause(unsigned n, pliteral const* lits);
};
struct card2bv_rewriter_cfg : public default_rewriter_cfg {
card2bv_rewriter m_r;
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 m_r.mk_app_core(f, num, args, result);
}
card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
};
class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
card2bv_rewriter_cfg m_cfg;
pb_util pb;
expr_ref_vector m_lemmas;
public:
card_pb_rewriter(ast_manager & m):
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
m_cfg(m),
pb(m),
m_lemmas(m) {}
void rewrite(expr* e, expr_ref& result);
expr_ref_vector& lemmas() { return m_lemmas; }
};
class card2bv_tactic_factory : public dependent_expr_simplifier_factory {
public:
dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
return alloc(card2bv, m, p, s);
}
};
tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p, alloc(card2bv_tactic_factory), "card2bv");
}
/*
ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)")
*/