From bd63458778d020fb037ff11af2e2d597a865a00d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 15:35:49 -0400 Subject: [PATCH] Shuffle assumptions on every call 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. --- src/muz/spacer/spacer_prop_solver.cpp | 3 +++ src/muz/spacer/spacer_prop_solver.h | 2 ++ 2 files changed, 5 insertions(+) diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 7bd21a1b5..004ea6754 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m, m_use_push_bg(p.spacer_keep_proxy()) { + m_random.set_seed(p.spacer_random_seed()); m_solvers[0] = solver0; 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()); flatten_and(hard); + shuffle(hard.size(), hard.c_ptr(), m_random); + m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get(); // can be disabled if use_push_bg == true diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 1db65dc3e..0eed969bd 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -61,6 +61,8 @@ private: bool m_use_push_bg; unsigned m_current_level; // set when m_in_level + random_gen m_random; + void assert_level_atoms(unsigned level); void ensure_level(unsigned lvl);