From d686448356961b4f03b3191f74b8d852cf312baf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Sep 2013 21:52:01 -0700 Subject: [PATCH 1/3] local changes Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_util.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index a6bd7f7f8..f2c50487f 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -719,7 +719,7 @@ namespace datalog { T& operator*() { return *m_t; } const T& operator*() const { return *m_t; } operator bool() const { return m_t!=0; } - T* get() { return m_t; } + T* get() const { return m_t; } /** \brief Remove object from \c scoped_rel without deleting it. */ From 1496333e5bafeaec1f6d3afba54a930915b74f0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Sep 2013 09:22:45 -0700 Subject: [PATCH 2/3] fix mint64 build errors Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_util.cpp | 2 -- src/muz/rel/dl_lazy_table.cpp | 3 +-- src/muz/rel/dl_lazy_table.h | 20 ++++++++++---------- 3 files changed, 11 insertions(+), 14 deletions(-) diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index c23f222e5..218f9906a 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -34,8 +34,6 @@ Revision History: namespace datalog { - static unsigned verbose_action_inside = 0; - verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) { IF_VERBOSE(m_lvl, (verbose_stream() << msg << "...").flush(); diff --git a/src/muz/rel/dl_lazy_table.cpp b/src/muz/rel/dl_lazy_table.cpp index 16dbc2d21..ec97a4bf5 100644 --- a/src/muz/rel/dl_lazy_table.cpp +++ b/src/muz/rel/dl_lazy_table.cpp @@ -19,7 +19,7 @@ Revision History: #include "dl_lazy_table.h" #include "dl_relation_manager.h" -#include +#include namespace datalog { @@ -53,7 +53,6 @@ namespace datalog { virtual table_base* operator()(const table_base& _t1, const table_base& _t2) { lazy_table const& t1 = get(_t1); lazy_table const& t2 = get(_t2); - lazy_table_plugin& p = t1.get_lplugin(); lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature()); return alloc(lazy_table, tr); } diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h index 34a8b6b92..3c0b47367 100644 --- a/src/muz/rel/dl_lazy_table.h +++ b/src/muz/rel/dl_lazy_table.h @@ -156,7 +156,7 @@ namespace datalog { virtual table_base::iterator begin() const; virtual table_base::iterator end() const; - lazy_table_ref* ref() const { return m_ref.get(); } + lazy_table_ref* get_ref() const { return m_ref.get(); } void set(lazy_table_ref* r) { m_ref = r; } }; @@ -184,8 +184,8 @@ namespace datalog { : lazy_table_ref(t1.get_lplugin(), sig), m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2), - m_t1(t1.ref()), - m_t2(t2.ref()) { } + m_t1(t1.get_ref()), + m_t2(t2.get_ref()) { } virtual ~lazy_table_join() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; } unsigned_vector const& cols1() const { return m_cols1; } @@ -203,7 +203,7 @@ namespace datalog { lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig) : lazy_table_ref(src.get_lplugin(), sig), m_cols(col_cnt, cols), - m_src(src.ref()) {} + m_src(src.get_ref()) {} virtual ~lazy_table_project() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; } @@ -219,7 +219,7 @@ namespace datalog { lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig) : lazy_table_ref(src.get_lplugin(), sig), m_cols(col_cnt, cols), - m_src(src.ref()) {} + m_src(src.get_ref()) {} virtual ~lazy_table_rename() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; } @@ -233,7 +233,7 @@ namespace datalog { ref m_src; public: lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src) - : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.ref()) {} + : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {} virtual ~lazy_table_filter_identical() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; } @@ -251,7 +251,7 @@ namespace datalog { : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_col(col), m_value(value), - m_src(src.ref()) {} + m_src(src.get_ref()) {} virtual ~lazy_table_filter_equal() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; } @@ -267,7 +267,7 @@ namespace datalog { public: lazy_table_filter_interpreted(lazy_table const& src, app* condition) : lazy_table_ref(src.get_lplugin(), src.get_signature()), - m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.ref()) {} + m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {} virtual ~lazy_table_filter_interpreted() {} virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; } @@ -286,8 +286,8 @@ namespace datalog { lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src, unsigned_vector const& c1, unsigned_vector const& c2) : lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()), - m_tgt(tgt.ref()), - m_src(src.ref()), + m_tgt(tgt.get_ref()), + m_src(src.get_ref()), m_cols1(c1), m_cols2(c2) {} virtual ~lazy_table_filter_by_negation() {} From 4ad6660f3585c156e136747da08f4f8c97e45c4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Sep 2013 09:24:35 -0700 Subject: [PATCH 3/3] add const qualifiers to fix warning messages Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.tab.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tptp/tptp5.tab.c b/examples/tptp/tptp5.tab.c index 7fcf7915b..c97225f4c 100644 --- a/examples/tptp/tptp5.tab.c +++ b/examples/tptp/tptp5.tab.c @@ -107,7 +107,7 @@ struct pTreeNode { pTree children[MAX_CHILDREN+1]; }; //----------------------------------------------------------------------------- -int yyerror( char *s ) { +int yyerror( char const *s ) { fprintf( stderr, "%s in line %d at item \"%s\".\n", s, yylineno, yytext); return 0;