mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

randomize m_to_refine() init

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-17 20:48:29 -07:00
parent 5d5d4a2264
commit 2560c9b739
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/emonomials.h
View file

@ -95,7 +95,6 @@ class emonomials {
hashtable<lpvar, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
unsigned number_of_monomials() const { return m_monomials.size(); }
void inc_visited() const;
void remove_cell(head_tail& v, unsigned mIndex);
@ -115,6 +114,7 @@ class emonomials {
bool is_visited(monomial const& m) const;
std::ostream& display_use(std::ostream& out) const;
public:
unsigned number_of_monomials() const { return m_monomials.size(); }
/**
\brief emonomials builds on top of var_eqs.
push and pop on emonomials calls push/pop on var_eqs, so no