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

Refactor final_check_eh by removing comments

Browse source 
Removed redundant comments and cleaned up code.
This commit is contained in:
Nikolaj Bjorner 2025-10-15 14:45:57 +02:00 • committed by GitHub
parent 63847be2c0
commit d7035a25e7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_finite_set.cpp
View file

@ -98,15 +98,20 @@ namespace smt {
final_check_status theory_finite_set::final_check_eh() { final_check_status theory_finite_set::final_check_eh() {
TRACE("finite_set", tout << "final_check_eh\n";); TRACE("finite_set", tout << "final_check_eh\n";);
// walk all parents of elem in congruence table.
// if a parent is of the form elem' in S u T, or similar.
// create clauses for elem = elem' => clause.
// if a new clause was added, return FC_CONTINUE
bool new_clause = false; bool new_clause = false;
expr* elem1 = nullptr, *set1 = nullptr;
for (auto elem : m_elements) { for (auto elem : m_elements) {
for (auto p : enode::parents(elem)) { for (auto p : enode::parents(elem)) {
if (!u.is_in(p->get_expr(), elem1, set1))
continue;
if (elem->get_root() != p->get_arg(0)->get_root())
continue; // elem is then equal to set1 but not elem1. This is a different case.
instantiate_axioms(elem->get_expr(), set1->get_expr());
} }
// walk all parents of elem in congruence table.
// if a parent is of the form elem' in S u T, or similar.
// create clauses for elem = elem' => clause.
// if a new clause was added, return FC_CONTINUE
} }
return new_clause ? FC_CONTINUE : FC_DONE; return new_clause ? FC_CONTINUE : FC_DONE;