mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Fix compiler warnings

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2019-10-24 12:34:32 +01:00
parent 823bf317c5
commit efa3c0f68e
No known key found for this signature in database
GPG key ID: BCF6360F86294467
4 changed files with 208 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/for_each_expr.cpp
View file

@ -45,7 +45,7 @@ unsigned get_num_exprs(expr * n) {
} }
namespace has_skolem_functions_ns { namespace has_skolem_functions_ns {
struct found {}; struct found {};
struct proc { struct proc {
void operator()(var * n) const {} void operator()(var * n) const {}
void operator()(app const * n) const { if (n->get_decl()->is_skolem() && n->get_num_args() > 0) throw found(); } 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; break;
} }
} }
} }
subterms_postorder::iterator& subterms_postorder::iterator::operator++() { subterms_postorder::iterator& subterms_postorder::iterator::operator++() {
expr* e = m_es.back();
next(); next();
return *this; return *this;
} }
@ -172,4 +171,3 @@ bool subterms_postorder::iterator::operator==(iterator const& other) const {
bool subterms_postorder::iterator::operator!=(iterator const& other) const { bool subterms_postorder::iterator::operator!=(iterator const& other) const {
return !(*this == other); return !(*this == other);
} }

197
src/muz/rel/dl_base.h
View file

@ -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. 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) { const unsigned * cols1, const unsigned * cols2, signature & result) {
result.reset(); result.reset();
@ -137,14 +137,14 @@ namespace datalog {
The array of removed columns must be sorted in ascending order. 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) { const unsigned * removed_cols, signature & result) {
result = src; result = src;
project_out_vector_columns(result, col_cnt, removed_cols); project_out_vector_columns(result, col_cnt, removed_cols);
} }
static void from_join_project(const signature & s1, const signature & s2, unsigned joined_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 * cols1, const unsigned * cols2, unsigned removed_col_cnt,
const unsigned * removed_cols, signature & result) { const unsigned * removed_cols, signature & result) {
signature aux(s1); signature aux(s1);
from_join(s1, s2, joined_col_cnt, cols1, cols2, aux); 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 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) { const unsigned * permutation_cycle, signature & result) {
SASSERT(cycle_len>=2); SASSERT(cycle_len>=2);
result=src; result=src;
@ -167,7 +167,7 @@ namespace datalog {
/** /**
\brief Into \c result assign signature \c src with reordered columns. \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) { const unsigned * permutation, signature & result) {
result.reset(); result.reset();
unsigned n = src.size(); unsigned n = src.size();
@ -211,11 +211,11 @@ namespace datalog {
combination. combination.
- supports_attachment - 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. constraints to relations of the kind of the relation.
- attach - attach
is used to associate downstream clients. is used to associate downstream clients.
It assumes that the relation kind is supported (supports_kind returns true) It assumes that the relation kind is supported (supports_kind returns true)
*/ */
class mutator_fn : public base_fn { class mutator_fn : public base_fn {
@ -256,7 +256,7 @@ namespace datalog {
symbol m_name; symbol m_name;
relation_manager & m_manager; relation_manager & m_manager;
protected: 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) {} : 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 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 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 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, 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; } 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; } const unsigned * removed_cols) { return nullptr; }
virtual join_fn * mk_join_project_fn(const base_object & t1, const base_object & t2, 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; } 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; } const unsigned * permutation_cycle) { return nullptr; }
virtual transformer_fn * mk_permutation_rename_fn(const base_object & t, virtual transformer_fn * mk_permutation_rename_fn(const base_object & t,
const unsigned * permutation) { return nullptr; } const unsigned * permutation) { return nullptr; }
public: 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; } const base_object * delta) { return nullptr; }
protected: 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; } 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; } 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; } unsigned col) { return nullptr; }
virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition) 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) app * condition, unsigned removed_col_cnt, const unsigned * removed_cols)
{ return nullptr; } { 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; } const element & value, unsigned col) { return nullptr; }
virtual intersection_filter_fn * mk_filter_by_intersection_fn(const base_object & t, virtual intersection_filter_fn * mk_filter_by_intersection_fn(const base_object & t,
const base_object & src, unsigned joined_col_cnt, const base_object & src, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * src_cols) const unsigned * t_cols, const unsigned * src_cols)
{ return nullptr; } { return nullptr; }
virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t, virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t,
const base_object & negated_obj, unsigned joined_col_cnt, const base_object & negated_obj, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * negated_cols) const unsigned * t_cols, const unsigned * negated_cols)
{ return nullptr; } { return nullptr; }
virtual intersection_join_filter_fn * mk_filter_by_negated_join_fn( virtual intersection_join_filter_fn * mk_filter_by_negated_join_fn(
const base_object & t, const base_object & t,
const base_object & src1, const base_object & src1,
const base_object & src2, const base_object & src2,
unsigned_vector const& t_cols, unsigned_vector const& t_cols,
unsigned_vector const& src_cols, unsigned_vector const& src_cols,
unsigned_vector const& src1_cols, unsigned_vector const& src1_cols,
unsigned_vector const& src2_cols) unsigned_vector const& src2_cols)
{ return nullptr; } { return nullptr; }
}; };
@ -405,8 +405,8 @@ namespace datalog {
sort_ref m_leak_guard; sort_ref m_leak_guard;
#endif #endif
protected: protected:
base_ancestor(plugin & p, const signature & s) base_ancestor(plugin & p, const signature & s)
: m_plugin(p), m_signature(s), m_kind(p.get_kind()) : m_plugin(p), m_signature(s), m_kind(p.get_kind())
#if DL_LEAK_HUNTING #if DL_LEAK_HUNTING
, m_leak_guard(p.get_ast_manager().mk_fresh_sort(p.get_name().bare_str()), p.get_ast_manager()) , m_leak_guard(p.get_ast_manager().mk_fresh_sort(p.get_name().bare_str()), p.get_ast_manager())
#endif #endif
@ -417,11 +417,11 @@ namespace datalog {
} }
#if DL_LEAK_HUNTING #if DL_LEAK_HUNTING
base_ancestor(const base_ancestor & o) base_ancestor(const base_ancestor & o)
: m_plugin(o.m_plugin), : m_plugin(o.m_plugin),
m_signature(o.m_signature), m_signature(o.m_signature),
m_kind(o.m_kind), 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()) { m_plugin.get_ast_manager()) {
leak_guard_check(m_leak_guard->get_name()); 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. Since the destructor is protected, we cannot use the \c dealloc macro.
*/ */
void destroy() { void destroy() {
SASSERT(this); SASSERT(this != nullptr);
this->~base_ancestor(); this->~base_ancestor();
memory::deallocate(this); memory::deallocate(this);
} }
@ -445,15 +445,15 @@ namespace datalog {
Pointers and references to the current object become invalid after a call to this function. Pointers and references to the current object become invalid after a call to this function.
*/ */
virtual void deallocate() { virtual void deallocate() {
destroy(); destroy();
} }
/** /**
It must hold that operations created for particular table/relation are able to operate on 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 tables/relations of the same signature and kind. In most cases it is sufficient to use the kind
of the plugin object. 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. allocate different kind numbers to the tables is creates.
*/ */
family_id get_kind() const { return m_kind; } family_id get_kind() const { return m_kind; }
@ -464,7 +464,7 @@ namespace datalog {
virtual bool empty() const = 0; virtual bool empty() const = 0;
/** /**
\brief fast emptiness check. This may be partial. \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. then the table or relation is in fact empty.
It is allowed to return false even if the relation is 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 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); std::swap(m_kind, o.m_kind);
#if DL_LEAK_HUNTING #if DL_LEAK_HUNTING
m_leak_guard = get_plugin().get_ast_manager().mk_fresh_sort(get_plugin().get_name().bare_str()); 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; unsigned_vector m_cols2;
convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt, convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2) const unsigned * cols1, const unsigned * cols2)
: m_cols1(col_cnt, cols1), : m_cols1(col_cnt, cols1),
m_cols2(col_cnt, cols2) { m_cols2(col_cnt, cols2) {
signature::from_join(o1_sig, o2_sig, col_cnt, cols1, cols2, m_result_sig); 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 //it is non-const because it needs to be modified in sparse_table version of the join_project operator
unsigned_vector m_removed_cols; unsigned_vector m_removed_cols;
convenient_join_project_fn(const signature & o1_sig, const signature & o2_sig, convenient_join_project_fn(const signature & o1_sig, const signature & o2_sig,
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) unsigned removed_col_cnt, const unsigned * removed_cols)
: m_cols1(joined_col_cnt, cols1), : m_cols1(joined_col_cnt, cols1),
m_cols2(joined_col_cnt, cols2), m_cols2(joined_col_cnt, cols2),
m_removed_cols(removed_col_cnt, removed_cols) { 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); removed_col_cnt, removed_cols, m_result_sig);
} }
@ -557,9 +557,9 @@ namespace datalog {
protected: protected:
unsigned_vector m_removed_cols; 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) { : 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()); convenient_transformer_fn::get_result_signature());
} }
}; };
@ -569,9 +569,9 @@ namespace datalog {
const unsigned_vector m_cycle; const unsigned_vector m_cycle;
convenient_rename_fn(const signature & orig_sig, unsigned cycle_len, convenient_rename_fn(const signature & orig_sig, unsigned cycle_len,
const unsigned * permutation_cycle) const unsigned * permutation_cycle)
: m_cycle(cycle_len, 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()); convenient_transformer_fn::get_result_signature());
} }
}; };
@ -585,9 +585,9 @@ namespace datalog {
bool m_overlap; //one column in negated table is bound multiple times bool m_overlap; //one column in negated table is bound multiple times
svector<bool> m_bound; svector<bool> m_bound;
convenient_negation_filter_fn(const base_object & tgt, const base_object & neg_t, 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) 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_joined_col_cnt(joined_col_cnt), m_cols1(joined_col_cnt, t_cols),
m_cols2(joined_col_cnt, negated_cols) { m_cols2(joined_col_cnt, negated_cols) {
unsigned neg_sig_size = neg_t.get_signature().size(); unsigned neg_sig_size = neg_t.get_signature().size();
m_overlap = false; m_overlap = false;
@ -598,12 +598,12 @@ namespace datalog {
} }
m_bound[negated_cols[i]]=true; 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(); 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. be assigned two different values, return false; otherwise return true.
Each negative column must correspond to exactly column in the first table. Each negative column must correspond to exactly column in the first table.
@ -651,7 +651,7 @@ namespace datalog {
bool m_renamers_initialized; bool m_renamers_initialized;
renamer_vector m_renamers; renamer_vector m_renamers;
public: 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_permutation(o.get_signature().size(), permutation),
m_renamers_initialized(false) {} m_renamers_initialized(false) {}
@ -755,7 +755,7 @@ namespace datalog {
void output(ast_manager & m, std::ostream & out) const; void output(ast_manager & m, std::ostream & out) const;
struct hash { struct hash {
unsigned operator()(relation_signature const& s) const { unsigned operator()(relation_signature const& s) const {
return obj_vector_hash<relation_signature>(s); return obj_vector_hash<relation_signature>(s);
} }
}; };
@ -779,8 +779,8 @@ namespace datalog {
private: private:
special_relation_type m_special_type; special_relation_type m_special_type;
protected: protected:
relation_plugin(symbol const& name, relation_manager & manager, relation_plugin(symbol const& name, relation_manager & manager,
special_relation_type special_type = ST_ORDINARY) special_relation_type special_type = ST_ORDINARY)
: plugin_object(name, manager), : plugin_object(name, manager),
m_special_type(special_type) {} m_special_type(special_type) {}
public: public:
@ -801,7 +801,7 @@ namespace datalog {
class relation_base : public relation_infrastructure::base_ancestor { class relation_base : public relation_infrastructure::base_ancestor {
protected: protected:
relation_base(relation_plugin & plugin, const relation_signature & s) relation_base(relation_plugin & plugin, const relation_signature & s)
: base_ancestor(plugin, s) {} : base_ancestor(plugin, s) {}
~relation_base() override {} ~relation_base() override {}
public: public:
@ -827,7 +827,7 @@ namespace datalog {
// table_base // table_base
// //
// ----------------------------------- // -----------------------------------
class table_signature; class table_signature;
class table_plugin; class table_plugin;
class table_base; class table_base;
@ -873,11 +873,11 @@ namespace datalog {
public: public:
virtual ~table_row_mutator_fn() {} virtual ~table_row_mutator_fn() {}
/** /**
\brief The function is called for a particular table row. The \c func_columns contains \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 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. 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. the same functional column values.
*/ */
virtual bool operator()(table_element * func_columns) = 0; virtual bool operator()(table_element * func_columns) = 0;
@ -888,7 +888,7 @@ namespace datalog {
virtual ~table_row_pair_reduce_fn() {} virtual ~table_row_pair_reduce_fn() {}
/** /**
\brief The function is called for pair of table rows that became duplicit due to projection. \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. resulting row.
It is assumed that the function is idempotent: when the two functional sub-tuples are equal, 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 { class table_signature : public table_infrastructure::signature_base {
public: public:
struct hash { struct hash {
unsigned operator()(table_signature const& s) const { unsigned operator()(table_signature const& s) const {
return svector_hash<table_sort_hash>()(s); return svector_hash<table_sort_hash>()(s);
} }
}; };
@ -915,7 +915,7 @@ namespace datalog {
unsigned m_functional_columns; unsigned m_functional_columns;
public: public:
table_signature() : m_functional_columns(0) {} table_signature() : m_functional_columns(0) {}
void swap(table_signature & s) { void swap(table_signature & s) {
signature_base::swap(s); signature_base::swap(s);
std::swap(m_functional_columns, s.m_functional_columns); 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; } 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. are no functional columns.
*/ */
unsigned first_functional() const { return size()-m_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 \brief Into \c result assign signature of result of join of relations with signatures \c s1
and \c s2. The result is and \c s2. The result is
(non-functional of s1)(non-functional of s2)(functional of s1)(functional of s2) (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); const unsigned * cols1, const unsigned * cols2, table_signature & result);
static void from_join_project(const table_signature & s1, const table_signature & s2, 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, unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
const unsigned * removed_cols, table_signature & result); 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. 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); 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); const unsigned * removed_cols, table_signature & result);
/** /**
@ -983,7 +983,7 @@ namespace datalog {
Permutations between functional and nonfunctional columns are not allowed. 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) { const unsigned * permutation_cycle, table_signature & result) {
signature_base::from_rename(src, cycle_len, permutation_cycle, result); signature_base::from_rename(src, cycle_len, permutation_cycle, result);
result.set_functional_columns(src.functional_columns()); result.set_functional_columns(src.functional_columns());
@ -998,10 +998,10 @@ namespace datalog {
/** /**
\brief Into \c result assign signature \c src with reordered columns. \brief Into \c result assign signature \c src with reordered columns.
Permutations mixing functional and nonfunctional columns are not allowed. 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) { const unsigned * permutation, table_signature & result) {
signature_base::from_permutation_rename(src, permutation, result); signature_base::from_permutation_rename(src, permutation, result);
result.set_functional_columns(src.functional_columns()); 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. If the returned value is non-zero, the returned object must take ownership of \c reducer.
Otherwise \c reducer must remain unmodified. 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; } const unsigned * removed_cols, table_row_pair_reduce_fn * reducer) { return nullptr; }
}; };
class table_base : public table_infrastructure::base_ancestor { class table_base : public table_infrastructure::base_ancestor {
protected: protected:
table_base(table_plugin & plugin, const table_signature & s) table_base(table_plugin & plugin, const table_signature & s)
: base_ancestor(plugin, s) {} : base_ancestor(plugin, s) {}
~table_base() override {} ~table_base() override {}
public: public:
@ -1057,15 +1057,15 @@ namespace datalog {
bool contains_fact(const table_fact & f) const override; 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, \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 add it and return true. Otherwise update \c f, so that the values of functional
columns correspond to the ones present in the table. columns correspond to the ones present in the table.
*/ */
virtual bool suggest_fact(table_fact & f); virtual bool suggest_fact(table_fact & f);
/** /**
\brief If \c f (i.e. its non-functional part) is not present in the table, \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 return false. Otherwise update \c f, so that the values of functional
columns correspond to the ones present in the table and return true. columns correspond to the ones present in the table and return true.
*/ */
virtual bool fetch_fact(table_fact & f) const; virtual bool fetch_fact(table_fact & f) const;
@ -1075,7 +1075,7 @@ namespace datalog {
*/ */
virtual void ensure_fact(const table_fact & f); 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()); SASSERT(fact.size() == get_signature().size());
remove_fact(fact.c_ptr()); } remove_fact(fact.c_ptr()); }
@ -1105,7 +1105,7 @@ namespace datalog {
virtual ~iterator_core() {} virtual ~iterator_core() {}
void inc_ref() { m_ref_cnt++; } void inc_ref() { m_ref_cnt++; }
void dec_ref() { void dec_ref() {
SASSERT(m_ref_cnt>0); SASSERT(m_ref_cnt>0);
m_ref_cnt--; m_ref_cnt--;
if(m_ref_cnt==0) { if(m_ref_cnt==0) {
@ -1118,7 +1118,7 @@ namespace datalog {
virtual row_interface & operator*() = 0; virtual row_interface & operator*() = 0;
virtual void operator++() = 0; virtual void operator++() = 0;
virtual bool operator==(const iterator_core & it) { 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 //the equality with the end() iterator
return is_finished() && it.is_finished(); return is_finished() && it.is_finished();
} }
@ -1135,7 +1135,7 @@ namespace datalog {
virtual ~row_iterator_core() {} virtual ~row_iterator_core() {}
void inc_ref() { m_ref_cnt++; } void inc_ref() { m_ref_cnt++; }
void dec_ref() { void dec_ref() {
SASSERT(m_ref_cnt>0); SASSERT(m_ref_cnt>0);
m_ref_cnt--; m_ref_cnt--;
if(m_ref_cnt==0) { if(m_ref_cnt==0) {
@ -1148,7 +1148,7 @@ namespace datalog {
virtual table_element operator*() = 0; virtual table_element operator*() = 0;
virtual void operator++() = 0; virtual void operator++() = 0;
virtual bool operator==(const row_iterator_core & it) { 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 //the equality with the end() iterator
return is_finished() && it.is_finished(); return is_finished() && it.is_finished();
} }
@ -1231,8 +1231,8 @@ namespace datalog {
mutable table_fact m_current; mutable table_fact m_current;
bool populated() const { return !m_current.empty(); } bool populated() const { return !m_current.empty(); }
void ensure_populated() const { void ensure_populated() const {
if(!populated()) { if(!populated()) {
get_fact(m_current); 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. //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. //inheritor classes cannot see it directly.
static iterator mk_iterator(iterator_core * core) { static iterator mk_iterator(iterator_core * core) {
return iterator(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. \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 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. 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); expr_ref_vector & renaming_arg);
}; };
#endif /* DL_BASE_H_ */ #endif /* DL_BASE_H_ */

175
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -68,7 +68,7 @@ namespace datalog {
return symbol(str.c_str()); 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) { relation_plugin & inner) {
finite_product_relation_plugin * res; finite_product_relation_plugin * res;
if(!rmgr.try_get_finite_product_relation_plugin(inner, res)) { if(!rmgr.try_get_finite_product_relation_plugin(inner, res)) {
@ -78,25 +78,25 @@ namespace datalog {
return *res; return *res;
} }
finite_product_relation_plugin::finite_product_relation_plugin(relation_plugin & inner_plugin, finite_product_relation_plugin::finite_product_relation_plugin(relation_plugin & inner_plugin,
relation_manager & manager) relation_manager & manager)
: relation_plugin(get_name(inner_plugin), manager, ST_FINITE_PRODUCT_RELATION), : relation_plugin(get_name(inner_plugin), manager, ST_FINITE_PRODUCT_RELATION),
m_inner_plugin(inner_plugin), m_spec_store(*this) { 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); relation_plugin::initialize(fid);
m_spec_store.add_available_kind(get_kind()); 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 bool * table_columns) {
const relation_signature & sig = r.get_signature(); const relation_signature & sig = r.get_signature();
svector<bool> table_cols_vect(sig.size(), table_columns); svector<bool> table_cols_vect(sig.size(), table_columns);
return m_spec_store.get_relation_kind(sig, rel_spec(table_cols_vect)); 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<bool> & table_columns) { const relation_signature & s, svector<bool> & table_columns) {
SASSERT(table_columns.empty()); SASSERT(table_columns.empty());
unsigned s_sz = s.size(); 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) { table_signature & table_sig, relation_signature & remaining_sig) {
relation_manager & rmgr = get_manager(); relation_manager & rmgr = get_manager();
unsigned n = s.size(); unsigned n = s.size();
@ -143,7 +143,7 @@ namespace datalog {
table_signature table_sig; table_signature table_sig;
relation_signature remaining_sig; relation_signature remaining_sig;
split_signatures(s, table_sig, 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); && get_manager().try_get_appropriate_plugin(table_sig);
} }
@ -175,7 +175,7 @@ namespace datalog {
return mk_empty(s, table_columns.c_ptr()); 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) { const bool * table_columns, family_id inner_kind) {
//find table_plugin that can handle the table signature //find table_plugin that can handle the table signature
table_signature table_sig; table_signature table_sig;
@ -221,7 +221,7 @@ namespace datalog {
const table_base & t = r.get_table(); const table_base & t = r.get_table();
unsigned removed_col = t.get_signature().size()-1; unsigned removed_col = t.get_signature().size()-1;
scoped_ptr<table_transformer_fn> project_fun = scoped_ptr<table_transformer_fn> project_fun =
get_manager().mk_project_fn(r.get_table(), 1, &removed_col); get_manager().mk_project_fn(r.get_table(), 1, &removed_col);
table_base * res_table = (*project_fun)(t); table_base * res_table = (*project_fun)(t);
@ -328,9 +328,9 @@ namespace datalog {
} }
public: public:
converting_join_fn(finite_product_relation_plugin & plugin, const relation_signature & sig1, converting_join_fn(finite_product_relation_plugin & plugin, const relation_signature & sig1,
const relation_signature & sig2, unsigned col_cnt, const unsigned * cols1, const relation_signature & sig2, unsigned col_cnt, const unsigned * cols1,
const unsigned * cols2) const unsigned * cols2)
: convenient_relation_join_fn(sig1, sig2, col_cnt, cols1, cols2), : convenient_relation_join_fn(sig1, sig2, col_cnt, cols1, cols2),
m_plugin(plugin) {} m_plugin(plugin) {}
@ -361,14 +361,14 @@ namespace datalog {
class finite_product_relation_plugin::join_fn : public convenient_relation_join_fn { class finite_product_relation_plugin::join_fn : public convenient_relation_join_fn {
scoped_ptr<table_join_fn> m_tjoin_fn; scoped_ptr<table_join_fn> m_tjoin_fn;
scoped_ptr<relation_join_fn> m_rjoin_fn; scoped_ptr<relation_join_fn> m_rjoin_fn;
unsigned_vector m_t_joined_cols1; unsigned_vector m_t_joined_cols1;
unsigned_vector m_t_joined_cols2; unsigned_vector m_t_joined_cols2;
unsigned_vector m_r_joined_cols1; unsigned_vector m_r_joined_cols1;
unsigned_vector m_r_joined_cols2; unsigned_vector m_r_joined_cols2;
//Column equalities betweet table and inner relations. //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 //in the result of the join operation
unsigned_vector m_tr_table_joined_cols; unsigned_vector m_tr_table_joined_cols;
unsigned_vector m_tr_rel_joined_cols; unsigned_vector m_tr_rel_joined_cols;
@ -394,8 +394,6 @@ namespace datalog {
bool operator()(table_element * func_columns) override { bool operator()(table_element * func_columns) override {
const relation_base & or1 = m_r1.get_inner_rel(func_columns[0]); const relation_base & or1 = m_r1.get_inner_rel(func_columns[0]);
const relation_base & or2 = m_r2.get_inner_rel(func_columns[1]); const relation_base & or2 = m_r2.get_inner_rel(func_columns[1]);
SASSERT(&or1);
SASSERT(&or2);
unsigned new_rel_num = m_rjoins.size(); unsigned new_rel_num = m_rjoins.size();
m_rjoins.push_back(m_parent.do_rjoin(or1, or2)); m_rjoins.push_back(m_parent.do_rjoin(or1, or2));
func_columns[0]=new_rel_num; 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, join_fn(const finite_product_relation & r1, const finite_product_relation & r2, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2) const unsigned * cols1, const unsigned * cols2)
: convenient_relation_join_fn(r1.get_signature(), r2.get_signature(), col_cnt, cols1, 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_table_after_join_ofs = r1.m_table2sig.size();
unsigned second_inner_rel_after_join_ofs = r1.m_other2sig.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_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()); m_t_joined_cols1.c_ptr(), m_t_joined_cols2.c_ptr());
SASSERT(m_tjoin_fn); SASSERT(m_tjoin_fn);
@ -442,7 +440,7 @@ namespace datalog {
} }
} }
relation_base * do_rjoin(const relation_base & r1, const relation_base & r2) { relation_base * do_rjoin(const relation_base & r1, const relation_base & r2) {
if(!m_rjoin_fn) { if(!m_rjoin_fn) {
m_rjoin_fn = r1.get_manager().mk_join_fn(r1, r2, m_r_joined_cols1, m_r_joined_cols2, false); 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 //to the table signature of the resulting relation
scoped_rel<table_base> res_table = (*m_tjoined_second_rel_remover)(*tjoined); scoped_rel<table_base> 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(); 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. //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 //determines which columns of the result are table columns and which are in the inner relation
svector<bool> m_res_table_columns; svector<bool> m_res_table_columns;
public: 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) { : convenient_relation_project_fn(r.get_signature(), col_cnt, removed_cols) {
SASSERT(col_cnt>0); SASSERT(col_cnt>0);
for(unsigned i=0; i<col_cnt; i++) { for(unsigned i=0; i<col_cnt; i++) {
@ -563,7 +561,7 @@ namespace datalog {
relation_vector & m_relations; relation_vector & m_relations;
public: public:
project_reducer(project_fn & parent, relation_vector & relations) project_reducer(project_fn & parent, relation_vector & relations)
: m_parent(parent), m_relations(relations) {} : m_parent(parent), m_relations(relations) {}
void operator()(table_element * func_columns, const table_element * merged_func_columns) override { void operator()(table_element * func_columns, const table_element * merged_func_columns) override {
@ -604,7 +602,7 @@ namespace datalog {
} }
else { else {
project_reducer * preducer = alloc(project_reducer, *this, res_relations); project_reducer * preducer = alloc(project_reducer, *this, res_relations);
scoped_ptr<table_transformer_fn> tproject = scoped_ptr<table_transformer_fn> tproject =
rmgr.mk_project_with_reduce_fn(rtable, m_removed_table_cols.size(), m_removed_table_cols.c_ptr(), preducer); rmgr.mk_project_with_reduce_fn(rtable, m_removed_table_cols.size(), m_removed_table_cols.c_ptr(), preducer);
res_table = (*tproject)(rtable); res_table = (*tproject)(rtable);
} }
@ -638,7 +636,7 @@ namespace datalog {
finite_product_relation * res = alloc(finite_product_relation, r.get_plugin(), get_result_signature(), 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); m_res_table_columns.c_ptr(), res_table->get_plugin(), *res_oplugin, null_family_id);
res->init(*res_table, res_relations, false); res->init(*res_table, res_relations, false);
if(!shared_res_table) { 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) { const unsigned * removed_cols) {
if(&rb.get_plugin()!=this) { if(&rb.get_plugin()!=this) {
return nullptr; return nullptr;
@ -669,7 +667,7 @@ namespace datalog {
//determines which columns of the result are table columns and which are in the inner relation //determines which columns of the result are table columns and which are in the inner relation
svector<bool> m_res_table_columns; svector<bool> m_res_table_columns;
public: 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) { : convenient_relation_rename_fn(r.get_signature(), cycle_len, permutation_cycle) {
SASSERT(cycle_len>1); 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) { unsigned permutation_cycle_len, const unsigned * permutation_cycle) {
if(&rb.get_plugin()!=this) { if(&rb.get_plugin()!=this) {
@ -789,11 +787,11 @@ namespace datalog {
If \c delta_indexes is 0, it means we are not collecting indexes. 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, union_mapper(union_fn & parent, finite_product_relation & tgt, const finite_product_relation & src,
table_base * delta_indexes, relation_vector * delta_rels) table_base * delta_indexes, relation_vector * delta_rels)
: m_parent(parent), : m_parent(parent),
m_tgt(tgt), m_tgt(tgt),
m_src(src), m_src(src),
m_delta_indexes(delta_indexes), m_delta_indexes(delta_indexes),
m_delta_rels(delta_rels) {} m_delta_rels(delta_rels) {}
~union_mapper() override {} ~union_mapper() override {}
@ -808,7 +806,7 @@ namespace datalog {
if(m_delta_indexes) { if(m_delta_indexes) {
relation_base * odelta = otgt->get_plugin().mk_empty(otgt->get_signature()); relation_base * odelta = otgt->get_plugin().mk_empty(otgt->get_signature());
m_parent.get_inner_rel_union_op(*otgt)(*otgt, osrc, odelta); m_parent.get_inner_rel_union_op(*otgt)(*otgt, osrc, odelta);
unsigned delta_idx = m_delta_rels->size(); unsigned delta_idx = m_delta_rels->size();
m_delta_rels->push_back(odelta); m_delta_rels->push_back(odelta);
m_di_fact.reset(); m_di_fact.reset();
@ -836,7 +834,7 @@ namespace datalog {
/** /**
If \c delta_indexes is 0, it means we are not collecting indexes. 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) {} : m_tgt(tgt), m_src(src) {}
bool operator()(table_element * func_columns) override { bool operator()(table_element * func_columns) override {
@ -857,7 +855,7 @@ namespace datalog {
scoped_rel<finite_product_relation> src_aux_copy; //copy of src in case its specification needs to be modified scoped_rel<finite_product_relation> 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)) ) { || (delta && !vectors_equal(tgt.m_table2sig, delta->m_table2sig)) ) {
src_aux_copy = src0.clone(); src_aux_copy = src0.clone();
ptr_vector<finite_product_relation> orig_rels; ptr_vector<finite_product_relation> orig_rels;
@ -880,7 +878,7 @@ namespace datalog {
for(unsigned i=0; i<data_cols_cnt; i++) { for(unsigned i=0; i<data_cols_cnt; i++) {
m_data_cols.push_back(i); m_data_cols.push_back(i);
} }
m_common_join = rmgr.mk_join_project_fn(tgt.get_table(), tgt.get_table(), m_data_cols, m_data_cols, m_common_join = rmgr.mk_join_project_fn(tgt.get_table(), tgt.get_table(), m_data_cols, m_data_cols,
m_data_cols); m_data_cols);
} }
@ -962,11 +960,11 @@ namespace datalog {
&table_fn_col, &first_col, 2, removed_cols); &table_fn_col, &first_col, 2, removed_cols);
} }
scoped_rel<table_base> overlap_delta_table = scoped_rel<table_base> overlap_delta_table =
(*m_overlap_delta_table_builder)(*regular_overlap, *delta_indexes); (*m_overlap_delta_table_builder)(*regular_overlap, *delta_indexes);
cdelta->init(*overlap_delta_table, delta_rels, true); cdelta->init(*overlap_delta_table, delta_rels, true);
{ {
src_copying_mapper * cpmapper = alloc(src_copying_mapper, *cdelta, src); src_copying_mapper * cpmapper = alloc(src_copying_mapper, *cdelta, src);
scoped_ptr<table_mutator_fn> mapping_fn = rmgr.mk_map_fn(*src_only2, cpmapper); scoped_ptr<table_mutator_fn> 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_obj->m_ofs = src_rel_offset;
(*m_offset_mapper_fun)(*offsetted_src); (*m_offset_mapper_fun)(*offsetted_src);
//if we need to generate a delta, we get collect it into an empty relation and then union //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. //it with the delta passed in as argument.
scoped_rel<finite_product_relation> loc_delta = delta ? get(plugin.mk_empty(*delta)) : 0; scoped_rel<finite_product_relation> 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. //table to know which relations to copy.
scoped_rel<table_base> loc_delta_table_scoped; scoped_rel<table_base> loc_delta_table_scoped;
if(!loc_delta) { if(!loc_delta) {
@ -1131,7 +1129,7 @@ namespace datalog {
scoped_ptr<relation_mutator_fn> m_rel_filter; scoped_ptr<relation_mutator_fn> m_rel_filter;
scoped_ptr<relation_mutator_fn> m_tr_filter; scoped_ptr<relation_mutator_fn> m_tr_filter;
public: 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) { : m_table_filter(nullptr), m_rel_filter(nullptr), m_tr_filter(nullptr) {
finite_product_relation_plugin & plugin = r.get_plugin(); finite_product_relation_plugin & plugin = r.get_plugin();
for(unsigned i=0; i<col_cnt; i++) { for(unsigned i=0; i<col_cnt; i++) {
@ -1144,7 +1142,7 @@ namespace datalog {
} }
} }
if(m_table_cols.size()>1) { if(m_table_cols.size()>1) {
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()); m_table_cols.c_ptr());
SASSERT(m_table_filter); 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) { unsigned col_cnt, const unsigned * identical_cols) {
if(&rb.get_plugin()!=this) { if(&rb.get_plugin()!=this) {
return nullptr; 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) { const relation_element & value, unsigned col) {
if(&rb.get_plugin()!=this) { if(&rb.get_plugin()!=this) {
return nullptr; return nullptr;
@ -1256,7 +1254,7 @@ namespace datalog {
idx_set m_table_cond_columns; idx_set m_table_cond_columns;
idx_set m_rel_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 //table/relation, not to the signature of the whole relation
idx_set m_table_local_cond_columns; idx_set m_table_local_cond_columns;
idx_set m_rel_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 \brief Renaming that transforms the variable numbers pointing to the global relation into
variables that point to the inner relation variables. 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 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 columns) is modified in \c operator() when evaluating the condition for all the relevant
combinations of table values. combinations of table values.
*/ */
expr_ref_vector m_renaming_for_inner_rel; expr_ref_vector m_renaming_for_inner_rel;
public: public:
filter_interpreted_fn(const finite_product_relation & r, app * condition) 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_subst(r.get_context().get_var_subst()),
m_cond(condition, m_manager), m_cond(condition, m_manager),
m_renaming_for_inner_rel(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); get_renaming_args(r.m_sig2other, r.get_signature(), m_renaming_for_inner_rel);
if(!m_table_cond_columns.empty()) { 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 //with the index column and then iterate through the tuples, evaluating
//the rest of the condition on the inner relations. //the rest of the condition on the inner relations.
unsigned_vector removed_cols; unsigned_vector removed_cols;
@ -1346,7 +1344,7 @@ namespace datalog {
const relation_signature & osig = r.get_signature(); const relation_signature & osig = r.get_signature();
relation_manager & rmgr = r.get_manager(); relation_manager & rmgr = r.get_manager();
unsigned rsig_sz = r.get_signature().size(); unsigned rsig_sz = r.get_signature().size();
if(m_rel_cond_columns.empty()) { if(m_rel_cond_columns.empty()) {
SASSERT(m_table_filter); SASSERT(m_table_filter);
(*m_table_filter)(rtable); (*m_table_filter)(rtable);
@ -1382,7 +1380,7 @@ namespace datalog {
} }
unsigned projected_data_cols = tproj->get_signature().size()-1; unsigned projected_data_cols = tproj->get_signature().size()-1;
SASSERT(m_table_cond_columns.num_elems()==projected_data_cols); SASSERT(m_table_cond_columns.num_elems()==projected_data_cols);
table_signature filtered_sig = tproj->get_signature(); table_signature filtered_sig = tproj->get_signature();
filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); filtered_sig.push_back(finite_product_relation::s_rel_idx_sort);
filtered_sig.set_functional_columns(1); filtered_sig.set_functional_columns(1);
@ -1417,10 +1415,10 @@ namespace datalog {
} }
relation_base * new_rel = old_rel.clone(); relation_base * new_rel = old_rel.clone();
scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond)); scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond));
(*filter)(*new_rel); (*filter)(*new_rel);
if(new_rel->empty()) { if(new_rel->empty()) {
new_rel->deallocate(); new_rel->deallocate();
continue; 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); 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) { app * condition) {
if(&rb.get_plugin()!=this) { if(&rb.get_plugin()!=this) {
return nullptr; return nullptr;
@ -1481,7 +1479,7 @@ namespace datalog {
unsigned_vector m_r_shared_rel_cols; unsigned_vector m_r_shared_rel_cols;
unsigned_vector m_neg_shared_rel_cols; unsigned_vector m_neg_shared_rel_cols;
public: 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) unsigned joined_col_cnt, const unsigned * r_cols, const unsigned * neg_cols)
: m_r_cols(joined_col_cnt, r_cols), : m_r_cols(joined_col_cnt, r_cols),
m_neg_cols(joined_col_cnt, neg_cols), m_neg_cols(joined_col_cnt, neg_cols),
@ -1500,7 +1498,7 @@ namespace datalog {
} }
} }
if(m_table_overlaps_only) { 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); m_r_shared_table_cols, m_neg_shared_table_cols);
SASSERT(m_table_neg_filter); SASSERT(m_table_neg_filter);
} }
@ -1515,7 +1513,7 @@ namespace datalog {
removed_cols.reset(); removed_cols.reset();
//remove the second copy of table data columns //remove the second copy of table data columns
add_sequence(tsig.size()-1, tsig.size()-1, removed_cols); 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); removed_cols);
SASSERT(m_table_intersection_join); SASSERT(m_table_intersection_join);
@ -1535,7 +1533,7 @@ namespace datalog {
finite_product_relation & m_r; finite_product_relation & m_r;
const finite_product_relation & m_inters; //intersection of the relation and the negated one const finite_product_relation & m_inters; //intersection of the relation and the negated one
public: 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) const finite_product_relation & inters)
: m_parent(parent), m_r(r), m_inters(inters) {} : m_parent(parent), m_r(r), m_inters(inters) {}
@ -1546,7 +1544,7 @@ namespace datalog {
if(!m_parent.m_inner_subtract) { if(!m_parent.m_inner_subtract) {
unsigned_vector all_rel_cols; unsigned_vector all_rel_cols;
add_sequence(0, r_inner->get_signature().size() , 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); inters_inner, all_rel_cols, all_rel_cols);
} }
(*m_parent.m_inner_subtract)(*r_inner, inters_inner); (*m_parent.m_inner_subtract)(*r_inner, inters_inner);
@ -1579,17 +1577,17 @@ namespace datalog {
relation_manager & rmgr = r.get_manager(); relation_manager & rmgr = r.get_manager();
//we need to do this before we perform the \c m_table_subtract //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) //(data_columns)(original rel idx)(subtracted rel idx)
scoped_rel<table_base> table_overlap0 = (*m_table_intersection_join)(r_table, scoped_rel<table_base> table_overlap0 = (*m_table_intersection_join)(r_table,
intersection->get_table()); intersection->get_table());
//the rows that don't appear in the table of the intersection are safe to stay //the rows that don't appear in the table of the intersection are safe to stay
(*m_table_subtract)(r_table, intersection->get_table()); (*m_table_subtract)(r_table, intersection->get_table());
//now we will examine the rows that do appear in the intersection //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. //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. //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; unsigned removed_col = table_overlap->get_signature().size()-1;
m_overlap_table_last_column_remover = rmgr.mk_project_fn(*table_overlap, 1, &removed_col); m_overlap_table_last_column_remover = rmgr.mk_project_fn(*table_overlap, 1, &removed_col);
} }
scoped_rel<table_base> final_overlapping_rows_table = scoped_rel<table_base> final_overlapping_rows_table =
(*m_overlap_table_last_column_remover)(*table_overlap); (*m_overlap_table_last_column_remover)(*table_overlap);
if(!m_r_table_union) { 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, 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 relation_base & negb, unsigned joined_col_cnt,
const unsigned * r_cols, const unsigned * negated_cols) { const unsigned * r_cols, const unsigned * negated_cols) {
if(&rb.get_plugin()!=this || &negb.get_plugin()!=this) { if(&rb.get_plugin()!=this || &negb.get_plugin()!=this) {
return nullptr; return nullptr;
} }
return alloc(negation_filter_fn, get(rb), get(negb), joined_col_cnt, r_cols, negated_cols); return alloc(negation_filter_fn, get(rb), get(negb), joined_col_cnt, r_cols, negated_cols);
} }
@ -1644,7 +1642,7 @@ namespace datalog {
scoped_ptr<table_join_fn> m_assembling_join_project; scoped_ptr<table_join_fn> m_assembling_join_project;
scoped_ptr<table_union_fn> m_updating_union; scoped_ptr<table_union_fn> m_updating_union;
public: 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) : const unsigned * rel_cols) :
m_col_cnt(col_cnt), m_col_cnt(col_cnt),
m_table_cols(col_cnt, table_cols), m_table_cols(col_cnt, table_cols),
@ -1683,7 +1681,7 @@ namespace datalog {
tproj = r.get_table().clone(); tproj = r.get_table().clone();
} }
SASSERT(m_col_cnt+1==tproj->get_signature().size()); SASSERT(m_col_cnt+1==tproj->get_signature().size());
table_signature filtered_sig = tproj->get_signature(); table_signature filtered_sig = tproj->get_signature();
filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); filtered_sig.push_back(finite_product_relation::s_rel_idx_sort);
filtered_sig.set_functional_columns(1); 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) { unsigned col_cnt, const unsigned * table_cols, const unsigned * rel_cols) {
return alloc(filter_identical_pairs_fn, r, col_cnt, table_cols, 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) { const table_base & filtered_table, const unsigned_vector & selected_columns) {
table_plugin & tplugin = relation_table.get_plugin(); 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); //unfiltered relation indexes from 'filtered'
removed_cols.push_back(idx_ofs+1); //unfiltered relation indexes from rtable 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); rtable_joined_cols, filtered_joined_cols, removed_cols);
SASSERT(res); SASSERT(res);
return 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, const relation_signature & s, const bool * table_columns, table_plugin & tplugin,
relation_plugin & oplugin, family_id other_kind) relation_plugin & oplugin, family_id other_kind)
: relation_base(p, s), : relation_base(p, s),
m_other_plugin(oplugin), m_other_plugin(oplugin),
m_other_kind(other_kind), m_other_kind(other_kind),
m_full_rel_idx(UINT_MAX) { m_full_rel_idx(UINT_MAX) {
@ -1811,7 +1809,7 @@ namespace datalog {
} }
finite_product_relation::finite_product_relation(const finite_product_relation & r) 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_table_sig(r.m_table_sig),
m_table2sig(r.m_table2sig), m_table2sig(r.m_table2sig),
m_sig2table(r.m_sig2table), m_sig2table(r.m_sig2table),
@ -1860,7 +1858,7 @@ namespace datalog {
relation_base::swap(r0); relation_base::swap(r0);
} }
finite_product_relation::~finite_product_relation() { finite_product_relation::~finite_product_relation() {
m_table->deallocate(); m_table->deallocate();
relation_vector::iterator it = m_others.begin(); relation_vector::iterator it = m_others.begin();
relation_vector::iterator end = m_others.end(); relation_vector::iterator end = m_others.end();
@ -2028,7 +2026,7 @@ namespace datalog {
} }
table_element full_rel_idx = get_full_rel_idx(); table_element full_rel_idx = get_full_rel_idx();
scoped_rel<table_base> complement_table = m_table->complement(p, &full_rel_idx); scoped_rel<table_base> complement_table = m_table->complement(p, &full_rel_idx);
scoped_ptr<table_union_fn> u_fn = get_manager().mk_union_fn(*m_table, *complement_table, nullptr); scoped_ptr<table_union_fn> u_fn = get_manager().mk_union_fn(*m_table, *complement_table, nullptr);
SASSERT(u_fn); SASSERT(u_fn);
(*u_fn)(*m_table, *complement_table, nullptr); (*u_fn)(*m_table, *complement_table, nullptr);
@ -2204,7 +2202,7 @@ namespace datalog {
} }
//remove also the last column with inner relation index //remove also the last column with inner relation index
to_project_away.push_back(get_table().get_signature().size()-1); to_project_away.push_back(get_table().get_signature().size()-1);
if(new_rel_columns.empty()) { if(new_rel_columns.empty()) {
//the specifications are the same //the specifications are the same
return true; return true;
@ -2220,15 +2218,15 @@ namespace datalog {
scoped_ptr<table_transformer_fn> pr_fun = get_manager().mk_project_fn(get_table(), to_project_away); scoped_ptr<table_transformer_fn> 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 table_base * moved_cols_table = (*pr_fun)(get_table()); //gets destroyed inside moved_cols_trel
scoped_rel<relation_base> moved_cols_trel = scoped_rel<relation_base> moved_cols_trel =
rmgr.get_table_relation_plugin(moved_cols_table->get_plugin()).mk_from_table(moved_cols_sig, moved_cols_table); rmgr.get_table_relation_plugin(moved_cols_table->get_plugin()).mk_from_table(moved_cols_sig, moved_cols_table);
svector<bool> moved_cols_table_flags(moved_cols_sig.size(), false); svector<bool> moved_cols_table_flags(moved_cols_sig.size(), false);
scoped_rel<finite_product_relation> moved_cols_rel = get_plugin().mk_empty(moved_cols_sig, scoped_rel<finite_product_relation> moved_cols_rel = get_plugin().mk_empty(moved_cols_sig,
moved_cols_table_flags.c_ptr()); moved_cols_table_flags.c_ptr());
scoped_ptr<relation_union_fn> union_fun = scoped_ptr<relation_union_fn> union_fun =
get_manager().mk_union_fn(*moved_cols_rel, *moved_cols_trel); 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 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 //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<relation_base> unordered_rel. //since it points to the content of scoped_rel<relation_base> unordered_rel.
swap(new_rel); swap(new_rel);
return true; return true;
} }
@ -2371,8 +2369,7 @@ namespace datalog {
conjs.push_back(tmp); conjs.push_back(tmp);
disjs.push_back(m.mk_and(conjs.size(), conjs.c_ptr())); 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);
} }
}; };

46
src/shell/datalog_frontend.cpp
View file

@ -53,7 +53,7 @@ static void display_statistics(
datalog::instruction_block& code, datalog::instruction_block& code,
datalog::execution_context& ex_ctx, datalog::execution_context& ex_ctx,
bool verbose bool verbose
) )
{ {
std::lock_guard<std::mutex> lock(*display_stats_mux); std::lock_guard<std::mutex> lock(*display_stats_mux);
g_piece_timer.stop(); g_piece_timer.stop();
@ -67,11 +67,11 @@ static void display_statistics(
p.set_uint("profile_milliseconds_threshold", 100); p.set_uint("profile_milliseconds_threshold", 100);
ctx.updt_params(p); ctx.updt_params(p);
IF_VERBOSE(2, IF_VERBOSE(2,
out << "--------------\n"; out << "--------------\n";
out << "original rules\n"; out << "original rules\n";
orig_rules.display(out); orig_rules.display(out);
out << "---------------\n"; out << "---------------\n";
out << "generated rules\n"; out << "generated rules\n";
ctx.display_rules(out); ctx.display_rules(out);
@ -79,12 +79,12 @@ static void display_statistics(
out << "--------------\n"; out << "--------------\n";
out << "instructions \n"; out << "instructions \n";
code.display(ex_ctx, out); code.display(ex_ctx, out);
out << "--------------\n"; out << "--------------\n";
out << "big relations \n"; out << "big relations \n";
ex_ctx.report_big_relations(1000, out);); ex_ctx.report_big_relations(1000, out););
} }
IF_VERBOSE(2, IF_VERBOSE(2,
out << "--------------\n"; out << "--------------\n";
out << "relation sizes\n"; out << "relation sizes\n";
ctx.get_rel_context()->get_rmanager().display_relation_sizes(out);); 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::context ctx(m, re, s_params, params);
datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager(); datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable")); 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)); rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
g_piece_timer.reset(); g_piece_timer.reset();
g_piece_timer.start(); g_piece_timer.start();
@ -178,26 +177,26 @@ unsigned read_datalog(char const * file) {
g_code = &rules_code; g_code = &rules_code;
g_ectx = &ex_ctx; g_ectx = &ex_ctx;
try { try {
g_piece_timer.reset(); g_piece_timer.reset();
g_piece_timer.start(); g_piece_timer.start();
bool early_termination; bool early_termination;
unsigned timeout = ctx.initial_restart_timeout(); unsigned timeout = ctx.initial_restart_timeout();
if (timeout == 0) { if (timeout == 0) {
timeout = UINT_MAX; timeout = UINT_MAX;
} }
do { do {
ctx.get_rel_context()->transform_rules(); ctx.get_rel_context()->transform_rules();
datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
TRACE("dl_compiler", rules_code.display(ex_ctx, tout);); TRACE("dl_compiler", rules_code.display(ex_ctx, tout););
rules_code.make_annotations(ex_ctx); rules_code.make_annotations(ex_ctx);
ex_ctx.set_timelimit(timeout); ex_ctx.set_timelimit(timeout);
early_termination = !rules_code.perform(ex_ctx); early_termination = !rules_code.perform(ex_ctx);
if(early_termination) { if(early_termination) {
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream());); 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(); ex_ctx.reset_timelimit();
TRUSTME( termination_code.perform(ex_ctx) ); TRUSTME( termination_code.perform(ex_ctx) );
ctx.saturation_was_run(); ctx.saturation_was_run();
if (early_termination) { if (early_termination) {
IF_VERBOSE(1, verbose_stream() << "restarting saturation\n";); IF_VERBOSE(1, verbose_stream() << "restarting saturation\n";);
uint64_t new_timeout = static_cast<uint64_t>(timeout)*ctx.initial_restart_timeout(); uint64_t new_timeout = static_cast<uint64_t>(timeout)*ctx.initial_restart_timeout();
if(new_timeout>UINT_MAX) { if(new_timeout>UINT_MAX) {
timeout=UINT_MAX; timeout=UINT_MAX;
@ -219,7 +218,7 @@ unsigned read_datalog(char const * file) {
else { else {
timeout=static_cast<unsigned>(new_timeout); timeout=static_cast<unsigned>(new_timeout);
} }
rules_code.process_all_costs(); rules_code.process_all_costs();
rules_code.reset(); rules_code.reset();
termination_code.reset(); termination_code.reset();
@ -229,29 +228,29 @@ unsigned read_datalog(char const * file) {
ctx.close(); ctx.close();
} }
} while (early_termination); } while (early_termination);
TRACE("dl_compiler", ctx.display(tout); TRACE("dl_compiler", ctx.display(tout);
rules_code.display(ex_ctx, tout);); rules_code.display(ex_ctx, tout););
if (ctx.output_tuples()) { if (ctx.output_tuples()) {
ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout); ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout);
} }
display_statistics( display_statistics(
std::cout, std::cout,
ctx, ctx,
original_rules, original_rules,
rules_code, rules_code,
ex_ctx, ex_ctx,
false); false);
} }
catch (const out_of_memory_error &) { catch (const out_of_memory_error &) {
std::cout << "\n\nOUT OF MEMORY!\n\n"; std::cout << "\n\nOUT OF MEMORY!\n\n";
display_statistics( display_statistics(
std::cout, std::cout,
ctx, ctx,
original_rules, original_rules,
rules_code, rules_code,
ex_ctx, ex_ctx,
true); true);
@ -259,4 +258,3 @@ unsigned read_datalog(char const * file) {
} }
return 0; return 0;
} }