mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

remove ad-hoc parameters, deprecating dimacs cube mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-05 14:08:55 -08:00
parent 70ee030228
commit 9a4fb4ff76
5 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_config.cpp
View file

@ -89,7 +89,6 @@ namespace sat {
m_local_search = p.local_search();
m_local_search_threads = p.local_search_threads();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_cube = p.lookahead_cube();
m_lookahead_search = p.lookahead_search();
if (p.lookahead_reward() == symbol("heule_schur")) {
m_lookahead_reward = heule_schur_reward;

1
src/sat/sat_config.h
View file

@ -84,7 +84,6 @@ namespace sat {
bool m_local_search;
bool m_lookahead_search;
bool m_lookahead_simplify;
bool m_lookahead_cube;
unsigned m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
reward_t m_lookahead_reward;

1
src/sat/sat_params.pyg
View file

@ -36,7 +36,6 @@ 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', BOOL, False, 'use lookahead solver to create cubes'),
('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_search', BOOL, False, 'use lookahead solver'),

4
src/sat/sat_solver.cpp
View file

@ -871,9 +871,13 @@ namespace sat {
if (m_config.m_lookahead_search && num_lits == 0) {
return lookahead_search();
}
#if 0
// deprecated
if (m_config.m_lookahead_cube && num_lits == 0) {
return lookahead_cube();
}
#endif
if (m_config.m_local_search) {
return do_local_search(num_lits, lits);
}

31
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -111,7 +111,6 @@ class parallel_tactic : public tactic {
solver_state* st = try_get_task();
if (st) return st;
inc_wait();
std::unique_lock<std::mutex> lock(m_mutex);
m_cond.wait(lock, [this] { --m_num_waiters; return true; });
}
@ -289,14 +288,11 @@ class parallel_tactic : public tactic {
}
void set_simplify_params(bool pb_simp, bool retain_blocked) {
m_params.set_bool("bca", true);
m_params.set_bool("cardinality.solver", pb_simp);
m_params.set_bool("cce", true);
// m_params.set_bool("elim_blocked_clauses", true);
m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX)
m_params.set_uint("inprocess.max", 2);
m_params.set_bool("lookahead_simplify", true);
m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
m_params.set_uint("restart.max", UINT_MAX);
m_params.set_bool("retain_blocked_clauses", retain_blocked);
get_solver().updt_params(m_params);
@ -344,7 +340,7 @@ private:
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
if (status == l_true) verbose_stream() << ":status sat ";
if (status == l_undef) verbose_stream() << ":status unknown ";
verbose_stream() <<o ":unsat " << m_num_unsat << ")\n";);
verbose_stream() << ":unsat " << m_num_unsat << ")\n";);
}
void report_sat(solver_state& s) {
@ -387,13 +383,13 @@ private:
cube:
SASSERT(s.type() == cube_task);
s.inc_depth(1);
// extract up to one cube and add it.
cube.reset();
cube.append(s.split_cubes(1));
SASSERT(cube.size() <= 1);
if (!s.cubes().empty()) m_queue.add_task(s.clone());
if (!cube.empty()) s.assert_cube(cube.get(0));
s.inc_depth(1);
// simplify
switch (s.simplify()) {
@ -401,7 +397,7 @@ private:
case l_true: report_sat(s); return;
case l_false: report_unsat(s); return;
}
if (s.canceled()) return;
if (canceled(s)) return;
// extract cubes.
cubes.reset();
@ -419,7 +415,8 @@ private:
cubes.push_back(c);
}
IF_VERBOSE(1, verbose_stream() << "cubes: " << cubes << "\n";);
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";);
IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";);
if (cubes.empty()) {
report_unsat(s);
@ -448,7 +445,7 @@ private:
case l_true: report_sat(s); break;
case l_false: report_unsat(s); break;
}
if (s.canceled()) return;
if (canceled(s)) return;
}
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";);
if (hard_cubes.empty()) return;
@ -458,6 +455,16 @@ private:
goto cube;
}
bool canceled(solver_state& s) {
if (s.canceled()) {
m_has_undef = true;
return true;
}
else {
return false;
}
}
void run_solver() {
try {
while (solver_state* st = m_queue.get_task()) {
@ -490,10 +497,12 @@ private:
}
if (!m_models.empty()) {
mdl = m_models.back();
m_manager.limit().reset_cancel();
return l_true;
}
if (m_has_undef || m_manager.canceled())
if (m_has_undef)
return l_undef;
m_manager.limit().reset_cancel();
return l_false;
}