From 1b7cb110d34b748e2b501bd13947c943c6aaf0c4 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Fri, 1 Dec 2017 11:02:29 -0800 Subject: [PATCH 1/5] freevars cube cutoff Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 15 ++++++++++++++- src/sat/sat_config.h | 10 +++++++++- src/sat/sat_lookahead.cpp | 10 ++++++++-- src/sat/sat_lookahead.h | 11 ++++++++--- src/sat/sat_params.pyg | 9 +++++++-- 5 files changed, 46 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 24d2bca9b..bd2a48ff2 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -112,8 +112,21 @@ namespace sat { throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); } + if (p.lookahead_cube_cutoff() == symbol("adaptive")) { + m_lookahead_cube_cutoff = adaptive_cutoff; + } + else if (p.lookahead_cube_cutoff() == symbol("fixed_depth")) { + m_lookahead_cube_cutoff = fixed_depth_cutoff; + } + else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { + m_lookahead_cube_cutoff = fixed_freevars_cutoff; + } + else { + throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); + } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); - m_lookahead_cube_cutoff = p.lookahead_cube_cutoff(); + m_lookahead_cube_depth = p.lookahead_cube_depth(); + m_lookahead_cube_freevars = p.lookahead_cube_freevars(); m_lookahead_global_autarky = p.lookahead_global_autarky(); // These parameters are not exposed diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 9a20bbc63..f6f6774fc 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -65,6 +65,12 @@ namespace sat { march_cu_reward }; + enum cutoff_t { + adaptive_cutoff, + fixed_depth_cutoff, + fixed_freevars_cutoff + }; + struct config { unsigned long long m_max_memory; phase_selection m_phase; @@ -85,8 +91,10 @@ namespace sat { bool m_lookahead_search; bool m_lookahead_simplify; bool m_lookahead_simplify_bca; - unsigned m_lookahead_cube_cutoff; + cutoff_t m_lookahead_cube_cutoff; double m_lookahead_cube_fraction; + unsigned m_lookahead_cube_depth; + double m_lookahead_cube_freevars; reward_t m_lookahead_reward; bool m_lookahead_global_autarky; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 306912b57..2784b97d2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1032,6 +1032,7 @@ namespace sat { } propagate(); m_qhead = m_trail.size(); + m_init_freevars = m_freevars.size(); TRACE("sat", m_s.display(tout); display(tout);); } @@ -2054,8 +2055,11 @@ namespace sat { } backtrack_level = UINT_MAX; depth = m_cube_state.m_cube.size(); - if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || - (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) { + if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) || + (m_config.m_cube_cutoff == adaptive_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || + /* m_cube_cutoff is fixed_freevars */ m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) { + /*if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || + (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/ m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); set_conflict(); #if 0 @@ -2413,6 +2417,8 @@ namespace sat { m_config.m_reward_type = m_s.m_config.m_lookahead_reward; m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff; m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction; + m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth; + m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars; } void lookahead::collect_statistics(statistics& st) const { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 6f0c256a7..db9ebdaa4 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -80,8 +80,10 @@ namespace sat { unsigned m_dl_max_iterations; unsigned m_tc1_limit; reward_t m_reward_type; - unsigned m_cube_cutoff; + cutoff_t m_cube_cutoff; + unsigned m_cube_depth; double m_cube_fraction; + double m_cube_freevars; config() { memset(this, sizeof(*this), 0); @@ -96,8 +98,10 @@ namespace sat { m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; - m_cube_cutoff = 0; + m_cube_cutoff = adaptive_cutoff; + m_cube_depth = 10; m_cube_fraction = 0.4; + m_cube_freevars = 0.8; } }; @@ -222,11 +226,12 @@ namespace sat { svector m_vprefix; // var: prefix where variable participates in propagation unsigned m_rating_throttle; // throttle to recompute rating indexed_uint_set m_freevars; + unsigned m_init_freevars; lookahead_mode m_search_mode; // mode of search stats m_stats; model m_model; cube_state m_cube_state; - scoped_ptr m_ext; + scoped_ptr m_ext; // --------------------------------------- // truth values diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 4f65b100b..085f0c067 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -37,8 +37,13 @@ def_module_params('sat', ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search', BOOL, False, 'use local search instead of CDCL'), - ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'), - ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), + ('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'), + ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'), + ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is fixed_freevars'), + ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), + ('lookahead.cube.psat.clause_base', DOUBLE, 1, 'clause base for PSAT cutoff') + ('lookahead.cube.psat.probability', DOUBLE' 0.5, 'probability to create lookahead cubes for PSAT cutoff') ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), From e0dfbd6d1cf7341da84a315bb1e715d3767c9126 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Mon, 4 Dec 2017 14:33:48 -0800 Subject: [PATCH 2/5] fixed freevars and psat cube cutoffs Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 6 ++++++ src/sat/sat_config.h | 6 +++++- src/sat/sat_lookahead.cpp | 38 +++++++++++++++++++++++++++++++++++--- src/sat/sat_lookahead.h | 8 ++++++++ src/sat/sat_params.pyg | 4 ++-- 5 files changed, 56 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index bd2a48ff2..b0797dae9 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -121,12 +121,18 @@ namespace sat { else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { m_lookahead_cube_cutoff = fixed_freevars_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("psat")) { + m_lookahead_cube_cutoff = psat_cutoff; + } else { throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_depth = p.lookahead_cube_depth(); m_lookahead_cube_freevars = p.lookahead_cube_freevars(); + m_lookahead_cube_psat_var_exp = p.lookahead_cube_psat_var_exp(); + m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base(); + m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger(); m_lookahead_global_autarky = p.lookahead_global_autarky(); // These parameters are not exposed diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f6f6774fc..1529466ee 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -68,7 +68,8 @@ namespace sat { enum cutoff_t { adaptive_cutoff, fixed_depth_cutoff, - fixed_freevars_cutoff + fixed_freevars_cutoff, + psat_cutoff }; struct config { @@ -95,6 +96,9 @@ namespace sat { double m_lookahead_cube_fraction; unsigned m_lookahead_cube_depth; double m_lookahead_cube_freevars; + double m_lookahead_cube_psat_var_exp; + double m_lookahead_cube_psat_clause_base; + double m_lookahead_cube_psat_trigger; reward_t m_lookahead_reward; bool m_lookahead_global_autarky; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 6aae5738e..3feb9455d 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2019,6 +2019,35 @@ namespace sat { st.update("lh cube conflicts", m_cube_state.m_conflicts); } + double lookahead::psat_heur() { + double h = 0.0; + for (bool_var x : m_freevars) { + literal l(x, false); + for (literal lit : m_binary[l.index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (literal lit : m_binary[(~l).index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (binary b : m_ternary[l.index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + for (binary b : m_ternary[(~l).index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + } + for (nary * n : m_nary_clauses) { + h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1); + } + h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp); + IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";); + return h; + } + lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); @@ -2065,9 +2094,8 @@ namespace sat { depth = m_cube_state.m_cube.size(); if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) || (m_config.m_cube_cutoff == adaptive_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || - /* m_cube_cutoff is fixed_freevars */ m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) { - /*if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || - (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/ + (m_config.m_cube_cutoff == fixed_freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger)) { m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); set_conflict(); m_cube_state.inc_cutoff(); @@ -2085,6 +2113,7 @@ namespace sat { if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } @@ -2503,6 +2532,9 @@ namespace sat { m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction; m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth; m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars; + m_config.m_cube_psat_var_exp = m_s.m_config.m_lookahead_cube_psat_var_exp; + m_config.m_cube_psat_clause_base = m_s.m_config.m_lookahead_cube_psat_clause_base; + m_config.m_cube_psat_trigger = m_s.m_config.m_lookahead_cube_psat_trigger; } void lookahead::collect_statistics(statistics& st) const { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index bd4198dcd..254dd614f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -84,6 +84,9 @@ namespace sat { unsigned m_cube_depth; double m_cube_fraction; double m_cube_freevars; + double m_cube_psat_var_exp; + double m_cube_psat_clause_base; + double m_cube_psat_trigger; config() { memset(this, sizeof(*this), 0); @@ -102,6 +105,9 @@ namespace sat { m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; + m_cube_psat_var_exp = 1.0; + m_cube_psat_clause_base = 2.0; + m_cube_psat_trigger = 5.0; } }; @@ -547,6 +553,8 @@ namespace sat { void add_hyper_binary(); + double psat_heur(); + public: lookahead(solver& s) : m_s(s), diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 085f0c067..565c6dbcc 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -42,8 +42,8 @@ def_module_params('sat', ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'), ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is fixed_freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), - ('lookahead.cube.psat.clause_base', DOUBLE, 1, 'clause base for PSAT cutoff') - ('lookahead.cube.psat.probability', DOUBLE' 0.5, 'probability to create lookahead cubes for PSAT cutoff') + ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), + ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff'), ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), From 38751430df4078e14feda6d8e50f9bf5ae1b1419 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 5 Dec 2017 17:53:48 -0800 Subject: [PATCH 3/5] adaptive psat cutoff Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 19 +++++++++++-------- src/sat/sat_config.h | 9 +++++---- src/sat/sat_lookahead.cpp | 15 ++++++++++----- src/sat/sat_lookahead.h | 4 +++- src/sat/sat_params.pyg | 10 +++++----- 5 files changed, 34 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 87d84f133..660337071 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -109,20 +109,23 @@ namespace sat { throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); } - if (p.lookahead_cube_cutoff() == symbol("adaptive")) { - m_lookahead_cube_cutoff = adaptive_cutoff; + if (p.lookahead_cube_cutoff() == symbol("depth")) { + m_lookahead_cube_cutoff = depth_cutoff; } - else if (p.lookahead_cube_cutoff() == symbol("fixed_depth")) { - m_lookahead_cube_cutoff = fixed_depth_cutoff; - } - else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { - m_lookahead_cube_cutoff = fixed_freevars_cutoff; + else if (p.lookahead_cube_cutoff() == symbol("freevars")) { + m_lookahead_cube_cutoff = freevars_cutoff; } else if (p.lookahead_cube_cutoff() == symbol("psat")) { m_lookahead_cube_cutoff = psat_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) { + m_lookahead_cube_cutoff = adaptive_freevars_cutoff; + } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) { + m_lookahead_cube_cutoff = adaptive_psat_cutoff; + } else { - throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); + throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'"); } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_depth = p.lookahead_cube_depth(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ed7802cef..f66c0dbdf 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -66,10 +66,11 @@ namespace sat { }; enum cutoff_t { - adaptive_cutoff, - fixed_depth_cutoff, - fixed_freevars_cutoff, - psat_cutoff + depth_cutoff, + freevars_cutoff, + psat_cutoff, + adaptive_freevars_cutoff, + adaptive_psat_cutoff }; struct config { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index a9ae3b641..ec1bf23f2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2092,11 +2092,14 @@ namespace sat { } backtrack_level = UINT_MAX; depth = m_cube_state.m_cube.size(); - if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) || - (m_config.m_cube_cutoff == adaptive_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || - (m_config.m_cube_cutoff == fixed_freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || - (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger)) { - m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); + if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) || + (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) || + (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || + (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) { + double dec = (1.0 - pow(m_config.m_cube_fraction, depth)); + m_cube_state.m_freevars_threshold *= dec; + m_cube_state.m_psat_threshold *= dec; set_conflict(); m_cube_state.inc_cutoff(); #if 0 @@ -2109,10 +2112,12 @@ namespace sat { return l_undef; } int prev_nfreevars = m_freevars.size(); + double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled literal lit = choose(); if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.m_psat_threshold = prev_psat; m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 254dd614f..6a7bb7449 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -101,7 +101,7 @@ namespace sat { m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; - m_cube_cutoff = adaptive_cutoff; + m_cube_cutoff = adaptive_freevars_cutoff; m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; @@ -177,6 +177,7 @@ namespace sat { svector m_is_decision; literal_vector m_cube; double m_freevars_threshold; + double m_psat_threshold; unsigned m_conflicts; unsigned m_cutoffs; cube_state() { reset(); } @@ -185,6 +186,7 @@ namespace sat { m_is_decision.reset(); m_cube.reset(); m_freevars_threshold = 0; + m_psat_threshold = DBL_MAX; reset_stats(); } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 0e6823030..4432c0b16 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -37,13 +37,13 @@ def_module_params('sat', ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), - ('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'), - ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'), - ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is fixed_freevars'), + ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), + ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), - ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff'), + ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), From 6d729f1f158ebc406262dad703b31470a42ea0a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2017 10:36:42 -0800 Subject: [PATCH 4/5] disable UHLT Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 8e5e556e3..dbb5ea123 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -208,7 +208,6 @@ namespace sat { m_to_delete.reset(); for (unsigned i = m_pos.size() - 1; i-- > 0; ) { literal lit = m_pos[i]; - SASSERT(scc.get_left(lit) < scc.get_left(last)); int right2 = scc.get_right(lit); if (right2 > right) { // lit => last, so lit can be deleted @@ -345,10 +344,12 @@ namespace sat { bool asymm_branch::process_sampled(scc& scc, clause & c) { scoped_detach scoped_d(s, c); sort(scc, c); +#if 0 if (uhte(scc, c)) { scoped_d.del_clause(); return false; } +#endif return uhle(scoped_d, scc, c); } From 35a3523fd6fb612fc796f6c0d1794ea1e5a93373 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2017 14:09:34 -0800 Subject: [PATCH 5/5] fix bug in double collection of declarations Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 3 +++ src/ast/decl_collector.cpp | 25 ++++++++++--------------- src/ast/decl_collector.h | 2 +- 3 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index e579e4565..682660638 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -622,6 +622,9 @@ public: sort * const * get_domain() const { return m_domain; } sort * get_range() const { return m_range; } unsigned get_size() const { return get_obj_size(m_arity); } + sort * const * begin() const { return get_domain(); } + sort * const * end() const { return get_domain() + get_arity(); } + }; // ----------------------------------- diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index 0df4b0fc5..5d47170ee 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -20,20 +20,15 @@ Revision History: #include "ast/decl_collector.h" void decl_collector::visit_sort(sort * n) { + SASSERT(!m_visited.is_marked(n)); family_id fid = n->get_family_id(); if (m().is_uninterp(n)) m_sorts.push_back(n); - if (fid == m_dt_fid) { + else if (fid == m_dt_fid) { m_sorts.push_back(n); - - unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); - for (unsigned i = 0; i < num_cnstr; i++) { - func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); + for (func_decl* cnstr : *m_dt_util.get_datatype_constructors(n)) { m_decls.push_back(cnstr); - ptr_vector const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); - unsigned num_cas = cnstr_acc.size(); - for (unsigned j = 0; j < num_cas; j++) { - func_decl * accsr = cnstr_acc.get(j); + for (func_decl * accsr : *m_dt_util.get_constructor_accessors(cnstr)) { m_decls.push_back(accsr); } } @@ -53,6 +48,7 @@ void decl_collector::visit_func(func_decl * n) { else m_decls.push_back(n); } + m_visited.mark(n, true); } } @@ -72,11 +68,10 @@ void decl_collector::visit(ast* n) { if (!m_visited.is_marked(n)) { switch(n->get_kind()) { case AST_APP: { - app * a = to_app(n); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - m_todo.push_back(a->get_arg(i)); + for (expr * e : *to_app(n)) { + m_todo.push_back(e); } - m_todo.push_back(a->get_decl()); + m_todo.push_back(to_app(n)->get_decl()); break; } case AST_QUANTIFIER: { @@ -96,8 +91,8 @@ void decl_collector::visit(ast* n) { break; case AST_FUNC_DECL: { func_decl * d = to_func_decl(n); - for (unsigned i = 0; i < d->get_arity(); ++i) { - m_todo.push_back(d->get_domain(i)); + for (sort* srt : *d) { + m_todo.push_back(srt); } m_todo.push_back(d->get_range()); visit_func(d); diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 0a812bb2c..36d7c930b 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -41,7 +41,7 @@ class decl_collector { public: // if preds == true, then predicates are stored in a separate collection. - decl_collector(ast_manager & m, bool preds=true); + decl_collector(ast_manager & m, bool preds = true); ast_manager & m() { return m_manager; } void visit_func(func_decl* n);