mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
adding udoc_relation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
887e6e5392
commit
1058de1aa7
9 changed files with 590 additions and 76 deletions
|
|
@ -66,7 +66,7 @@ def init_project_def():
|
|||
add_lib('clp', ['muz', 'transforms'], 'muz/clp')
|
||||
add_lib('tab', ['muz', 'transforms'], 'muz/tab')
|
||||
add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
|
||||
add_lib('ddnf', ['muz', 'transforms'], 'muz/ddnf')
|
||||
add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf')
|
||||
add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
|
||||
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
|
||||
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
|
||||
|
|
|
|||
|
|
@ -793,8 +793,10 @@ bool substitution_tree::visit(expr * e, st_visitor & st, node * r) {
|
|||
}
|
||||
else {
|
||||
TRACE("st_bug", tout << "found match:\n"; m_subst->display(tout); tout << "m_subst: " << m_subst << "\n";);
|
||||
if (!st(n->m_expr))
|
||||
if (!st(n->m_expr)) {
|
||||
clear_stack();
|
||||
return false;
|
||||
}
|
||||
if (!backtrack())
|
||||
break;
|
||||
}
|
||||
|
|
@ -806,12 +808,16 @@ bool substitution_tree::visit(expr * e, st_visitor & st, node * r) {
|
|||
else if (!backtrack())
|
||||
break;
|
||||
}
|
||||
clear_stack();
|
||||
return true;
|
||||
}
|
||||
|
||||
void substitution_tree::clear_stack() {
|
||||
while (!m_bstack.empty()) {
|
||||
m_subst->pop_scope();
|
||||
m_bstack.pop_back();
|
||||
}
|
||||
m_subst->pop_scope();
|
||||
return true;
|
||||
}
|
||||
|
||||
template<substitution_tree::st_visit_mode Mode>
|
||||
|
|
|
|||
|
|
@ -123,6 +123,8 @@ class substitution_tree {
|
|||
template<st_visit_mode Mode>
|
||||
void visit(expr * e, st_visitor & st, unsigned in_offset, unsigned st_offset, unsigned reg_offset);
|
||||
|
||||
void clear_stack();
|
||||
|
||||
public:
|
||||
substitution_tree(ast_manager & m);
|
||||
~substitution_tree();
|
||||
|
|
|
|||
82
src/muz/ddnf/doc.cpp
Normal file
82
src/muz/ddnf/doc.cpp
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
doc.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
difference of cubes.
|
||||
|
||||
Author:
|
||||
|
||||
Nuno Lopes (a-nlopes) 2013-03-01
|
||||
Nikolaj Bjorner (nbjorner) 2014-09-15
|
||||
|
||||
Revision History:
|
||||
|
||||
Based on ternary_diff_bitvector by Nuno Lopes.
|
||||
|
||||
--*/
|
||||
|
||||
#include "doc.h"
|
||||
void doc_manager::reset() {
|
||||
}
|
||||
doc* doc_manager::allocate() {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate1() {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate0() {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocateX() {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate(doc const& src) {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate(uint64 n) {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate(rational const& r) {
|
||||
return 0;
|
||||
}
|
||||
doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
|
||||
return 0;
|
||||
}
|
||||
void doc_manager::deallocate(doc* src) {
|
||||
}
|
||||
void doc_manager::copy(doc& dst, doc const& src) const {
|
||||
}
|
||||
doc& doc_manager::fill0(doc& src) const {
|
||||
return src;
|
||||
}
|
||||
doc& doc_manager::fill1(doc& src) const {
|
||||
return src;
|
||||
}
|
||||
doc& doc_manager::fillX(doc& src) const {
|
||||
return src;
|
||||
}
|
||||
bool doc_manager::set_and(doc& dst, doc const& src) const {
|
||||
return false;
|
||||
}
|
||||
void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
|
||||
}
|
||||
void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
|
||||
}
|
||||
bool doc_manager::equals(doc const& a, doc const& b) const {
|
||||
return false;
|
||||
}
|
||||
unsigned doc_manager::hash(doc const& src) const {
|
||||
return 0;
|
||||
}
|
||||
bool doc_manager::contains(doc const& a, doc const& b) const {
|
||||
return false;
|
||||
}
|
||||
std::ostream& doc_manager::display(std::ostream& out, doc const& b) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
@ -11,6 +11,7 @@ Abstract:
|
|||
|
||||
Author:
|
||||
|
||||
Nuno Lopes (a-nlopes) 2013-03-01
|
||||
Nikolaj Bjorner (nbjorner) 2014-09-15
|
||||
|
||||
Revision History:
|
||||
|
|
@ -22,8 +23,6 @@ Revision History:
|
|||
#ifndef _DOC_H_
|
||||
#define _DOC_H_
|
||||
|
||||
#if 0
|
||||
|
||||
#include "tbv.h"
|
||||
|
||||
class doc;
|
||||
|
|
@ -50,27 +49,38 @@ public:
|
|||
doc& fill1(doc& src) const;
|
||||
doc& fillX(doc& src) const;
|
||||
bool set_and(doc& dst, doc const& src) const;
|
||||
// doc& set_or(doc& dst, doc const& src) const;
|
||||
void neg(doc const& src, union_bvec<doc_mananger, doc>& result) const;
|
||||
void complement(doc const& src, ptr_vector<doc>& result);
|
||||
void subtract(doc const& A, doc const& B, ptr_vector<doc>& result);
|
||||
bool equals(doc const& a, doc const& b) const;
|
||||
unsigned hash(doc const& src) const;
|
||||
bool contains(doc const& a, doc const& b) const;
|
||||
std::ostream& display(std::ostream& out, doc const& b) const;
|
||||
unsigned num_tbits() const { return m.num_tbits(); }
|
||||
};
|
||||
|
||||
// union of tbv*, union of doc*
|
||||
template<typename M, typename T>
|
||||
class union_bvec {
|
||||
class union_bvec {
|
||||
ptr_vector<T> m_elems; // TBD: reuse allocator of M
|
||||
public:
|
||||
unsigned size() const { return m_elems.size(); }
|
||||
T& operator[](unsigned idx) const { return *m_elems[idx]; }
|
||||
bool empty() const { return m_elems.empty(); }
|
||||
bool contains(M& m, T& t) const {
|
||||
for (unsigned i = 0; i < m_elems.size(); ++i) {
|
||||
if (m.contains(*m_elems[i], t)) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
void push_back(T* t) {
|
||||
m_elems.push_back(t);
|
||||
}
|
||||
void reset(M& m) {
|
||||
for (unsigned i = 0; i < m_elems.size(); ++i) {
|
||||
m.deallocate(m_elems[i]);
|
||||
}
|
||||
m_elems.reset();
|
||||
}
|
||||
}
|
||||
void insert(M& m, T* t) {
|
||||
unsigned sz = size(), j = 0;
|
||||
bool found = false;
|
||||
|
|
@ -102,13 +112,13 @@ public:
|
|||
}
|
||||
return true;
|
||||
}
|
||||
void insert(M& m, union_set const& other) {
|
||||
void insert(M& m, union_bvec const& other) {
|
||||
for (unsigned i = 0; i < other.size(); ++i) {
|
||||
insert(m, other[i]);
|
||||
}
|
||||
}
|
||||
void intersect(M& m, union_set const& other, union_set& result) {
|
||||
result.reset(m);
|
||||
void intersect(M& m, union_bvec const& other) {
|
||||
union_bvec result;
|
||||
unsigned sz1 = size();
|
||||
unsigned sz2 = other.size();
|
||||
T* inter = m.allocate();
|
||||
|
|
@ -121,29 +131,30 @@ public:
|
|||
}
|
||||
}
|
||||
m.deallocate(inter);
|
||||
std::swap(result, *this);
|
||||
result.reset();
|
||||
}
|
||||
void neg(M& m, union_set& result) {
|
||||
union_set negated;
|
||||
void complement(M& m, union_bvec& result) {
|
||||
union_bvec negated;
|
||||
result.reset(m);
|
||||
result.push_back(m.allocateX());
|
||||
unsigned sz = size();
|
||||
for (unsigned i = 0; !result.empty() && i < sz; ++i) {
|
||||
// m.set_neg(*m_elems[i]);
|
||||
// result.intersect(m, negated);
|
||||
for (unsigned i = 0; !empty() && i < sz; ++i) {
|
||||
m.complement(*m_elems[i], negated.m_elems);
|
||||
result.intersect(m, negated);
|
||||
negated.reset(m);
|
||||
}
|
||||
}
|
||||
|
||||
void subtract(M& m, union_set const& other, union_set& result) {
|
||||
result.reset(m);
|
||||
|
||||
}
|
||||
};
|
||||
|
||||
typedef union_bvec<tbv_manager, tbv> utbv;
|
||||
|
||||
class doc {
|
||||
// pos \ (neg_0 \/ ... \/ neg_n)
|
||||
friend class doc_manager;
|
||||
tbv* m_pos;
|
||||
union_bvec<tbv_manager, tbv> m_neg;
|
||||
utbv m_neg;
|
||||
public:
|
||||
|
||||
struct eq {
|
||||
|
|
@ -161,55 +172,31 @@ public:
|
|||
return m.hash(d);
|
||||
}
|
||||
};
|
||||
|
||||
tbv& pos() { return *m_pos; }
|
||||
utbv& neg() { return m_neg; }
|
||||
tbv const& pos() const { return *m_pos; }
|
||||
utbv const& neg() const { return m_neg; }
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
typedef union_bvec<doc_manager, doc> udoc;
|
||||
|
||||
class doc_ref {
|
||||
doc_manager& dm;
|
||||
doc* d;
|
||||
public:
|
||||
doc_ref(doc_manager& dm):dm(dm),d(0) {}
|
||||
doc_ref(doc_manager& dm, doc* d):dm(dm),d(d) {}
|
||||
~doc_ref() {
|
||||
if (d) dm.deallocate(d);
|
||||
}
|
||||
doc_ref& operator=(doc* d2) {
|
||||
if (d) dm.deallocate(d);
|
||||
d = d2;
|
||||
}
|
||||
doc& operator*() { return *d; }
|
||||
};
|
||||
|
||||
#endif /* _DOC_H_ */
|
||||
|
||||
#if 0
|
||||
|
||||
class utbv {
|
||||
friend class ternary_bitvector;
|
||||
|
||||
ternary_bitvector m_pos;
|
||||
union_ternary_bitvector<ternary_bitvector> m_neg;
|
||||
|
||||
public:
|
||||
utbv() : m_pos(), m_neg(0) {}
|
||||
utbv(unsigned size) : m_pos(size), m_neg(size) {}
|
||||
utbv(unsigned size, bool full);
|
||||
utbv(const rational& n, unsigned num_bits);
|
||||
explicit utbv(const ternary_bitvector & tbv);
|
||||
|
||||
bool contains(const utbv & other) const;
|
||||
bool contains(const ternary_bitvector & other) const;
|
||||
bool contains(unsigned offset, const utbv& other,
|
||||
unsigned other_offset, unsigned length) const;
|
||||
bool is_empty() const;
|
||||
|
||||
utbv band(const utbv& other) const;
|
||||
void neg(union_ternary_bitvector<utbv>& result) const;
|
||||
|
||||
static bool has_subtract() { return true; }
|
||||
void subtract(const union_ternary_bitvector<utbv>& other,
|
||||
union_ternary_bitvector<utbv>& result) const;
|
||||
|
||||
|
||||
unsigned get(unsigned idx);
|
||||
void set(unsigned idx, unsigned val);
|
||||
|
||||
void swap(utbv & other);
|
||||
void reset();
|
||||
|
||||
|
||||
void display(std::ostream & out) const;
|
||||
|
||||
private:
|
||||
void add_negated(const ternary_bitvector& neg);
|
||||
void add_negated(const union_ternary_bitvector<ternary_bitvector>& neg);
|
||||
bool fold_neg();
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -60,11 +60,33 @@ tbv* tbv_manager::allocate(uint64 val) {
|
|||
tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
|
||||
tbv* v = allocateX();
|
||||
SASSERT(64 >= m.num_bits() && m.num_bits() > hi && hi >= lo);
|
||||
for (unsigned i = 0; i < hi - lo + 1; ++i) {
|
||||
v->set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
|
||||
}
|
||||
v->set(val, hi, lo);
|
||||
return v;
|
||||
}
|
||||
void tbv::set(uint64 val, unsigned hi, unsigned lo) {
|
||||
for (unsigned i = 0; i < hi - lo + 1; ++i) {
|
||||
set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
|
||||
}
|
||||
}
|
||||
void tbv::set(rational const& r, unsigned hi, unsigned lo) {
|
||||
if (r.is_uint64()) {
|
||||
set(r.get_uint64(), hi, lo);
|
||||
return;
|
||||
}
|
||||
for (unsigned i = 0; i < hi - lo + 1; ++i) {
|
||||
if (bitwise_and(r, rational::power_of_two(i)).is_zero())
|
||||
set(lo + i, BIT_0);
|
||||
else
|
||||
set(lo + i, BIT_1);
|
||||
}
|
||||
}
|
||||
|
||||
void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
|
||||
for (unsigned i = 0; i < hi - lo + 1; ++i) {
|
||||
set(lo + i, other.get(i));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
tbv* tbv_manager::allocate(rational const& r) {
|
||||
if (r.is_uint64()) {
|
||||
|
|
@ -113,10 +135,28 @@ bool tbv_manager::set_and(tbv& dst, tbv const& src) const {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
tbv& tbv_manager::set_neg(tbv& dst) const {
|
||||
m.set_neg(dst);
|
||||
return dst;
|
||||
|
||||
void tbv_manager::complement(tbv const& src, ptr_vector<tbv>& result) {
|
||||
tbv* r;
|
||||
unsigned n = num_tbits();
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
switch (src.get(i)) {
|
||||
case BIT_0:
|
||||
r = allocate(src);
|
||||
r->set(i, BIT_1);
|
||||
result.push_back(r);
|
||||
break;
|
||||
case BIT_1:
|
||||
r = allocate(src);
|
||||
r->set(i, BIT_0);
|
||||
result.push_back(r);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool tbv_manager::equals(tbv const& a, tbv const& b) const {
|
||||
return m.equals(a, b);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@ Revision History:
|
|||
class tbv;
|
||||
|
||||
class tbv_manager {
|
||||
friend class tbv;
|
||||
static const unsigned BIT_0 = 0x1;
|
||||
static const unsigned BIT_1 = 0x2;
|
||||
static const unsigned BIT_x = 0x3;
|
||||
|
|
@ -54,7 +55,7 @@ public:
|
|||
tbv& fillX(tbv& bv) const;
|
||||
bool set_and(tbv& dst, tbv const& src) const;
|
||||
tbv& set_or(tbv& dst, tbv const& src) const;
|
||||
tbv& set_neg(tbv& dst) const;
|
||||
void complement(tbv const& src, ptr_vector<tbv>& result);
|
||||
bool equals(tbv const& a, tbv const& b) const;
|
||||
unsigned hash(tbv const& src) const;
|
||||
bool contains(tbv const& a, tbv const& b) const;
|
||||
|
|
@ -65,8 +66,14 @@ public:
|
|||
class tbv: private fixed_bit_vector {
|
||||
friend class fixed_bit_vector_manager;
|
||||
friend class tbv_manager;
|
||||
|
||||
public:
|
||||
|
||||
static const unsigned BIT_0 = tbv_manager::BIT_0;
|
||||
static const unsigned BIT_1 = tbv_manager::BIT_1;
|
||||
static const unsigned BIT_x = tbv_manager::BIT_x;
|
||||
static const unsigned BIT_z = tbv_manager::BIT_z;
|
||||
|
||||
struct eq {
|
||||
tbv_manager& m;
|
||||
eq(tbv_manager& m):m(m) {}
|
||||
|
|
@ -83,13 +90,19 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
private:
|
||||
void set(uint64 n, unsigned hi, unsigned lo);
|
||||
void set(rational const& r, unsigned hi, unsigned lo);
|
||||
void set(tbv const& other, unsigned hi, unsigned lo);
|
||||
|
||||
unsigned operator[](unsigned idx) { return get(idx); }
|
||||
void set(unsigned index, unsigned value) {
|
||||
SASSERT(value <= 3);
|
||||
fixed_bit_vector::set(2*index, (value & 2) != 0);
|
||||
fixed_bit_vector::set(2*index+1, (value & 1) != 0);
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
unsigned get(unsigned index) const {
|
||||
index *= 2;
|
||||
return (fixed_bit_vector::get(index) << 1) | (unsigned)fixed_bit_vector::get(index+1);
|
||||
|
|
|
|||
274
src/muz/ddnf/udoc_relation.cpp
Normal file
274
src/muz/ddnf/udoc_relation.cpp
Normal file
|
|
@ -0,0 +1,274 @@
|
|||
#include "udoc_relation.h"
|
||||
#include "dl_relation_manager.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
udoc_relation::udoc_relation(udoc_plugin& p, relation_signature const& sig):
|
||||
relation_base(p, sig),
|
||||
dm(p.dm(num_signature_bits(p.bv, sig))) {
|
||||
unsigned column = 0;
|
||||
for (unsigned i = 0; i < sig.size(); ++i) {
|
||||
m_column_info.push_back(column);
|
||||
column += p.bv.get_bv_size(sig[i]);
|
||||
}
|
||||
m_column_info.push_back(column);
|
||||
}
|
||||
udoc_relation::~udoc_relation() {
|
||||
reset();
|
||||
}
|
||||
unsigned udoc_relation::num_signature_bits(bv_util& bv, relation_signature const& sig) {
|
||||
unsigned result = 0;
|
||||
for (unsigned i = 0; i < sig.size(); ++i) {
|
||||
result += bv.get_bv_size(sig[i]);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
void udoc_relation::reset() {
|
||||
m_elems.reset(dm);
|
||||
}
|
||||
void udoc_relation::expand_column_vector(unsigned_vector& v, udoc_relation* other) const {
|
||||
unsigned_vector orig;
|
||||
orig.swap(v);
|
||||
for (unsigned i = 0; i < orig.size(); ++i) {
|
||||
unsigned col, limit;
|
||||
if (orig[i] < get_num_cols()) {
|
||||
col = column_idx(orig[i]);
|
||||
limit = col + column_num_bits(orig[i]);
|
||||
} else {
|
||||
unsigned idx = orig[i] - get_num_cols();
|
||||
col = get_num_bits() + other->column_idx(idx);
|
||||
limit = col + other->column_num_bits(idx);
|
||||
}
|
||||
for (; col < limit; ++col) {
|
||||
v.push_back(col);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
doc* udoc_relation::fact2doc(const relation_fact & f) const {
|
||||
doc* d = dm.allocate0();
|
||||
for (unsigned i = 0; i < f.size(); ++i) {
|
||||
unsigned bv_size;
|
||||
rational val;
|
||||
VERIFY(get_plugin().bv.is_numeral(f[i], val, bv_size));
|
||||
SASSERT(bv_size == column_num_bits(i));
|
||||
unsigned lo = column_idx(i);
|
||||
unsigned hi = column_idx(i + 1);
|
||||
d->pos().set(val, hi, lo);
|
||||
}
|
||||
return d;
|
||||
}
|
||||
void udoc_relation::add_fact(const relation_fact & f) {
|
||||
doc* d = fact2doc(f);
|
||||
m_elems.insert(dm, d);
|
||||
}
|
||||
bool udoc_relation::contains_fact(const relation_fact & f) const {
|
||||
doc_ref d(dm, fact2doc(f));
|
||||
return m_elems.contains(dm, *d);
|
||||
}
|
||||
udoc_relation * udoc_relation::clone() const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
udoc_relation * udoc_relation::complement(func_decl* f) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
void udoc_relation::to_formula(expr_ref& fml) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
udoc_plugin& udoc_relation::get_plugin() const {
|
||||
return static_cast<udoc_plugin&>(relation_base::get_plugin());
|
||||
}
|
||||
|
||||
void udoc_relation::display(std::ostream& out) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
// -------------
|
||||
|
||||
udoc_plugin::udoc_plugin(relation_manager& rm):
|
||||
relation_plugin(udoc_plugin::get_name(), rm),
|
||||
m(rm.get_context().get_manager()),
|
||||
bv(m) {
|
||||
}
|
||||
udoc_plugin::~udoc_plugin() {
|
||||
u_map<doc_manager*>::iterator it = m_dms.begin(), end = m_dms.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
}
|
||||
udoc_relation& udoc_plugin::get(relation_base& r) {
|
||||
return dynamic_cast<udoc_relation&>(r);
|
||||
}
|
||||
udoc_relation* udoc_plugin::get(relation_base* r) {
|
||||
return r?dynamic_cast<udoc_relation*>(r):0;
|
||||
}
|
||||
udoc_relation const & udoc_plugin::get(relation_base const& r) {
|
||||
return dynamic_cast<udoc_relation const&>(r);
|
||||
}
|
||||
|
||||
doc_manager& udoc_plugin::dm(unsigned n) {
|
||||
doc_manager* r;
|
||||
if (!m_dms.find(n, r)) {
|
||||
r = alloc(doc_manager, n);
|
||||
m_dms.insert(n, r);
|
||||
}
|
||||
return *r;
|
||||
}
|
||||
bool udoc_plugin::can_handle_signature(const relation_signature & s) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
}
|
||||
relation_base * udoc_plugin::mk_empty(const relation_signature & s) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_base * udoc_plugin::mk_full(func_decl* p, const relation_signature & s) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
class udoc_plugin::join_fn : public convenient_relation_join_fn {
|
||||
doc_manager& dm;
|
||||
doc_manager& dm1;
|
||||
doc_manager& dm2;
|
||||
public:
|
||||
join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
|
||||
const unsigned * cols1, const unsigned * cols2)
|
||||
: convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
|
||||
dm(p.dm(get_result_signature())),
|
||||
dm1(t1.get_dm()),
|
||||
dm2(t2.get_dm()) {
|
||||
t1.expand_column_vector(m_cols1);
|
||||
t2.expand_column_vector(m_cols2);
|
||||
}
|
||||
|
||||
void join(doc const& d1, doc const& d2, udoc& result) {
|
||||
doc* d = dm.allocateX();
|
||||
tbv& pos = d->pos();
|
||||
utbv& neg = d->neg();
|
||||
unsigned mid = dm1.num_tbits();
|
||||
unsigned hi = dm.num_tbits();
|
||||
pos.set(d1.pos(), mid-1, 0);
|
||||
pos.set(d2.pos(), hi-1, mid);
|
||||
// first fix bits
|
||||
for (unsigned i = 0; i < m_cols1.size(); ++i) {
|
||||
unsigned idx1 = m_cols1[i];
|
||||
unsigned idx2 = mid + m_cols2[i];
|
||||
unsigned v1 = pos[idx1];
|
||||
unsigned v2 = pos[idx2];
|
||||
|
||||
if (v1 == tbv::BIT_x) {
|
||||
if (v2 != tbv::BIT_x)
|
||||
pos.set(idx1, v2);
|
||||
} else if (v2 == tbv::BIT_x) {
|
||||
pos.set(idx2, v1);
|
||||
} else if (v1 != v2) {
|
||||
dm.deallocate(d);
|
||||
// columns don't match
|
||||
return;
|
||||
}
|
||||
}
|
||||
// fix equality of don't care columns
|
||||
for (unsigned i = 0; i < m_cols1.size(); ++i) {
|
||||
unsigned idx1 = m_cols1[i];
|
||||
unsigned idx2 = mid + m_cols2[i];
|
||||
unsigned v1 = pos[idx1];
|
||||
unsigned v2 = pos[idx2];
|
||||
|
||||
if (v1 == tbv::BIT_x && v2 == tbv::BIT_x) {
|
||||
// add to subtracted TBVs: 1xx0 and 0xx1
|
||||
tbv* r = dm.tbv().allocate(pos);
|
||||
r->set(idx1, tbv::BIT_0);
|
||||
r->set(idx2, tbv::BIT_1);
|
||||
neg.push_back(r);
|
||||
|
||||
r = dm.tbv().allocate(pos);
|
||||
r->set(idx1, tbv::BIT_1);
|
||||
r->set(idx2, tbv::BIT_0);
|
||||
neg.push_back(r);
|
||||
}
|
||||
}
|
||||
|
||||
// handle subtracted TBVs: 1010 -> 1010xxx
|
||||
for (unsigned i = 0; i < d1.neg().size(); ++i) {
|
||||
tbv* t = dm.tbv().allocate();
|
||||
t->set(d1.neg()[i], mid-1, 0);
|
||||
t->set(d2.pos(), hi - 1, mid);
|
||||
neg.push_back(t);
|
||||
}
|
||||
for (unsigned i = 0; i < d2.neg().size(); ++i) {
|
||||
tbv* t = dm.tbv().allocate();
|
||||
t->set(d1.pos(), mid-1, 0);
|
||||
t->set(d2.neg()[i], hi - 1, mid);
|
||||
neg.push_back(t);
|
||||
}
|
||||
result.insert(dm, d);
|
||||
}
|
||||
|
||||
virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {
|
||||
udoc_relation const& r1 = get(_r1);
|
||||
udoc_relation const& r2 = get(_r2);
|
||||
udoc_plugin& p = r1.get_plugin();
|
||||
relation_signature const& sig = get_result_signature();
|
||||
udoc_relation * result = alloc(udoc_relation, p, sig);
|
||||
udoc const& d1 = r1.get_udoc();
|
||||
udoc const& d2 = r2.get_udoc();
|
||||
udoc& r = result->get_udoc();
|
||||
for (unsigned i = 0; i < d1.size(); ++i) {
|
||||
for (unsigned j = 0; j < d2.size(); ++j) {
|
||||
join(d1[i], d2[j], r);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
};
|
||||
relation_join_fn * udoc_plugin::mk_join_fn(
|
||||
const relation_base & t1, const relation_base & t2,
|
||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
|
||||
if (!check_kind(t1) || !check_kind(t2)) {
|
||||
return 0;
|
||||
}
|
||||
return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2);
|
||||
}
|
||||
relation_transformer_fn * udoc_plugin::mk_project_fn(
|
||||
const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * removed_cols) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_transformer_fn * udoc_plugin::mk_rename_fn(
|
||||
const relation_base & t, unsigned permutation_cycle_len,
|
||||
const unsigned * permutation_cycle) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_union_fn * udoc_plugin::mk_union_fn(
|
||||
const relation_base & tgt, const relation_base & src,
|
||||
const relation_base * delta) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_union_fn * udoc_plugin::mk_widen_fn(
|
||||
const relation_base & tgt, const relation_base & src,
|
||||
const relation_base * delta) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_mutator_fn * udoc_plugin::mk_filter_identical_fn(
|
||||
const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * identical_cols) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_mutator_fn * udoc_plugin::mk_filter_equal_fn(
|
||||
const relation_base & t, const relation_element & value, unsigned col) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
|
||||
}
|
||||
110
src/muz/ddnf/udoc_relation.h
Normal file
110
src/muz/ddnf/udoc_relation.h
Normal file
|
|
@ -0,0 +1,110 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
udoc_relation.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Relation based on union of DOCs.
|
||||
|
||||
Author:
|
||||
|
||||
Nuno Lopes (a-nlopes) 2013-03-01
|
||||
Nikolaj Bjorner (nbjorner) 2014-09-15
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _UDOC_RELATION_H_
|
||||
#define _UDOC_RELATION_H_
|
||||
|
||||
#include "doc.h"
|
||||
#include "dl_base.h"
|
||||
|
||||
namespace datalog {
|
||||
class udoc_plugin;
|
||||
class udoc_relation;
|
||||
|
||||
class udoc_relation : public relation_base {
|
||||
friend class udoc_relation;
|
||||
doc_manager& dm;
|
||||
udoc m_elems;
|
||||
unsigned_vector m_column_info;
|
||||
static unsigned num_signature_bits(bv_util& bv, relation_signature const& sig);
|
||||
doc* fact2doc(relation_fact const& f) const;
|
||||
public:
|
||||
udoc_relation(udoc_plugin& p, relation_signature const& s);
|
||||
virtual ~udoc_relation();
|
||||
virtual void reset();
|
||||
virtual void add_fact(const relation_fact & f);
|
||||
virtual bool contains_fact(const relation_fact & f) const;
|
||||
virtual udoc_relation * clone() const;
|
||||
virtual udoc_relation * complement(func_decl*) const;
|
||||
virtual void to_formula(expr_ref& fml) const;
|
||||
udoc_plugin& get_plugin() const;
|
||||
virtual bool empty() const { return m_elems.empty(); }
|
||||
virtual void display(std::ostream& out) const;
|
||||
virtual bool is_precise() const { return true; }
|
||||
|
||||
doc_manager& get_dm() const { return dm; }
|
||||
udoc const& get_udoc() const { return m_elems; }
|
||||
udoc& get_udoc() { return m_elems; }
|
||||
unsigned get_num_bits() const { return m_column_info.back(); }
|
||||
unsigned get_num_cols() const { return m_column_info.size()-1; }
|
||||
unsigned column_idx(unsigned col) const { return m_column_info[col]; }
|
||||
unsigned column_num_bits(unsigned col) const { return m_column_info[col+1] - m_column_info[col]; }
|
||||
void expand_column_vector(unsigned_vector& v, udoc_relation* other = 0) const;
|
||||
};
|
||||
|
||||
class udoc_plugin : public relation_plugin {
|
||||
friend class udoc_relation;
|
||||
class join_fn;
|
||||
class project_fn;
|
||||
class union_fn;
|
||||
class rename_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;
|
||||
u_map<doc_manager*> m_dms;
|
||||
doc_manager& dm(unsigned sz);
|
||||
doc_manager& dm(relation_signature const& sig);
|
||||
static udoc_relation& get(relation_base& r);
|
||||
static udoc_relation* get(relation_base* r);
|
||||
static udoc_relation const & get(relation_base const& r);
|
||||
|
||||
public:
|
||||
udoc_plugin(relation_manager& rm);
|
||||
~udoc_plugin();
|
||||
virtual bool can_handle_signature(const relation_signature & s);
|
||||
static symbol get_name() { return symbol("doc"); }
|
||||
virtual relation_base * mk_empty(const relation_signature & s);
|
||||
virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
|
||||
virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
|
||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
|
||||
virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * removed_cols);
|
||||
virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len,
|
||||
const unsigned * permutation_cycle);
|
||||
virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src,
|
||||
const relation_base * delta);
|
||||
virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src,
|
||||
const relation_base * delta);
|
||||
virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * identical_cols);
|
||||
virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value,
|
||||
unsigned col);
|
||||
virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
|
||||
// project join select
|
||||
};
|
||||
};
|
||||
|
||||
#endif /* _UDOC_RELATION_H_ */
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue