mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +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 21:53:27 -07:00
parent 12ccd99e84
commit dce9740a38
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,6 +36,7 @@ namespace polysat {
m_level(lvl), m_kind(k), m_dep(dep) {}
public:
static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d);
virtual ~constraint() {}
bool is_eq() const { return m_kind == ckind_t::eq_t; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
bool is_sle() const { return m_kind == ckind_t::sle_t; }
@ -59,6 +60,7 @@ namespace polysat {
constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
m_vars.append(p.free_vars());
}
~eq_constraint() override {}
pdd const & p() const { return m_poly; }
std::ostream& display(std::ostream& out) const override;
bool propagate(solver& s, pvar v) override;