mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

add global autarky option, update translation of solvers to retain vsids, remove stale code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-14 18:19:21 -08:00
parent 38e4fb307c
commit f7e14b3283
8 changed files with 76 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/c++/z3++.h
View file

@ -2117,6 +2117,7 @@ namespace z3 {
return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
}
}
std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); }
friend std::ostream & operator<<(std::ostream & out, goal const & g);
};
inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }

1
src/sat/sat_config.cpp
View file

@ -112,6 +112,7 @@ namespace sat {
m_lookahead_cube_fraction = p.lookahead_cube_fraction();
m_lookahead_cube_cutoff = p.lookahead_cube_cutoff();
m_lookahead_global_autarky = p.lookahead_global_autarky();
// These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);

1
src/sat/sat_config.h
View file

@ -87,6 +87,7 @@ namespace sat {
unsigned m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
reward_t m_lookahead_reward;
bool m_lookahead_global_autarky;
bool m_incremental;
unsigned m_simplify_mult1;

77
src/sat/sat_lookahead.cpp
View file

@ -233,6 +233,7 @@ namespace sat {
if (is_sat()) {
return false;
}
std::cout << "include newbies\n";
}
SASSERT(!m_candidates.empty());
// cut number of candidates down to max_num_cand.
@ -314,12 +315,19 @@ namespace sat {
double lookahead::init_candidates(unsigned level, bool newbies) {
m_candidates.reset();
double sum = 0;
unsigned skip_candidates = 0;
bool autarky = get_config().m_lookahead_global_autarky;
for (bool_var x : m_freevars) {
SASSERT(is_undef(x));
if (!m_select_lookahead_vars.empty()) {
if (m_select_lookahead_vars.contains(x)) {
m_candidates.push_back(candidate(x, m_rating[x]));
sum += m_rating[x];
if (!autarky || newbies || in_reduced_clause(x)) {
m_candidates.push_back(candidate(x, m_rating[x]));
sum += m_rating[x];
}
else {
skip_candidates++;
}
}
}
else if (newbies || active_prefix(x)) {
@ -328,6 +336,9 @@ namespace sat {
}
}
TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
if (skip_candidates > 0) {
IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";);
}
return sum;
}
@ -1294,8 +1305,7 @@ namespace sat {
unsigned idx = l.index();
unsigned sz = m_ternary_count[idx]--;
auto& tv = m_ternary[idx];
for (unsigned i = sz; i > 0; ) {
--i;
for (unsigned i = sz; i-- > 0; ) {
binary const& b = tv[i];
if (b.m_u == u && b.m_v == v) {
std::swap(tv[i], tv[sz-1]);
@ -1769,10 +1779,6 @@ namespace sat {
0 : get_lookahead_reward(p));
}
bool lookahead::check_autarky(literal l, unsigned level) {
return false;
}
void lookahead::update_lookahead_reward(literal l, unsigned level) {
if (m_lookahead_reward != 0) {
inc_lookahead_reward(l, m_lookahead_reward);
@ -1859,6 +1865,43 @@ namespace sat {
return m_trail.size() - old_sz;
}
/**
\brief check if literal occurs in a non-tautological reduced clause.
*/
bool lookahead::in_reduced_clause(bool_var v) {
return
in_reduced_clause(literal(v, false)) ||
in_reduced_clause(literal(v, true));
}
bool lookahead::in_reduced_clause(literal lit) {
if (lit == null_literal) return true;
if (m_trail_lim.empty()) return true;
unsigned sz = m_nary_count[lit.index()];
for (nary* n : m_nary[lit.index()]) {
if (sz-- == 0) break;
if (!n->is_reduced()) continue;
bool has_true = false;
for (literal l : *n) {
if (is_true(l)) {
has_true = true;
break;
}
}
if (!has_true) return true;
}
auto const& tv = m_ternary[lit.index()];
sz = tv.size();
unsigned i = m_ternary_count[lit.index()];
for (; i < sz; ++i) {
binary const& b = tv[i];
if (!is_true(b.m_u) && !is_true(b.m_v))
return true;
}
return false;
}
void lookahead::validate_assign(literal l) {
if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) {
m_assumptions.push_back(l);
@ -1959,20 +2002,6 @@ namespace sat {
return true;
}
lbool lookahead::cube() {
literal_vector lits;
bool_var_vector vars;
for (bool_var v : m_freevars) vars.push_back(v);
while (true) {
lbool result = cube(vars, lits, UINT_MAX);
if (lits.empty() || result != l_undef) {
return l_undef;
}
display_cube(std::cout, lits);
}
return l_undef;
}
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this);
lits.reset();
@ -2330,13 +2359,9 @@ namespace sat {
// TBD: keep count of ternary and >3-ary clauses.
st.update("lh add binary", m_stats.m_add_binary);
st.update("lh del binary", m_stats.m_del_binary);
st.update("lh add ternary", m_stats.m_add_ternary);
st.update("lh del ternary", m_stats.m_del_ternary);
st.update("lh propagations", m_stats.m_propagations);
st.update("lh decisions", m_stats.m_decisions);
st.update("lh windfalls", m_stats.m_windfall_binaries);
st.update("lh autarky propagations", m_stats.m_autarky_propagations);
st.update("lh autarky equivalences", m_stats.m_autarky_equivalences);
st.update("lh double lookahead propagations", m_stats.m_double_lookahead_propagations);
st.update("lh double lookahead rounds", m_stats.m_double_lookahead_rounds);
}

12
src/sat/sat_lookahead.h
View file

@ -115,12 +115,8 @@ namespace sat {
unsigned m_propagations;
unsigned m_add_binary;
unsigned m_del_binary;
unsigned m_add_ternary;
unsigned m_del_ternary;
unsigned m_decisions;
unsigned m_windfall_binaries;
unsigned m_autarky_propagations;
unsigned m_autarky_equivalences;
unsigned m_double_lookahead_propagations;
unsigned m_double_lookahead_rounds;
stats() { reset(); }
@ -151,9 +147,10 @@ namespace sat {
}
unsigned size() const { return m_size; }
unsigned dec_size() { SASSERT(m_size > 0); return --m_size; }
void inc_size() { SASSERT(m_size < num_lits()); ++m_size; }
void inc_size() { SASSERT(is_reduced()); ++m_size; }
literal get_head() const { return m_head; }
void set_head(literal l) { m_head = l; }
bool is_reduced() const { return m_size < num_lits(); }
literal operator[](unsigned i) { SASSERT(i < num_lits()); return m_literals[i]; }
literal const* begin() const { return m_literals; }
@ -497,7 +494,6 @@ namespace sat {
double get_lookahead_reward(literal l) const { return m_lits[l.index()].m_lookahead_reward; }
void reset_lookahead_reward(literal l);
bool check_autarky(literal l, unsigned level);
void update_lookahead_reward(literal l, unsigned level);
bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; }
void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; }
@ -510,6 +506,8 @@ namespace sat {
unsigned scope_lvl() const { return m_trail_lim.size(); }
bool in_reduced_clause(literal l);
bool in_reduced_clause(bool_var v);
void validate_assign(literal l);
void assign(literal l);
void propagated(literal l);
@ -565,8 +563,6 @@ namespace sat {
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
*/
lbool cube();
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);

1
src/sat/sat_params.pyg
View file

@ -41,6 +41,7 @@ def_module_params('sat',
('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'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))

41
src/sat/sat_solver.cpp
View file

@ -98,7 +98,12 @@ namespace sat {
}
m_phase[v] = src.m_phase[v];
m_prev_phase[v] = src.m_prev_phase[v];
// m_activity[v] = src.m_activity[v], but then update case_split_queue ?
#if 1
// inherit activity:
m_activity[v] = src.m_activity[v];
m_case_split_queue.activity_changed_eh(v, false);
#endif
}
}
@ -115,7 +120,7 @@ namespace sat {
assign(src.m_trail[i], justification());
}
// copy binary clauses that are unblocked.
// copy binary clauses
{
unsigned sz = src.m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
@ -123,13 +128,21 @@ namespace sat {
if (src.was_eliminated(l.var())) continue;
watch_list const & wlist = src.m_watches[l_idx];
for (auto & wi : wlist) {
if (!wi.is_binary_unblocked_clause())
if (!wi.is_binary_clause())
continue;
literal l2 = wi.get_literal();
if (l.index() > l2.index() ||
src.was_eliminated(l2.var()))
continue;
mk_clause_core(l, l2);
watched w1(l2, wi.is_learned());
watched w2(l, wi.is_learned());
if (wi.is_blocked()) {
w1.set_blocked();
w2.set_blocked();
}
m_watches[(~l).index()].push_back(w1);
m_watches[(~l2).index()].push_back(w2);
}
}
}
@ -868,12 +881,6 @@ 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);
@ -976,20 +983,6 @@ namespace sat {
return r;
}
lbool solver::lookahead_cube() {
lookahead lh(*this);
lbool r = l_undef;
try {
r = lh.cube();
}
catch (z3_exception&) {
lh.collect_statistics(m_aux_stats);
throw;
}
lh.collect_statistics(m_aux_stats);
return r;
}
lbool solver::lookahead_search() {
lookahead lh(*this);
lbool r = l_undef;

3
src/sat/sat_solver.h
View file

@ -180,7 +180,6 @@ namespace sat {
friend class lookahead;
friend class local_search;
friend struct mk_stat;
friend class ccc;
friend class elim_vars;
friend class scoped_detach;
public:
@ -395,9 +394,7 @@ namespace sat {
void exchange_par();
lbool check_par(unsigned num_lits, literal const* lits);
lbool lookahead_search();
lbool lookahead_cube();
lbool do_local_search(unsigned num_lits, literal const* lits);
lbool do_ccc();
// -----------------------
//