mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

rename var_info to var_lists in niil_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-19 15:46:13 +08:00
parent 93ec6360bd
commit 95ffc029d4
1 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/util/lp/niil_solver.cpp
View file

@ -177,7 +177,7 @@ struct solver::imp {
typedef lp::lar_base_constraint lpcon; typedef lp::lar_base_constraint lpcon;
struct var_info { struct var_lists {
svector<unsigned> m_monomials; // of the var svector<unsigned> m_monomials; // of the var
svector<const lpcon*> m_constraints; // of the var svector<const lpcon*> m_constraints; // of the var
const svector<unsigned>& mons() const { return m_monomials;} const svector<unsigned>& mons() const { return m_monomials;}
@ -191,7 +191,7 @@ struct solver::imp {
vector<mon_eq> m_monomials; vector<mon_eq> m_monomials;
unsigned_vector m_monomials_lim; unsigned_vector m_monomials_lim;
lp::lar_solver& m_lar_solver; lp::lar_solver& m_lar_solver;
std::unordered_map<lpvar, var_info> m_var_infos; std::unordered_map<lpvar, var_lists> m_var_listss;
lp::explanation * m_expl; lp::explanation * m_expl;
lemma * m_lemma; lemma * m_lemma;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
@ -303,7 +303,7 @@ struct solver::imp {
bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon, bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon,
unsigned j_var, const svector<lpvar>& mon_vars, int sign) { unsigned j_var, const svector<lpvar>& mon_vars, int sign) {
auto it = m_var_infos.find(j_var); auto it = m_var_listss.find(j_var);
for (auto other_i_mon : it->second.mons()) { for (auto other_i_mon : it->second.mons()) {
if (other_i_mon == i_mon) continue; if (other_i_mon == i_mon) continue;
if (generate_basic_lemma_for_mon_sign_var_other_mon( if (generate_basic_lemma_for_mon_sign_var_other_mon(
@ -368,11 +368,11 @@ struct solver::imp {
void map_monominals_vars(unsigned i) { void map_monominals_vars(unsigned i) {
const mon_eq& m = m_monomials[i]; const mon_eq& m = m_monomials[i];
for (lpvar j : m.m_vs) { for (lpvar j : m.m_vs) {
auto it = m_var_infos.find(j); auto it = m_var_listss.find(j);
if (it == m_var_infos.end()) { if (it == m_var_listss.end()) {
var_info v; var_lists v;
v.add_monomial(i); v.add_monomial(i);
m_var_infos[j] = v; m_var_listss[j] = v;
} }
else { else {
it->second.add_monomial(i); it->second.add_monomial(i);
@ -381,11 +381,11 @@ struct solver::imp {
} }
void bind_var_and_constraint(lpvar j, const lpcon* c) { void bind_var_and_constraint(lpvar j, const lpcon* c) {
auto it = m_var_infos.find(j); auto it = m_var_listss.find(j);
if (it == m_var_infos.end()) { if (it == m_var_listss.end()) {
var_info v; var_lists v;
v.add_constraint(c); v.add_constraint(c);
m_var_infos.insert(std::pair<lpvar, var_info>(j, v)); m_var_listss.insert(std::pair<lpvar, var_lists>(j, v));
} else { } else {
it->second.add_constraint(c); it->second.add_constraint(c);
} }