From bb5d81195c124f74906da83c4a58e03c3624f14b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Aug 2022 18:17:07 -0700 Subject: [PATCH] use equalities --- src/sat/sat_solver.h | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e5b13af986f..60aadf8a171 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -527,20 +527,21 @@ namespace sat { unsigned m_conflicts_since_init { 0 }; unsigned m_restarts { 0 }; - unsigned m_restart_next_out { 0 }; - unsigned m_conflicts_since_restart { 0 }; - bool m_force_conflict_analysis { false }; - unsigned m_simplifications { 0 }; - unsigned m_restart_threshold { 0 }; - unsigned m_luby_idx { 0 }; - unsigned m_conflicts_since_gc { 0 }; - unsigned m_gc_threshold { 0 }; - unsigned m_defrag_threshold { 0 }; - unsigned m_num_checkpoints { 0 }; - double m_min_d_tk { 0 } ; - unsigned m_next_simplify { 0 }; - bool m_simplify_enabled { true }; - bool m_restart_enabled { true }; + unsigned m_restart_next_out = 0; + unsigned m_conflicts_since_restart = 0; + bool m_force_conflict_analysis = false; + unsigned m_simplifications = 0; + unsigned m_restart_threshold = 0; + unsigned m_luby_idx = 0; + unsigned m_conflicts_since_gc = 0; + unsigned m_gc_threshold = 0; + unsigned m_defrag_threshold = 0; + unsigned m_num_checkpoints = 0; + double m_min_d_tk = 0.0 ; + unsigned m_next_simplify = 0; + double m_simplify_mult = 1.5; + bool m_simplify_enabled = true; + bool m_restart_enabled = true; bool guess(bool_var next); bool decide(); bool_var next_var();