mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

consistent

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-12 19:08:15 -07:00
parent 26631ce38d
commit 846a9fc25f
3 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/emonics.cpp
View file

@ -42,6 +42,7 @@ void emonics::push() {
m_region.push_scope(); m_region.push_scope();
m_ve.push(); m_ve.push();
SASSERT(monics_are_canonized()); SASSERT(monics_are_canonized());
SASSERT(consistent());
} }
void emonics::pop(unsigned n) { void emonics::pop(unsigned n) {
@ -63,6 +64,7 @@ void emonics::pop(unsigned n) {
m_monics.shrink(old_sz); m_monics.shrink(old_sz);
m_region.pop_scope(n); m_region.pop_scope(n);
m_lim.shrink(m_lim.size() - n); m_lim.shrink(m_lim.size() - n);
SASSERT(consistent());
SASSERT(monics_are_canonized()); SASSERT(monics_are_canonized());
m_u_f_stack.pop_scope(n); m_u_f_stack.pop_scope(n);
} }
@ -288,7 +290,6 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
lpvar w = vs[i]; lpvar w = vs[i];
SASSERT(m_ve.is_root(w));
if (w != last_var) { if (w != last_var) {
m_use_lists.reserve(w + 1); m_use_lists.reserve(w + 1);
insert_cell(m_use_lists[w], idx); insert_cell(m_use_lists[w], idx);

11
src/math/lp/emonics.h
View file

@ -107,7 +107,6 @@ class emonics {
void insert_cg_mon(monic & m); void insert_cg_mon(monic & m);
void remove_cg_mon(const monic & m); void remove_cg_mon(const monic & m);
void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
void do_canonize(monic& m) const; void do_canonize(monic& m) const;
cell* head(lpvar v) const; cell* head(lpvar v) const;
void set_visited(monic& m) const; void set_visited(monic& m) const;
@ -328,6 +327,16 @@ public:
bool is_used_in_monic(lpvar v) const { return v < m_use_lists.size() && m_use_lists[v].m_head != nullptr; } bool is_used_in_monic(lpvar v) const { return v < m_use_lists.size() && m_use_lists[v].m_head != nullptr; }
bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const; bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const;
bool consistent() const {
unsigned mons = 0;
for (lpvar v = 0; v < m_var2index.size(); v++) {
if (is_monic_var(v)) {
mons ++;
}
}
return m_monics.size() == mons;
}
}; // end of emonics }; // end of emonics

1
src/math/lp/nla_core.cpp
View file

@ -960,6 +960,7 @@ void core::clear() {
void core::init_search() { void core::init_search() {
clear(); clear();
init_vars_equivalence(); init_vars_equivalence();
SASSERT(m_emons.consistent());
SASSERT(elists_are_consistent(false)); SASSERT(elists_are_consistent(false));
} }