| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | ast_lt.cpp | 112 check_symbol(to_quantifier(n1)->get_decl_name(i), to_quantifier(n2)->get_decl_name(i)); in lt()
|
| H A D | used_symbols.h | 77 found(to_quantifier(n)->get_decl_name(i)); in operator()
|
| H A D | ast_ll_pp.cpp | 253 m_out << "(" << n->get_decl_name(i) << " "; in operator ()()
|
| H A D | ast_smt_pp.cpp | 513 print_bound(m_renaming.get_symbol(q->get_decl_name(i), false)); in visit_quantifier()
578 symbol name = m_renaming.get_symbol(q->get_decl_name(offs), false); in visit_var()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | ast_lt.cpp | 116 check_symbol(to_quantifier(n1)->get_decl_name(i), to_quantifier(n2)->get_decl_name(i)); in lt()
|
| H A D | used_symbols.h | 77 found(to_quantifier(n)->get_decl_name(i)); in operator()
|
| H A D | ast_ll_pp.cpp | 262 m_out << "(" << n->get_decl_name(i) << " "; in display_quantifier_header()
|
| H A D | ast_smt_pp.cpp | 513 print_bound(m_renaming.get_symbol(q->get_decl_name(i), false)); in visit_quantifier()
578 symbol name = m_renaming.get_symbol(q->get_decl_name(offs), false); in visit_var()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | bv_elim.cpp | 43 symbol nm = q->get_decl_name(i); in reduce_quantifier()
|
| H A D | var_subst.cpp | 117 used_decl_names.push_back(q->get_decl_name(i)); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | bv_elim.cpp | 43 symbol nm = q->get_decl_name(i); in reduce_quantifier()
|
| H A D | var_subst.cpp | 103 used_decl_names.push_back(q->get_decl_name(i)); in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/model/ |
| H A D | model2expr.cpp | 34 m_symbols.insert(n->get_decl_name(i)); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
| H A D | model2expr.cpp | 34 m_symbols.insert(n->get_decl_name(i)); in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | euf_proof.cpp | 52 … strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")"; in drat_log_expr1()
|
| H A D | q_solver.cpp | 136 return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i)); in skolemize()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | q_solver.cpp | 106 return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_boogie_proof.cpp | 223 s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i])); in get_subst()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_boogie_proof.cpp | 223 s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i])); in get_subst()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/bv/ |
| H A D | elim_small_bv_tactic.cpp | 144 TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) << in reduce_quantifier()
|
| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | quant_solve.cpp | 145 vars.push_back(m.mk_const(q->get_decl_name(i), q->get_decl_sort(i))); in parse_fml()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/ |
| H A D | elim_small_bv_tactic.cpp | 144 TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) << in reduce_quantifier()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
| H A D | quant_solve.cpp | 145 vars.push_back(m.mk_const(q->get_decl_name(i), q->get_decl_sort(i))); in parse_fml()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/normal_forms/ |
| H A D | pull_quant.cpp | 85 symbol s = nested_q->get_decl_name(j); in pull_quant1_core()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/normal_forms/ |
| H A D | pull_quant.cpp | 87 symbol s = nested_q->get_decl_name(j); in pull_quant1_core()
|