mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
Nikolaj Bjorner
commit
58229f4c8e
27 changed files with 196 additions and 708 deletions
|
|
@ -61,13 +61,14 @@ namespace datalog {
|
|||
void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
|
||||
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
|
||||
relation_signature aux_sig;
|
||||
relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(),
|
||||
vars.get_cols1(), vars.get_cols2(), aux_sig);
|
||||
relation_signature sig1 = m_reg_signatures[t1];
|
||||
relation_signature sig2 = m_reg_signatures[t2];
|
||||
relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig);
|
||||
relation_signature res_sig;
|
||||
relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(),
|
||||
res_sig);
|
||||
|
||||
result = get_fresh_register(res_sig);
|
||||
|
||||
acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(),
|
||||
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
|
||||
}
|
||||
|
|
@ -798,6 +799,8 @@ namespace datalog {
|
|||
typedef rule_dependencies::item_set item_set; //set of T
|
||||
|
||||
rule_dependencies & m_deps;
|
||||
rule_set const& m_rules;
|
||||
context& m_context;
|
||||
item_set & m_removed;
|
||||
svector<T> m_stack;
|
||||
ast_mark m_stack_content;
|
||||
|
|
@ -820,7 +823,7 @@ namespace datalog {
|
|||
T d = *it;
|
||||
if(m_stack_content.is_marked(d)) {
|
||||
//TODO: find the best vertex to remove in the cycle
|
||||
m_removed.insert(v);
|
||||
remove_from_stack();
|
||||
break;
|
||||
}
|
||||
traverse(d);
|
||||
|
|
@ -830,9 +833,36 @@ namespace datalog {
|
|||
m_stack.pop_back();
|
||||
m_stack_content.mark(v, false);
|
||||
}
|
||||
|
||||
void remove_from_stack() {
|
||||
for (unsigned i = 0; i < m_stack.size(); ++i) {
|
||||
func_decl* p = m_stack[i];
|
||||
rule_vector const& rules = m_rules.get_predicate_rules(p);
|
||||
unsigned stratum = m_rules.get_predicate_strat(p);
|
||||
if (m_context.has_facts(p)) {
|
||||
m_removed.insert(p);
|
||||
return;
|
||||
}
|
||||
for (unsigned j = 0; j < rules.size(); ++j) {
|
||||
rule const& r = *rules[j];
|
||||
bool ok = true;
|
||||
for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
|
||||
ok &= m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
|
||||
}
|
||||
if (ok) {
|
||||
m_removed.insert(p);
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// nothing was found.
|
||||
m_removed.insert(m_stack.back());
|
||||
|
||||
}
|
||||
public:
|
||||
cycle_breaker(rule_dependencies & deps, item_set & removed)
|
||||
: m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); }
|
||||
cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed)
|
||||
: m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }
|
||||
|
||||
void operator()() {
|
||||
rule_dependencies::iterator it = m_deps.begin();
|
||||
|
|
@ -854,7 +884,7 @@ namespace datalog {
|
|||
|
||||
rule_dependencies deps(m_rule_set.get_dependencies());
|
||||
deps.restrict(preds);
|
||||
cycle_breaker(deps, global_deltas)();
|
||||
cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
|
||||
VERIFY( deps.sort_deps(ordered_preds) );
|
||||
|
||||
//the predicates that were removed to get acyclic induced subgraph are put last
|
||||
|
|
@ -892,6 +922,40 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void compiler::compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
|
||||
const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) {
|
||||
func_decl_vector::const_iterator hpit = head_preds.begin();
|
||||
func_decl_vector::const_iterator hpend = head_preds.end();
|
||||
reg_idx void_reg = execution_context::void_register;
|
||||
for(; hpit!=hpend; ++hpit) {
|
||||
func_decl * head_pred = *hpit;
|
||||
const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred);
|
||||
rule_vector::const_iterator rit = pred_rules.begin();
|
||||
rule_vector::const_iterator rend = pred_rules.end();
|
||||
unsigned stratum = m_rule_set.get_predicate_strat(head_pred);
|
||||
|
||||
for(; rit != rend; ++rit) {
|
||||
rule * r = *rit;
|
||||
SASSERT(head_pred==r->get_decl());
|
||||
|
||||
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
|
||||
unsigned stratum1 = m_rule_set.get_predicate_strat(r->get_decl(i));
|
||||
if (stratum1 >= stratum) {
|
||||
goto next_loop;
|
||||
}
|
||||
}
|
||||
compile_rule_evaluation(r, input_deltas, void_reg, false, acc);
|
||||
next_loop:
|
||||
;
|
||||
}
|
||||
|
||||
reg_idx d_head_reg;
|
||||
if (output_deltas.find(head_pred, d_head_reg)) {
|
||||
acc.push_back(instruction::mk_clone(m_pred_regs.find(head_pred), d_head_reg));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void compiler::make_inloop_delta_transition(const pred2idx & global_head_deltas,
|
||||
const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc) {
|
||||
//move global head deltas into tail ones
|
||||
|
|
@ -942,7 +1006,7 @@ namespace datalog {
|
|||
const pred2idx * input_deltas, const pred2idx & output_deltas,
|
||||
bool add_saturation_marks, instruction_block & acc) {
|
||||
|
||||
if(!output_deltas.empty()) {
|
||||
if (!output_deltas.empty()) {
|
||||
func_decl_set::iterator hpit = head_preds.begin();
|
||||
func_decl_set::iterator hpend = head_preds.end();
|
||||
for(; hpit!=hpend; ++hpit) {
|
||||
|
|
@ -979,7 +1043,8 @@ namespace datalog {
|
|||
func_decl_set empty_func_decl_set;
|
||||
|
||||
//generate code for the initial run
|
||||
compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
|
||||
// compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
|
||||
compile_preds_init(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
|
||||
|
||||
if (compile_with_widening()) {
|
||||
compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc);
|
||||
|
|
|
|||
|
|
@ -209,6 +209,12 @@ namespace datalog {
|
|||
void compile_preds(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
|
||||
const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc);
|
||||
|
||||
/**
|
||||
\brief Generate code to evaluate predicates in a stratum based on their non-recursive rules.
|
||||
*/
|
||||
void compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
|
||||
const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc);
|
||||
|
||||
void make_inloop_delta_transition(const pred2idx & global_head_deltas,
|
||||
const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc);
|
||||
void compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
|
||||
|
|
|
|||
|
|
@ -814,16 +814,15 @@ namespace datalog {
|
|||
|
||||
void context::transform_rules() {
|
||||
m_transf.reset();
|
||||
m_transf.register_plugin(alloc(mk_filter_rules,*this));
|
||||
m_transf.register_plugin(alloc(mk_simple_joins,*this));
|
||||
|
||||
if (unbound_compressor()) {
|
||||
m_transf.register_plugin(alloc(mk_unbound_compressor,*this));
|
||||
if (get_params().filter_rules()) {
|
||||
m_transf.register_plugin(alloc(mk_filter_rules, *this));
|
||||
}
|
||||
m_transf.register_plugin(alloc(mk_simple_joins, *this));
|
||||
if (unbound_compressor()) {
|
||||
m_transf.register_plugin(alloc(mk_unbound_compressor, *this));
|
||||
}
|
||||
|
||||
if (similarity_compressor()) {
|
||||
m_transf.register_plugin(alloc(mk_similarity_compressor, *this,
|
||||
similarity_compressor_threshold()));
|
||||
m_transf.register_plugin(alloc(mk_similarity_compressor, *this));
|
||||
}
|
||||
m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
|
||||
|
||||
|
|
|
|||
|
|
@ -452,7 +452,7 @@ namespace datalog {
|
|||
|
||||
|
||||
class instr_filter_identical : public instruction {
|
||||
typedef vector<unsigned> column_vector;
|
||||
typedef unsigned_vector column_vector;
|
||||
reg_idx m_reg;
|
||||
column_vector m_cols;
|
||||
public:
|
||||
|
|
@ -651,7 +651,7 @@ namespace datalog {
|
|||
|
||||
|
||||
class instr_project_rename : public instruction {
|
||||
typedef vector<unsigned> column_vector;
|
||||
typedef unsigned_vector column_vector;
|
||||
bool m_projection;
|
||||
reg_idx m_src;
|
||||
column_vector m_cols;
|
||||
|
|
@ -723,7 +723,8 @@ namespace datalog {
|
|||
instr_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, const unsigned * cols1,
|
||||
const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, reg_idx result)
|
||||
: m_rel1(rel1), m_rel2(rel2), m_cols1(joined_col_cnt, cols1),
|
||||
m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) {}
|
||||
m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) {
|
||||
}
|
||||
virtual bool perform(execution_context & ctx) {
|
||||
ctx.make_empty(m_res);
|
||||
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
|
||||
|
|
@ -830,7 +831,7 @@ namespace datalog {
|
|||
|
||||
|
||||
class instr_filter_by_negation : public instruction {
|
||||
typedef vector<unsigned> column_vector;
|
||||
typedef unsigned_vector column_vector;
|
||||
reg_idx m_tgt;
|
||||
reg_idx m_neg_rel;
|
||||
column_vector m_cols1;
|
||||
|
|
|
|||
|
|
@ -152,7 +152,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
rule_set * mk_filter_rules::operator()(rule_set const & source) {
|
||||
// TODO mc, pc
|
||||
if (!m_context.get_params().filter_rules()) {
|
||||
return 0;
|
||||
}
|
||||
m_tail2filter.reset();
|
||||
m_result = alloc(rule_set, m_context);
|
||||
m_modified = false;
|
||||
|
|
|
|||
|
|
@ -23,14 +23,14 @@ Revision History:
|
|||
|
||||
namespace datalog {
|
||||
|
||||
mk_similarity_compressor::mk_similarity_compressor(context & ctx, unsigned threshold_count) :
|
||||
mk_similarity_compressor::mk_similarity_compressor(context & ctx) :
|
||||
plugin(5000),
|
||||
m_context(ctx),
|
||||
m_manager(ctx.get_manager()),
|
||||
m_threshold_count(threshold_count),
|
||||
m_threshold_count(ctx.similarity_compressor_threshold()),
|
||||
m_result_rules(ctx.get_rule_manager()),
|
||||
m_pinned(m_manager) {
|
||||
SASSERT(threshold_count>1);
|
||||
SASSERT(m_threshold_count>1);
|
||||
}
|
||||
|
||||
void mk_similarity_compressor::reset() {
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ namespace datalog {
|
|||
|
||||
void reset();
|
||||
public:
|
||||
mk_similarity_compressor(context & ctx, unsigned threshold_count);
|
||||
mk_similarity_compressor(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source);
|
||||
};
|
||||
|
|
|
|||
|
|
@ -316,6 +316,12 @@ namespace datalog {
|
|||
}
|
||||
container[i-ofs] = container[i];
|
||||
}
|
||||
if (r_i != removed_col_cnt) {
|
||||
for (unsigned i = 0; i < removed_col_cnt; ++i) {
|
||||
std::cout << removed_cols[i] << " ";
|
||||
}
|
||||
std::cout << " container size: " << n << "\n";
|
||||
}
|
||||
SASSERT(r_i==removed_col_cnt);
|
||||
container.resize(n-removed_col_cnt);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,311 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
fdd.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Finite decision diagram trie.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-07-03.
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "fdd.h"
|
||||
#include "hash.h"
|
||||
#include "bit_vector.h"
|
||||
#include "trace.h"
|
||||
|
||||
#define OFFSET_OF(th, ty, field) (unsigned char*)(&((ty*)(th))->field) - (unsigned char*)(ty*)(th)
|
||||
|
||||
using namespace fdd;
|
||||
|
||||
unsigned node::get_hash() const {
|
||||
return string_hash((char*)this, static_cast<unsigned>(OFFSET_OF(this, node, m_ref_count)), 11);
|
||||
}
|
||||
|
||||
bool node::operator==(node const& other) const {
|
||||
return
|
||||
m_var == other.m_var &&
|
||||
m_lo == other.m_lo &&
|
||||
m_hi == other.m_hi;
|
||||
}
|
||||
|
||||
|
||||
// ------------------------------------------
|
||||
// manager
|
||||
|
||||
manager::manager() :
|
||||
m_alloc_node(2),
|
||||
m_false(0),
|
||||
m_true(1),
|
||||
m_root(m_false)
|
||||
{
|
||||
m_nodes.push_back(node()); // false
|
||||
m_nodes.push_back(node()); // true
|
||||
inc_ref(m_false);
|
||||
inc_ref(m_true);
|
||||
alloc_node(); // pre-allocate a node.
|
||||
}
|
||||
|
||||
manager::~manager() {
|
||||
}
|
||||
|
||||
void manager::alloc_node() {
|
||||
unsigned index;
|
||||
while (!m_free.empty()) {
|
||||
index = m_free.back();
|
||||
node& n = m_nodes[index];
|
||||
m_free.pop_back();
|
||||
if (n.get_ref_count() == 0) {
|
||||
if (!is_leaf(n.lo())) {
|
||||
m_free.push_back(n.lo());
|
||||
}
|
||||
if (!is_leaf(n.hi())) {
|
||||
m_free.push_back(n.hi());
|
||||
}
|
||||
m_alloc_node = index;
|
||||
m_table.erase(n);
|
||||
return;
|
||||
}
|
||||
}
|
||||
index = m_nodes.size();
|
||||
m_nodes.push_back(node());
|
||||
m_alloc_node = index;
|
||||
}
|
||||
|
||||
node_id manager::mk_node(unsigned var, node_id lo, node_id hi) {
|
||||
if (lo == hi) {
|
||||
return lo;
|
||||
}
|
||||
node n(var, lo, hi);
|
||||
unsigned index = m_alloc_node;
|
||||
|
||||
node_id result = m_table.insert_if_not_there(n, index).m_value;
|
||||
|
||||
if (result == index) {
|
||||
alloc_node();
|
||||
m_nodes[result] = n;
|
||||
inc_ref(lo);
|
||||
inc_ref(hi);
|
||||
}
|
||||
|
||||
TRACE("fdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";);
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
void manager::inc_ref(node_id n) {
|
||||
TRACE("fdd", tout << "incref: " << n << "\n";);
|
||||
if (!is_leaf(n)) {
|
||||
m_nodes[n].inc_ref();
|
||||
}
|
||||
}
|
||||
|
||||
void manager::dec_ref(node_id n) {
|
||||
if (!is_leaf(n) && 0 == m_nodes[n].dec_ref()) {
|
||||
m_free.push_back(n);
|
||||
}
|
||||
}
|
||||
|
||||
void manager::setup_keys(Key const* keys) {
|
||||
for (unsigned i = 0; i < m_num_keys; ++i) {
|
||||
m_keys[i] = (uint64)keys[i];
|
||||
m_sign[i] = keys[i] < 0;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void manager::insert(Key const* keys) {
|
||||
setup_keys(keys);
|
||||
m_insert_cache.reset();
|
||||
node_id result = insert_sign(m_num_idx + m_num_keys, m_root);
|
||||
inc_ref(result);
|
||||
dec_ref(m_root);
|
||||
m_root = result;
|
||||
}
|
||||
|
||||
node_id manager::insert_sign(unsigned idx, node_id n) {
|
||||
if (idx > m_num_idx) {
|
||||
--idx;
|
||||
bool s = idx2sign(idx);
|
||||
node nd = m_nodes[n];
|
||||
if (!is_leaf(n) && nd.var() == idx) {
|
||||
if (s) {
|
||||
return mk_node(idx, insert_sign(idx, nd.lo()), nd.hi());
|
||||
}
|
||||
else {
|
||||
return mk_node(idx, nd.lo(), insert_sign(idx, nd.hi()));
|
||||
}
|
||||
}
|
||||
else {
|
||||
if (s) {
|
||||
return mk_node(idx, insert_sign(idx, n), n);
|
||||
}
|
||||
else {
|
||||
return mk_node(idx, n, insert_sign(idx, n));
|
||||
}
|
||||
}
|
||||
}
|
||||
SASSERT(m_num_idx == idx);
|
||||
return insert(idx, n);
|
||||
}
|
||||
|
||||
node_id manager::insert(unsigned idx, node_id n) {
|
||||
node_id result;
|
||||
SASSERT(0 <= idx && idx <= m_num_idx);
|
||||
TRACE("fdd", tout << "insert: " << idx << " " << n << "\n";);
|
||||
if (is_leaf(n)) {
|
||||
while (idx > 0) {
|
||||
--idx;
|
||||
if (idx2bit(idx) && !is_dont_care(idx2key(idx))) {
|
||||
return mk_node(idx, n, insert(idx, n));
|
||||
}
|
||||
}
|
||||
return m_true;
|
||||
}
|
||||
|
||||
SASSERT(0 < idx);
|
||||
--idx;
|
||||
|
||||
config c(m_dont_cares, idx, n);
|
||||
if (m_insert_cache.find(c, result)) {
|
||||
return result;
|
||||
}
|
||||
|
||||
node nd = m_nodes[n];
|
||||
SASSERT(idx >= nd.var());
|
||||
while (idx > nd.var()) {
|
||||
if (idx2bit(idx) && !is_dont_care(idx2key(idx))) {
|
||||
return mk_node(idx, n, insert(idx, n));
|
||||
}
|
||||
--idx;
|
||||
}
|
||||
SASSERT(nd.var() == idx);
|
||||
unsigned key = idx2key(idx);
|
||||
if (is_dont_care(key)) {
|
||||
result = mk_node(idx, insert(idx, nd.lo()), insert(idx, nd.hi()));
|
||||
}
|
||||
else {
|
||||
bool bit = idx2bit(idx);
|
||||
node_id lo, hi;
|
||||
if (bit) {
|
||||
hi = insert(idx, nd.hi());
|
||||
lo = nd.lo();
|
||||
}
|
||||
else {
|
||||
lo = insert(idx, nd.lo());
|
||||
scoped_dont_cares _set(*this, key);
|
||||
hi = insert(idx, nd.hi());
|
||||
}
|
||||
result = mk_node(idx, lo, hi);
|
||||
}
|
||||
m_insert_cache.insert(c, result);
|
||||
return result;
|
||||
}
|
||||
|
||||
void manager::set_dont_care(unsigned key) {
|
||||
SASSERT(!is_dont_care(key));
|
||||
m_dont_cares |= (1ull << key);
|
||||
}
|
||||
|
||||
void manager::unset_dont_care(unsigned key) {
|
||||
m_dont_cares &= ~(1ull << key);
|
||||
}
|
||||
|
||||
bool manager::is_dont_care(unsigned key) const {
|
||||
return 0 != (m_dont_cares & (1ull << key));
|
||||
}
|
||||
|
||||
void manager::collect_statistics(statistics& st) const {
|
||||
st.update("fdd.num_nodes", m_nodes.size());
|
||||
}
|
||||
|
||||
|
||||
void manager::reset(unsigned num_keys) {
|
||||
m_num_keys = num_keys;
|
||||
m_num_idx = m_num_keys * m_num_bits;
|
||||
m_dont_cares = 0;
|
||||
m_sign.resize(num_keys);
|
||||
m_keys.resize(num_keys);
|
||||
SASSERT(num_keys <= 8*sizeof(m_dont_cares));
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool manager::find_le(Key const* keys) {
|
||||
setup_keys(keys);
|
||||
unsigned idx = m_num_idx + m_num_keys;
|
||||
node_id n = m_root;
|
||||
node nc = m_nodes[n];
|
||||
while (n > 1 && idx > m_num_idx) {
|
||||
--idx;
|
||||
if (nc.var() == idx) {
|
||||
if (idx2sign(idx)) {
|
||||
n = nc.lo();
|
||||
}
|
||||
else {
|
||||
n = nc.hi();
|
||||
}
|
||||
nc = m_nodes[n];
|
||||
}
|
||||
}
|
||||
while (n > 1) {
|
||||
SASSERT(idx > 0);
|
||||
--idx;
|
||||
while (nc.var() < idx) {
|
||||
if (idx2bit(idx) && is_dont_care(idx2key(idx))) {
|
||||
set_dont_care(idx2key(idx));
|
||||
}
|
||||
--idx;
|
||||
}
|
||||
SASSERT(nc.var() == idx);
|
||||
if (is_dont_care(idx2key(idx)) || idx2bit(idx)) {
|
||||
n = nc.hi();
|
||||
}
|
||||
else {
|
||||
n = nc.lo();
|
||||
}
|
||||
nc = m_nodes[n];
|
||||
}
|
||||
m_dont_cares = 0;
|
||||
return n == 1;
|
||||
}
|
||||
|
||||
|
||||
std::ostream& manager::display(std::ostream& out, node_id n) const{
|
||||
svector<bool> mark;
|
||||
svector<node_id> nodes;
|
||||
nodes.push_back(n);
|
||||
while (!nodes.empty()) {
|
||||
n = nodes.back();
|
||||
nodes.pop_back();
|
||||
if (mark.size() <= n) {
|
||||
mark.resize(n+1, false);
|
||||
}
|
||||
node const& nc = m_nodes[n];
|
||||
if (is_leaf(n) || mark[n]) {
|
||||
continue;
|
||||
}
|
||||
nodes.push_back(nc.lo());
|
||||
nodes.push_back(nc.hi());
|
||||
mark[n] = true;
|
||||
|
||||
if (nc.var() >= m_num_idx) {
|
||||
out << n << " if " << idx2key(nc.var()) << " then " << nc.hi() << " else " << nc.lo() << "\n";
|
||||
}
|
||||
else {
|
||||
out << n << " if " << idx2key(nc.var()) << ":" << idx2bitnum(nc.var()) << " then " << nc.hi() << " else " << nc.lo() << "\n";
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
173
src/muz_qe/fdd.h
173
src/muz_qe/fdd.h
|
|
@ -1,173 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
fdd.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Finite decision diagram.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-07-03.
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef __FDD_H__
|
||||
#define __FDD_H__
|
||||
|
||||
#include "hashtable.h"
|
||||
#include "hash.h"
|
||||
#include "map.h"
|
||||
#include "vector.h"
|
||||
#include "statistics.h"
|
||||
|
||||
namespace fdd {
|
||||
|
||||
|
||||
typedef unsigned node_id;
|
||||
|
||||
class node {
|
||||
unsigned m_var;
|
||||
node_id m_lo;
|
||||
node_id m_hi;
|
||||
unsigned m_ref_count;
|
||||
void reset();
|
||||
public:
|
||||
node() : m_var(0), m_lo(0), m_hi(0), m_ref_count(0) {}
|
||||
node(unsigned var, node_id l, node_id h): m_var(var), m_lo(l), m_hi(h), m_ref_count(0) {}
|
||||
|
||||
unsigned get_hash() const;
|
||||
bool operator==(node const& other) const;
|
||||
|
||||
void inc_ref() { ++m_ref_count; }
|
||||
unsigned dec_ref() { return --m_ref_count; }
|
||||
unsigned get_ref_count() const { return m_ref_count; }
|
||||
node_id lo() const { return m_lo; }
|
||||
node_id hi() const { return m_hi; }
|
||||
unsigned var() const { return m_var; }
|
||||
|
||||
struct hash { unsigned operator()(node const& n) const { return n.get_hash(); } };
|
||||
struct eq { bool operator()(node const& l, node const& r) const { return l == r; } };
|
||||
std::ostream& display(std::ostream& out) const { return out << m_var << " " << m_lo << " " << m_hi << ""; }
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, node const& n) { return n.display(out); }
|
||||
|
||||
class config {
|
||||
uint64 m_dont_cares;
|
||||
unsigned m_idx;
|
||||
node_id m_node;
|
||||
public:
|
||||
|
||||
config(): m_dont_cares(0), m_idx(0), m_node(0) {}
|
||||
|
||||
config(uint64 dont_cares, unsigned idx, node_id n):
|
||||
m_dont_cares(dont_cares),
|
||||
m_idx(idx),
|
||||
m_node(n)
|
||||
{}
|
||||
|
||||
struct hash {
|
||||
unsigned operator()(config const& c) const {
|
||||
return string_hash((char*)&c, sizeof(c), 12);
|
||||
};
|
||||
};
|
||||
|
||||
struct eq {
|
||||
bool operator()(config const& a, config const& b) const {
|
||||
return
|
||||
a.m_dont_cares == b.m_dont_cares &&
|
||||
a.m_idx == b.m_idx &&
|
||||
a.m_node == b.m_node;
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
|
||||
class manager {
|
||||
public:
|
||||
typedef int64 Key;
|
||||
typedef node::hash node_hash;
|
||||
typedef node::eq node_eq;
|
||||
typedef config::hash config_hash;
|
||||
typedef config::eq config_eq;
|
||||
private:
|
||||
typedef map<node, unsigned, node_hash, node_eq> node_table;
|
||||
typedef map<config, node_id, config_hash, config_eq> insert_cache;
|
||||
node_table m_table;
|
||||
insert_cache m_insert_cache;
|
||||
svector<node> m_nodes;
|
||||
unsigned_vector m_free;
|
||||
unsigned m_alloc_node;
|
||||
node_id m_false;
|
||||
node_id m_true;
|
||||
node_id m_root;
|
||||
|
||||
static const unsigned m_num_bits = 64;
|
||||
unsigned m_num_keys;
|
||||
unsigned m_num_idx; // = m_num_keys * m_num_bits
|
||||
|
||||
// state associated with insert.
|
||||
svector<uint64> m_keys;
|
||||
svector<bool> m_sign;
|
||||
|
||||
uint64 m_dont_cares;
|
||||
|
||||
public:
|
||||
manager();
|
||||
~manager();
|
||||
|
||||
void reset(unsigned num_keys);
|
||||
|
||||
void insert(Key const* keys);
|
||||
|
||||
bool find_le(Key const* keys);
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
void reset_statistics() {}
|
||||
unsigned size() const { return m_nodes.size(); }
|
||||
|
||||
void display(std::ostream& out) const { display(out, m_root); }
|
||||
|
||||
private:
|
||||
void dec_ref(node_id n);
|
||||
void inc_ref(node_id n);
|
||||
node_id mk_node(unsigned var, node_id lo, node_id hi);
|
||||
inline unsigned get_ref_count(node_id n) { return m_nodes[n].get_ref_count(); }
|
||||
|
||||
std::ostream& display(std::ostream& out, node_id n) const;
|
||||
|
||||
void setup_keys(Key const* keys);
|
||||
node_id insert(unsigned idx, node_id n);
|
||||
node_id insert_sign(unsigned idx, node_id n);
|
||||
bool is_dont_care(unsigned idx) const;
|
||||
|
||||
void set_dont_care(unsigned key);
|
||||
void unset_dont_care(unsigned key);
|
||||
|
||||
struct scoped_dont_cares {
|
||||
manager& m;
|
||||
unsigned m_key;
|
||||
scoped_dont_cares(manager& m, unsigned key):m(m), m_key(key) { m.set_dont_care(key); }
|
||||
~scoped_dont_cares() { m.unset_dont_care(m_key); }
|
||||
};
|
||||
|
||||
void alloc_node();
|
||||
|
||||
unsigned idx2key(unsigned i) const { return i % m_num_keys; }
|
||||
unsigned idx2bitnum(unsigned i) const { SASSERT(i < m_num_idx); return (i / m_num_keys); }
|
||||
bool idx2bit(unsigned i) const { return 0 != (m_keys[idx2key(i)] & (1LL << idx2bitnum(i))); }
|
||||
bool idx2sign(unsigned i) const { return m_sign[idx2key(i)]; }
|
||||
|
||||
bool is_leaf(node_id n) const { return n <= 1; }
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -13,6 +13,7 @@ def_module_params('fixedpoint',
|
|||
('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
|
||||
('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
|
||||
('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
|
||||
('filter_rules', BOOL, True, "(DATALOG) apply filter compression on rules"),
|
||||
('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"),
|
||||
('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"),
|
||||
('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"),
|
||||
|
|
|
|||
|
|
@ -21,7 +21,6 @@ Revision History:
|
|||
#include "heap.h"
|
||||
#include "map.h"
|
||||
#include "heap_trie.h"
|
||||
#include "fdd.h"
|
||||
#include "stopwatch.h"
|
||||
|
||||
|
||||
|
|
@ -237,64 +236,8 @@ public:
|
|||
void display(std::ostream& out) const {
|
||||
// m_trie.display(out);
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
class hilbert_basis::value_index3 {
|
||||
hilbert_basis& hb;
|
||||
fdd::manager m_fdd;
|
||||
unsigned m_offset;
|
||||
svector<int64> m_keys;
|
||||
|
||||
int64 const* get_keys(values const& vs) {
|
||||
numeral const* nums = vs()-m_offset;
|
||||
for (unsigned i = 0; i < m_keys.size(); ++i) {
|
||||
m_keys[i] = nums[i].get_int64();
|
||||
}
|
||||
return m_keys.c_ptr();
|
||||
}
|
||||
|
||||
public:
|
||||
|
||||
value_index3(hilbert_basis & hb): hb(hb), m_offset(1) {}
|
||||
|
||||
void insert(offset_t, values const& vs) {
|
||||
m_fdd.insert(get_keys(vs));
|
||||
}
|
||||
|
||||
bool find(offset_t, values const& vs) {
|
||||
return m_fdd.find_le(get_keys(vs));
|
||||
}
|
||||
|
||||
void reset(unsigned offset) {
|
||||
m_offset = offset;
|
||||
m_fdd.reset(hb.get_num_vars()+m_offset);
|
||||
m_keys.resize(hb.get_num_vars()+m_offset);
|
||||
}
|
||||
|
||||
void collect_statistics(statistics& st) const {
|
||||
m_fdd.collect_statistics(st);
|
||||
}
|
||||
|
||||
void reset_statistics() {
|
||||
m_fdd.reset_statistics();
|
||||
}
|
||||
|
||||
unsigned size() const {
|
||||
return m_fdd.size();
|
||||
}
|
||||
|
||||
void remove(offset_t idx, values const& vs) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
void display(std::ostream& out) const {
|
||||
m_fdd.display(out);
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
class hilbert_basis::index {
|
||||
|
|
|
|||
|
|
@ -102,8 +102,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
lbool rel_context::saturate() {
|
||||
m_context.ensure_closed();
|
||||
|
||||
m_context.ensure_closed();
|
||||
bool time_limit = m_context.soft_timeout()!=0;
|
||||
unsigned remaining_time_limit = m_context.soft_timeout();
|
||||
unsigned restart_time = m_context.initial_restart_timeout();
|
||||
|
|
@ -126,6 +125,8 @@ namespace datalog {
|
|||
result = l_undef;
|
||||
break;
|
||||
}
|
||||
TRACE("dl", m_context.display(tout););
|
||||
|
||||
compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
|
||||
|
||||
TRACE("dl", m_code.display(*this, tout); );
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue