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

look expressions in terms at the beginning

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-01 09:28:06 -07:00
parent 8d05894db7
commit 7cd90537c3
1 changed files with 28 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/math/lp/lar_solver.h
View file

@ -47,16 +47,20 @@ namespace lp {
class lar_solver : public column_namer { class lar_solver : public column_namer {
#if Z3DEBUG_CHECK_UNIQUE_TERMS
struct term_hasher { struct term_hasher {
std::size_t operator()(const lar_term *t) const std::size_t operator()(const lar_term *t) const
{ {
using std::size_t; using std::size_t;
using std::hash; using std::hash;
using std::string; using std::string;
size_t seed = 0; size_t seed = 0;
for (const auto& p : t->m_coeffs) { int i = 0;
hash_combine(seed, p); for (const auto& p : t->coeffs()) {
hash_combine(seed, p.m_key);
hash_combine(seed, p.m_value);
if (i++ > 10)
break;
} }
return seed; return seed;
} }
@ -65,27 +69,29 @@ class lar_solver : public column_namer {
struct term_ls_comparer { struct term_ls_comparer {
bool operator()(const lar_term *a, const lar_term* b) const bool operator()(const lar_term *a, const lar_term* b) const
{ {
// a is contained in b return a->coeffs() == b->coeffs();
for (auto & p : a->m_coeffs) {
auto t = b->m_coeffs.find(p.first); // // a is contained in b
if (t == b->m_coeffs.end()) // for (auto & p : a->coeffs()) {
return false; // auto t = b->coeffs().find_iterator(p.m_key);
if (p.second != t->second) // if (t == b->coeffs().end())
return false; // return false;
} // if (p.m_value != t->m_value)
// zz is contained in b // return false;
for (auto & p : b->m_coeffs) { // }
auto t = a->m_coeffs.find(p.first); // // zz is contained in b
if (t == a->m_coeffs.end()) // for (auto & p : b->coeffs()) {
return false; // auto t = a->coeffs().find_iterator(p.m_key);
if (p.second != t->second) // if (t == a->coeffs().end())
return false; // return false;
} // if (p.m_value != t->m_value)
return true; // return false;
// }
// return true;
} }
}; };
std::unordered_set<lar_term*, term_hasher, term_ls_comparer> m_set_of_terms; std::unordered_set<lar_term*, term_hasher, term_ls_comparer> m_set_of_terms;
#endif
//////////////////// fields ////////////////////////// //////////////////// fields //////////////////////////
std::unordered_set<unsigned> m_cube_rounded_columns; std::unordered_set<unsigned> m_cube_rounded_columns;