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

fix coi-filter to not ignore relational tables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-04 08:54:02 -07:00
parent 1cf2b7c2d3
commit 7c4b2b04a7

View file

@ -52,10 +52,14 @@ namespace datalog {
ptr_vector<func_decl> todo;
rule_set::decl2rules body2rules;
// initialization for reachability
rel_context_base* rc = m_context.get_rel_context();
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
rule * r = *it;
all.insert(r->get_decl());
if (r->get_uninterpreted_tail_size() == 0) {
bool non_empty =
(rc && !rc->is_empty_relation(r->get_decl())) ||
r->get_uninterpreted_tail_size() == 0;
if (non_empty) {
if (!reached.contains(r->get_decl())) {
reached.insert(r->get_decl());
todo.insert(r->get_decl());