Home
last modified time | relevance | path

Searched refs:mk_str_fun (Results 1 – 4 of 4) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/ast/
H A Dseq_decl_plugin.cpp520 return mk_str_fun(k, arity, domain, range, k); in mk_func_decl()
539 return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE); in mk_func_decl()
556 return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX); in mk_func_decl()
567 return mk_str_fun(k, arity, domain, range, OP_SEQ_PREFIX); in mk_func_decl()
572 return mk_str_fun(k, arity, domain, range, OP_SEQ_SUFFIX); in mk_func_decl()
577 return mk_str_fun(k, arity, domain, range, OP_SEQ_LENGTH); in mk_func_decl()
582 return mk_str_fun(k, arity, domain, range, OP_SEQ_CONTAINS); in mk_func_decl()
589 return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE); in mk_func_decl()
596 return mk_str_fun(k, arity, domain, range, OP_SEQ_IN_RE); in mk_func_decl()
601 return mk_str_fun(k, arity, domain, range, OP_SEQ_AT); in mk_func_decl()
[all …]
H A Dseq_decl_plugin.h150 …func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_s…
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/
H A Dseq_decl_plugin.cpp873 return mk_str_fun(k, arity, domain, range, k); in mk_func_decl()
892 return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE); in mk_func_decl()
909 return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX); in mk_func_decl()
920 return mk_str_fun(k, arity, domain, range, OP_SEQ_PREFIX); in mk_func_decl()
925 return mk_str_fun(k, arity, domain, range, OP_SEQ_SUFFIX); in mk_func_decl()
930 return mk_str_fun(k, arity, domain, range, OP_SEQ_LENGTH); in mk_func_decl()
935 return mk_str_fun(k, arity, domain, range, OP_SEQ_CONTAINS); in mk_func_decl()
942 return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE); in mk_func_decl()
965 return mk_str_fun(k, arity, domain, range, OP_SEQ_IN_RE); in mk_func_decl()
970 return mk_str_fun(k, arity, domain, range, OP_SEQ_AT); in mk_func_decl()
[all …]
H A Dseq_decl_plugin.h189 …func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_s…