diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 1ca8a8c69..07ef61247 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -35,7 +35,7 @@ Notes: namespace polysat { - class inference_logger { + class old_inference_logger { uint_set m_used_constraints; uint_set m_used_vars; scoped_ptr m_out = nullptr; @@ -55,7 +55,10 @@ namespace polysat { public: void begin_conflict(char const* text) { ++m_conflicts; - LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")"); + if (text) + LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")"); + else + LOG("Begin CONFLICT #" << m_conflicts); m_used_constraints.reset(); m_used_vars.reset(); if (!m_out) @@ -139,7 +142,7 @@ namespace polysat { inf_engines.push_back(alloc(inf_saturate, s)); // TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it if (true || s.get_config().m_log_conflicts) - m_logger = alloc(inference_logger); + m_logger = alloc(old_inference_logger); } conflict::~conflict() {} diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 5cc314a47..ce54f97c5 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -72,6 +72,7 @@ Lemma: y < z or xz <= xy or O(x,y) #pragma once #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" +#include "math/polysat/inference_logger.h" #include namespace polysat { @@ -81,22 +82,7 @@ namespace polysat { class inference_engine; class variable_elimination_engine; class conflict_iterator; - class inference_logger; - - class inference { - public: - virtual ~inference() {} - virtual std::ostream& display(std::ostream& out) const = 0; - }; - - inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); } - - class inference_named : public inference { - char const* m_name; - public: - inference_named(char const* name) : m_name(name) { SASSERT(name); } - std::ostream& display(std::ostream& out) const override { return out << m_name; } - }; + class old_inference_logger; enum class conflict_kind_t { ok, @@ -122,8 +108,8 @@ namespace polysat { */ conflict_kind_t m_kind = conflict_kind_t::ok; - friend class inference_logger; - scoped_ptr m_logger; + friend class old_inference_logger; + scoped_ptr m_logger; bool_vector m_bvar2mark; // mark of Boolean variables @@ -142,7 +128,7 @@ namespace polysat { ~conflict(); /// Begin next conflict - void begin_conflict(char const* text); + void begin_conflict(char const* text = nullptr); /// Log inference at the current state. void log_inference(inference const& inf); void log_inference(char const* name) { log_inference(inference_named(name)); } diff --git a/src/math/polysat/conflict2.h b/src/math/polysat/conflict2.h index 6cec7714c..6d8811994 100644 --- a/src/math/polysat/conflict2.h +++ b/src/math/polysat/conflict2.h @@ -72,6 +72,7 @@ Lemma: y < z or xz <= xy or O(x,y) #pragma once #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" +#include "math/polysat/inference_logger.h" #include namespace polysat { diff --git a/src/math/polysat/inference_logger.h b/src/math/polysat/inference_logger.h index 3c0623e24..9fe84b228 100644 --- a/src/math/polysat/inference_logger.h +++ b/src/math/polysat/inference_logger.h @@ -24,9 +24,23 @@ namespace polysat { class clause_builder; class search_item; - class inference; class solver; + class inference { + public: + virtual ~inference() {} + virtual std::ostream& display(std::ostream& out) const = 0; + }; + + inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); } + + class inference_named : public inference { + char const* m_name; + public: + inference_named(char const* name) : m_name(name) { SASSERT(name); } + std::ostream& display(std::ostream& out) const override { return out << m_name; } + }; + class inference_logger { public: virtual ~inference_logger() {} @@ -86,23 +100,4 @@ namespace polysat { void log_lemma(clause_builder const& cb) override; }; - - - class inference { - public: - virtual ~inference() {} - virtual std::ostream& display(std::ostream& out) const = 0; - }; - - inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); } - - - - class inference_named : public inference { - char const* m_name; - public: - inference_named(char const* name) : m_name(name) { SASSERT(name); } - std::ostream& display(std::ostream& out) const override { return out << m_name; } - }; - } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 1f38af748..53ff102b9 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -33,6 +33,7 @@ namespace polysat { m_viable_fallback(*this), m_linear_solver(*this), m_conflict(*this), + m_conflict2(*this), m_simplify_clause(*this), m_simplify(*this), m_restart(*this), diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ba940d7d5..23e967142 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -22,6 +22,7 @@ Author: #include "util/params.h" #include "math/polysat/boolean.h" #include "math/polysat/conflict.h" +#include "math/polysat/conflict2.h" #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" #include "math/polysat/simplify_clause.h" @@ -69,13 +70,14 @@ namespace polysat { friend class clause; friend class clause_builder; friend class conflict; + friend class conflict2; friend class conflict_explainer; friend class simplify_clause; friend class simplify; friend class restart; friend class explainer; friend class inference_engine; - friend class inference_logger; + friend class old_inference_logger; friend class file_inference_logger; friend class forbidden_intervals; friend class linear_solver; @@ -101,7 +103,8 @@ namespace polysat { viable m_viable; // viable sets per variable viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints linear_solver m_linear_solver; - conflict m_conflict; + conflict m_conflict; + conflict2 m_conflict2; simplify_clause m_simplify_clause; simplify m_simplify; restart m_restart;