mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

replace size by data_size

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-22 11:16:36 -07:00
parent 85661c415d
commit 4b6ca6a10c
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/nra_solver.cpp
View file

@ -1,6 +1,6 @@
/* /*
Copyright (c) 2017 Microsoft Corporation Copyright (c) 2017 Microsoft Corporation
Author: Nikolaj Bjorner Author: Nikolaj Bjorner, Lev Nachmanson
*/ */
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
@ -85,7 +85,12 @@ struct solver::imp {
throw; throw;
} }
} }
TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n");); TRACE("arith",
m_nlsat->display(tout << r << "\n");
display(tout);
for (auto kv : m_lp2nl)
tout << "j" << kv.m_key << " := x" << kv.m_value << "\n";
);
switch (r) { switch (r) {
case l_true: case l_true:
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
@ -183,14 +188,11 @@ struct solver::imp {
if (!m_lp2nl.find(v, r)) { if (!m_lp2nl.find(v, r)) {
r = m_nlsat->mk_var(is_int(v)); r = m_nlsat->mk_var(is_int(v));
m_lp2nl.insert(v, r); m_lp2nl.insert(v, r);
TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
#if 1
if (!m_term_set.contains(v) && s.column_corresponds_to_term(v)) { if (!m_term_set.contains(v) && s.column_corresponds_to_term(v)) {
if (v >= m_term_set.size()) if (v >= m_term_set.data_size())
m_term_set.resize(v + 1); m_term_set.resize(v + 1);
m_term_set.insert(v); m_term_set.insert(v);
} }
#endif
} }
return r; return r;
} }