mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

[dl] remove 2 uneeded fields from sparse_table::rename_fn

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-04-16 10:48:57 -07:00
parent adc8224dba
commit 51d3db8105
1 changed files with 5 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/muz_qe/dl_sparse_table.cpp
View file

@ -1022,19 +1022,16 @@ namespace datalog {
class sparse_table_plugin::rename_fn : public convenient_table_rename_fn { class sparse_table_plugin::rename_fn : public convenient_table_rename_fn {
const unsigned m_cycle_len;
const unsigned m_col_cnt;
unsigned_vector m_out_of_cycle; unsigned_vector m_out_of_cycle;
public: public:
rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle)
: convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle), : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) {
m_cycle_len(permutation_cycle_len), m_col_cnt(orig_sig.size()) {
SASSERT(permutation_cycle_len>=2); SASSERT(permutation_cycle_len>=2);
idx_set cycle_cols; idx_set cycle_cols;
for (unsigned i=0; i<m_cycle_len; i++) { for (unsigned i=0; i < permutation_cycle_len; ++i) {
cycle_cols.insert(permutation_cycle[i]); cycle_cols.insert(permutation_cycle[i]);
} }
for (unsigned i=0; i<m_col_cnt; i++) { for (unsigned i=0; i < orig_sig.size(); ++i) {
if (!cycle_cols.contains(i)) { if (!cycle_cols.contains(i)) {
m_out_of_cycle.push_back(i); m_out_of_cycle.push_back(i);
} }
@ -1045,10 +1042,10 @@ namespace datalog {
const sparse_table::column_layout & src_layout, const sparse_table::column_layout & src_layout,
const sparse_table::column_layout & tgt_layout) { const sparse_table::column_layout & tgt_layout) {
for (unsigned i=1; i<m_cycle_len; i++) { for (unsigned i=1; i < m_cycle.size(); ++i) {
tgt_layout.set(tgt, m_cycle[i-1], src_layout.get(src, m_cycle[i])); tgt_layout.set(tgt, m_cycle[i-1], src_layout.get(src, m_cycle[i]));
} }
tgt_layout.set(tgt, m_cycle[m_cycle_len-1], src_layout.get(src, m_cycle[0])); tgt_layout.set(tgt, m_cycle[m_cycle.size()-1], src_layout.get(src, m_cycle[0]));
unsigned_vector::const_iterator it = m_out_of_cycle.begin(); unsigned_vector::const_iterator it = m_out_of_cycle.begin();
unsigned_vector::const_iterator end = m_out_of_cycle.end(); unsigned_vector::const_iterator end = m_out_of_cycle.end();