mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

assignment helpers

Browse source
This commit is contained in:
Jakob Rath 2022-11-30 14:50:14 +01:00
parent 54a21e764d
commit 9b10733ebd
2 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polysat/assignment.cpp
View file

@ -31,6 +31,11 @@ namespace polysat {
return p.subst_val(m_subst);
}
bool substitution::contains(pvar var) const {
rational out_value;
return value(var, out_value);
}
bool substitution::value(pvar var, rational& out_value) const {
return m_subst.subst_get(var, out_value);
}
@ -49,6 +54,14 @@ namespace polysat {
return a;
}
bool assignment::contains(pvar var) const {
return subst(s().size(var)).contains(var);
}
bool assignment::value(pvar var, rational& out_value) const {
return subst(s().size(var)).value(var, out_value);
}
substitution& assignment::subst(unsigned sz) {
return const_cast<substitution&>(std::as_const(*this).subst(sz));
}

4
src/math/polysat/assignment.h
View file

@ -56,6 +56,7 @@ namespace polysat {
substitution add(pvar var, rational const& value) const;
pdd apply_to(pdd const& p) const;
bool contains(pvar var) const;
bool value(pvar var, rational& out_value) const;
bool empty() const { return m_subst.is_one(); }
@ -96,6 +97,9 @@ namespace polysat {
pdd apply_to(pdd const& p) const;
bool contains(pvar var) const;
bool value(pvar var, rational& out_value) const;
rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
bool empty() const { return pairs().empty(); }
substitution const& subst(unsigned sz) const;
vector<assignment_item_t> const& pairs() const { return m_pairs; }