From efa3c0f68e72833a4cc2854f8ef61c4ab58c5afd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Oct 2019 12:34:32 +0100 Subject: [PATCH] Fix compiler warnings --- src/ast/for_each_expr.cpp | 6 +- src/muz/rel/dl_base.h | 197 ++++++++++----------- src/muz/rel/dl_finite_product_relation.cpp | 175 +++++++++--------- src/shell/datalog_frontend.cpp | 46 +++-- 4 files changed, 208 insertions(+), 216 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 77dc02d46..6b7ebd1ee 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -45,7 +45,7 @@ unsigned get_num_exprs(expr * n) { } namespace has_skolem_functions_ns { - struct found {}; + struct found {}; struct proc { void operator()(var * n) const {} void operator()(app const * n) const { if (n->get_decl()->is_skolem() && n->get_num_args() > 0) throw found(); } @@ -148,11 +148,10 @@ void subterms_postorder::iterator::next() { break; } } - + } subterms_postorder::iterator& subterms_postorder::iterator::operator++() { - expr* e = m_es.back(); next(); return *this; } @@ -172,4 +171,3 @@ bool subterms_postorder::iterator::operator==(iterator const& other) const { bool subterms_postorder::iterator::operator!=(iterator const& other) const { return !(*this == other); } - diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index d307912be..53072d0b4 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -109,10 +109,10 @@ namespace datalog { } /** - \brief Into \c result assign signature of result of join of relations with signatures \c s1 + \brief Into \c result assign signature of result of join of relations with signatures \c s1 and \c s2. */ - static void from_join(const signature & s1, const signature & s2, unsigned col_cnt, + static void from_join(const signature & s1, const signature & s2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, signature & result) { result.reset(); @@ -137,14 +137,14 @@ namespace datalog { The array of removed columns must be sorted in ascending order. */ - static void from_project(const signature & src, unsigned col_cnt, + static void from_project(const signature & src, unsigned col_cnt, const unsigned * removed_cols, signature & result) { result = src; project_out_vector_columns(result, col_cnt, removed_cols); } - static void from_join_project(const signature & s1, const signature & s2, unsigned joined_col_cnt, - const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + static void from_join_project(const signature & s1, const signature & s2, unsigned joined_col_cnt, + const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, signature & result) { signature aux(s1); from_join(s1, s2, joined_col_cnt, cols1, cols2, aux); @@ -156,7 +156,7 @@ namespace datalog { For description of the permutation format see \c relation_base::rename */ - static void from_rename(const signature & src, unsigned cycle_len, + static void from_rename(const signature & src, unsigned cycle_len, const unsigned * permutation_cycle, signature & result) { SASSERT(cycle_len>=2); result=src; @@ -167,7 +167,7 @@ namespace datalog { /** \brief Into \c result assign signature \c src with reordered columns. */ - static void from_permutation_rename(const signature & src, + static void from_permutation_rename(const signature & src, const unsigned * permutation, signature & result) { result.reset(); unsigned n = src.size(); @@ -211,11 +211,11 @@ namespace datalog { combination. - supports_attachment - is used to query the mutator if it allows communicating + is used to query the mutator if it allows communicating constraints to relations of the kind of the relation. - - attach - is used to associate downstream clients. + - attach + is used to associate downstream clients. It assumes that the relation kind is supported (supports_kind returns true) */ class mutator_fn : public base_fn { @@ -256,7 +256,7 @@ namespace datalog { symbol m_name; relation_manager & m_manager; protected: - plugin_object(symbol const& name, relation_manager & manager) + plugin_object(symbol const& name, relation_manager & manager) : m_kind(null_family_id), m_name(name), m_manager(manager) {} /** @@ -283,7 +283,7 @@ namespace datalog { } /** - \brief Create empty table/relation with given signature and return pointer to it. + \brief Create empty table/relation with given signature and return pointer to it. Precondition: can_handle_signature(s)==true */ @@ -300,7 +300,7 @@ namespace datalog { } /** - \brief Create empty table/relation of the same specification as \c orig and return pointer to it. + \brief Create empty table/relation of the same specification as \c orig and return pointer to it. Precondition: &orig.get_plugin()==this */ @@ -309,7 +309,7 @@ namespace datalog { } /** - \brief Create full table/relation with given signature and return pointer to it. + \brief Create full table/relation with given signature and return pointer to it. Precondition: can_handle_signature(s)==true */ @@ -337,31 +337,31 @@ namespace datalog { virtual join_fn * mk_join_fn(const base_object & t1, const base_object & t2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { return nullptr; } - virtual transformer_fn * mk_project_fn(const base_object & t, unsigned col_cnt, + virtual transformer_fn * mk_project_fn(const base_object & t, unsigned col_cnt, const unsigned * removed_cols) { return nullptr; } virtual join_fn * mk_join_project_fn(const base_object & t1, const base_object & t2, - unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, + unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols) { return nullptr; } - virtual transformer_fn * mk_rename_fn(const base_object & t, unsigned permutation_cycle_len, + virtual transformer_fn * mk_rename_fn(const base_object & t, unsigned permutation_cycle_len, const unsigned * permutation_cycle) { return nullptr; } virtual transformer_fn * mk_permutation_rename_fn(const base_object & t, const unsigned * permutation) { return nullptr; } public: - virtual union_fn * mk_union_fn(const base_object & tgt, const base_object & src, + virtual union_fn * mk_union_fn(const base_object & tgt, const base_object & src, const base_object * delta) { return nullptr; } protected: - virtual union_fn * mk_widen_fn(const base_object & tgt, const base_object & src, + virtual union_fn * mk_widen_fn(const base_object & tgt, const base_object & src, const base_object * delta) { return nullptr; } - virtual mutator_fn * mk_filter_identical_fn(const base_object & t, unsigned col_cnt, + virtual mutator_fn * mk_filter_identical_fn(const base_object & t, unsigned col_cnt, const unsigned * identical_cols) { return nullptr; } - virtual mutator_fn * mk_filter_equal_fn(const base_object & t, const element & value, + virtual mutator_fn * mk_filter_equal_fn(const base_object & t, const element & value, unsigned col) { return nullptr; } virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition) @@ -371,28 +371,28 @@ namespace datalog { app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { return nullptr; } - virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t, + virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t, const element & value, unsigned col) { return nullptr; } - virtual intersection_filter_fn * mk_filter_by_intersection_fn(const base_object & t, - const base_object & src, unsigned joined_col_cnt, - const unsigned * t_cols, const unsigned * src_cols) + virtual intersection_filter_fn * mk_filter_by_intersection_fn(const base_object & t, + const base_object & src, unsigned joined_col_cnt, + const unsigned * t_cols, const unsigned * src_cols) { return nullptr; } - virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t, - const base_object & negated_obj, unsigned joined_col_cnt, - const unsigned * t_cols, const unsigned * negated_cols) + virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t, + const base_object & negated_obj, unsigned joined_col_cnt, + const unsigned * t_cols, const unsigned * negated_cols) { return nullptr; } virtual intersection_join_filter_fn * mk_filter_by_negated_join_fn( - const base_object & t, - const base_object & src1, - const base_object & src2, + const base_object & t, + const base_object & src1, + const base_object & src2, unsigned_vector const& t_cols, unsigned_vector const& src_cols, unsigned_vector const& src1_cols, - unsigned_vector const& src2_cols) + unsigned_vector const& src2_cols) { return nullptr; } }; @@ -405,8 +405,8 @@ namespace datalog { sort_ref m_leak_guard; #endif protected: - base_ancestor(plugin & p, const signature & s) - : m_plugin(p), m_signature(s), m_kind(p.get_kind()) + base_ancestor(plugin & p, const signature & s) + : m_plugin(p), m_signature(s), m_kind(p.get_kind()) #if DL_LEAK_HUNTING , m_leak_guard(p.get_ast_manager().mk_fresh_sort(p.get_name().bare_str()), p.get_ast_manager()) #endif @@ -417,11 +417,11 @@ namespace datalog { } #if DL_LEAK_HUNTING - base_ancestor(const base_ancestor & o) + base_ancestor(const base_ancestor & o) : m_plugin(o.m_plugin), m_signature(o.m_signature), m_kind(o.m_kind), - m_leak_guard(m_plugin.get_ast_manager().mk_fresh_sort(m_plugin.get_name().bare_str()), + m_leak_guard(m_plugin.get_ast_manager().mk_fresh_sort(m_plugin.get_name().bare_str()), m_plugin.get_ast_manager()) { leak_guard_check(m_leak_guard->get_name()); } @@ -435,7 +435,7 @@ namespace datalog { Since the destructor is protected, we cannot use the \c dealloc macro. */ void destroy() { - SASSERT(this); + SASSERT(this != nullptr); this->~base_ancestor(); memory::deallocate(this); } @@ -445,15 +445,15 @@ namespace datalog { Pointers and references to the current object become invalid after a call to this function. */ - virtual void deallocate() { + virtual void deallocate() { destroy(); } /** It must hold that operations created for particular table/relation are able to operate on tables/relations of the same signature and kind. In most cases it is sufficient to use the kind of the plugin object. - - However, it there is some parameter that is not reflected in the signature, the plugin may need to + + However, it there is some parameter that is not reflected in the signature, the plugin may need to allocate different kind numbers to the tables is creates. */ family_id get_kind() const { return m_kind; } @@ -464,7 +464,7 @@ namespace datalog { virtual bool empty() const = 0; /** \brief fast emptiness check. This may be partial. - The requirement is that if fast_empty returns true + The requirement is that if fast_empty returns true then the table or relation is in fact empty. It is allowed to return false even if the relation is empty. */ @@ -489,7 +489,7 @@ namespace datalog { virtual bool can_swap(const base_object & o) const { return false; } - virtual void swap(base_object & o) { + virtual void swap(base_object & o) { std::swap(m_kind, o.m_kind); #if DL_LEAK_HUNTING m_leak_guard = get_plugin().get_ast_manager().mk_fresh_sort(get_plugin().get_name().bare_str()); @@ -515,8 +515,8 @@ namespace datalog { unsigned_vector m_cols2; convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt, - const unsigned * cols1, const unsigned * cols2) - : m_cols1(col_cnt, cols1), + const unsigned * cols1, const unsigned * cols2) + : m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2) { signature::from_join(o1_sig, o2_sig, col_cnt, cols1, cols2, m_result_sig); } @@ -532,14 +532,14 @@ namespace datalog { //it is non-const because it needs to be modified in sparse_table version of the join_project operator unsigned_vector m_removed_cols; - convenient_join_project_fn(const signature & o1_sig, const signature & o2_sig, - unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, - unsigned removed_col_cnt, const unsigned * removed_cols) - : m_cols1(joined_col_cnt, cols1), + convenient_join_project_fn(const signature & o1_sig, const signature & o2_sig, + unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, + unsigned removed_col_cnt, const unsigned * removed_cols) + : m_cols1(joined_col_cnt, cols1), m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols) { - signature::from_join_project(o1_sig, o2_sig, joined_col_cnt, cols1, cols2, + signature::from_join_project(o1_sig, o2_sig, joined_col_cnt, cols1, cols2, removed_col_cnt, removed_cols, m_result_sig); } @@ -557,9 +557,9 @@ namespace datalog { protected: unsigned_vector m_removed_cols; - convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols) + convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols) : m_removed_cols(col_cnt, removed_cols) { - signature::from_project(orig_sig, col_cnt, removed_cols, + signature::from_project(orig_sig, col_cnt, removed_cols, convenient_transformer_fn::get_result_signature()); } }; @@ -569,9 +569,9 @@ namespace datalog { const unsigned_vector m_cycle; convenient_rename_fn(const signature & orig_sig, unsigned cycle_len, - const unsigned * permutation_cycle) + const unsigned * permutation_cycle) : m_cycle(cycle_len, permutation_cycle) { - signature::from_rename(orig_sig, cycle_len, permutation_cycle, + signature::from_rename(orig_sig, cycle_len, permutation_cycle, convenient_transformer_fn::get_result_signature()); } }; @@ -585,9 +585,9 @@ namespace datalog { bool m_overlap; //one column in negated table is bound multiple times svector m_bound; - convenient_negation_filter_fn(const base_object & tgt, const base_object & neg_t, - unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) - : m_joined_col_cnt(joined_col_cnt), m_cols1(joined_col_cnt, t_cols), + convenient_negation_filter_fn(const base_object & tgt, const base_object & neg_t, + unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) + : m_joined_col_cnt(joined_col_cnt), m_cols1(joined_col_cnt, t_cols), m_cols2(joined_col_cnt, negated_cols) { unsigned neg_sig_size = neg_t.get_signature().size(); m_overlap = false; @@ -598,12 +598,12 @@ namespace datalog { } m_bound[negated_cols[i]]=true; } - m_all_neg_bound = neg_sig_size<=joined_col_cnt && + m_all_neg_bound = neg_sig_size<=joined_col_cnt && std::find(m_bound.begin(), m_bound.end(), false)== m_bound.end(); } /** - \brief Assign values in src to corresponding columns in tgt_neg. If one column should + \brief Assign values in src to corresponding columns in tgt_neg. If one column should be assigned two different values, return false; otherwise return true. Each negative column must correspond to exactly column in the first table. @@ -651,7 +651,7 @@ namespace datalog { bool m_renamers_initialized; renamer_vector m_renamers; public: - default_permutation_rename_fn(const base_object & o, const unsigned * permutation) + default_permutation_rename_fn(const base_object & o, const unsigned * permutation) : m_permutation(o.get_signature().size(), permutation), m_renamers_initialized(false) {} @@ -755,7 +755,7 @@ namespace datalog { void output(ast_manager & m, std::ostream & out) const; struct hash { - unsigned operator()(relation_signature const& s) const { + unsigned operator()(relation_signature const& s) const { return obj_vector_hash(s); } }; @@ -779,8 +779,8 @@ namespace datalog { private: special_relation_type m_special_type; protected: - relation_plugin(symbol const& name, relation_manager & manager, - special_relation_type special_type = ST_ORDINARY) + relation_plugin(symbol const& name, relation_manager & manager, + special_relation_type special_type = ST_ORDINARY) : plugin_object(name, manager), m_special_type(special_type) {} public: @@ -801,7 +801,7 @@ namespace datalog { class relation_base : public relation_infrastructure::base_ancestor { protected: - relation_base(relation_plugin & plugin, const relation_signature & s) + relation_base(relation_plugin & plugin, const relation_signature & s) : base_ancestor(plugin, s) {} ~relation_base() override {} public: @@ -827,7 +827,7 @@ namespace datalog { // table_base // // ----------------------------------- - + class table_signature; class table_plugin; class table_base; @@ -873,11 +873,11 @@ namespace datalog { public: virtual ~table_row_mutator_fn() {} /** - \brief The function is called for a particular table row. The \c func_columns contains - a pointer to an array of functional column values that can be modified. If the function + \brief The function is called for a particular table row. The \c func_columns contains + a pointer to an array of functional column values that can be modified. If the function returns true, the modification will appear in the table; otherwise the row will be deleted. - It is possible that one call to the function stands for multiple table rows that share + It is possible that one call to the function stands for multiple table rows that share the same functional column values. */ virtual bool operator()(table_element * func_columns) = 0; @@ -888,7 +888,7 @@ namespace datalog { virtual ~table_row_pair_reduce_fn() {} /** \brief The function is called for pair of table rows that became duplicit due to projection. - The values that are in the first array after return from the function will be used for the + The values that are in the first array after return from the function will be used for the resulting row. It is assumed that the function is idempotent: when the two functional sub-tuples are equal, @@ -901,7 +901,7 @@ namespace datalog { class table_signature : public table_infrastructure::signature_base { public: struct hash { - unsigned operator()(table_signature const& s) const { + unsigned operator()(table_signature const& s) const { return svector_hash()(s); } }; @@ -915,7 +915,7 @@ namespace datalog { unsigned m_functional_columns; public: table_signature() : m_functional_columns(0) {} - + void swap(table_signature & s) { signature_base::swap(s); std::swap(m_functional_columns, s.m_functional_columns); @@ -931,7 +931,7 @@ namespace datalog { void set_functional_columns(unsigned val) { SASSERT(size()>=val); m_functional_columns = val; } /** - \brief Return index of the first functional column, or the size of the signature if there + \brief Return index of the first functional column, or the size of the signature if there are no functional columns. */ unsigned first_functional() const { return size()-m_functional_columns; } @@ -952,16 +952,16 @@ namespace datalog { /** - \brief Into \c result assign signature of result of join of relations with signatures \c s1 - and \c s2. The result is - + \brief Into \c result assign signature of result of join of relations with signatures \c s1 + and \c s2. The result is + (non-functional of s1)(non-functional of s2)(functional of s1)(functional of s2) */ - static void from_join(const table_signature & s1, const table_signature & s2, unsigned col_cnt, + static void from_join(const table_signature & s1, const table_signature & s2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, table_signature & result); - static void from_join_project(const table_signature & s1, const table_signature & s2, - unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + static void from_join_project(const table_signature & s1, const table_signature & s2, + unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, table_signature & result); @@ -972,10 +972,10 @@ namespace datalog { If we remove at least one non-functional column, all the columns in the result are non-functional. */ - static void from_project(const table_signature & src, unsigned col_cnt, + static void from_project(const table_signature & src, unsigned col_cnt, const unsigned * removed_cols, table_signature & result); - static void from_project_with_reduce(const table_signature & src, unsigned col_cnt, + static void from_project_with_reduce(const table_signature & src, unsigned col_cnt, const unsigned * removed_cols, table_signature & result); /** @@ -983,7 +983,7 @@ namespace datalog { Permutations between functional and nonfunctional columns are not allowed. */ - static void from_rename(const table_signature & src, unsigned cycle_len, + static void from_rename(const table_signature & src, unsigned cycle_len, const unsigned * permutation_cycle, table_signature & result) { signature_base::from_rename(src, cycle_len, permutation_cycle, result); result.set_functional_columns(src.functional_columns()); @@ -998,10 +998,10 @@ namespace datalog { /** \brief Into \c result assign signature \c src with reordered columns. - + Permutations mixing functional and nonfunctional columns are not allowed. */ - static void from_permutation_rename(const table_signature & src, + static void from_permutation_rename(const table_signature & src, const unsigned * permutation, table_signature & result) { signature_base::from_permutation_rename(src, permutation, result); result.set_functional_columns(src.functional_columns()); @@ -1035,14 +1035,14 @@ namespace datalog { If the returned value is non-zero, the returned object must take ownership of \c reducer. Otherwise \c reducer must remain unmodified. */ - virtual table_transformer_fn * mk_project_with_reduce_fn(const table_base & t, unsigned col_cnt, + virtual table_transformer_fn * mk_project_with_reduce_fn(const table_base & t, unsigned col_cnt, const unsigned * removed_cols, table_row_pair_reduce_fn * reducer) { return nullptr; } }; class table_base : public table_infrastructure::base_ancestor { protected: - table_base(table_plugin & plugin, const table_signature & s) + table_base(table_plugin & plugin, const table_signature & s) : base_ancestor(plugin, s) {} ~table_base() override {} public: @@ -1057,15 +1057,15 @@ namespace datalog { bool contains_fact(const table_fact & f) const override; /** - \brief If \c f (i.e. its non-functional part) is not present in the table, - add it and return true. Otherwise update \c f, so that the values of functional + \brief If \c f (i.e. its non-functional part) is not present in the table, + add it and return true. Otherwise update \c f, so that the values of functional columns correspond to the ones present in the table. */ virtual bool suggest_fact(table_fact & f); /** - \brief If \c f (i.e. its non-functional part) is not present in the table, - return false. Otherwise update \c f, so that the values of functional + \brief If \c f (i.e. its non-functional part) is not present in the table, + return false. Otherwise update \c f, so that the values of functional columns correspond to the ones present in the table and return true. */ virtual bool fetch_fact(table_fact & f) const; @@ -1075,7 +1075,7 @@ namespace datalog { */ virtual void ensure_fact(const table_fact & f); - virtual void remove_fact(const table_fact & fact) { + virtual void remove_fact(const table_fact & fact) { SASSERT(fact.size() == get_signature().size()); remove_fact(fact.c_ptr()); } @@ -1105,7 +1105,7 @@ namespace datalog { virtual ~iterator_core() {} void inc_ref() { m_ref_cnt++; } - void dec_ref() { + void dec_ref() { SASSERT(m_ref_cnt>0); m_ref_cnt--; if(m_ref_cnt==0) { @@ -1118,7 +1118,7 @@ namespace datalog { virtual row_interface & operator*() = 0; virtual void operator++() = 0; virtual bool operator==(const iterator_core & it) { - //we worry about the equality operator only because of checking + //we worry about the equality operator only because of checking //the equality with the end() iterator return is_finished() && it.is_finished(); } @@ -1135,7 +1135,7 @@ namespace datalog { virtual ~row_iterator_core() {} void inc_ref() { m_ref_cnt++; } - void dec_ref() { + void dec_ref() { SASSERT(m_ref_cnt>0); m_ref_cnt--; if(m_ref_cnt==0) { @@ -1148,7 +1148,7 @@ namespace datalog { virtual table_element operator*() = 0; virtual void operator++() = 0; virtual bool operator==(const row_iterator_core & it) { - //we worry about the equality operator only because of checking + //we worry about the equality operator only because of checking //the equality with the end() iterator return is_finished() && it.is_finished(); } @@ -1231,8 +1231,8 @@ namespace datalog { mutable table_fact m_current; bool populated() const { return !m_current.empty(); } - void ensure_populated() const { - if(!populated()) { + void ensure_populated() const { + if(!populated()) { get_fact(m_current); } } @@ -1254,7 +1254,7 @@ namespace datalog { }; //This function is here to create iterator instances in classes that derive from table_base. - //We do not want to make the constructor of the iterator class public, and being private, the + //We do not want to make the constructor of the iterator class public, and being private, the //inheritor classes cannot see it directly. static iterator mk_iterator(iterator_core * core) { return iterator(core); @@ -1264,14 +1264,13 @@ namespace datalog { /** \brief Populate vector \c renaming_args so that it can be used as an argument to \c var_subst. The renaming we want is one that transforms variables with numbers of indexes of \c map into the - values of at those indexes. If a value if \c UINT_MAX, it means we do not transform the index + values of at those indexes. If a value if \c UINT_MAX, it means we do not transform the index corresponding to it. */ - void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, + void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, expr_ref_vector & renaming_arg); }; #endif /* DL_BASE_H_ */ - diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 7858ab9a9..42434942c 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -68,7 +68,7 @@ namespace datalog { return symbol(str.c_str()); } - finite_product_relation_plugin & finite_product_relation_plugin::get_plugin(relation_manager & rmgr, + finite_product_relation_plugin & finite_product_relation_plugin::get_plugin(relation_manager & rmgr, relation_plugin & inner) { finite_product_relation_plugin * res; if(!rmgr.try_get_finite_product_relation_plugin(inner, res)) { @@ -78,25 +78,25 @@ namespace datalog { return *res; } - finite_product_relation_plugin::finite_product_relation_plugin(relation_plugin & inner_plugin, - relation_manager & manager) - : relation_plugin(get_name(inner_plugin), manager, ST_FINITE_PRODUCT_RELATION), + finite_product_relation_plugin::finite_product_relation_plugin(relation_plugin & inner_plugin, + relation_manager & manager) + : relation_plugin(get_name(inner_plugin), manager, ST_FINITE_PRODUCT_RELATION), m_inner_plugin(inner_plugin), m_spec_store(*this) { } - void finite_product_relation_plugin::initialize(family_id fid) { + void finite_product_relation_plugin::initialize(family_id fid) { relation_plugin::initialize(fid); m_spec_store.add_available_kind(get_kind()); } - family_id finite_product_relation_plugin::get_relation_kind(finite_product_relation & r, + family_id finite_product_relation_plugin::get_relation_kind(finite_product_relation & r, const bool * table_columns) { const relation_signature & sig = r.get_signature(); svector table_cols_vect(sig.size(), table_columns); return m_spec_store.get_relation_kind(sig, rel_spec(table_cols_vect)); } - void finite_product_relation_plugin::get_all_possible_table_columns(relation_manager & rmgr, + void finite_product_relation_plugin::get_all_possible_table_columns(relation_manager & rmgr, const relation_signature & s, svector & table_columns) { SASSERT(table_columns.empty()); unsigned s_sz = s.size(); @@ -108,7 +108,7 @@ namespace datalog { } } - void finite_product_relation_plugin::split_signatures(const relation_signature & s, + void finite_product_relation_plugin::split_signatures(const relation_signature & s, table_signature & table_sig, relation_signature & remaining_sig) { relation_manager & rmgr = get_manager(); unsigned n = s.size(); @@ -143,7 +143,7 @@ namespace datalog { table_signature table_sig; relation_signature remaining_sig; split_signatures(s, table_sig, remaining_sig); - return m_inner_plugin.can_handle_signature(remaining_sig) + return m_inner_plugin.can_handle_signature(remaining_sig) && get_manager().try_get_appropriate_plugin(table_sig); } @@ -175,7 +175,7 @@ namespace datalog { return mk_empty(s, table_columns.c_ptr()); } - finite_product_relation * finite_product_relation_plugin::mk_empty(const relation_signature & s, + finite_product_relation * finite_product_relation_plugin::mk_empty(const relation_signature & s, const bool * table_columns, family_id inner_kind) { //find table_plugin that can handle the table signature table_signature table_sig; @@ -221,7 +221,7 @@ namespace datalog { const table_base & t = r.get_table(); unsigned removed_col = t.get_signature().size()-1; - scoped_ptr project_fun = + scoped_ptr project_fun = get_manager().mk_project_fn(r.get_table(), 1, &removed_col); table_base * res_table = (*project_fun)(t); @@ -328,9 +328,9 @@ namespace datalog { } public: - converting_join_fn(finite_product_relation_plugin & plugin, const relation_signature & sig1, - const relation_signature & sig2, unsigned col_cnt, const unsigned * cols1, - const unsigned * cols2) + converting_join_fn(finite_product_relation_plugin & plugin, const relation_signature & sig1, + const relation_signature & sig2, unsigned col_cnt, const unsigned * cols1, + const unsigned * cols2) : convenient_relation_join_fn(sig1, sig2, col_cnt, cols1, cols2), m_plugin(plugin) {} @@ -361,14 +361,14 @@ namespace datalog { class finite_product_relation_plugin::join_fn : public convenient_relation_join_fn { scoped_ptr m_tjoin_fn; scoped_ptr m_rjoin_fn; - + unsigned_vector m_t_joined_cols1; unsigned_vector m_t_joined_cols2; unsigned_vector m_r_joined_cols1; unsigned_vector m_r_joined_cols2; //Column equalities betweet table and inner relations. - //The columns numbers correspont to the columns of the table/inner relation + //The columns numbers correspont to the columns of the table/inner relation //in the result of the join operation unsigned_vector m_tr_table_joined_cols; unsigned_vector m_tr_rel_joined_cols; @@ -394,8 +394,6 @@ namespace datalog { bool operator()(table_element * func_columns) override { const relation_base & or1 = m_r1.get_inner_rel(func_columns[0]); const relation_base & or2 = m_r2.get_inner_rel(func_columns[1]); - SASSERT(&or1); - SASSERT(&or2); unsigned new_rel_num = m_rjoins.size(); m_rjoins.push_back(m_parent.do_rjoin(or1, or2)); func_columns[0]=new_rel_num; @@ -403,8 +401,8 @@ namespace datalog { } }; - join_fn(const finite_product_relation & r1, const finite_product_relation & r2, unsigned col_cnt, - const unsigned * cols1, const unsigned * cols2) + join_fn(const finite_product_relation & r1, const finite_product_relation & r2, unsigned col_cnt, + const unsigned * cols1, const unsigned * cols2) : convenient_relation_join_fn(r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2) { unsigned second_table_after_join_ofs = r1.m_table2sig.size(); unsigned second_inner_rel_after_join_ofs = r1.m_other2sig.size(); @@ -427,7 +425,7 @@ namespace datalog { m_tr_rel_joined_cols.push_back(second_inner_rel_after_join_ofs + r2.m_sig2other[cols2[i]]); } } - m_tjoin_fn = r1.get_manager().mk_join_fn(r1.get_table(), r2.get_table(), m_t_joined_cols1.size(), + m_tjoin_fn = r1.get_manager().mk_join_fn(r1.get_table(), r2.get_table(), m_t_joined_cols1.size(), m_t_joined_cols1.c_ptr(), m_t_joined_cols2.c_ptr()); SASSERT(m_tjoin_fn); @@ -442,7 +440,7 @@ namespace datalog { } } - + relation_base * do_rjoin(const relation_base & r1, const relation_base & r2) { if(!m_rjoin_fn) { m_rjoin_fn = r1.get_manager().mk_join_fn(r1, r2, m_r_joined_cols1, m_r_joined_cols2, false); @@ -477,7 +475,7 @@ namespace datalog { //to the table signature of the resulting relation scoped_rel res_table = (*m_tjoined_second_rel_remover)(*tjoined); - relation_plugin & res_oplugin = + relation_plugin & res_oplugin = joined_orelations.empty() ? r1.m_other_plugin : joined_orelations.back()->get_plugin(); //TODO: Maybe we might want to specify a particular relation kind, instead of just null_family_id. @@ -533,7 +531,7 @@ namespace datalog { //determines which columns of the result are table columns and which are in the inner relation svector m_res_table_columns; public: - project_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * removed_cols) + project_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * removed_cols) : convenient_relation_project_fn(r.get_signature(), col_cnt, removed_cols) { SASSERT(col_cnt>0); for(unsigned i=0; i tproject = + scoped_ptr tproject = rmgr.mk_project_with_reduce_fn(rtable, m_removed_table_cols.size(), m_removed_table_cols.c_ptr(), preducer); res_table = (*tproject)(rtable); } @@ -638,7 +636,7 @@ namespace datalog { finite_product_relation * res = alloc(finite_product_relation, r.get_plugin(), get_result_signature(), m_res_table_columns.c_ptr(), res_table->get_plugin(), *res_oplugin, null_family_id); - + res->init(*res_table, res_relations, false); if(!shared_res_table) { @@ -649,7 +647,7 @@ namespace datalog { } }; - relation_transformer_fn * finite_product_relation_plugin::mk_project_fn(const relation_base & rb, unsigned col_cnt, + relation_transformer_fn * finite_product_relation_plugin::mk_project_fn(const relation_base & rb, unsigned col_cnt, const unsigned * removed_cols) { if(&rb.get_plugin()!=this) { return nullptr; @@ -669,7 +667,7 @@ namespace datalog { //determines which columns of the result are table columns and which are in the inner relation svector m_res_table_columns; public: - rename_fn(const finite_product_relation & r, unsigned cycle_len, const unsigned * permutation_cycle) + rename_fn(const finite_product_relation & r, unsigned cycle_len, const unsigned * permutation_cycle) : convenient_relation_rename_fn(r.get_signature(), cycle_len, permutation_cycle) { SASSERT(cycle_len>1); @@ -743,7 +741,7 @@ namespace datalog { } }; - relation_transformer_fn * finite_product_relation_plugin::mk_rename_fn(const relation_base & rb, + relation_transformer_fn * finite_product_relation_plugin::mk_rename_fn(const relation_base & rb, unsigned permutation_cycle_len, const unsigned * permutation_cycle) { if(&rb.get_plugin()!=this) { @@ -789,11 +787,11 @@ namespace datalog { If \c delta_indexes is 0, it means we are not collecting indexes. */ union_mapper(union_fn & parent, finite_product_relation & tgt, const finite_product_relation & src, - table_base * delta_indexes, relation_vector * delta_rels) - : m_parent(parent), - m_tgt(tgt), - m_src(src), - m_delta_indexes(delta_indexes), + table_base * delta_indexes, relation_vector * delta_rels) + : m_parent(parent), + m_tgt(tgt), + m_src(src), + m_delta_indexes(delta_indexes), m_delta_rels(delta_rels) {} ~union_mapper() override {} @@ -808,7 +806,7 @@ namespace datalog { if(m_delta_indexes) { relation_base * odelta = otgt->get_plugin().mk_empty(otgt->get_signature()); m_parent.get_inner_rel_union_op(*otgt)(*otgt, osrc, odelta); - + unsigned delta_idx = m_delta_rels->size(); m_delta_rels->push_back(odelta); m_di_fact.reset(); @@ -836,7 +834,7 @@ namespace datalog { /** If \c delta_indexes is 0, it means we are not collecting indexes. */ - src_copying_mapper(finite_product_relation & tgt, const finite_product_relation & src) + src_copying_mapper(finite_product_relation & tgt, const finite_product_relation & src) : m_tgt(tgt), m_src(src) {} bool operator()(table_element * func_columns) override { @@ -857,7 +855,7 @@ namespace datalog { scoped_rel src_aux_copy; //copy of src in case its specification needs to be modified - if(!vectors_equal(tgt.m_table2sig, src0.m_table2sig) + if(!vectors_equal(tgt.m_table2sig, src0.m_table2sig) || (delta && !vectors_equal(tgt.m_table2sig, delta->m_table2sig)) ) { src_aux_copy = src0.clone(); ptr_vector orig_rels; @@ -880,7 +878,7 @@ namespace datalog { for(unsigned i=0; i overlap_delta_table = + scoped_rel overlap_delta_table = (*m_overlap_delta_table_builder)(*regular_overlap, *delta_indexes); cdelta->init(*overlap_delta_table, delta_rels, true); - + { src_copying_mapper * cpmapper = alloc(src_copying_mapper, *cdelta, src); scoped_ptr mapping_fn = rmgr.mk_map_fn(*src_only2, cpmapper); @@ -1061,11 +1059,11 @@ namespace datalog { m_offset_mapper_obj->m_ofs = src_rel_offset; (*m_offset_mapper_fun)(*offsetted_src); - + //if we need to generate a delta, we get collect it into an empty relation and then union //it with the delta passed in as argument. scoped_rel loc_delta = delta ? get(plugin.mk_empty(*delta)) : 0; - //even if we don't need to generate the delta for the caller, we still want to have a delta + //even if we don't need to generate the delta for the caller, we still want to have a delta //table to know which relations to copy. scoped_rel loc_delta_table_scoped; if(!loc_delta) { @@ -1131,7 +1129,7 @@ namespace datalog { scoped_ptr m_rel_filter; scoped_ptr m_tr_filter; public: - filter_identical_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * identical_cols) + filter_identical_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * identical_cols) : m_table_filter(nullptr), m_rel_filter(nullptr), m_tr_filter(nullptr) { finite_product_relation_plugin & plugin = r.get_plugin(); for(unsigned i=0; i1) { - m_table_filter = r.get_manager().mk_filter_identical_fn(r.get_table(), m_table_cols.size(), + m_table_filter = r.get_manager().mk_filter_identical_fn(r.get_table(), m_table_cols.size(), m_table_cols.c_ptr()); SASSERT(m_table_filter); } @@ -1190,7 +1188,7 @@ namespace datalog { } }; - relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_fn(const relation_base & rb, + relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_fn(const relation_base & rb, unsigned col_cnt, const unsigned * identical_cols) { if(&rb.get_plugin()!=this) { return nullptr; @@ -1236,7 +1234,7 @@ namespace datalog { }; - relation_mutator_fn * finite_product_relation_plugin::mk_filter_equal_fn(const relation_base & rb, + relation_mutator_fn * finite_product_relation_plugin::mk_filter_equal_fn(const relation_base & rb, const relation_element & value, unsigned col) { if(&rb.get_plugin()!=this) { return nullptr; @@ -1256,7 +1254,7 @@ namespace datalog { idx_set m_table_cond_columns; idx_set m_rel_cond_columns; - //like m_table_cond_columns and m_rel_cond_columns, only the indexes are local to the + //like m_table_cond_columns and m_rel_cond_columns, only the indexes are local to the //table/relation, not to the signature of the whole relation idx_set m_table_local_cond_columns; idx_set m_rel_local_cond_columns; @@ -1279,14 +1277,14 @@ namespace datalog { \brief Renaming that transforms the variable numbers pointing to the global relation into variables that point to the inner relation variables. - The elements that do not correspond to columns of the inner relation (but rather to the table - columns) is modified in \c operator() when evaluating the condition for all the relevant + The elements that do not correspond to columns of the inner relation (but rather to the table + columns) is modified in \c operator() when evaluating the condition for all the relevant combinations of table values. */ expr_ref_vector m_renaming_for_inner_rel; public: filter_interpreted_fn(const finite_product_relation & r, app * condition) - : m_manager(r.get_context().get_manager()), + : m_manager(r.get_context().get_manager()), m_subst(r.get_context().get_var_subst()), m_cond(condition, m_manager), m_renaming_for_inner_rel(m_manager) { @@ -1319,7 +1317,7 @@ namespace datalog { get_renaming_args(r.m_sig2other, r.get_signature(), m_renaming_for_inner_rel); if(!m_table_cond_columns.empty()) { - //We will keep the table variables that appear in the condition together + //We will keep the table variables that appear in the condition together //with the index column and then iterate through the tuples, evaluating //the rest of the condition on the inner relations. unsigned_vector removed_cols; @@ -1346,7 +1344,7 @@ namespace datalog { const relation_signature & osig = r.get_signature(); relation_manager & rmgr = r.get_manager(); unsigned rsig_sz = r.get_signature().size(); - + if(m_rel_cond_columns.empty()) { SASSERT(m_table_filter); (*m_table_filter)(rtable); @@ -1382,7 +1380,7 @@ namespace datalog { } unsigned projected_data_cols = tproj->get_signature().size()-1; SASSERT(m_table_cond_columns.num_elems()==projected_data_cols); - + table_signature filtered_sig = tproj->get_signature(); filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); filtered_sig.set_functional_columns(1); @@ -1417,10 +1415,10 @@ namespace datalog { } relation_base * new_rel = old_rel.clone(); - + scoped_ptr filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond)); (*filter)(*new_rel); - + if(new_rel->empty()) { new_rel->deallocate(); continue; @@ -1440,7 +1438,7 @@ namespace datalog { } } - m_assembling_join_project = mk_assembler_of_filter_result(rtable, *filtered_table, + m_assembling_join_project = mk_assembler_of_filter_result(rtable, *filtered_table, table_cond_columns_vect); } @@ -1450,7 +1448,7 @@ namespace datalog { } }; - relation_mutator_fn * finite_product_relation_plugin::mk_filter_interpreted_fn(const relation_base & rb, + relation_mutator_fn * finite_product_relation_plugin::mk_filter_interpreted_fn(const relation_base & rb, app * condition) { if(&rb.get_plugin()!=this) { return nullptr; @@ -1481,7 +1479,7 @@ namespace datalog { unsigned_vector m_r_shared_rel_cols; unsigned_vector m_neg_shared_rel_cols; public: - negation_filter_fn(const finite_product_relation & r, const finite_product_relation & neg, + negation_filter_fn(const finite_product_relation & r, const finite_product_relation & neg, unsigned joined_col_cnt, const unsigned * r_cols, const unsigned * neg_cols) : m_r_cols(joined_col_cnt, r_cols), m_neg_cols(joined_col_cnt, neg_cols), @@ -1500,7 +1498,7 @@ namespace datalog { } } if(m_table_overlaps_only) { - m_table_neg_filter = rmgr.mk_filter_by_negation_fn(rtable, neg.get_table(), + m_table_neg_filter = rmgr.mk_filter_by_negation_fn(rtable, neg.get_table(), m_r_shared_table_cols, m_neg_shared_table_cols); SASSERT(m_table_neg_filter); } @@ -1515,7 +1513,7 @@ namespace datalog { removed_cols.reset(); //remove the second copy of table data columns add_sequence(tsig.size()-1, tsig.size()-1, removed_cols); - m_table_intersection_join = rmgr.mk_join_project_fn(rtable, rtable, data_cols, data_cols, + m_table_intersection_join = rmgr.mk_join_project_fn(rtable, rtable, data_cols, data_cols, removed_cols); SASSERT(m_table_intersection_join); @@ -1535,7 +1533,7 @@ namespace datalog { finite_product_relation & m_r; const finite_product_relation & m_inters; //intersection of the relation and the negated one public: - rel_subtractor(negation_filter_fn & parent, finite_product_relation & r, + rel_subtractor(negation_filter_fn & parent, finite_product_relation & r, const finite_product_relation & inters) : m_parent(parent), m_r(r), m_inters(inters) {} @@ -1546,7 +1544,7 @@ namespace datalog { if(!m_parent.m_inner_subtract) { unsigned_vector all_rel_cols; add_sequence(0, r_inner->get_signature().size() , all_rel_cols); - m_parent.m_inner_subtract = m_r.get_manager().mk_filter_by_negation_fn(*r_inner, + m_parent.m_inner_subtract = m_r.get_manager().mk_filter_by_negation_fn(*r_inner, inters_inner, all_rel_cols, all_rel_cols); } (*m_parent.m_inner_subtract)(*r_inner, inters_inner); @@ -1579,17 +1577,17 @@ namespace datalog { relation_manager & rmgr = r.get_manager(); //we need to do this before we perform the \c m_table_subtract - //the sigrature of the \c table_overlap0 relation is + //the sigrature of the \c table_overlap0 relation is //(data_columns)(original rel idx)(subtracted rel idx) - scoped_rel table_overlap0 = (*m_table_intersection_join)(r_table, + scoped_rel table_overlap0 = (*m_table_intersection_join)(r_table, intersection->get_table()); - + //the rows that don't appear in the table of the intersection are safe to stay (*m_table_subtract)(r_table, intersection->get_table()); - + //now we will examine the rows that do appear in the intersection - //There are no functional columns in the \c table_overlap0 relation (because of + //There are no functional columns in the \c table_overlap0 relation (because of //the project we did). We need to make both rel idx columns functional. //We do not lose any rows, since the data columns by themselves are unique. @@ -1613,7 +1611,7 @@ namespace datalog { unsigned removed_col = table_overlap->get_signature().size()-1; m_overlap_table_last_column_remover = rmgr.mk_project_fn(*table_overlap, 1, &removed_col); } - scoped_rel final_overlapping_rows_table = + scoped_rel final_overlapping_rows_table = (*m_overlap_table_last_column_remover)(*table_overlap); if(!m_r_table_union) { @@ -1624,13 +1622,13 @@ namespace datalog { } }; - relation_intersection_filter_fn * finite_product_relation_plugin::mk_filter_by_negation_fn(const relation_base & rb, - const relation_base & negb, unsigned joined_col_cnt, + relation_intersection_filter_fn * finite_product_relation_plugin::mk_filter_by_negation_fn(const relation_base & rb, + const relation_base & negb, unsigned joined_col_cnt, const unsigned * r_cols, const unsigned * negated_cols) { if(&rb.get_plugin()!=this || &negb.get_plugin()!=this) { return nullptr; } - + return alloc(negation_filter_fn, get(rb), get(negb), joined_col_cnt, r_cols, negated_cols); } @@ -1644,7 +1642,7 @@ namespace datalog { scoped_ptr m_assembling_join_project; scoped_ptr m_updating_union; public: - filter_identical_pairs_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * table_cols, + filter_identical_pairs_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * table_cols, const unsigned * rel_cols) : m_col_cnt(col_cnt), m_table_cols(col_cnt, table_cols), @@ -1683,7 +1681,7 @@ namespace datalog { tproj = r.get_table().clone(); } SASSERT(m_col_cnt+1==tproj->get_signature().size()); - + table_signature filtered_sig = tproj->get_signature(); filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); filtered_sig.set_functional_columns(1); @@ -1727,12 +1725,12 @@ namespace datalog { } }; - relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_pairs(const finite_product_relation & r, + relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_pairs(const finite_product_relation & r, unsigned col_cnt, const unsigned * table_cols, const unsigned * rel_cols) { return alloc(filter_identical_pairs_fn, r, col_cnt, table_cols, rel_cols); } - table_join_fn * finite_product_relation_plugin::mk_assembler_of_filter_result(const table_base & relation_table, + table_join_fn * finite_product_relation_plugin::mk_assembler_of_filter_result(const table_base & relation_table, const table_base & filtered_table, const unsigned_vector & selected_columns) { table_plugin & tplugin = relation_table.get_plugin(); @@ -1762,7 +1760,7 @@ namespace datalog { removed_cols.push_back(idx_ofs); //unfiltered relation indexes from 'filtered' removed_cols.push_back(idx_ofs+1); //unfiltered relation indexes from rtable - table_join_fn * res = tplugin.get_manager().mk_join_project_fn(relation_table, filtered_table, + table_join_fn * res = tplugin.get_manager().mk_join_project_fn(relation_table, filtered_table, rtable_joined_cols, filtered_joined_cols, removed_cols); SASSERT(res); return res; @@ -1774,10 +1772,10 @@ namespace datalog { // // ----------------------------------- - finite_product_relation::finite_product_relation(finite_product_relation_plugin & p, + finite_product_relation::finite_product_relation(finite_product_relation_plugin & p, const relation_signature & s, const bool * table_columns, table_plugin & tplugin, relation_plugin & oplugin, family_id other_kind) - : relation_base(p, s), + : relation_base(p, s), m_other_plugin(oplugin), m_other_kind(other_kind), m_full_rel_idx(UINT_MAX) { @@ -1811,7 +1809,7 @@ namespace datalog { } finite_product_relation::finite_product_relation(const finite_product_relation & r) - : relation_base(r), + : relation_base(r), m_table_sig(r.m_table_sig), m_table2sig(r.m_table2sig), m_sig2table(r.m_sig2table), @@ -1860,7 +1858,7 @@ namespace datalog { relation_base::swap(r0); } - finite_product_relation::~finite_product_relation() { + finite_product_relation::~finite_product_relation() { m_table->deallocate(); relation_vector::iterator it = m_others.begin(); relation_vector::iterator end = m_others.end(); @@ -2028,7 +2026,7 @@ namespace datalog { } table_element full_rel_idx = get_full_rel_idx(); scoped_rel complement_table = m_table->complement(p, &full_rel_idx); - + scoped_ptr u_fn = get_manager().mk_union_fn(*m_table, *complement_table, nullptr); SASSERT(u_fn); (*u_fn)(*m_table, *complement_table, nullptr); @@ -2204,7 +2202,7 @@ namespace datalog { } //remove also the last column with inner relation index to_project_away.push_back(get_table().get_signature().size()-1); - + if(new_rel_columns.empty()) { //the specifications are the same return true; @@ -2220,15 +2218,15 @@ namespace datalog { scoped_ptr pr_fun = get_manager().mk_project_fn(get_table(), to_project_away); table_base * moved_cols_table = (*pr_fun)(get_table()); //gets destroyed inside moved_cols_trel - scoped_rel moved_cols_trel = + scoped_rel moved_cols_trel = rmgr.get_table_relation_plugin(moved_cols_table->get_plugin()).mk_from_table(moved_cols_sig, moved_cols_table); svector moved_cols_table_flags(moved_cols_sig.size(), false); - scoped_rel moved_cols_rel = get_plugin().mk_empty(moved_cols_sig, + scoped_rel moved_cols_rel = get_plugin().mk_empty(moved_cols_sig, moved_cols_table_flags.c_ptr()); - scoped_ptr union_fun = + scoped_ptr union_fun = get_manager().mk_union_fn(*moved_cols_rel, *moved_cols_trel); SASSERT(union_fun); //the table_relation should be able to be 'unioned into' any relation @@ -2271,7 +2269,7 @@ namespace datalog { //Swap the content of the current object and new_rel. On exitting the function new_rel will be destroyed //since it points to the content of scoped_rel unordered_rel. swap(new_rel); - + return true; } @@ -2371,8 +2369,7 @@ namespace datalog { conjs.push_back(tmp); disjs.push_back(m.mk_and(conjs.size(), conjs.c_ptr())); } - bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml); + bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml); } }; - diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 8323f96dd..94a9a1537 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -53,7 +53,7 @@ static void display_statistics( datalog::instruction_block& code, datalog::execution_context& ex_ctx, bool verbose - ) + ) { std::lock_guard lock(*display_stats_mux); g_piece_timer.stop(); @@ -67,11 +67,11 @@ static void display_statistics( p.set_uint("profile_milliseconds_threshold", 100); ctx.updt_params(p); - IF_VERBOSE(2, + IF_VERBOSE(2, out << "--------------\n"; out << "original rules\n"; orig_rules.display(out); - + out << "---------------\n"; out << "generated rules\n"; ctx.display_rules(out); @@ -79,12 +79,12 @@ static void display_statistics( out << "--------------\n"; out << "instructions \n"; code.display(ex_ctx, out); - + out << "--------------\n"; out << "big relations \n"; ex_ctx.report_big_relations(1000, out);); } - IF_VERBOSE(2, + IF_VERBOSE(2, out << "--------------\n"; out << "relation sizes\n"; ctx.get_rel_context()->get_rmanager().display_relation_sizes(out);); @@ -132,9 +132,8 @@ unsigned read_datalog(char const * file) { datalog::context ctx(m, re, s_params, params); datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager(); datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable")); - SASSERT(&inner_plg); rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr)); - + g_piece_timer.reset(); g_piece_timer.start(); @@ -178,26 +177,26 @@ unsigned read_datalog(char const * file) { g_code = &rules_code; g_ectx = &ex_ctx; - try { + try { g_piece_timer.reset(); g_piece_timer.start(); - + bool early_termination; - unsigned timeout = ctx.initial_restart_timeout(); + unsigned timeout = ctx.initial_restart_timeout(); if (timeout == 0) { timeout = UINT_MAX; } do { ctx.get_rel_context()->transform_rules(); - + datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); - + TRACE("dl_compiler", rules_code.display(ex_ctx, tout);); - + rules_code.make_annotations(ex_ctx); - + ex_ctx.set_timelimit(timeout); - + early_termination = !rules_code.perform(ex_ctx); if(early_termination) { IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream());); @@ -208,10 +207,10 @@ unsigned read_datalog(char const * file) { ex_ctx.reset_timelimit(); TRUSTME( termination_code.perform(ex_ctx) ); ctx.saturation_was_run(); - + if (early_termination) { IF_VERBOSE(1, verbose_stream() << "restarting saturation\n";); - + uint64_t new_timeout = static_cast(timeout)*ctx.initial_restart_timeout(); if(new_timeout>UINT_MAX) { timeout=UINT_MAX; @@ -219,7 +218,7 @@ unsigned read_datalog(char const * file) { else { timeout=static_cast(new_timeout); } - + rules_code.process_all_costs(); rules_code.reset(); termination_code.reset(); @@ -229,29 +228,29 @@ unsigned read_datalog(char const * file) { ctx.close(); } } while (early_termination); - + TRACE("dl_compiler", ctx.display(tout); rules_code.display(ex_ctx, tout);); - + if (ctx.output_tuples()) { ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout); } display_statistics( std::cout, ctx, - original_rules, + original_rules, rules_code, ex_ctx, false); } catch (const out_of_memory_error &) { - std::cout << "\n\nOUT OF MEMORY!\n\n"; + std::cout << "\n\nOUT OF MEMORY!\n\n"; display_statistics( std::cout, ctx, - original_rules, + original_rules, rules_code, ex_ctx, true); @@ -259,4 +258,3 @@ unsigned read_datalog(char const * file) { } return 0; } -