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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-03-21 17:15:36 -07:00
commit 7b148a73a2
2 changed files with 3 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz_qe/dl_check_table.cpp
View file

@ -287,9 +287,6 @@ namespace datalog {
bool check_table::well_formed() const {
get_plugin().m_count++;
if (get_plugin().m_count == 497) {
std::cout << "here\n";
}
iterator it = m_tocheck->begin(), end = m_tocheck->end();
for (; it != end; ++it) {
table_fact fact;
@ -354,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(); }