mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

remove unused min-aggregate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-04 09:23:36 -08:00
parent 3f02beb820
commit 4bbe1d4674
7 changed files with 3 additions and 232 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/ast/dl_decl_plugin.cpp
View file

@ -44,8 +44,7 @@ namespace datalog {
m_num_sym("N"),
m_lt_sym("<"),
m_le_sym("<="),
m_rule_sym("R"),
m_min_sym("min")
m_rule_sym("R")
{
}
@ -491,65 +490,6 @@ namespace datalog {
return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
}
/**
In SMT2 syntax, we can write \c ((_ min R N) v_0 v_1 ... v_k)) where 0 <= N <= k,
R is a relation of sort V_0 x V_1 x ... x V_k and each v_i is a zero-arity function
(also known as a "constant" in SMT2 parlance) whose range is of sort V_i.
Example:
(define-sort number_t () (_ BitVec 2))
(declare-rel numbers (number_t number_t))
(declare-rel is_min (number_t number_t))
(declare-var x number_t)
(declare-var y number_t)
(rule (numbers #b00 #b11))
(rule (numbers #b00 #b01))
(rule (=> (and (numbers x y) ((_ min numbers 1) x y)) (is_min x y)))
This says that we want to find the mininum y grouped by x.
*/
func_decl * dl_decl_plugin::mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters) {
if (num_parameters < 2) {
m_manager->raise_exception("invalid min aggregate definition due to missing parameters");
return 0;
}
parameter const & relation_parameter = parameters[0];
if (!relation_parameter.is_ast() || !is_func_decl(relation_parameter.get_ast())) {
m_manager->raise_exception("invalid min aggregate definition, first parameter is not a function declaration");
return 0;
}
func_decl* f = to_func_decl(relation_parameter.get_ast());
if (!m_manager->is_bool(f->get_range())) {
m_manager->raise_exception("invalid min aggregate definition, first paramater must be a predicate");
return 0;
}
parameter const & min_col_parameter = parameters[1];
if (!min_col_parameter.is_int()) {
m_manager->raise_exception("invalid min aggregate definition, second parameter must be an integer");
return 0;
}
if (min_col_parameter.get_int() < 0) {
m_manager->raise_exception("invalid min aggregate definition, second parameter must be non-negative");
return 0;
}
if ((unsigned)min_col_parameter.get_int() >= f->get_arity()) {
m_manager->raise_exception("invalid min aggregate definition, second parameter exceeds the arity of the relation");
return 0;
}
func_decl_info info(m_family_id, k, num_parameters, parameters);
SASSERT(f->get_info() == 0);
return m_manager->mk_func_decl(m_min_sym, f->get_arity(), f->get_domain(), f->get_range(), info);
}
func_decl * dl_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -678,8 +618,6 @@ namespace datalog {
break;
}
case OP_DL_MIN:
return mk_min(k, num_parameters, parameters);
default:
m_manager->raise_exception("operator not recognized");
@ -691,7 +629,6 @@ namespace datalog {
}
void dl_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.push_back(builtin_name(m_min_sym.bare_str(), OP_DL_MIN));
}
void dl_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

58
src/ast/dl_decl_plugin.h
View file

