mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +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 dc3fe93e84
commit 3cbeb99ab3
2 changed files with 24 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -20,17 +20,17 @@ Author:
namespace polysat {
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) {
m_pdd.reserve(sz + 1);
if (!m_pdd[sz])
@ -128,7 +128,7 @@ namespace polysat {
// TODO reduce p using assignment (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);
auto const& vars = c->vars();
if (vars.size() > 0)
@ -348,7 +348,7 @@ namespace polysat {
if (r.is_val()) {
SASSERT(!r.is_zero());
// TBD: UNSAT, set conflict
return 0;
return i;
}
justification& j = m_justification[v];
if (j.is_decision()) {
@ -356,7 +356,7 @@ namespace polysat {
// propagate if new value is given uniquely
// set conflict if viable set is empty
// adding r and reverting last decision.
break;
break;
}
SASSERT(j.is_propagation());
for (auto w : r.free_vars())
@ -423,6 +423,8 @@ namespace polysat {
}
std::ostream& solver::display(std::ostream& out) const {
for (auto* c : m_constraints)
out << *c << "\n";
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 };
class constraint {
unsigned m_level;
ckind_t m_kind;
pdd m_poly;
pdd m_other;
u_dependency* m_dep;
unsigned_vector m_vars;
constraint(pdd const& p, pdd const& q, u_dependency* dep, ckind_t k):
m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
constraint(unsigned lvl, pdd const& p, pdd const& q, u_dependency* dep, ckind_t k):
m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
m_vars.append(p.free_vars());
if (q != p)
for (auto v : q.free_vars())
m_vars.insert(v);
}
public:
static constraint* eq(pdd const& p, u_dependency* d) { return alloc(constraint, p, p, d, ckind_t::eq_t); }
static constraint* ule(pdd const& p, pdd const& q, u_dependency* d) { return alloc(constraint, p, q, d, ckind_t::ule_t); }
static constraint* eq(unsigned lvl, pdd const& p, u_dependency* d) {
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; }
pdd const & p() const { return m_poly; }
pdd const & lhs() const { return m_poly; }
@ -55,35 +60,11 @@ namespace polysat {
std::ostream& display(std::ostream& out) const;
u_dependency* dep() const { return m_dep; }
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); }
/**
* 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.