mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix parameter checking on quantifiers (thanks to Esteban Pavese), fix query tracking in rel_context (thanks to Nuno Lopes), fix counter for free variables under quantfiers (thanks to Tomer Weiss)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0b56440cba
commit
5c145dcd4b
|
@ -165,7 +165,10 @@ extern "C" {
|
|||
}
|
||||
for (unsigned i = 0; i < num_bound; ++i) {
|
||||
app* a = to_app(bound[i]);
|
||||
SASSERT(a->get_kind() == AST_APP);
|
||||
if (a->get_kind() != AST_APP) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
symbol s(to_app(a)->get_decl()->get_name());
|
||||
names.push_back(of_symbol(s));
|
||||
types.push_back(of_sort(mk_c(c)->m().get_sort(a)));
|
||||
|
|
|
@ -108,6 +108,7 @@ void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
|
|||
unsigned var_counter::get_max_var(bool& has_var) {
|
||||
has_var = false;
|
||||
unsigned max_var = 0;
|
||||
ptr_vector<quantifier> qs;
|
||||
while (!m_todo.empty()) {
|
||||
expr* e = m_todo.back();
|
||||
m_todo.pop_back();
|
||||
|
@ -117,14 +118,7 @@ unsigned var_counter::get_max_var(bool& has_var) {
|
|||
m_visited.mark(e, true);
|
||||
switch(e->get_kind()) {
|
||||
case AST_QUANTIFIER: {
|
||||
var_counter aux_counter;
|
||||
quantifier* q = to_quantifier(e);
|
||||
bool has_var1 = false;
|
||||
unsigned max_v = aux_counter.get_max_var(has_var1);
|
||||
if (max_v > max_var + q->get_num_decls()) {
|
||||
max_var = max_v - q->get_num_decls();
|
||||
has_var = true;
|
||||
}
|
||||
qs.push_back(to_quantifier(e));
|
||||
break;
|
||||
}
|
||||
case AST_VAR: {
|
||||
|
@ -147,6 +141,20 @@ unsigned var_counter::get_max_var(bool& has_var) {
|
|||
}
|
||||
}
|
||||
m_visited.reset();
|
||||
|
||||
while (!qs.empty()) {
|
||||
var_counter aux_counter;
|
||||
quantifier* q = qs.back();
|
||||
qs.pop_back();
|
||||
aux_counter.m_todo.push_back(q->get_expr());
|
||||
bool has_var1 = false;
|
||||
unsigned max_v = aux_counter.get_max_var(has_var1);
|
||||
if (max_v >= max_var + q->get_num_decls()) {
|
||||
max_var = max_v - q->get_num_decls();
|
||||
has_var = has_var || has_var1;
|
||||
}
|
||||
}
|
||||
|
||||
return max_var;
|
||||
}
|
||||
|
||||
|
|
|
@ -652,6 +652,7 @@ namespace datalog {
|
|||
if (check_pred(e)) {
|
||||
std::ostringstream out;
|
||||
out << "recursive predicate " << mk_ismt2_pp(e, get_manager()) << " occurs nested in body";
|
||||
r->display(*this, out << "\n");
|
||||
throw default_exception(out.str());
|
||||
|
||||
}
|
||||
|
|
|
@ -186,15 +186,20 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
|
||||
DEBUG_CODE(ptr_vector<sort> sorts;
|
||||
::get_free_vars(fml, sorts); );
|
||||
expr_ref_vector fmls(m);
|
||||
proof_ref_vector prs(m);
|
||||
m_hnf.reset();
|
||||
m_hnf.set_name(name);
|
||||
|
||||
m_hnf(fml, p, fmls, prs);
|
||||
for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) {
|
||||
m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
|
||||
}
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
DEBUG_CODE(ptr_vector<sort> sorts;
|
||||
::get_free_vars(fmls[i].get(), sorts); );
|
||||
mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name);
|
||||
}
|
||||
}
|
||||
|
@ -265,7 +270,7 @@ namespace datalog {
|
|||
}
|
||||
else {
|
||||
head = ensure_app(fml);
|
||||
}
|
||||
}
|
||||
return index;
|
||||
}
|
||||
|
||||
|
@ -491,6 +496,12 @@ namespace datalog {
|
|||
app * * uninterp_tail = r->m_tail; //grows upwards
|
||||
app * * interp_tail = r->m_tail+n; //grows downwards
|
||||
|
||||
DEBUG_CODE(ptr_vector<sort> sorts;
|
||||
::get_free_vars(head, sorts);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
::get_free_vars(tail[i], sorts);
|
||||
});
|
||||
|
||||
bool has_neg = false;
|
||||
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
|
|
|
@ -128,7 +128,12 @@ public:
|
|||
}
|
||||
|
||||
void set_name(symbol const& n) {
|
||||
m_name = n;
|
||||
if (n == symbol::null) {
|
||||
m_name = symbol("P");
|
||||
}
|
||||
else {
|
||||
m_name = n;
|
||||
}
|
||||
}
|
||||
|
||||
func_decl_ref_vector const& get_fresh_predicates() {
|
||||
|
|
|
@ -105,14 +105,12 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
lbool rel_context::saturate() {
|
||||
lbool rel_context::saturate(scoped_query& sq) {
|
||||
m_context.ensure_closed();
|
||||
bool time_limit = m_context.soft_timeout()!=0;
|
||||
unsigned remaining_time_limit = m_context.soft_timeout();
|
||||
unsigned restart_time = m_context.initial_restart_timeout();
|
||||
|
||||
scoped_query scoped_query(m_context);
|
||||
|
||||
|
||||
instruction_block termination_code;
|
||||
|
||||
lbool result;
|
||||
|
@ -191,7 +189,7 @@ namespace datalog {
|
|||
else {
|
||||
restart_time = static_cast<unsigned>(new_restart_time);
|
||||
}
|
||||
scoped_query.reset();
|
||||
sq.reset();
|
||||
}
|
||||
m_context.record_transformed_rules();
|
||||
TRACE("dl", display_profile(tout););
|
||||
|
@ -206,7 +204,7 @@ namespace datalog {
|
|||
}
|
||||
m_context.close();
|
||||
reset_negated_tables();
|
||||
lbool res = saturate();
|
||||
lbool res = saturate(_scoped_query);
|
||||
|
||||
switch(res) {
|
||||
case l_true: {
|
||||
|
@ -215,7 +213,8 @@ namespace datalog {
|
|||
bool some_non_empty = num_rels == 0;
|
||||
bool is_approx = false;
|
||||
for (unsigned i = 0; i < num_rels; ++i) {
|
||||
relation_base& rel = get_relation(rels[i]);
|
||||
func_decl* q = m_context.get_rules().get_pred(rels[i]);
|
||||
relation_base& rel = get_relation(q);
|
||||
if (!rel.empty()) {
|
||||
some_non_empty = true;
|
||||
}
|
||||
|
@ -272,13 +271,14 @@ namespace datalog {
|
|||
|
||||
if (m_context.magic_sets_for_queries()) {
|
||||
m_context.transform_rules(alloc(mk_magic_sets, m_context, query_pred));
|
||||
query_pred = m_context.get_rules().get_pred(query_pred);
|
||||
}
|
||||
|
||||
lbool res = saturate(_scoped_query);
|
||||
|
||||
query_pred = m_context.get_rules().get_pred(query_pred);
|
||||
|
||||
lbool res = saturate();
|
||||
|
||||
if (res != l_undef) {
|
||||
if (res != l_undef) {
|
||||
m_last_result_relation = get_relation(query_pred).clone();
|
||||
if (m_last_result_relation->empty()) {
|
||||
res = l_false;
|
||||
|
|
|
@ -109,7 +109,7 @@ namespace datalog {
|
|||
|
||||
void display_profile(std::ostream& out);
|
||||
|
||||
lbool saturate();
|
||||
lbool saturate(scoped_query& sq);
|
||||
|
||||
};
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue