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

add mode to display to get constraints without wild-card notation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-14 14:13:31 +02:00
parent 15ebbbda2c
commit f9b1b4e65d
3 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -160,7 +160,8 @@ namespace polysat {
virtual bool is_eq() const { return false; } virtual bool is_eq() const { return false; }
bool is_ule() const { return m_kind == ckind_t::ule_t; } bool is_ule() const { return m_kind == ckind_t::ule_t; }
ckind_t kind() const { return m_kind; } ckind_t kind() const { return m_kind; }
virtual std::ostream& display(std::ostream& out, lbool status = l_undef) const = 0; virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
bool propagate(solver& s, bool is_positive, pvar v); bool propagate(solver& s, bool is_positive, pvar v);
virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v); virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);

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

@ -42,6 +42,15 @@ namespace polysat {
return display_extra(out, status); return display_extra(out, status);
} }
std::ostream& ule_constraint::display(std::ostream& out) const {
out << m_lhs;
if (is_eq())
out << " == ";
else
out << " <= ";
return out << m_rhs;
}
void ule_constraint::narrow(solver& s, bool is_positive) { void ule_constraint::narrow(solver& s, bool is_positive) {
LOG_H3("Narrowing " << *this); LOG_H3("Narrowing " << *this);
LOG("Assignment: " << assignments_pp(s)); LOG("Assignment: " << assignments_pp(s));

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

@ -36,6 +36,7 @@ namespace polysat {
pdd const& lhs() const { return m_lhs; } pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; } pdd const& rhs() const { return m_rhs; }
std::ostream& display(std::ostream& out, lbool status) const override; std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const;
bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const; bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const;
bool is_always_false(bool is_positive) const override; bool is_always_false(bool is_positive) const override;
bool is_currently_false(solver& s, bool is_positive) const override; bool is_currently_false(solver& s, bool is_positive) const override;