mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
more efficient lar_solver::get_model
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
parent
712619a9cf
commit
95f86ae2c0
|
@ -1259,7 +1259,7 @@ public:
|
|||
|
||||
|
||||
void get_model(std::unordered_map<var_index, mpq> & variable_values) const {
|
||||
mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
|
||||
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes
|
||||
lean_assert(m_status == OPTIMAL);
|
||||
unsigned i;
|
||||
do {
|
||||
|
@ -1267,7 +1267,6 @@ public:
|
|||
// different pairs have to produce different singleton values
|
||||
std::unordered_set<impq> set_of_different_pairs;
|
||||
std::unordered_set<mpq> set_of_different_singles;
|
||||
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
|
||||
for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
|
||||
const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
|
||||
set_of_different_pairs.insert(rp);
|
||||
|
|
Loading…
Reference in a new issue