mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add vocabulary for arbitrary PB inequalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
293a97bdfc
commit
3e8c7d85aa
|
@ -20,7 +20,8 @@ Revision History:
|
|||
#include "card_decl_plugin.h"
|
||||
|
||||
card_decl_plugin::card_decl_plugin():
|
||||
m_at_most_sym("at-most")
|
||||
m_at_most_sym("at-most"),
|
||||
m_pble_sym("pble")
|
||||
{}
|
||||
|
||||
func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
|
@ -32,16 +33,36 @@ func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
|
||||
}
|
||||
}
|
||||
if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
|
||||
m.raise_exception("function 'at-most' expects one non-negative integer parameter");
|
||||
switch(k) {
|
||||
case OP_AT_MOST_K: {
|
||||
if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
|
||||
m.raise_exception("function 'at-most' expects one non-negative integer parameter");
|
||||
}
|
||||
func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters);
|
||||
return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info);
|
||||
}
|
||||
case OP_PB_LE: {
|
||||
if (num_parameters != 1 + arity || !parameters[0].is_int()) {
|
||||
m.raise_exception("function 'pble' expects arity+1 integer parameters");
|
||||
}
|
||||
for (unsigned i = 1; i < num_parameters; ++i) {
|
||||
if (!parameters[i].is_int()) {
|
||||
m.raise_exception("function 'pble' expects arity+1 integer parameters");
|
||||
}
|
||||
}
|
||||
func_decl_info info(m_family_id, OP_PB_LE, num_parameters, parameters);
|
||||
return m.mk_func_decl(m_pble_sym, arity, domain, m.mk_bool_sort(), info);
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return 0;
|
||||
}
|
||||
func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters);
|
||||
return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info);
|
||||
}
|
||||
|
||||
void card_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
|
||||
if (logic == symbol::null) {
|
||||
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
|
||||
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -65,8 +86,30 @@ bool card_util::is_at_most_k(app *a, unsigned& k) const {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned card_util::get_k(app *a) const {
|
||||
SASSERT(is_at_most_k(a));
|
||||
return static_cast<unsigned>(a->get_decl()->get_parameter(0).get_int());
|
||||
int card_util::get_k(app *a) const {
|
||||
SASSERT(is_at_most_k(a) || is_le(a));
|
||||
return a->get_decl()->get_parameter(0).get_int();
|
||||
}
|
||||
|
||||
|
||||
bool card_util::is_le(app *a) const {
|
||||
return is_app_of(a, m_fid, OP_PB_LE);
|
||||
}
|
||||
|
||||
bool card_util::is_le(app* a, int& k) const {
|
||||
if (is_le(a)) {
|
||||
k = get_k(a);
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
int card_util::get_le_coeff(app* a, unsigned index) {
|
||||
SASSERT(is_le(a));
|
||||
SASSERT(1 + index < a->get_decl()->get_num_parameters());
|
||||
return a->get_decl()->get_parameter(index + 1).get_int();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -30,14 +30,17 @@ hence:
|
|||
#include"ast.h"
|
||||
|
||||
enum card_op_kind {
|
||||
OP_AT_MOST_K,
|
||||
OP_AT_MOST_K, // at most K Booleans are true.
|
||||
OP_PB_LE, // pseudo-Boolean <= (generalizes at_most_k)
|
||||
LAST_CARD_OP
|
||||
};
|
||||
|
||||
|
||||
class card_decl_plugin : public decl_plugin {
|
||||
symbol m_at_most_sym;
|
||||
symbol m_pble_sym;
|
||||
func_decl * mk_at_most(unsigned arity, unsigned k);
|
||||
func_decl * mk_le(unsigned arity, int const* coeffs, int k);
|
||||
public:
|
||||
card_decl_plugin();
|
||||
virtual ~card_decl_plugin() {}
|
||||
|
@ -54,7 +57,8 @@ public:
|
|||
//
|
||||
// Contract for func_decl:
|
||||
// parameters[0] - integer (at most k elements)
|
||||
// all sorts are Booleans
|
||||
// all sorts are Booleans
|
||||
// parameters[1] .. parameters[arity] - coefficients
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
@ -68,9 +72,13 @@ public:
|
|||
card_util(ast_manager& m):m(m), m_fid(m.mk_family_id("card")) {}
|
||||
ast_manager & get_manager() const { return m; }
|
||||
app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k);
|
||||
app * mk_le(unsigned num_args, int * const* coeffs, expr * const * args, int k);
|
||||
bool is_at_most_k(app *a) const;
|
||||
bool is_at_most_k(app *a, unsigned& k) const;
|
||||
unsigned get_k(app *a) const;
|
||||
int get_k(app *a) const;
|
||||
bool is_le(app *a) const;
|
||||
bool is_le(app* a, int& k) const;
|
||||
int get_le_coeff(app* a, unsigned index);
|
||||
};
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue