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

Perform clause simplification earlier

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 13:07:38 +01:00
parent 44f0f88172
commit 5f2fd039ba
8 changed files with 57 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/boolean.cpp
View file

@ -72,7 +72,7 @@ namespace polysat {
}
void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
LOG_V("Evaluate " << lit << " @ " << lvl);
LOG_V(10, "Evaluate " << lit << " @ " << lvl);
assign(kind_t::evaluation, lit, lvl, nullptr);
SASSERT(is_evaluation(lit));
}

7
src/math/polysat/conflict.cpp
View file

@ -304,12 +304,13 @@ namespace polysat {
void conflict::add_lemma(char const* name, clause_ref lemma) {
for (auto lit : *lemma)
if (s.m_bvars.is_true(lit))
for (auto lit : *lemma)
if (s.m_bvars.is_true(lit))
verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
SASSERT(lemma);
s.m_simplify_clause.apply(*lemma);
lemma->set_redundant(true);
for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit));

2
src/math/polysat/constraint_manager.cpp
View file

@ -56,7 +56,7 @@ namespace polysat {
/** Add constraint to per-level storage */
void constraint_manager::store(constraint* c) {
LOG_V("Store constraint: " << show_deref(c));
LOG_V(20, "Store constraint: " << show_deref(c));
m_constraints.push_back(c);
}

4
src/math/polysat/log.cpp
View file

@ -65,9 +65,11 @@ static LogLevel get_max_log_level(std::string const& fn, std::string const& pret
}
/// Filter log messages
bool polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn) {
bool polysat_should_log(unsigned verbose_lvl, LogLevel msg_level, std::string fn, std::string pretty_fn) {
if (!g_log_enabled)
return false;
if (get_verbosity_level() < verbose_lvl)
return false;
LogLevel max_log_level = get_max_log_level(fn, pretty_fn);
return msg_level <= max_log_level;
}

68
src/math/polysat/log.h
View file

@ -61,7 +61,7 @@ enum class LogLevel : int {
/// Filter log messages
bool
polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
polysat_should_log(unsigned verbose_lvl, LogLevel msg_level, std::string fn, std::string pretty_fn);
std::pair<std::ostream&, bool>
polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
@ -70,31 +70,36 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
#define __PRETTY_FUNCTION__ __FUNCSIG__
#endif
#define LOG_(lvl, x) \
do { \
if (polysat_should_log(lvl, __func__, __PRETTY_FUNCTION__)) { \
auto pair = polysat_log(lvl, __func__, __PRETTY_FUNCTION__); \
std::ostream& os = pair.first; \
bool should_reset = pair.second; \
os << x; \
if (should_reset) \
os << color_reset(); \
os << std::endl; \
} \
#define LOG_(verbose_lvl, log_lvl, x) \
do { \
if (polysat_should_log(verbose_lvl, log_lvl, __func__, __PRETTY_FUNCTION__)) { \
auto pair = polysat_log(log_lvl, __func__, __PRETTY_FUNCTION__); \
std::ostream& os = pair.first; \
bool should_reset = pair.second; \
os << x; \
if (should_reset) \
os << color_reset(); \
os << std::endl; \
} \
} while (false)
#define LOG_CONCAT_HELPER(a,b) a ## b
#define LOG_CONCAT(a,b) LOG_CONCAT_HELPER(a,b)
#define LOG_INDENT(lvl, x) \
LOG_(lvl, x); \
#define LOG_INDENT(verbose_lvl, log_lvl, x) \
LOG_(verbose_lvl, log_lvl, x); \
polysat_log_indent LOG_CONCAT(polysat_log_indent_obj_, __LINE__) (4);
#define LOG_H1(x) LOG_INDENT(LogLevel::Heading1, x)
#define LOG_H2(x) LOG_INDENT(LogLevel::Heading2, x)
#define LOG_H3(x) LOG_INDENT(LogLevel::Heading3, x)
#define LOG(x) LOG_(LogLevel::Default , x)
#define LOG_V(x) LOG_(LogLevel::Verbose , x)
#define LOG_H1(x) LOG_INDENT(0, LogLevel::Heading1, x)
#define LOG_H2(x) LOG_INDENT(0, LogLevel::Heading2, x)
#define LOG_H3(x) LOG_INDENT(0, LogLevel::Heading3, x)
#define LOG(x) LOG_(0, LogLevel::Default , x)
#define LOG_H1_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading1, x)
#define LOG_H2_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading2, x)
#define LOG_H3_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading3, x)
#define LOG_V(verbose_lvl, x) LOG_(verbose_lvl, LogLevel::Verbose , x)
#define COND_LOG(c, x) if (c) LOG(x)
#define LOGE(x) LOG(#x << " = " << (x))
@ -110,18 +115,23 @@ inline void set_log_enabled(bool) {}
inline bool get_log_enabled() { return false; }
class scoped_set_log_enabled {};
#define LOG_(lvl, x) \
do { \
/* do nothing */ \
#define LOG_(vlvl, lvl, x) \
do { \
/* do nothing */ \
} while (false)
#define LOG_H1(x) LOG_(0, x)
#define LOG_H2(x) LOG_(0, x)
#define LOG_H3(x) LOG_(0, x)
#define LOG(x) LOG_(0, x)
#define LOG_V(x) LOG_(0, x)
#define COND_LOG(c, x) LOG_(c, x)
#define LOGE(x) LOG_(0, x)
#define LOG_H1(x) LOG_(0, 0, x)
#define LOG_H2(x) LOG_(0, 0, x)
#define LOG_H3(x) LOG_(0, 0, x)
#define LOG(x) LOG_(0, 0, x)
#define LOG_H1_V(v, x) LOG_(v, 0, x)
#define LOG_H2_V(v, x) LOG_(v, 0, x)
#define LOG_H3_V(v, x) LOG_(v, 0, x)
#define LOG_V(v, x) LOG_(v, 0, x)
#define COND_LOG(c, x) LOG_(0, c, x)
#define LOGE(x) LOG_(0, 0, x)
#define IF_LOGGING(x) \
do { \

6
src/math/polysat/simplify_clause.cpp
View file

@ -94,7 +94,7 @@ namespace polysat {
sat::literal eq = sat::null_literal;
rational k;
for (sat::literal lit : cl) {
LOG_V("Examine " << lit_pp(s, lit));
LOG_V(10, "Examine " << lit_pp(s, lit));
lbool status = s.m_bvars.value(lit);
// skip premise literals
if (status == l_false)
@ -237,7 +237,7 @@ namespace polysat {
for (unsigned i = 0; i < cl.size(); ++i) {
subs_entry& entry = m_entries[i];
sat::literal lit = cl[i];
LOG("Literal " << lit_pp(s, lit));
LOG_V(10, "Literal " << lit_pp(s, lit));
signed_constraint c = s.lit2cnstr(lit);
prepare_subs_entry(entry, c);
}
@ -254,7 +254,7 @@ namespace polysat {
continue;
if (e.interval.currently_contains(f.interval)) {
// f subset of e ==> f.src subsumed by e.src
LOG("Removing " << s.lit2cnstr(cl[i]) << " because it subsumes " << s.lit2cnstr(cl[j]));
LOG("Removing " << cl[i] << ": " << s.lit2cnstr(cl[i]) << " because it subsumes " << cl[j] << ": " << s.lit2cnstr(cl[j]));
e.subsuming = true;
any_subsumed = true;
break;

7
src/math/polysat/solver.cpp
View file

@ -397,7 +397,7 @@ namespace polysat {
void solver::add_pwatch(constraint* c, pvar v) {
SASSERT(m_locked_wlist != v); // the propagate loop will not discover the new size
LOG_V("Watching v" << v << " in constraint " << show_deref(c));
LOG_V(20, "Watching v" << v << " in constraint " << show_deref(c));
m_pwatch[v].push_back(c);
}
@ -498,7 +498,7 @@ namespace polysat {
}
case trail_instr_t::assign_i: {
auto v = m_search.back().var();
LOG_V("Undo assign_i: v" << v);
LOG_V(20, "Undo assign_i: v" << v);
unsigned active_level = get_level(v);
if (active_level <= target_level) {
@ -514,7 +514,7 @@ namespace polysat {
}
case trail_instr_t::assign_bool_i: {
sat::literal lit = m_search.back().lit();
LOG_V("Undo assign_bool_i: " << lit);
LOG_V(20, "Undo assign_bool_i: " << lit);
unsigned active_level = m_bvars.level(lit);
if (active_level <= target_level)
@ -944,7 +944,6 @@ namespace polysat {
clause* best_lemma = nullptr;
auto appraise_lemma = [&](clause* lemma) {
m_simplify_clause.apply(*lemma);
auto score = compute_lemma_score(*lemma);
if (score)
LOG(" score: " << *score);

6
src/math/polysat/ule_constraint.cpp
View file

@ -185,9 +185,9 @@ namespace polysat {
signed_constraint sc(this, is_positive);
LOG_H3("Narrowing " << sc);
LOG_V("Assignment: " << assignments_pp(s));
LOG_V("Substituted LHS: " << lhs() << " := " << p);
LOG_V("Substituted RHS: " << rhs() << " := " << q);
LOG_V(10, "Assignment: " << assignments_pp(s));
LOG_V(10, "Substituted LHS: " << lhs() << " := " << p);
LOG_V(10, "Substituted RHS: " << rhs() << " := " << q);
if (is_always_false(is_positive, p, q)) {
s.set_conflict(sc);