mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
110 lines
3.4 KiB
C++
110 lines
3.4 KiB
C++
/*++
|
|
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:
|
|
|
|
--*/
|
|
#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"
|
|
|
|
|
|
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; }
|
|
};
|
|
};
|
|
|
|
tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
|
|
/*
|
|
ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)")
|
|
*/
|
|
|
|
|