mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Shuffle assumptions on every call

Browse source 
Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
This commit is contained in:
Arie Gurfinkel 2018-06-28 15:35:49 -04:00
parent 6422fa3739
commit bd63458778
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m,
m_use_push_bg(p.spacer_keep_proxy()) m_use_push_bg(p.spacer_keep_proxy())
{ {
m_random.set_seed(p.spacer_random_seed());
m_solvers[0] = solver0; m_solvers[0] = solver0;
m_solvers[1] = solver1; m_solvers[1] = solver1;
@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
hard.append(_hard.size(), _hard.c_ptr()); hard.append(_hard.size(), _hard.c_ptr());
flatten_and(hard); flatten_and(hard);
shuffle(hard.size(), hard.c_ptr(), m_random);
m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get(); m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
// can be disabled if use_push_bg == true // can be disabled if use_push_bg == true

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

@ -61,6 +61,8 @@ private:
bool m_use_push_bg; bool m_use_push_bg;
unsigned m_current_level; // set when m_in_level unsigned m_current_level; // set when m_in_level
random_gen m_random;
void assert_level_atoms(unsigned level); void assert_level_atoms(unsigned level);
void ensure_level(unsigned lvl); void ensure_level(unsigned lvl);