From c92e6ac658faefcf906645ffb11ca080cb1daf84 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 12 Dec 2017 14:35:24 -0800 Subject: [PATCH] merge Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_params.pyg | 9 +++++++-- src/sat/sat_simplifier.cpp | 2 +- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index a72a896cc..0632d3076 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2420,7 +2420,7 @@ namespace sat { } } } - std::cout << candidates.size() << " -> " << k << "\n"; + //std::cout << candidates.size() << " -> " << k << "\n"; if (k == candidates.size()) break; candidates.shrink(k); if (k == 0) break; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index fde5f1272..3fc5194f0 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -38,8 +38,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.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_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. Used when lookahead.cube.cutoff is psat'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 87218b735..558bfb11e 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1357,7 +1357,7 @@ namespace sat { void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); VERIFY(!s.is_external(l)); - if (new_entry == 0 && !s.m_retain_blocked_clauses) + if (new_entry == 0) new_entry = &(mc.mk(k, l.var())); m_to_remove.push_back(&c); for (literal lit : c) {