mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
comment
This commit is contained in:
parent
a3de478c93
commit
05abf19009
|
@ -767,11 +767,15 @@ namespace qe {
|
|||
val2rep.insert(val, rep);
|
||||
}
|
||||
}
|
||||
// TBD: ignore distinct on Booleans
|
||||
|
||||
// TBD: optimize further based on implied values (e.g.,
|
||||
// some literals are forced to be true/false) and based on
|
||||
// unique_values (e.g., (x=1 & y=1) does not require
|
||||
// (x!=y) to be added
|
||||
ptr_buffer<expr> reps;
|
||||
for (auto &kv : val2rep) {
|
||||
expr *val = kv.m_value;
|
||||
if (!m.is_unique_value(val))
|
||||
expr *rep = kv.m_value;
|
||||
if (!m.is_unique_value(rep))
|
||||
reps.push_back(kv.m_value);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue