mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

make it compile

Browse source
This commit is contained in:
Jakob Rath 2022-08-26 16:28:52 +02:00
parent f819c2bad8
commit acf9976df9
6 changed files with 33 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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<std::ostream> 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() {}

24
src/math/polysat/conflict.h
View file

@ -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 <optional>
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<inference_logger> m_logger;
friend class old_inference_logger;
scoped_ptr<old_inference_logger> 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)); }

1
src/math/polysat/conflict2.h
View file

@ -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 <optional>
namespace polysat {

35
src/math/polysat/inference_logger.h
View file

@ -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; }
};
}

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

@ -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),

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

@ -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;