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

spacer::context: Factor params into udpt_params

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-05 16:20:55 -07:00
parent 521392a8f1
commit cb683389f6
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2244,8 +2244,7 @@ context::context(fixedpoint_params const& params,
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()); updt_params()
m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
} }
context::~context() context::~context()
@ -2254,6 +2253,11 @@ context::~context()
reset(); reset();
} }
void context::updt_params() {
m_random.set_seed(m_params.spacer_random_seed());
m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
}
void context::reset() void context::reset()
{ {
TRACE("spacer", tout << "\n";); TRACE("spacer", tout << "\n";);

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

@ -897,6 +897,7 @@ class context {
void predecessor_eh(); void predecessor_eh();
void updt_params();
public: public:
/** /**
Initial values of predicates are stored in corresponding relations in dctx. Initial values of predicates are stored in corresponding relations in dctx.
@ -905,6 +906,7 @@ public:
context(fixedpoint_params const& params, ast_manager& m); context(fixedpoint_params const& params, ast_manager& m);
~context(); ~context();
const fixedpoint_params &get_params() const { return m_params; } const fixedpoint_params &get_params() const { return m_params; }
bool use_native_mbp () {return m_use_native_mbp;} bool use_native_mbp () {return m_use_native_mbp;}
bool use_ground_cti () {return m_ground_cti;} bool use_ground_cti () {return m_ground_cti;}