mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

compile

Browse source
This commit is contained in:
Jakob Rath 2023-01-03 14:55:50 +01:00
parent 84a5ec221f
commit 283e60a5cb
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/fixed_bits.h
View file

@ -68,6 +68,7 @@ namespace polysat {
bit_justification() = default; bit_justification() = default;
public: public:
virtual ~bit_justification() = default;
// if we reduce this value we would have to reduce some decision levels of justifications depending on it. // if we reduce this value we would have to reduce some decision levels of justifications depending on it.
// However, we don't do this for now. (Should be still correct but generate weaker justifications) // However, we don't do this for now. (Should be still correct but generate weaker justifications)
@ -92,7 +93,7 @@ namespace polysat {
bit_justification* get_justification() { return m_justification; } bit_justification* get_justification() { return m_justification; }
virtual bool can_dealloc() { bool can_dealloc() override {
m_references = m_references == 0 ? 0 : m_references - 1; m_references = m_references == 0 ? 0 : m_references - 1;
if (m_references != 0) if (m_references != 0)
return false; return false;
@ -103,7 +104,7 @@ namespace polysat {
return true; return true;
} }
virtual void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override { void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override {
SASSERT(m_justification); SASSERT(m_justification);
m_justification->get_dependencies(fixed, to_process); m_justification->get_dependencies(fixed, to_process);
} }
@ -124,7 +125,7 @@ namespace polysat {
public: public:
bool has_constraint(constraint*& constr) { bool has_constraint(constraint*& constr) override {
constr = m_constraint; constr = m_constraint;
return true; return true;
} }