mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

add lipstick note

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-26 08:46:14 -07:00
parent 061a18efcf
commit 08ef9f34bc
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -58,7 +58,9 @@ Notes:
return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
We have most of the facilities required for a join project operation.
For example, the filter_project function uses both equalities and deleted columns.
- Lipstick service:
- filter_proj_fn uses both a bit_vector and a svector<bool> for representing removed bits.
This is due to underlying routines using different types for the same purpose.
--*/
#include "udoc_relation.h"
#include "dl_relation_manager.h"
@ -1218,17 +1220,15 @@ namespace datalog {
m_original_condition(condition, m),
m_reduced_condition(m),
m_equalities(union_ctx) {
t.expand_column_vector(m_removed_cols);
unsigned num_bits = t.get_num_bits();
m_col_list.resize(num_bits, false);
t.expand_column_vector(m_removed_cols);
m_col_list.resize(num_bits, false);
m_to_delete.resize(num_bits, false);
for (unsigned i = 0; i < num_bits; ++i) {
m_equalities.mk_var();
}
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_col_list.set(m_removed_cols[i], true);
}
m_to_delete.resize(t.get_num_bits(), false);
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_to_delete[m_removed_cols[i]] = true;
}
expr_ref guard(m), non_eq_cond(condition, m);