mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Enable conflict logger with polysat.log_conflicts=true

Browse source
This commit is contained in:
Jakob Rath 2023-08-16 09:40:16 +02:00
parent 20ab0bc13a
commit 0bfebe3de1
1 changed files with 8 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -54,8 +54,6 @@ TODO:
#include "math/polysat/variable_elimination.h" #include "math/polysat/variable_elimination.h"
#include <algorithm> #include <algorithm>
#define ENABLE_CONFLICTS_TXT 0
namespace polysat { namespace polysat {
class conflict_resolver { class conflict_resolver {
@ -131,21 +129,18 @@ namespace polysat {
}; };
conflict::conflict(solver& s) : s(s) { conflict::conflict(solver& s) : s(s) {
// TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line
#if ENABLE_CONFLICTS_TXT
if (true || s.get_config().m_log_conflicts)
m_logger = alloc(file_inference_logger, s);
else
m_logger = alloc(dummy_inference_logger);
#else
m_logger = alloc(dummy_inference_logger);
#endif
m_resolver = alloc(conflict_resolver, s); m_resolver = alloc(conflict_resolver, s);
} }
conflict::~conflict() {} conflict::~conflict() {}
inference_logger& conflict::logger() { inference_logger& conflict::logger() {
if (!m_logger) {
if (s.config().m_log_conflicts)
m_logger = alloc(file_inference_logger, s);
else
m_logger = alloc(dummy_inference_logger);
}
return *m_logger; return *m_logger;
} }
@ -232,6 +227,7 @@ namespace polysat {
SASSERT(!empty()); SASSERT(!empty());
// TODO: logger().begin_conflict??? // TODO: logger().begin_conflict???
// TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after... // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
logger().begin_conflict("base level");
} }
void conflict::init(dependency dep, signed_constraint c) { void conflict::init(dependency dep, signed_constraint c) {
@ -504,7 +500,7 @@ namespace polysat {
SASSERT(s.is_assigned(w)); SASSERT(s.is_assigned(w));
m_vars.insert(w); m_vars.insert(w);
}); });
// logger().log(inf_resolve_value(s, v)); TODO logger().log("value was propagated by slicing"); // TODO: add information about v
revert_pvar(v); revert_pvar(v);
} }