mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-01-03 17:48:21 +01:00
commit 075b548089
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;
public:
virtual ~bit_justification() = default;
// 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)
@ -92,7 +93,7 @@ namespace polysat {
bit_justification* get_justification() { return m_justification; }
virtual bool can_dealloc() {
bool can_dealloc() override {
m_references = m_references == 0 ? 0 : m_references - 1;
if (m_references != 0)
return false;
@ -103,7 +104,7 @@ namespace polysat {
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);
m_justification->get_dependencies(fixed, to_process);
}
@ -124,7 +125,7 @@ namespace polysat {
public:
bool has_constraint(constraint*& constr) {
bool has_constraint(constraint*& constr) override {
constr = m_constraint;
return true;
}