From ea2b17d83b9edd5363e298dd653b01f4343c218d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Mar 2013 10:40:52 -0700 Subject: [PATCH 1/2] remove debug code Signed-off-by: Nuno Lopes --- src/muz_qe/dl_check_table.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp index d7dfbe1ae..18d5feb39 100644 --- a/src/muz_qe/dl_check_table.cpp +++ b/src/muz_qe/dl_check_table.cpp @@ -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; From 39d72462516084a9c0fa1d33ec43b5e43a5d263c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Mar 2013 15:47:56 -0700 Subject: [PATCH 2/2] fix overloading of complement from base_table Signed-off-by: Nuno Lopes --- src/muz_qe/dl_check_table.cpp | 4 ++-- src/muz_qe/dl_check_table.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp index 18d5feb39..5081654b5 100644 --- a/src/muz_qe/dl_check_table.cpp +++ b/src/muz_qe/dl_check_table.cpp @@ -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; } diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 6f098f8bc..7126bde66 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -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(); }