Searched refs:mk_fresh_name (Results 1 – 12 of 12) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/model/ |
| H A D | model2expr.h | 30 class mk_fresh_name {
35 mk_fresh_name(): m_char('A'), m_num(0) {} in mk_fresh_name() function
|
| H A D | model2expr.cpp | 43 void mk_fresh_name::add(ast* a) { in add()
48 symbol mk_fresh_name::next() { in next()
100 mk_fresh_name fresh_name; in model2expr()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
| H A D | model2expr.h | 30 class mk_fresh_name {
35 mk_fresh_name(): m_char('A'), m_num(0) {} in mk_fresh_name() function
|
| H A D | model2expr.cpp | 43 void mk_fresh_name::add(ast* a) { in add()
48 symbol mk_fresh_name::next() { in next()
100 mk_fresh_name fresh_name; in model2expr()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_context.cpp | 1039 mk_fresh_name& fresh_names) { in collect_free_funcs()
1142 mk_fresh_name fresh_names; in display_smt2()
1278 …void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) { in declare_vars()
|
| H A D | dl_context.h | 615 void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_context.cpp | 1038 mk_fresh_name& fresh_names) { in collect_free_funcs()
1141 mk_fresh_name fresh_names; in display_smt2()
1277 …void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) { in declare_vars()
|
| H A D | dl_context.h | 615 void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/tab/ |
| H A D | tab_context.cpp | 241 mk_fresh_name fresh; in to_formula()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/tab/ |
| H A D | tab_context.cpp | 241 mk_fresh_name fresh; in to_formula()
|
| /dports/math/z3/z3-z3-4.8.13/scripts/ |
| H A D | mk_util.py | 838 def mk_fresh_name(prefix): function
1071 include_defs = mk_fresh_name('includes')
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/scripts/ |
| H A D | mk_util.py | 838 def mk_fresh_name(prefix): function
1034 include_defs = mk_fresh_name('includes')
|