1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 reg_decl_plugins
7
8 Abstract:
9
10 Goodie for installing all available declarations
11 plugins in an ast_manager
12
13 Author:
14
15 Leonardo de Moura (leonardo) 2012-10-24.
16
17 Revision History:
18
19 --*/
20 #include "ast/ast.h"
21 #include "ast/arith_decl_plugin.h"
22 #include "ast/array_decl_plugin.h"
23 #include "ast/bv_decl_plugin.h"
24 #include "ast/datatype_decl_plugin.h"
25 #include "ast/recfun_decl_plugin.h"
26 #include "ast/dl_decl_plugin.h"
27 #include "ast/char_decl_plugin.h"
28 #include "ast/seq_decl_plugin.h"
29 #include "ast/pb_decl_plugin.h"
30 #include "ast/fpa_decl_plugin.h"
31 #include "ast/special_relations_decl_plugin.h"
32
reg_decl_plugins(ast_manager & m)33 void reg_decl_plugins(ast_manager & m) {
34 if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
35 m.register_plugin(symbol("arith"), alloc(arith_decl_plugin));
36 }
37 if (!m.get_plugin(m.mk_family_id(symbol("bv")))) {
38 m.register_plugin(symbol("bv"), alloc(bv_decl_plugin));
39 }
40 if (!m.get_plugin(m.mk_family_id(symbol("array")))) {
41 m.register_plugin(symbol("array"), alloc(array_decl_plugin));
42 }
43 if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) {
44 m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
45 }
46 if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) {
47 m.register_plugin(symbol("recfun"), alloc(recfun::decl::plugin));
48 }
49 if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
50 m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
51 }
52 if (!m.get_plugin(m.mk_family_id(symbol("char")))) {
53 m.register_plugin(symbol("char"), alloc(char_decl_plugin));
54 }
55 if (!m.get_plugin(m.mk_family_id(symbol("seq")))) {
56 m.register_plugin(symbol("seq"), alloc(seq_decl_plugin));
57 }
58 if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
59 m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
60 }
61 if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
62 m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
63 }
64 if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) {
65 m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin));
66 }
67 }
68