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

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-22 12:10:31 -08:00
commit 86589c2553
3 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -50,9 +50,6 @@ static LogLevel get_max_log_level(std::string const& fn, std::string const& pret
(void)fn;
(void)pretty_fn;
if (fn == "push_cjust")
return LogLevel::Verbose;
// if (fn == "pop_levels")
// return LogLevel::Default;

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

@ -56,7 +56,6 @@ enum class LogLevel : int {
Heading2 = 2,
Heading3 = 3,
Default = 4,
Verbose = 5,
};
/// Filter log messages
@ -98,7 +97,7 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
#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 LOG_V(verbose_lvl, x) LOG_(verbose_lvl, LogLevel::Default , x)
#define COND_LOG(c, x) if (c) LOG(x)
#define LOGE(x) LOG(#x << " = " << (x))

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

@ -115,6 +115,14 @@ namespace polysat {
continue;
if (c->is_eq())
continue;
#if 1
// Disable the case p<q && p=q for now.
// The merging of less-than and equality may remove premises from the lemma.
// See test_band5.
// TODO: fix and re-enable
if (c.is_negative())
continue;
#endif
LOG_V(10, "Examine: " << lit_pp(s, lit));
pdd const p = c->to_ule().lhs();
pdd const q = c->to_ule().rhs();