mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

cleaning up lookahead

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-22 07:42:44 -07:00
parent 5e2f7f7177
commit 9ebe980b44
6 changed files with 17 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_lookahead.cpp
View file

@ -299,7 +299,6 @@ namespace sat {
bool_var x = *it;
if (!m_select_lookahead_vars.empty()) {
if (m_select_lookahead_vars.contains(x)) {
// IF_VERBOSE(1, verbose_stream() << x << " " << m_rating[x] << "\n";);
m_candidates.push_back(candidate(x, m_rating[x]));
sum += m_rating[x];
}
@ -309,7 +308,6 @@ namespace sat {
sum += m_rating[x];
}
}
IF_VERBOSE(1, verbose_stream() << " " << sum << " " << m_candidates.size() << "\n";);
TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
return sum;
}
@ -424,12 +422,9 @@ namespace sat {
literal_vector::iterator it = m_binary[l.index()].begin(), end = m_binary[l.index()].end();
for (; it != end; ++it) {
bool_var v = it->var();
if (it->index() >= h.size())
IF_VERBOSE(0, verbose_stream() << l << " " << *it << " " << h.size() << "\n";);
if (is_undef(*it)) sum += h[it->index()];
// if (m_freevars.contains(it->var())) sum += h[it->index()];
}
// std::cout << "sum: " << sum << "\n";
watch_list& wlist = m_watches[l.index()];
watch_list::iterator wit = wlist.begin(), wend = wlist.end();
for (; wit != wend; ++wit) {
@ -930,7 +925,7 @@ namespace sat {
}
void lookahead::pop() {
if (m_assumptions.empty()) IF_VERBOSE(0, verbose_stream() << "empty pop\n";);
SASSERT(!m_assumptions.empty());
m_assumptions.pop_back();
m_inconsistent = false;
SASSERT(m_search_mode == lookahead_mode::searching);

3
src/sat/sat_params.pyg
View file

@ -23,7 +23,8 @@ def_module_params('sat',
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('core.minimize', BOOL, False, 'minimize computed core'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('threads', UINT, 1, 'number of parallel threads to use'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'),

1
src/sat/sat_simplifier.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include"sat_simplifier.h"
#include"sat_simplifier_params.hpp"
#include"sat_solver.h"
#include"sat_lookahead.h"
#include"stopwatch.h"
#include"trace.h"

24
src/sat/sat_solver.cpp
View file

@ -60,7 +60,7 @@ namespace sat {
init_reason_unknown();
updt_params(p);
m_conflicts_since_gc = 0;
m_conflicts = 0;
m_conflicts_since_init = 0;
m_next_simplify = 0;
m_num_checkpoints = 0;
}
@ -881,9 +881,9 @@ namespace sat {
if (r != l_undef)
return r;
if (m_conflicts > m_config.m_max_conflicts) {
if (m_conflicts_since_init > m_config.m_max_conflicts) {
m_reason_unknown = "sat.max.conflicts";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";);
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
return l_undef;
}
@ -1194,7 +1194,7 @@ namespace sat {
return l_true;
if (!resolve_conflict())
return l_false;
if (m_conflicts > m_config.m_max_conflicts)
if (m_conflicts_since_init > m_config.m_max_conflicts)
return l_undef;
if (m_conflicts_since_restart > m_restart_threshold)
return l_undef;
@ -1355,7 +1355,7 @@ namespace sat {
m_luby_idx = 1;
m_gc_threshold = m_config.m_gc_initial;
m_restarts = 0;
m_conflicts = 0;
m_conflicts_since_init = 0;
m_min_d_tk = 1.0;
m_search_lvl = 0;
m_stopwatch.reset();
@ -1371,7 +1371,7 @@ namespace sat {
*/
void solver::simplify_problem() {
if (m_conflicts < m_next_simplify) {
if (m_conflicts_since_init < m_next_simplify) {
return;
}
IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";);
@ -1429,9 +1429,9 @@ namespace sat {
m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
}
else {
m_next_simplify = static_cast<unsigned>(m_conflicts * m_config.m_simplify_mult2);
if (m_next_simplify > m_conflicts + m_config.m_simplify_max)
m_next_simplify = m_conflicts + m_config.m_simplify_max;
m_next_simplify = static_cast<unsigned>(m_conflicts_since_init * m_config.m_simplify_mult2);
if (m_next_simplify > m_conflicts_since_init + m_config.m_simplify_max)
m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max;
}
}
@ -1882,7 +1882,7 @@ namespace sat {
bool solver::resolve_conflict_core() {
m_conflicts++;
m_conflicts_since_init++;
m_conflicts_since_restart++;
m_conflicts_since_gc++;
m_stats.m_conflict++;
@ -3551,8 +3551,8 @@ namespace sat {
extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
if (m_conflicts > m_config.m_max_conflicts) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";);
if (m_conflicts_since_init > m_config.m_max_conflicts) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
return l_undef;
}

2
src/sat/sat_solver.h
View file

@ -358,7 +358,7 @@ namespace sat {
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
protected:
unsigned m_conflicts;
unsigned m_conflicts_since_init;
unsigned m_restarts;
unsigned m_conflicts_since_restart;
unsigned m_restart_threshold;

4
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -323,7 +323,6 @@ public:
IF_VERBOSE(0, verbose_stream() << "WARNING: could not handle " << mk_pp(c, m) << "\n";);
}
}
IF_VERBOSE(1, verbose_stream() << "vars: " << vars.size() << "\n";);
if (vars.empty()) {
return expr_ref(m.mk_true(), m);
}
@ -336,15 +335,14 @@ public:
return expr_ref(m.mk_true(), m);
}
expr_ref result(lit2expr[l.index()].get(), m);
IF_VERBOSE(1, verbose_stream() << "solution: " << l << " " << result << "\n";);
return result;
}
virtual void get_lemmas(expr_ref_vector & lemmas) {
IF_VERBOSE(1, verbose_stream() << "(sat-get-lemmas " << lemmas.size() << ")\n";);
if (!m_internalized) return;
sat2goal s2g;
goal g(m, false, false, false);
s2g.get_learned(m_solver, m_map, m_params, lemmas);
IF_VERBOSE(1, verbose_stream() << "(sat :lemmas " << lemmas.size() << ")\n";);
// TBD: handle externals properly.
}