mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 12:35:59 +00:00
Code Activity

Remove clause methods that should not be used

Browse source
This commit is contained in:
Jakob Rath 2022-12-12 11:47:27 +01:00
parent 5a27ae6b53
commit 9feefa4c0a
2 changed files with 0 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -68,10 +68,6 @@ namespace polysat {
const_iterator begin() const { return m_literals.begin(); }
const_iterator end() const { return m_literals.end(); }
// evaluates under pvar assignment
bool is_always_false(solver& s) const;
bool is_currently_false(solver& s) const;
std::ostream& display(std::ostream& out) const;
void set_redundant(bool r) { m_redundant = r; }