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

minor adjustments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-03-30 20:38:40 -07:00
parent d2e25989b3
commit 7d4818d52c
2 changed files with 24 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/polysat.cpp
View file

@ -20,15 +20,15 @@ Author:
namespace polysat { namespace polysat {
std::ostream& constraint::display(std::ostream& out) const { std::ostream& constraint::display(std::ostream& out) const {
return out << "constraint"; switch (kind()) {
case ckind_t::eq_t:
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& linear::display(std::ostream& out) const {
return out << "linear";
}
std::ostream& mono::display(std::ostream& out) const {
return out << "mono";
} }
dd::pdd_manager& solver::sz2pdd(unsigned sz) { dd::pdd_manager& solver::sz2pdd(unsigned sz) {
@ -128,7 +128,7 @@ namespace polysat {
// TODO reduce p using assignment (at current level, // TODO reduce p using assignment (at current level,
// assuming constraint is removed also at current level). // assuming constraint is removed also at current level).
// //
constraint* c = constraint::eq(p, m_dep_manager.mk_leaf(dep)); constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep));
m_constraints.push_back(c); m_constraints.push_back(c);
auto const& vars = c->vars(); auto const& vars = c->vars();
if (vars.size() > 0) if (vars.size() > 0)
@ -348,7 +348,7 @@ namespace polysat {
if (r.is_val()) { if (r.is_val()) {
SASSERT(!r.is_zero()); SASSERT(!r.is_zero());
// TBD: UNSAT, set conflict // TBD: UNSAT, set conflict
return 0; return i;
} }
justification& j = m_justification[v]; justification& j = m_justification[v];
if (j.is_decision()) { if (j.is_decision()) {
@ -423,6 +423,8 @@ namespace polysat {
} }
std::ostream& solver::display(std::ostream& out) const { std::ostream& solver::display(std::ostream& out) const {
for (auto* c : m_constraints)
out << *c << "\n";
return out; return out;
} }

39
src/math/polysat/polysat.h
View file

@ -33,21 +33,26 @@ namespace polysat {
enum ckind_t { eq_t, ule_t, sle_t }; enum ckind_t { eq_t, ule_t, sle_t };
class constraint { class constraint {
unsigned m_level;
ckind_t m_kind; ckind_t m_kind;
pdd m_poly; pdd m_poly;
pdd m_other; pdd m_other;
u_dependency* m_dep; u_dependency* m_dep;
unsigned_vector m_vars; unsigned_vector m_vars;
constraint(pdd const& p, pdd const& q, u_dependency* dep, ckind_t k): constraint(unsigned lvl, pdd const& p, pdd const& q, u_dependency* dep, ckind_t k):
m_kind(k), m_poly(p), m_other(q), m_dep(dep) { m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
m_vars.append(p.free_vars()); m_vars.append(p.free_vars());
if (q != p) if (q != p)
for (auto v : q.free_vars()) for (auto v : q.free_vars())
m_vars.insert(v); m_vars.insert(v);
} }
public: public:
static constraint* eq(pdd const& p, u_dependency* d) { return alloc(constraint, p, p, d, ckind_t::eq_t); } static constraint* eq(unsigned lvl, pdd const& p, u_dependency* d) {
static constraint* ule(pdd const& p, pdd const& q, u_dependency* d) { return alloc(constraint, p, q, d, ckind_t::ule_t); } return alloc(constraint, lvl, p, p, d, ckind_t::eq_t);
}
static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, u_dependency* d) {
return alloc(constraint, lvl, p, q, d, ckind_t::ule_t);
}
ckind_t kind() const { return m_kind; } ckind_t kind() const { return m_kind; }
pdd const & p() const { return m_poly; } pdd const & p() const { return m_poly; }
pdd const & lhs() const { return m_poly; } pdd const & lhs() const { return m_poly; }
@ -55,35 +60,11 @@ namespace polysat {
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
u_dependency* dep() const { return m_dep; } u_dependency* dep() const { return m_dep; }
unsigned_vector& vars() { return m_vars; } unsigned_vector& vars() { return m_vars; }
unsigned level() const { return m_level; }
}; };
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); }
/**
* linear term is has an offset and is linear addition of variables.
*/
class linear : public vector<std::pair<unsigned, rational>> {
rational m_offset;
public:
linear(rational const& offset): m_offset(offset) {}
rational const& offset() const { return m_offset; }
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, linear const& l) { return l.display(out); }
/**
* monomial is a list of variables and coefficient.
*/
class mono : public unsigned_vector {
rational m_coeff;
public:
mono(rational const& coeff): m_coeff(coeff) {}
rational const& coeff() const { return m_coeff; }
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, mono const& m) { return m.display(out); }
/** /**
* Justification kind for a variable assignment. * Justification kind for a variable assignment.