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

working on product sets

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-26 16:45:45 -07:00
parent 3ae10abf04
commit 9e7cef7d6b
8 changed files with 377 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/muz/rel/dl_relation_manager.cpp
View file

@ -668,6 +668,27 @@ namespace datalog {
return res;
}
class relation_manager::default_relation_apply_sequential_fn : public relation_mutator_fn {
ptr_vector<relation_mutator_fn> m_mutators;
public:
default_relation_apply_sequential_fn(unsigned n, relation_mutator_fn ** mutators):
m_mutators(n, mutators) {
}
virtual ~default_relation_apply_sequential_fn() {
std::for_each(m_mutators.begin(), m_mutators.end(), delete_proc<relation_mutator_fn>());
}
virtual void operator()(relation_base& t) {
for (unsigned i = 0; i < m_mutators.size(); ++i) {
if (t.empty()) return;
(*(m_mutators[i]))(t);
}
}
};
relation_mutator_fn * relation_manager::mk_apply_sequential_fn(unsigned n, relation_mutator_fn ** mutators) {
return alloc(default_relation_apply_sequential_fn, n, mutators);
}
class relation_manager::default_relation_join_project_fn : public relation_join_fn {
scoped_ptr<relation_join_fn> m_join;

5
src/muz/rel/dl_relation_manager.h
View file

@ -43,6 +43,7 @@ namespace datalog {
class default_relation_select_equal_and_project_fn;
class default_relation_intersection_filter_fn;
class default_relation_filter_interpreted_and_project_fn;
class default_relation_apply_sequential_fn;
class auxiliary_table_transformer_fn;
class auxiliary_table_filter_fn;
@ -352,9 +353,13 @@ namespace datalog {
relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition,
unsigned removed_col_cnt, const unsigned * removed_cols);
relation_mutator_fn * mk_apply_sequential_fn(unsigned n, relation_mutator_fn* * mutators);
/**
\brief Operations that returns all rows of \c t for which is column \c col equal to \c value
with the column \c col removed.

352
src/muz/rel/product_set.cpp
View file

@ -26,10 +26,14 @@ namespace datalog {
product_set::product_set(
product_set_plugin& p, relation_signature const& s,
bool is_empty, T const& t):
vector_relation(p, s, is_empty, t), m_refs(0) {
initial_t init, T const& t):
vector_relation(p, s, false, t), m_refs(0) {
for (unsigned i = 0; i < s.size(); ++i) {
(*this)[i] = bit_vector(p.set_size(s[i]));
unsigned sz = p.set_size(s[i]);
(*this)[i].resize(sz);
if (init == FULL_t) {
(*this)[i].neg();
}
}
}
@ -135,19 +139,43 @@ namespace datalog {
}
}
class product_set_plugin::filter_interpreted_fn : public relation_mutator_fn {
app_ref m_condition;
public:
filter_interpreted_fn(ast_manager& m, app* condition): m_condition(condition, m) {
};
virtual ~filter_interpreted_fn() {}
virtual void operator()(relation_base & _r) {
ast_manager& m = m_condition.get_manager();
if (m.is_false(m_condition)) {
_r.reset();
return;
}
if (m.is_true(m_condition)) {
return;
}
product_set_relation & r = get(_r);
product_set_plugin & p = r.get_plugin();
NOT_IMPLEMENTED_YET();
}
};
void product_set_relation::add_fact(const relation_fact & f) {
ast_manager& m = get_plugin().get_ast_manager();
bv_util bv(m);
product_set* s = alloc(product_set, get_plugin(), get_signature(), product_set::EMPTY_t);
rational v;
unsigned bv_size;
product_set* s = alloc(product_set, get_plugin(), get_signature(), false);
// the bit-vector sets are empty at this point so they need to be primed.
for (unsigned i = 0; i < f.size(); ++i) {
VERIFY(bv.is_numeral(f[i], v, bv_size));
SASSERT(v.is_unsigned());
(*s)[i] = bit_vector(get_plugin().set_size(m.get_sort(f[i])));
(*s)[i].set(v.get_unsigned(), true);
}
s->display(std::cout << "fact");
// s->display(std::cout << "fact");
if (m_elems.contains(s)) {
dealloc(s);
}
@ -201,7 +229,9 @@ namespace datalog {
// product_set_plugin
product_set_plugin::product_set_plugin(relation_manager& rm):
relation_plugin(product_set_plugin::get_name(), rm) {
relation_plugin(product_set_plugin::get_name(), rm),
m(rm.get_context().get_manager()),
bv(m) {
}
bool product_set_plugin::can_handle_signature(const relation_signature & sig) {
@ -226,15 +256,8 @@ namespace datalog {
}
relation_base * product_set_plugin::mk_full(func_decl* p, const relation_signature & sig) {
product_set_relation* result = alloc(product_set_relation, *this, sig);
product_set* s = alloc(product_set, *this, sig, false);
product_set* s = alloc(product_set, *this, sig, product_set::FULL_t);
s->inc_ref();
for (unsigned i = 0; i < sig.size(); ++i) {
bit_vector& t = (*s)[i];
t = bit_vector(set_size(sig[i]));
for (unsigned j = 0; j < t.size(); ++j) {
t.set(j, true);
}
}
result->m_elems.insert(s);
return result;
}
@ -248,7 +271,7 @@ namespace datalog {
else {
s->inc_ref();
r->m_elems.insert(s);
s = alloc(product_set, *this, r->get_signature(), false);
s = alloc(product_set, *this, r->get_signature(), product_set::FULL_t);
}
return s;
}
@ -276,7 +299,7 @@ namespace datalog {
product_set_plugin& p = r1.get_plugin();
relation_signature const& sig = get_result_signature();
product_set_relation * result = alloc(product_set_relation, p, sig);
product_set* s = alloc(product_set, p, sig, false);
product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
product_sets::iterator it1 = r1.m_elems.begin(), end1 = r1.m_elems.end();
for (; it1 != end1; ++it1) {
product_sets::iterator it2 = r2.m_elems.begin(), end2 = r2.m_elems.end();
@ -310,7 +333,7 @@ namespace datalog {
product_set_plugin& p = r.get_plugin();
relation_signature const& sig = get_result_signature();
product_set_relation* result = alloc(product_set_relation, p, sig);
product_set* s = alloc(product_set, p, sig, false);
product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
for (; it != end; ++it) {
s->mk_project(*(*it), m_removed_cols.size(), m_removed_cols.c_ptr());
@ -341,7 +364,7 @@ namespace datalog {
product_set_plugin& p = r.get_plugin();
relation_signature const& sig = get_result_signature();
product_set_relation* result = alloc(product_set_relation, p, sig);
product_set* s = alloc(product_set, p, sig, false);
product_set* s = alloc(product_set, p, sig, product_set::FULL_t);
product_sets::iterator it = r.m_elems.begin(), end = r.m_elems.end();
for (; it != end; ++it) {
s->mk_rename(*(*it), m_cycle.size(), m_cycle.c_ptr());
@ -373,20 +396,24 @@ namespace datalog {
product_set_relation& r = get(_r);
product_set_relation const& src = get(_src);
product_set_relation* d = get(_delta);
product_sets::iterator it = src.m_elems.begin(), end = src.m_elems.end();
for (; it != end; ++it) {
product_set* ps = *it;
if (!r.m_elems.contains(ps)) {
r.get_plugin().mk_union(r, src, d);
}
};
void product_set_plugin::mk_union(
product_set_relation& dst, product_set_relation const& src, product_set_relation* delta) {
product_sets::iterator it = src.m_elems.begin(), end = src.m_elems.end();
for (; it != end; ++it) {
product_set* ps = *it;
if (!dst.m_elems.contains(ps)) {
ps->inc_ref();
dst.m_elems.insert(ps);
if (delta) {
ps->inc_ref();
r.m_elems.insert(ps);
if (d) {
ps->inc_ref();
d->m_elems.insert(ps);
}
delta->m_elems.insert(ps);
}
}
}
};
}
relation_union_fn * product_set_plugin::mk_union_fn(
const relation_base & tgt, const relation_base & src,
const relation_base * delta) {
@ -442,31 +469,13 @@ namespace datalog {
return check_kind(t)?alloc(filter_identical_fn, col_cnt, identical_cols):0;
}
class product_set_plugin::filter_equal_fn : public relation_mutator_fn {
unsigned m_col;
bit_vector m_value;
class product_set_plugin::filter_mask_fn : public relation_mutator_fn {
unsigned m_col;
bit_vector m_mask;
public:
filter_equal_fn(product_set_plugin& p, const relation_element & value, unsigned col, bool is_eq)
: m_col(col) {
ast_manager& m = p.get_ast_manager();
// m.get_context().get_manager()
bv_util bv(m);
rational v;
unsigned bv_size;
unsigned sz = p.set_size(m.get_sort(value));
VERIFY(bv.is_numeral(value, v, bv_size));
SASSERT(v.is_unsigned());
unsigned w = v.get_unsigned();
SASSERT(w < sz);
m_value = bit_vector(sz);
if (is_eq) {
m_value.set(w, true);
}
else {
for (unsigned i = 0; i < sz; ++i) {
m_value.set(i, i != w);
}
}
filter_mask_fn(product_set_plugin& p, bit_vector const& mask, unsigned col)
: m_col(col), m_mask(mask) {
}
virtual void operator()(relation_base & _r) {
@ -482,7 +491,7 @@ namespace datalog {
for (unsigned i = 0; i < elems.size(); ++i) {
product_set* s = elems[i];
if (s->mk_intersect(m_col, m_value)) {
if (s->mk_intersect(m_col, m_mask)) {
r.m_elems.insert(s);
}
else {
@ -494,17 +503,246 @@ namespace datalog {
relation_mutator_fn * product_set_plugin::mk_filter_equal_fn(const relation_base & r,
const relation_element & value, unsigned col) {
return check_kind(r)?alloc(filter_equal_fn, *this, value, col, true):0;
bit_vector mask;
expr* v = value;
extract_mask(1, &v, mask);
return check_kind(r)?alloc(filter_mask_fn, *this, mask, col):0;
}
class product_set_plugin::filter_by_union_fn : public relation_mutator_fn {
ptr_vector<relation_mutator_fn> m_mutators;
public:
filter_by_union_fn(unsigned n, relation_mutator_fn ** mutators):
m_mutators(n, mutators) {
}
virtual ~filter_by_union_fn() {
std::for_each(m_mutators.begin(), m_mutators.end(), delete_proc<relation_mutator_fn>());
}
virtual void operator()(relation_base& _r) {
product_set_relation & r = get(_r);
product_set_plugin & p = r.get_plugin();
SASSERT(!m_mutators.empty());
if (m_mutators.size() == 1) {
(*(m_mutators[0]))(r);
return;
}
product_set_relation src(p, r.get_signature());
for (unsigned i = 1; i < m_mutators.size(); ++i) {
product_set_relation* r1 = r.clone();
(*(m_mutators[i]))(*r1);
p.mk_union(src, *r1, 0);
r1->deallocate();
}
(*(m_mutators[0]))(r);
p.mk_union(r, src, 0);
}
};
product_set_plugin::decomp_t product_set_plugin::decompose(
expr* condition, expr_ref_vector& args, unsigned& col) {
args.reset();
expr* e1, *e2;
app* value;
if (m.is_not(condition, e1) && m.is_not(e1, e2)) {
return decompose(e2, args, col);
}
if (m.is_not(condition, e1) && m.is_and(e1)) {
expr_ref tmp(m);
app* a = to_app(e1);
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
args.push_back(mk_not(a->get_arg(i)));
}
tmp = m.mk_or(args.size(), args.c_ptr());
return decompose(tmp, args, col);
}
if (m.is_not(condition, e1) && m.is_or(e1)) {
expr_ref tmp(m);
app* a = to_app(e1);
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
args.push_back(mk_not(a->get_arg(i)));
}
tmp = m.mk_and(args.size(), args.c_ptr());
return decompose(tmp, args, col);
}
if (m.is_and(condition)) {
app* a = to_app(condition);
unsigned sz = a->get_num_args();
args.append(sz, a->get_args());
return AND_d;
}
if (is_setof(condition, args, col)) {
return SET_d;
}
if (m.is_or(condition)) {
app* a = to_app(condition);
unsigned sz = a->get_num_args();
args.append(sz, a->get_args());
return OR_d;
}
if (is_value_ne(condition, value, col)) {
args.push_back(value);
return NE_d;
}
if (is_value_eq(condition, value, col)) {
args.push_back(value);
return EQ_d;
}
if (m.is_not(condition, e1) && m.is_true(e1)) {
return F_d;
}
if (m.is_false(condition)) {
return F_d;
}
if (m.is_not(condition, e1) && m.is_false(e1)) {
return T_d;
}
if (m.is_true(condition)) {
return T_d;
}
return UNHANDLED_d;
}
bool product_set_plugin::mk_filter_interpreted(
const relation_base & t, expr_ref_vector const& args,
ptr_vector<relation_mutator_fn>& mutators) {
unsigned sz = args.size();
for (unsigned i = 0; i < sz; ++i) {
expr* arg = args[i];
if (!is_app(arg)) {
break;
}
relation_mutator_fn* mut = mk_filter_interpreted_fn(t, to_app(arg));
if (!mut) {
break;
}
mutators.push_back(mut);
}
if (mutators.size() < sz) {
std::for_each(mutators.begin(), mutators.end(), delete_proc<relation_mutator_fn>());
return false;
}
else {
return true;
}
}
relation_mutator_fn * product_set_plugin::mk_filter_interpreted_fn(
const relation_base & t, app * condition) {
ast_manager& m =get_manager().get_context().get_manager();
std::cout << "filter interpreted '" << mk_pp(condition, m) << "'\n";
NOT_IMPLEMENTED_YET();
if (!check_kind(t)) return 0;
unsigned col;
ptr_vector<relation_mutator_fn> mutators;
expr_ref_vector args(m);
std::cout << mk_pp(condition, m) << "\n";
bit_vector mask;
switch (decompose(condition, args, col)) {
case NE_d:
SASSERT(args.size() == 1);
extract_mask(1, args.c_ptr(), mask);
mask.neg();
return alloc(filter_mask_fn, *this, mask, col);
case EQ_d:
SASSERT(args.size() == 1);
extract_mask(1, args.c_ptr(), mask);
return alloc(filter_mask_fn, *this, mask, col);
case AND_d:
if (!mk_filter_interpreted(t, args, mutators)) {
return 0;
}
return get_manager().mk_apply_sequential_fn(mutators.size(), mutators.c_ptr());
case OR_d:
if (!mk_filter_interpreted(t, args, mutators)) {
return 0;
}
return alloc(filter_by_union_fn, mutators.size(), mutators.c_ptr());
case F_d:
return alloc(filter_interpreted_fn, m, m.mk_false());
case T_d:
return alloc(filter_interpreted_fn, m, m.mk_true());
case SET_d:
extract_mask(args.size(), args.c_ptr(), mask);
return alloc(filter_mask_fn, *this, mask, col);
case UNHANDLED_d:
std::cout << "filter interpreted unhandled '" << mk_pp(condition, m) << "'\n";
NOT_IMPLEMENTED_YET();
return 0;
default:
UNREACHABLE();
}
return 0;
}
void product_set_plugin::extract_mask(unsigned n, expr* const* values, bit_vector& mask) {
SASSERT(n > 0);
unsigned sz = set_size(m.get_sort(values[0]));
mask.resize(sz, false);
rational v;
unsigned bv_size;
for (unsigned i = 0; i < n; ++i) {
expr* value = values[i];
VERIFY(bv.is_numeral(value, v, bv_size));
SASSERT(v.is_unsigned());
unsigned w = v.get_unsigned();
SASSERT(w < sz);
mask.set(w, true);
}
}
bool product_set_plugin::is_setof(expr* condition, expr_ref_vector& values, unsigned & col) {
if (!m.is_or(condition)) return false;
unsigned sz = to_app(condition)->get_num_args();
col = UINT_MAX;
unsigned col1;
if (sz == 0) return false;
values.reset();
app* value;
for (unsigned i = 0; i < sz; ++i) {
expr* arg = to_app(condition)->get_arg(i);
if (is_value_eq(arg, value, col1)) {
if (col == UINT_MAX) {
col = col1;
values.push_back(value);
}
else if (col != col1) {
return false;
}
else {
values.push_back(value);
}
}
}
return true;
}
bool product_set_plugin::is_value_eq(expr* e, app*& value, unsigned& col) {
expr* e1, *e2;
rational val;
unsigned bv_size;
if (!m.is_eq(e, e1, e2)) return false;
if (!is_var(e1)) {
std::swap(e1, e2);
}
if (!is_var(e1)) return false;
if (!bv.is_numeral(e2, val, bv_size)) return false;
if (!val.is_unsigned()) return false;
value = to_app(e2);
col = to_var(e1)->get_idx();
return true;
}
bool product_set_plugin::is_value_ne(expr* condition, relation_element& value, unsigned& col) {
expr* e;
if (m.is_not(condition, e)) {
return is_value_eq(e, value, col);
}
else {
return false;
}
}
};

34
src/muz/rel/product_set.h
View file

@ -40,7 +40,11 @@ namespace datalog {
typedef bit_vector T;
unsigned m_refs;
public:
product_set(product_set_plugin& p, relation_signature const& s, bool is_empty, T const& t = T());
enum initial_t {
EMPTY_t,
FULL_t
};
product_set(product_set_plugin& p, relation_signature const& s, initial_t init, T const& t = T());
virtual ~product_set() {}
unsigned get_hash() const;
@ -146,10 +150,13 @@ namespace datalog {
class project_fn;
class union_fn;
class rename_fn;
class filter_equal_fn;
class filter_mask_fn;
class filter_identical_fn;
class filter_interpreted_fn;
class filter_by_negation_fn;
class filter_by_union_fn;
ast_manager& m;
bv_util bv;
public:
product_set_plugin(relation_manager& rm);
@ -180,6 +187,29 @@ namespace datalog {
static product_set_relation* get(relation_base* r);
static product_set_relation const & get(relation_base const& r);
product_set* insert(product_set* s, product_set_relation* r);
enum decomp_t {
AND_d, // conjunction
OR_d, // disjunction
EQ_d, // value = col
NE_d, // value != col
F_d, // false
T_d, // true
SET_d, // disjunction value_i = col
UNHANDLED_d
};
decomp_t decompose(expr* condition, expr_ref_vector& args, unsigned& col);
bool is_value_ne(expr* condition, relation_element& value, unsigned& col);
bool is_value_eq(expr* condition, relation_element& value, unsigned& col);
bool is_setof(expr* condition, expr_ref_vector& values, unsigned& col);
expr* mk_not(expr* e) { return m.is_not(e,e)?e:m.mk_not(e); }
void mk_union(product_set_relation& dst, product_set_relation const& src, product_set_relation* delta);
void extract_mask(unsigned sz, expr* const* values, bit_vector& mask);
bool mk_filter_interpreted(
const relation_base & t, expr_ref_vector const& args,
ptr_vector<relation_mutator_fn>& mutators);
};
};

5
src/opt/opt_params.pyg
View file

@ -3,15 +3,12 @@ def_module_params('opt',
export=True,
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'hsmax'"),
('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('print_model', BOOL, False, 'display model for satisfiable constraints'),
('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'),
('debug_conflict', BOOL, False, 'debug conflict resolution'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
('sls_engine', SYMBOL, 'pb', "SLS engine. Either 'bv' or 'pb'"),
('elim_01', BOOL, True, 'eliminate 01 variables'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')

16
src/sat/sat_mus.cpp
View file

@ -71,18 +71,19 @@ namespace sat {
literal lit = core.back();
core.pop_back();
unsigned sz = mus.size();
// mus.push_back(~lit); // TBD: measure
mus.append(core);
mus.push_back(~lit); // TBD: measure
lbool is_sat = s.check(mus.size(), mus.c_ptr());
TRACE("sat", tout << "mus: " << mus << "\n";);
mus.resize(sz);
switch (is_sat) {
case l_undef:
mus.resize(sz);
core.push_back(lit);
set_core();
return l_undef;
case l_true: {
SASSERT(value_at(lit, s.get_model()) == l_false);
mus.resize(sz);
mus.push_back(lit);
if (!core.empty()) {
// mr(); // TBD: measure
@ -92,8 +93,18 @@ namespace sat {
case l_false:
literal_vector const& new_core = s.get_core();
if (new_core.contains(~lit)) {
mus.resize(sz);
break;
#if 0
mus.pop_back();
is_sat = s.check(mus.size(), mus.c_ptr());
SASSERT(is_sat != l_true);
if (is_sat != l_false) {
return l_undef;
}
#endif
}
mus.resize(sz);
TRACE("sat", tout << "new core: " << new_core << "\n";);
core.reset();
for (unsigned i = 0; i < new_core.size(); ++i) {
@ -102,7 +113,6 @@ namespace sat {
core.push_back(lit);
}
}
IF_VERBOSE(2, verbose_stream() << "reduced core: " << core.size() << "\n";);
break;
}
}

8
src/util/bit_vector.cpp
View file

@ -228,6 +228,14 @@ unsigned bit_vector::get_hash() const {
return string_hash(reinterpret_cast<char const* const>(m_data), size()/8, 0);
}
bit_vector& bit_vector::neg() {
unsigned n = num_words();
for (unsigned i = 0; i < n; ++i) {
m_data[i] = ~m_data[i];
}
return *this;
}
void fr_bit_vector::reset() {
unsigned sz = size();
unsigned_vector::const_iterator it = m_one_idxs.begin();

2
src/util/bit_vector.h
View file

@ -200,6 +200,8 @@ public:
bit_vector & operator|=(bit_vector const & source);
bit_vector & operator&=(bit_vector const & source);
bit_vector & neg();
void display(std::ostream & out) const;