mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix overloading of complement from base_table

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-03-20 15:47:56 -07:00
parent ab761c4c32
commit 39d7246251
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/dl_check_table.cpp
View file

@ -351,8 +351,8 @@ namespace datalog {
return result;
}
table_base * check_table::complement(func_decl* p) const {
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
table_base * check_table::complement(func_decl* p, const table_element * func_columns) const {
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p, func_columns), m_checker->complement(p, func_columns));
return result;
}

2
src/muz_qe/dl_check_table.h
View file

@ -119,7 +119,7 @@ namespace datalog {
virtual void add_fact(const table_fact & f);
virtual void remove_fact(const table_element* fact);
virtual bool contains_fact(const table_fact & f) const;
virtual table_base * complement(func_decl* p) const;
virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const;
virtual table_base * clone() const;
virtual iterator begin() const { SASSERT(well_formed()); return m_tocheck->begin(); }