mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

register Concat function

Browse source 
now reaches str_decl_plugin::mk_func_decl()
This commit is contained in:
Murphy Berzish 2015-09-06 21:05:32 -04:00
parent 8137e022e3
commit f0c301e920
2 changed files with 18 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/str_decl_plugin.cpp
View file

@ -23,7 +23,8 @@ Revision History:
str_decl_plugin::str_decl_plugin():
m_strv_sym("String"),
m_str_decl(0){
m_str_decl(0),
m_concat_decl(0){
}
str_decl_plugin::~str_decl_plugin(){
@ -39,7 +40,17 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_str_decl = m->mk_sort(symbol("String"), sort_info(id, STRING_SORT));
m->inc_ref(m_str_decl);
sort * s = m_str_decl;
/* TODO mk_pred, etc. */
#define MK_AC_OP(FIELD, NAME, KIND, SORT) { \
func_decl_info info(id, KIND); \
info.set_associative(); \
info.set_flat_associative(); \
info.set_commutative(); \
FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, info); \
m->inc_ref(FIELD); \
}
MK_AC_OP(m_concat_decl, "Concat", OP_STRCAT, s);
}
decl_plugin * str_decl_plugin::mk_fresh() {
@ -67,9 +78,7 @@ app * str_decl_plugin::mk_string(const char * val) {
}
void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
// TODO
// we would do something like:
// op_names.push_back(builtin_name("<=",OP_LE));
op_names.push_back(builtin_name("Concat", OP_STRCAT));
}
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

5
src/ast/str_decl_plugin.h
View file

@ -25,7 +25,8 @@ enum str_sort_kind {
enum str_op_kind {
OP_STR, /* string constants */
//
OP_STRCAT,
LAST_STR_OP
};
@ -34,6 +35,8 @@ protected:
symbol m_strv_sym;
sort * m_str_decl;
func_decl * m_concat_decl;
virtual void set_manager(ast_manager * m, family_id id);
public:
str_decl_plugin();