mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Add random order of children in spacer

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-04 12:53:45 -07:00
parent 5756871738
commit 3178f7f86d
2 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/muz/spacer/spacer_context.cpp
View file

@ -2241,6 +2241,9 @@ context::context(fixedpoint_params const& params,
m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts); m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts);
m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts); m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts);
m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts); m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts);
m_random.set_seed(m_params.spacer_random_seed());
m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
} }
context::~context() context::~context()
@ -3680,7 +3683,12 @@ bool context::create_children(pob& n, datalog::rule const& r,
unsigned_vector kid_order; unsigned_vector kid_order;
kid_order.resize(preds.size(), 0); kid_order.resize(preds.size(), 0);
for (unsigned i = 0, sz = preds.size(); i < sz; ++i) kid_order[i] = i; for (unsigned i = 0, sz = preds.size(); i < sz; ++i) kid_order[i] = i;
if (get_params().spacer_order_children() == 1) kid_order.reverse(); if (m_children_order == CO_REV_RULE) {
kid_order.reverse();
}
else if (m_children_order == CO_RANDOM) {
shuffle(kid_order.size(), kid_order.c_ptr(), m_random);
}
for (unsigned i = 0, sz = preds.size(); i < sz; ++i) { for (unsigned i = 0, sz = preds.size(); i < sz; ++i) {
unsigned j = kid_order[i]; unsigned j = kid_order[i];

8
src/muz/spacer/spacer_context.h
View file

@ -782,6 +782,12 @@ public:
}; };
// order in which children are processed
enum spacer_children_order {
CO_RULE, // same order as in the rule
CO_REV_RULE, // reverse order of the rule
CO_RANDOM // random shuffle
};
class context { class context {
@ -819,6 +825,8 @@ class context {
scoped_ptr<solver_pool> m_pool2; scoped_ptr<solver_pool> m_pool2;
random_gen m_random;
spacer_children_order m_children_order;
decl2rel m_rels; // Map from relation predicate to fp-operator. decl2rel m_rels; // Map from relation predicate to fp-operator.
func_decl_ref m_query_pred; func_decl_ref m_query_pred;
pred_transformer* m_query; pred_transformer* m_query;