mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 00:35:47 +00:00
Code Activity

DoC: remove unused class fields in join operation

Browse source
This commit is contained in:
Nuno Lopes 2015-01-23 14:56:25 +00:00
parent e50e02e656
commit 18b1372199
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/rel/udoc_relation.cpp
View file

@ -314,17 +314,13 @@ namespace datalog {
doc_manager& dm; doc_manager& dm;
doc_manager& dm1; doc_manager& dm1;
doc_manager& dm2; doc_manager& dm2;
unsigned_vector m_orig_cols1;
unsigned_vector m_orig_cols2;
public: public:
join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt, join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2) const unsigned * cols1, const unsigned * cols2)
: convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2), : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
dm(p.dm(get_result_signature())), dm(p.dm(get_result_signature())),
dm1(t1.get_dm()), dm1(t1.get_dm()),
dm2(t2.get_dm()), dm2(t2.get_dm()) {
m_orig_cols1(m_cols1),
m_orig_cols2(m_cols2) {
t1.expand_column_vector(m_cols1); t1.expand_column_vector(m_cols1);
t2.expand_column_vector(m_cols2); t2.expand_column_vector(m_cols2);
} }