@ -50,7 +50,6 @@ namespace datalog {
OP_DL_LT,
OP_DL_REP,
OP_DL_ABS,
OP_DL_MIN,
LAST_RA_OP
};
@ -72,7 +71,6 @@ namespace datalog {
symbol m_lt_sym;
symbol m_le_sym;
symbol m_rule_sym;
symbol m_min_sym;
bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const;
bool check_domain(unsigned low, unsigned up, unsigned val) const;
@ -96,68 +94,12 @@ namespace datalog {
func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain);
func_decl * mk_clone(sort* r);
func_decl * mk_rule(unsigned arity);
func_decl * mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_finite_sort(unsigned num_params, parameter const* params);
sort * mk_relation_sort(unsigned num_params, parameter const* params);
sort * mk_rule_sort();
public:
/**
Is \c decl a min aggregation function?
*/
static bool is_aggregate(const func_decl* const decl)
{
return decl->get_decl_kind() == OP_DL_MIN;
}
/**
\pre: is_aggregate(aggregate)
\returns function declaration of predicate which is subject to min aggregation function
*/
static func_decl * min_func_decl(const func_decl* const aggregate)
{
SASSERT(is_aggregate(aggregate));
parameter const & relation_parameter = aggregate->get_parameter(0);
return to_func_decl(relation_parameter.get_ast());
}
/**
\pre: is_aggregate(aggregate)
\returns column identifier (starting at zero) which is minimized by aggregation function
*/
static unsigned min_col(const func_decl* const aggregate)
{
SASSERT(is_aggregate(aggregate));
return (unsigned)aggregate->get_parameter(1).get_int();
}
/**
\pre: is_aggregate(aggregate)
\returns column identifiers for the "group by" in the given min aggregation function
*/
static unsigned_vector group_by_cols(const func_decl* const aggregate)
{
SASSERT(is_aggregate(aggregate));
unsigned _min_col = min_col(aggregate);
if (aggregate->get_arity() == 0U)
return unsigned_vector();
unsigned col_num = 0;
unsigned_vector cols(aggregate->get_arity() - 1U);
for (unsigned i = 0; i < cols.size(); ++i, ++col_num)
{
if (col_num == _min_col)
++col_num;
cols[i] = col_num;
}
return cols;
}
dl_decl_plugin();
virtual ~dl_decl_plugin() {}

7
src/muz/base/dl_rule.h
View file

@ -346,13 +346,6 @@ namespace datalog {
bool is_neg_tail(unsigned i) const { SASSERT(i < m_tail_size); return GET_TAG(m_tail[i]) == 1; }
/**
A predicate P(Xj) can be annotated by adding an interpreted predicate of the form ((_ min P N) ...)
where N is the column number that should be used for the min aggregation function.
Such an interpreted predicate is an example for which this function returns true.
*/
bool is_min_tail(unsigned i) const { return dl_decl_plugin::is_aggregate(get_tail(i)->get_decl()); }
/**
Check whether predicate p is in the interpreted tail.

44
src/muz/base/dl_rule_set.cpp
View file

@ -400,7 +400,7 @@ namespace datalog {
SASSERT(!is_closed()); //the rule_set is not already closed
m_deps.populate(*this);
m_stratifier = alloc(rule_stratifier, m_deps);
if (!stratified_negation() || !check_min()) {
if (!stratified_negation()) {
m_stratifier = 0;
m_deps.reset();
return false;
@ -441,48 +441,6 @@ namespace datalog {
return true;
}
bool rule_set::check_min() {
// For now, we check the following:
//
// if a min aggregation function occurs in an SCC, is this SCC
// free of any other non-monotonic functions, e.g. negation?
const unsigned NEG_BIT = 1U << 0;
const unsigned MIN_BIT = 1U << 1;
ptr_vector<rule>::const_iterator it = m_rules.c_ptr();
ptr_vector<rule>::const_iterator end = m_rules.c_ptr() + m_rules.size();
unsigned_vector component_status(m_stratifier->get_strats().size());
for (; it != end; it++) {
rule * r = *it;
// app * head = r->get_head();
// func_decl * head_decl = head->get_decl();
// unsigned head_strat = get_predicate_strat(head_decl);
unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; i++) {
func_decl * tail_decl = r->get_tail(i)->get_decl();
unsigned strat = get_predicate_strat(tail_decl);
if (r->is_neg_tail(i)) {
SASSERT(strat < component_status.size());
component_status[strat] |= NEG_BIT;
}
if (r->is_min_tail(i)) {
SASSERT(strat < component_status.size());
component_status[strat] |= MIN_BIT;
}
}
}
const unsigned CONFLICT = NEG_BIT | MIN_BIT;
for (unsigned k = 0; k < component_status.size(); ++k) {
if (component_status[k] == CONFLICT)
return false;
}
return true;
}
void rule_set::replace_rules(const rule_set & src) {
if (this != &src) {

1
src/muz/base/dl_rule_set.h
View file

@ -179,7 +179,6 @@ namespace datalog {
void compute_deps();
void compute_tc_deps();
bool stratified_negation();
bool check_min();
public:
rule_set(context & ctx);
rule_set(const rule_set & rs);

45
src/muz/rel/dl_compiler.cpp
View file

@ -73,12 +73,6 @@ namespace datalog {
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
const unsigned min_col, instruction_block & acc) {
target = get_register(m_reg_signatures[source], true, source);
acc.push_back(instruction::mk_min(source, target, group_by_cols, min_col));
}
void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) {
SASSERT(!removed_cols.empty());
@ -446,29 +440,7 @@ namespace datalog {
get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
}
void compiler::find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates) {
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned ft_len = r->get_tail_size(); // full tail
func_decl * aggregate;
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
aggregate = r->get_tail(tail_index)->get_decl();
if (dl_decl_plugin::is_aggregate(aggregate)) {
min_aggregates.push_back(aggregate);
}
}
}
bool compiler::prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
unsigned_vector & group_by_cols, unsigned & min_col) {
for (unsigned i = 0; i < min_aggregates.size(); ++i) {
if (dl_decl_plugin::min_func_decl(min_aggregates[i]) == decl) {
group_by_cols = dl_decl_plugin::group_by_cols(min_aggregates[i]);
min_col = dl_decl_plugin::min_col(min_aggregates[i]);
return true;
}
}
return false;
}
void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs,
reg_idx delta_reg, bool use_widening, instruction_block & acc) {
@ -496,10 +468,7 @@ namespace datalog {
bool dealloc = true;
// setup information for min aggregation
ptr_vector<func_decl> min_aggregates;
find_min_aggregates(r, min_aggregates);
unsigned_vector group_by_cols;
unsigned min_col;
if(pt_len == 2) {
reg_idx t1_reg=tail_regs[0];
@ -509,14 +478,6 @@ namespace datalog {
SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args());
SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args());
if (prepare_min_aggregate(a1->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(t1_reg, single_res, group_by_cols, min_col, acc);
}
if (prepare_min_aggregate(a2->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(t2_reg, single_res, group_by_cols, min_col, acc);
}
variable_intersection a1a2(m_context.get_manager());
a1a2.populate(a1,a2);
@ -558,9 +519,6 @@ namespace datalog {
single_res = tail_regs[0];
dealloc = false;
if (prepare_min_aggregate(a->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(single_res, single_res, group_by_cols, min_col, acc);
}
SASSERT(m_reg_signatures[single_res].size() == a->get_num_args());
@ -645,8 +603,7 @@ namespace datalog {
unsigned ft_len = r->get_tail_size(); // full tail
ptr_vector<expr> tail;
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
if (!r->is_min_tail(tail_index))
tail.push_back(r->get_tail(tail_index));
tail.push_back(r->get_tail(tail_index));
}
expr_ref_vector binding(m);

15
src/muz/rel/dl_compiler.h
View file

@ -120,21 +120,6 @@ namespace datalog {
instruction_observer m_instruction_observer;
expr_free_vars m_free_vars;
/**
\brief Finds all the min aggregation functions in the premise of a given rule.
*/
static void find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates);
/**
\brief Decides whether a predicate is subject to a min aggregation function.
If \c decl is subject to a min aggregation function, the output parameters are written
with the neccessary information.
\returns true if the output paramaters have been written
*/
static bool prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
unsigned_vector & group_by_cols, unsigned & min_col);
/**
If true, the union operation on the underlying structure only provides the information