Searched refs:m_fresh_id (Results 1 – 8 of 8) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | ast.cpp | 1356 m_fresh_id = std::max(m_fresh_id, m.m_fresh_id); in update_fresh_id()
1363 m_fresh_id = 0; in init()
2282 d = mk_func_decl(symbol(m_fresh_id), arity, domain, range, &info); in mk_fresh_func_decl()
2293 buffer << m_fresh_id; in mk_fresh_func_decl()
2296 m_fresh_id++; in mk_fresh_func_decl()
2304 buffer << prefix << "!" << m_fresh_id; in mk_fresh_sort()
2305 m_fresh_id++; in mk_fresh_sort()
2311 buffer << (prefix ? prefix : "var") << "!" << m_fresh_id; in mk_fresh_var_name()
2312 m_fresh_id++; in mk_fresh_var_name()
|
| H A D | ast.h | 1467 unsigned mk_fresh_id() { return ++m_fresh_id; } in mk_fresh_id()
1488 unsigned m_fresh_id; variable
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | ast.cpp | 1434 m_fresh_id = std::max(m_fresh_id, m.m_fresh_id); in update_fresh_id()
1441 m_fresh_id = 0; in init()
2360 d = mk_func_decl(symbol(m_fresh_id), arity, domain, range, &info); in mk_fresh_func_decl()
2371 buffer << m_fresh_id; in mk_fresh_func_decl()
2374 m_fresh_id++; in mk_fresh_func_decl()
2382 buffer << prefix << "!" << m_fresh_id; in mk_fresh_sort()
2383 m_fresh_id++; in mk_fresh_sort()
2389 buffer << (prefix ? prefix : "var") << "!" << m_fresh_id; in mk_fresh_var_name()
2390 m_fresh_id++; in mk_fresh_var_name()
|
| H A D | ast.h | 1517 unsigned mk_fresh_id() { return ++m_fresh_id; } in mk_fresh_id()
1544 unsigned m_fresh_id; variable
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_str.h | 474 unsigned m_fresh_id; variable
|
| H A D | theory_str.cpp | 87 m_fresh_id(0), in theory_str()
473 buffer << m_fresh_id; in mk_fresh_const()
474 m_fresh_id++; in mk_fresh_const()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_str.h | 527 unsigned m_fresh_id; variable
|
| H A D | theory_str.cpp | 87 m_fresh_id(0), in theory_str()
549 buffer << m_fresh_id; in mk_fresh_const()
550 m_fresh_id++; in mk_fresh_const()
|