z3 / src / nlsat / nlsat_types.cpp

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70``` ```/*++ Copyright (c) 2012 Microsoft Corporation Module Name: nlsat_types.cpp Abstract: Basic types used in the nonlinear arithmetic satisfiability procedure. Author: Leonardo de Moura (leonardo) 2012-01-02. Revision History: --*/ #include"nlsat_types.h" #include"debug.h" #include"hash.h" #include"polynomial.h" namespace nlsat { ineq_atom::ineq_atom(kind k, unsigned sz, poly * const * ps, bool const * is_even, var max_var): atom(k, max_var), m_size(sz) { for (unsigned i = 0; i < m_size; i++) { m_ps[i] = TAG(poly *, ps[i], is_even[i] ? 1 : 0); } SASSERT(is_ineq_atom()); } unsigned ineq_atom::hash_proc::operator()(ineq_atom const * a) const { return get_composite_hash(a, a->m_size); } bool ineq_atom::eq_proc::operator()(ineq_atom const * a1, ineq_atom const * a2) const { if (a1->m_size != a2->m_size || a1->m_kind != a2->m_kind) return false; unsigned sz = a1->m_size; for (unsigned i = 0; i < sz; i++) { if (a1->m_ps[i] != a2->m_ps[i]) return false; } return true; } root_atom::root_atom(kind k, var x, unsigned i, poly * p): atom(k, x), m_x(x), m_i(i), m_p(p) { SASSERT(is_root_atom()); } unsigned root_atom::hash_proc::operator()(root_atom const * a) const { unsigned _a = a->m_x; unsigned _b = ((a->m_i << 2) | (a->m_kind)); unsigned _c = polynomial::manager::id(a->m_p); mix(_a, _b, _c); return _c; } bool root_atom::eq_proc::operator()(root_atom const * a1, root_atom const * a2) const { return a1->m_kind == a2->m_kind && a1->m_x == a2->m_x && a1->m_i == a2->m_i && a1->m_p == a2->m_p; } }; ```
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.