mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

spacer: fail with exception on quantifiers in recursive rules

Browse source
This commit is contained in:
Arie Gurfinkel 2020-04-11 14:16:47 -04:00
parent 1e96570365
commit 1f6815213d
1 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/muz/spacer/spacer_context.cpp
View file

@ -1676,8 +1676,17 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule)
} }
TRACE("spacer_init_rule", tout << mk_pp(trans, m) << "\n";); TRACE("spacer_init_rule", tout << mk_pp(trans, m) << "\n";);
// allow quantifiers in init rule // no (universal) quantifiers in recursive rules
SASSERT(ut_size == 0 || is_ground(trans)); CTRACE("spacer", ut_size > 0 && !is_ground(trans),
tout << "Warning: quantifier in recursive rule: " << trans << "\n";);
if (ut_size > 0 && !is_ground(trans)) {
std::stringstream stm;
stm << "spacer: quantifier in a recursive rule:\n";
rule.display(get_context().get_datalog_context(), tout);
throw default_exception(stm.str());
}
if (!m.is_false(trans)) { if (!m.is_false(trans)) {
pt_rule &ptr = m_pt_rules.mk_rule(m, rule); pt_rule &ptr = m_pt_rules.mk_rule(m, rule);
ptr.set_trans(trans); ptr.set_trans(trans);