mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-15 12:11:33 -07:00
parent 55a908e357
commit 0d78a10630
3 changed files with 28 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/constraint.cpp
View file

@ -15,16 +15,13 @@ Author:
namespace polysat { namespace polysat {
std::ostream& constraint::display(std::ostream& out) const {
switch (kind()) { constraint* constraint::eq(unsigned lvl, pdd const& p, p_dependency_ref& d) {
case ckind_t::eq_t: return alloc(eq_constraint, lvl, p, dep);
return out << p() << " == 0";
case ckind_t::ule_t:
return out << lhs() << " <=u " << rhs();
case ckind_t::sle_t:
return out << lhs() << " <=s " << rhs();
} }
return out;
std::ostream& constraint::display(std::ostream& out) const {
return out << p() << " == 0";
} }
} }

40
src/math/polysat/constraint.h
View file

@ -22,40 +22,42 @@ namespace polysat {
enum ckind_t { eq_t, ule_t, sle_t }; enum ckind_t { eq_t, ule_t, sle_t };
class eq_constraint;
class ule_constraint;
class constraint { class constraint {
unsigned m_level; unsigned m_level;
ckind_t m_kind; ckind_t m_kind;
pdd m_poly;
pdd m_other;
p_dependency_ref m_dep; p_dependency_ref m_dep;
unsigned_vector m_vars; unsigned_vector m_vars;
constraint(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& dep, ckind_t k): constraint(unsigned lvl, p_dependency_ref& dep, ckind_t k):
m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) { m_level(lvl), m_kind(k), m_dep(dep) {}
m_vars.append(p.free_vars());
if (q != p)
for (auto v : q.free_vars())
m_vars.insert(v);
}
public: public:
static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d) { static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d);
return alloc(constraint, lvl, p, p, d, ckind_t::eq_t);
}
static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& d) {
return alloc(constraint, lvl, p, q, d, ckind_t::ule_t);
}
bool is_eq() const { return m_kind == ckind_t::eq_t; } bool is_eq() const { return m_kind == ckind_t::eq_t; }
bool is_ule() const { return m_kind == ckind_t::ule_t; } bool is_ule() const { return m_kind == ckind_t::ule_t; }
bool is_sle() const { return m_kind == ckind_t::sle_t; } bool is_sle() const { return m_kind == ckind_t::sle_t; }
ckind_t kind() const { return m_kind; } ckind_t kind() const { return m_kind; }
pdd const & p() const { return m_poly; } virtual std::ostream& display(std::ostream& out) const = 0;
pdd const & lhs() const { return m_poly; } eq_constraint& to_eq() { return *dynamic_cast<eq_constraint*>(this); }
pdd const & rhs() const { return m_other; } eq_constraint const& to_eq() { return *dynamic_cast<eq_constraint const*>(this); }
std::ostream& display(std::ostream& out) const;
p_dependency* dep() const { return m_dep; } p_dependency* dep() const { return m_dep; }
unsigned_vector& vars() { return m_vars; } unsigned_vector& vars() { return m_vars; }
unsigned level() const { return m_level; } unsigned level() const { return m_level; }
}; };
class eq_constraint : public constraint {
pdd m_poly;
public:
eq_constraint(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& dep,):
constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
m_vars.append(p.free_vars());
}
pdd const & p() const { return m_poly; }
std::ostream& display(std::ostream& out) const override;
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
} }

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

@ -3,6 +3,7 @@
#endif #endif
#include <utility> #include <utility>
#include "util/util.h"
#include "math/polysat/log.h" #include "math/polysat/log.h"
#if POLYSAT_LOGGING_ENABLED #if POLYSAT_LOGGING_ENABLED