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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-24 20:04:01 -07:00
parent 6250a29602 f58e8e961d
commit 4f9247a28a
8 changed files with 25 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

58
src/muz_qe/dl_compiler.cpp
View file

@ -832,19 +832,19 @@ 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;
ast_mark m_visited;
void traverse(T v) {
SASSERT(!m_visited.is_marked(v));
if (m_removed.contains(v)) {
SASSERT(!m_stack_content.is_marked(v));
if(m_visited.is_marked(v) || m_removed.contains(v)) {
return;
}
m_stack.push_back(v);
m_stack_content.mark(v, true);
m_visited.mark(v, true);
const item_set & deps = m_deps.get_deps(v);
@ -852,49 +852,22 @@ namespace datalog {
item_set::iterator end = deps.end();
for(; it!=end; ++it) {
T d = *it;
if (m_visited.is_marked(d)) {
if(m_stack_content.is_marked(d)) {
//TODO: find the best vertex to remove in the cycle
remove_from_stack();
continue;
m_removed.insert(v);
break;
}
traverse(d);
}
SASSERT(m_stack.back()==v);
m_stack.pop_back();
m_visited.mark(v, false);
}
void remove_from_stack() {
for (unsigned i = 0; i < m_stack.size(); ++i) {
func_decl* p = m_stack[i];
if (m_context.has_facts(p)) {
m_removed.insert(p);
return;
}
rule_vector const& rules = m_rules.get_predicate_rules(p);
unsigned stratum = m_rules.get_predicate_strat(p);
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());
m_stack_content.mark(v, false);
}
public:
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()); }
cycle_breaker(rule_dependencies & deps, item_set & removed)
: m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); }
void operator()() {
rule_dependencies::iterator it = m_deps.begin();
@ -916,7 +889,7 @@ namespace datalog {
rule_dependencies deps(m_rule_set.get_dependencies());
deps.restrict(preds);
cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
cycle_breaker(deps, global_deltas)();
VERIFY( deps.sort_deps(ordered_preds) );
//the predicates that were removed to get acyclic induced subgraph are put last
@ -1052,12 +1025,17 @@ namespace datalog {
}
func_decl_vector preds_vector;
func_decl_set global_deltas;
func_decl_set global_deltas_dummy;
detect_chains(head_preds, preds_vector, global_deltas);
detect_chains(head_preds, preds_vector, global_deltas_dummy);
/*
FIXME: right now we use all preds as global deltas for correctness purposes
func_decl_set local_deltas(head_preds);
set_difference(local_deltas, global_deltas);
*/
func_decl_set local_deltas;
func_decl_set global_deltas(head_preds);
pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop
get_fresh_registers(global_deltas, d_global_src);

1
src/muz_qe/dl_compiler.h
View file

@ -42,7 +42,6 @@ namespace datalog {
typedef u_map<unsigned> int2int;
typedef u_map<unsigned_vector> int2ints;
typedef obj_map<func_decl, reg_idx> pred2idx;
// typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
typedef unsigned_vector var_vector;
typedef ptr_vector<func_decl> func_decl_vector;

16
src/muz_qe/dl_instruction.cpp
View file

@ -359,21 +359,7 @@ namespace datalog {
r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
try {
ctx.set_reg(m_res, (*fn)(r1, r2));
}
catch(...)
{
std::string annotation;
unsigned sz;
ctx.get_register_annotation(m_rel1, annotation);
sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0;
std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n";
ctx.get_register_annotation(m_rel2, annotation);
sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0;
std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n";
throw;
}
ctx.set_reg(m_res, (*fn)(r1, r2));
TRACE("dl",
ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);

3
src/muz_qe/dl_mk_filter_rules.cpp
View file

@ -152,9 +152,6 @@ namespace datalog {
}
rule_set * mk_filter_rules::operator()(rule_set const & source) {
if (!m_context.get_params().filter_rules()) {
return 0;
}
m_tail2filter.reset();
m_result = alloc(rule_set, m_context);
m_modified = false;

3
src/muz_qe/dl_rule_transformer.cpp
View file

@ -107,9 +107,6 @@ namespace datalog {
tout << typeid(p).name()<<":\n";
new_rules->display(tout);
);
IF_VERBOSE(1, new_rules->get_rule(0)->display(m_context, verbose_stream() << typeid(p).name() <<"\n"););
IF_VERBOSE(1, verbose_stream() << new_rules->get_dependencies().begin()->m_key->get_name() << "\n";);
}
if (modified) {
rules.replace_rules(*new_rules);

1
src/muz_qe/fixedpoint_params.pyg
View file

@ -13,7 +13,6 @@ 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"),

11
src/muz_qe/rel_context.cpp
View file

@ -116,12 +116,10 @@ namespace datalog {
TRACE("dl", m_context.display(tout););
while (true) {
m_ectx.reset();
m_code.reset();
termination_code.reset();
m_context.ensure_closed();
IF_VERBOSE(1, verbose_stream() << "num rules: " << m_context.get_rules().get_num_rules() << "\n";);
m_context.transform_rules();
if (m_context.canceled()) {
result = l_undef;
@ -184,9 +182,7 @@ namespace datalog {
scoped_query.reset();
}
m_context.record_transformed_rules();
TRACE("dl", m_ectx.report_big_relations(100, tout););
m_code.process_all_costs();
m_code.make_annotations(m_ectx);
TRACE("dl", display_profile(tout););
return result;
}
@ -484,7 +480,10 @@ namespace datalog {
get_rmanager().display(out);
}
void rel_context::display_profile(std::ostream& out) const {
void rel_context::display_profile(std::ostream& out) {
m_code.make_annotations(m_ectx);
m_code.process_all_costs();
out << "\n--------------\n";
out << "Instructions\n";
m_code.display(*this, out);

2
src/muz_qe/rel_context.h
View file

@ -105,7 +105,7 @@ namespace datalog {
void display_output_facts(rule_set const& rules, std::ostream & out) const;
void display_facts(std::ostream & out) const;
void display_profile(std::ostream& out) const;
void display_profile(std::ostream& out);
lbool saturate();