mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

DoC: fix fast_empty() for tables without columns

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-01-28 11:38:26 +00:00
parent 9e447281ed
commit 1701af9dc9
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/rel/udoc_relation.cpp
View file

@ -1127,7 +1127,7 @@ namespace datalog {
// fast_pass(t, n); // fast_pass(t, n);
} }
*/ */
if (n.get_signature().size() == 0) if (n.get_signature().empty())
t.get_udoc().reset(t.get_dm()); t.get_udoc().reset(t.get_dm());
else if (m_is_subtract) else if (m_is_subtract)
t.get_udoc().subtract(t.get_dm(), n.get_udoc()); t.get_udoc().subtract(t.get_dm(), n.get_udoc());

2
src/muz/rel/udoc_relation.h
View file

@ -48,7 +48,7 @@ namespace datalog {
virtual udoc_relation * complement(func_decl*) const; virtual udoc_relation * complement(func_decl*) const;
virtual void to_formula(expr_ref& fml) const; virtual void to_formula(expr_ref& fml) const;
udoc_plugin& get_plugin() const; udoc_plugin& get_plugin() const;
virtual bool fast_empty() const { return !get_signature().empty() && m_elems.is_empty(); } virtual bool fast_empty() const { return m_elems.is_empty(); }
virtual bool empty() const; virtual bool empty() const;
virtual void display(std::ostream& out) const; virtual void display(std::ostream& out) const;
virtual bool is_precise() const { return true; } virtual bool is_precise() const { return true; }