mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix format bug (issue 126) and smaller nits in sat solver (const annotation, disable elimination of external or already elimianted variables)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-04 18:35:18 -07:00
parent fbb01f3699
commit 6a3f75822d
12 changed files with 22 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_asymm_branch.cpp
View file

@ -215,7 +215,7 @@ namespace sat {
sat_asymm_branch_params::collect_param_descrs(d); sat_asymm_branch_params::collect_param_descrs(d);
} }
void asymm_branch::collect_statistics(statistics & st) { void asymm_branch::collect_statistics(statistics & st) const {
st.update("elim literals", m_elim_literals); st.update("elim literals", m_elim_literals);
} }

2
src/sat/sat_asymm_branch.h
View file

@ -49,7 +49,7 @@ namespace sat {
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
void collect_statistics(statistics & st); void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();
void dec(unsigned c) { m_counter -= c; } void dec(unsigned c) { m_counter -= c; }

2
src/sat/sat_cleaner.cpp
View file

@ -206,7 +206,7 @@ namespace sat {
m_elim_literals = 0; m_elim_literals = 0;
} }
void cleaner::collect_statistics(statistics & st) { void cleaner::collect_statistics(statistics & st) const {
st.update("elim clauses", m_elim_clauses); st.update("elim clauses", m_elim_clauses);
st.update("elim literals", m_elim_literals); st.update("elim literals", m_elim_literals);
} }

2
src/sat/sat_cleaner.h
View file

@ -42,7 +42,7 @@ namespace sat {
bool operator()(bool force = false); bool operator()(bool force = false);
void collect_statistics(statistics & st); void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();
void dec() { m_cleanup_counter--; } void dec() { m_cleanup_counter--; }

3
src/sat/sat_probing.cpp
View file

@ -196,6 +196,7 @@ namespace sat {
s.propagate(false); // make sure propagation queue is empty s.propagate(false); // make sure propagation queue is empty
if (s.inconsistent()) if (s.inconsistent())
return true; return true;
SASSERT(s.m_qhead == s.m_trail.size());
CASSERT("probing", s.check_invariant()); CASSERT("probing", s.check_invariant());
if (!force && m_counter > 0) if (!force && m_counter > 0)
return true; return true;
@ -259,7 +260,7 @@ namespace sat {
m_to_assert.finalize(); m_to_assert.finalize();
} }
void probing::collect_statistics(statistics & st) { void probing::collect_statistics(statistics & st) const {
st.update("probing assigned", m_num_assigned); st.update("probing assigned", m_num_assigned);
} }

2
src/sat/sat_probing.h
View file

@ -71,7 +71,7 @@ namespace sat {
void free_memory(); void free_memory();
void collect_statistics(statistics & st); void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();
// return the literals implied by l. // return the literals implied by l.

2
src/sat/sat_scc.cpp
View file

@ -223,7 +223,7 @@ namespace sat {
return to_elim.size(); return to_elim.size();
} }
void scc::collect_statistics(statistics & st) { void scc::collect_statistics(statistics & st) const {
st.update("elim bool vars", m_num_elim); st.update("elim bool vars", m_num_elim);
} }

2
src/sat/sat_scc.h
View file

@ -40,7 +40,7 @@ namespace sat {
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
void collect_statistics(statistics & st); void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();
}; };
}; };

8
src/sat/sat_simplifier.cpp
View file

@ -918,7 +918,11 @@ namespace sat {
void process(literal l) { void process(literal l) {
TRACE("blocked_clause", tout << "processing: " << l << "\n";); TRACE("blocked_clause", tout << "processing: " << l << "\n";);
model_converter::entry * new_entry = 0; model_converter::entry * new_entry = 0;
if (s.is_external(l.var()) || s.was_eliminated(l.var()))
return;
{ {
m_to_remove.reset(); m_to_remove.reset();
{ {
clause_use_list & occs = s.m_use_list.get(l); clause_use_list & occs = s.m_use_list.get(l);
@ -1339,6 +1343,7 @@ namespace sat {
} }
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
// eliminate variable // eliminate variable
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
save_clauses(mc_entry, m_pos_cls); save_clauses(mc_entry, m_pos_cls);
@ -1421,6 +1426,7 @@ namespace sat {
}; };
void simplifier::elim_vars() { void simplifier::elim_vars() {
IF_VERBOSE(10, s.display(verbose_stream()););
elim_var_report rpt(*this); elim_var_report rpt(*this);
bool_var_vector vars; bool_var_vector vars;
order_vars_for_elim(vars); order_vars_for_elim(vars);
@ -1466,7 +1472,7 @@ namespace sat {
sat_simplifier_params::collect_param_descrs(r); sat_simplifier_params::collect_param_descrs(r);
} }
void simplifier::collect_statistics(statistics & st) { void simplifier::collect_statistics(statistics & st) const {
st.update("subsumed", m_num_subsumed); st.update("subsumed", m_num_subsumed);
st.update("subsumption resolution", m_num_sub_res); st.update("subsumption resolution", m_num_sub_res);
st.update("elim literals", m_num_elim_lits); st.update("elim literals", m_num_elim_lits);

2
src/sat/sat_simplifier.h
View file

@ -180,7 +180,7 @@ namespace sat {
void free_memory(); void free_memory();
void collect_statistics(statistics & st); void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();
}; };
}; };

4
src/sat/sat_solver.cpp
View file

@ -459,9 +459,6 @@ namespace sat {
void solver::set_conflict(justification c, literal not_l) { void solver::set_conflict(justification c, literal not_l) {
if (m_inconsistent) if (m_inconsistent)
return; return;
TRACE("sat_conflict", tout << "conflict\n";);
// int * p = 0;
// *p = 0;
m_inconsistent = true; m_inconsistent = true;
m_conflict = c; m_conflict = c;
m_not_l = not_l; m_not_l = not_l;
@ -863,6 +860,7 @@ namespace sat {
m_next_simplify = 0; m_next_simplify = 0;
m_stopwatch.reset(); m_stopwatch.reset();
m_stopwatch.start(); m_stopwatch.start();
TRACE("sat", display(tout););
} }
/** /**

8
src/util/cmd_context_types.h
View file

@ -55,12 +55,12 @@ class cmd_exception : public default_exception {
} }
public: public:
cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {} cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {}
cmd_exception(std::string const & msg):default_exception(msg.c_str()), m_line(-1), m_pos(-1) {} cmd_exception(std::string const & msg):default_exception(msg), m_line(-1), m_pos(-1) {}
cmd_exception(std::string const & msg, int line, int pos):default_exception(msg.c_str()), m_line(line), m_pos(pos) {} cmd_exception(std::string const & msg, int line, int pos):default_exception(msg), m_line(line), m_pos(pos) {}
cmd_exception(char const * msg, symbol const & s): cmd_exception(char const * msg, symbol const & s):
default_exception(compose(msg,s).c_str()),m_line(-1),m_pos(-1) {} default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {}
cmd_exception(char const * msg, symbol const & s, int line, int pos): cmd_exception(char const * msg, symbol const & s, int line, int pos):
default_exception(compose(msg,s).c_str()),m_line(line),m_pos(pos) {} default_exception(compose(msg,s)),m_line(line),m_pos(pos) {}
bool has_pos() const { return m_line >= 0; } bool has_pos() const { return m_line >= 0; }
int line() const { SASSERT(has_pos()); return m_line; } int line() const { SASSERT(has_pos()); return m_line; }