rpms
/
z3
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
z3/z3-export.patch

1762 lines
65 KiB
Diff
Raw Blame History

--- ./src/api/z3_replayer.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/api/z3_replayer.h 2015-05-25 21:35:48.981760111 -0600
@@ -29,7 +29,7 @@ typedef void (*z3_replayer_cmd)(z3_repla
typedef default_exception z3_replayer_exception;
-class z3_replayer {
+class __attribute__ ((visibility ("default"))) z3_replayer {
struct imp;
imp * m_imp;
public:
--- ./src/ast/ast.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/ast.h 2015-05-25 14:55:20.787742875 -0600
@@ -1378,7 +1378,7 @@ enum proof_gen_mode {
//
// -----------------------------------
-class ast_manager {
+class __attribute__ ((visibility ("default"))) ast_manager {
friend class basic_decl_plugin;
protected:
struct config {
--- ./src/ast/normal_forms/nnf.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/normal_forms/nnf.h 2015-05-26 20:25:53.053381028 -0600
@@ -24,7 +24,7 @@ Notes:
#include"params.h"
#include"defined_names.h"
-class nnf {
+class __attribute__ ((visibility ("default"))) nnf {
struct imp;
imp * m_imp;
public:
--- ./src/ast/pattern/pattern_inference_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/pattern/pattern_inference_params.h 2015-05-25 14:26:56.651190582 -0600
@@ -27,7 +27,7 @@ enum arith_pattern_inference_kind {
AP_FULL // always use patterns with arithmetic terms
};
-struct pattern_inference_params {
+struct __attribute__ ((visibility ("default"))) pattern_inference_params {
unsigned m_pi_max_multi_patterns;
bool m_pi_block_loop_patterns;
arith_pattern_inference_kind m_pi_arith;
--- ./src/ast/simplifier/arith_simplifier_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/simplifier/arith_simplifier_params.h 2015-05-25 14:48:30.378596329 -0600
@@ -21,7 +21,7 @@ Revision History:
#include"params.h"
-struct arith_simplifier_params {
+struct __attribute__ ((visibility ("default"))) arith_simplifier_params {
bool m_arith_expand_eqs;
bool m_arith_process_all_eqs;
--- ./src/ast/simplifier/array_simplifier_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/simplifier/array_simplifier_params.h 2015-05-25 14:52:47.414020040 -0600
@@ -21,7 +21,7 @@ Revision History:
#include"params.h"
-struct array_simplifier_params {
+struct __attribute__ ((visibility ("default"))) array_simplifier_params {
bool m_array_canonize_simplify;
bool m_array_simplify; // temporary hack for disabling array simplifier plugin.
--- ./src/ast/simplifier/bv_simplifier_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/ast/simplifier/bv_simplifier_params.h 2015-05-25 14:27:50.205900881 -0600
@@ -21,7 +21,7 @@ Revision History:
#include"params.h"
-struct bv_simplifier_params {
+struct __attribute__ ((visibility ("default"))) bv_simplifier_params {
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int.
--- ./src/cmd_context/cmd_context.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/cmd_context.h 2015-05-27 20:41:03.198613174 -0600
@@ -88,7 +88,7 @@ public:
virtual char const * kind() const { return cls_kind(); }
};
-class stream_ref {
+class __attribute__ ((visibility ("default"))) stream_ref {
std::string m_default_name;
std::ostream & m_default;
std::string m_name;
@@ -111,7 +111,7 @@ struct builtin_decl {
builtin_decl(family_id fid, decl_kind k, builtin_decl * n = 0):m_fid(fid), m_decl(k), m_next(n) {}
};
-class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
+class __attribute__ ((visibility ("default"))) cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
public:
enum status {
UNSAT, SAT, UNKNOWN
--- ./src/cmd_context/context_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/context_params.h 2015-05-25 21:34:39.475354751 -0600
@@ -23,7 +23,7 @@ Notes:
#include"params.h"
class ast_manager;
-class context_params {
+class __attribute__ ((visibility ("default"))) context_params {
void set_bool(bool & opt, char const * param, char const * value);
public:
--- ./src/cmd_context/extra_cmds/dbg_cmds.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/extra_cmds/dbg_cmds.cpp 2015-05-26 21:26:34.125971101 -0600
@@ -344,7 +344,7 @@ public:
#endif
-void install_dbg_cmds(cmd_context & ctx) {
+__attribute__ ((visibility ("default"))) void install_dbg_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(get_quantifier_body_cmd));
ctx.insert(alloc(set_cmd));
--- ./src/cmd_context/extra_cmds/polynomial_cmds.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/extra_cmds/polynomial_cmds.cpp 2015-05-26 21:28:05.438659456 -0600
@@ -234,7 +234,7 @@ public:
}
};
-void install_polynomial_cmds(cmd_context & ctx) {
+__attribute__ ((visibility ("default"))) void install_polynomial_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(to_poly_cmd));
ctx.insert(alloc(poly_factor_cmd));
--- ./src/cmd_context/extra_cmds/subpaving_cmds.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/extra_cmds/subpaving_cmds.cpp 2015-05-26 21:28:39.931897492 -0600
@@ -49,7 +49,7 @@ static void to_subpaving(cmd_context & c
UNARY_CMD(to_subpaving_cmd, "to-subpaving", "<expr>", "internalize expression into subpaving module", CPK_EXPR, expr *, to_subpaving(ctx, arg););
-void install_subpaving_cmds(cmd_context & ctx) {
+__attribute__ ((visibility ("default"))) void install_subpaving_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(to_subpaving_cmd));
#endif
--- ./src/cmd_context/tactic_cmds.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/tactic_cmds.h 2015-05-26 20:28:50.519864660 -0600
@@ -48,7 +48,7 @@ public:
void install_core_tactic_cmds(cmd_context & ctx);
tactic * sexpr2tactic(cmd_context & ctx, sexpr * n);
-class probe_info {
+class __attribute__ ((visibility ("default"))) probe_info {
symbol m_name;
char const * m_descr;
ref<probe> m_probe;
--- ./src/cmd_context/tactic_manager.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/cmd_context/tactic_manager.h 2015-05-26 20:26:32.954342054 -0600
@@ -21,7 +21,7 @@ Notes:
#include"tactic_cmds.h"
#include"dictionary.h"
-class tactic_manager {
+class __attribute__ ((visibility ("default"))) tactic_manager {
protected:
dictionary<tactic_cmd*> m_name2tactic;
dictionary<probe_info*> m_name2probe;
--- ./src/math/subpaving/tactic/subpaving_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/math/subpaving/tactic/subpaving_tactic.cpp 2015-05-27 20:35:16.361286643 -0600
@@ -287,11 +287,11 @@ protected:
};
-tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) {
return alloc(subpaving_tactic, m, p);
}
-tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool("arith_lhs", true);
simp_p.set_bool("expand_power", true);
--- ./src/muz/base/dl_context.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/base/dl_context.h 2015-05-25 14:22:17.592543012 -0600
@@ -135,7 +135,7 @@ namespace datalog {
virtual lbool saturate() = 0;
};
- class context {
+ class __attribute__ ((visibility ("default"))) context {
public:
typedef unsigned finite_element;
enum sort_kind {
--- ./src/muz/base/dl_costs.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/base/dl_costs.h 2015-05-25 21:24:06.798290770 -0600
@@ -53,7 +53,7 @@ namespace datalog {
};
- class accounted_object {
+ class __attribute__ ((visibility ("default"))) accounted_object {
friend class cost_recorder;
context * m_context;
--- ./src/muz/base/dl_rule_set.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/base/dl_rule_set.h 2015-05-25 13:41:40.339875157 -0600
@@ -152,7 +152,7 @@ namespace datalog {
/**
\brief Datalog "Program" (aka rule set).
*/
- class rule_set {
+ class __attribute__ ((visibility ("default"))) rule_set {
friend class rule_dependencies;
public:
typedef ptr_vector<func_decl_set> pred_set_vector;
--- ./src/muz/base/dl_util.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/base/dl_util.cpp 2015-05-26 21:29:24.351340712 -0600
@@ -597,7 +597,7 @@ namespace datalog {
return false;
}
- bool is_directory(std::string name) {
+ __attribute__ ((visibility ("default"))) bool is_directory(std::string name) {
if(!file_exists(name)) {
return false;
}
--- ./src/muz/fp/datalog_parser.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/fp/datalog_parser.h 2015-05-25 15:55:21.225477376 -0600
@@ -24,7 +24,7 @@ Revision History:
namespace datalog {
- class parser {
+ class __attribute__ ((visibility ("default"))) parser {
public:
static parser * create(context& ctx, ast_manager & ast_manager);
@@ -34,7 +34,7 @@ namespace datalog {
virtual bool parse_string(char const * string) = 0;
};
- class wpa_parser {
+ class __attribute__ ((visibility ("default"))) wpa_parser {
public:
static wpa_parser * create(context& ctx, ast_manager & ast_manager);
--- ./src/muz/fp/dl_cmds.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/fp/dl_cmds.cpp 2015-05-26 21:30:11.860536528 -0600
@@ -521,7 +521,7 @@ static void install_dl_cmds_aux(cmd_cont
// #endif
}
-void install_dl_cmds(cmd_context & ctx) {
+__attribute__ ((visibility ("default"))) void install_dl_cmds(cmd_context & ctx) {
install_dl_cmds_aux(ctx, 0);
}
--- ./src/muz/fp/dl_register_engine.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/fp/dl_register_engine.h 2015-05-25 14:56:40.563357664 -0600
@@ -23,7 +23,7 @@ Revision History:
namespace datalog {
- class register_engine : public register_engine_base {
+ class __attribute__ ((visibility ("default"))) register_engine : public register_engine_base {
context* m_ctx;
public:
register_engine();
--- ./src/muz/fp/horn_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/fp/horn_tactic.cpp 2015-05-27 20:26:51.058602745 -0600
@@ -412,11 +412,11 @@ protected:
}
};
-tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(horn_tactic, false, m, p));
}
-tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(horn_tactic, true, m, p));
}
--- ./src/muz/rel/dl_compiler.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/rel/dl_compiler.h 2015-05-25 15:54:35.142168156 -0600
@@ -36,7 +36,7 @@ Revision History:
namespace datalog {
- class compiler {
+ class __attribute__ ((visibility ("default"))) compiler {
typedef instruction::reg_idx reg_idx;
typedef hashtable<unsigned, u_hash, u_eq> int_set;
typedef u_map<unsigned> int2int;
--- ./src/muz/rel/dl_finite_product_relation.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/rel/dl_finite_product_relation.h 2015-05-25 15:50:36.528278571 -0600
@@ -31,7 +31,7 @@ namespace datalog {
void universal_delete(finite_product_relation* ptr);
- class finite_product_relation_plugin : public relation_plugin {
+ class __attribute__ ((visibility ("default"))) finite_product_relation_plugin : public relation_plugin {
friend class finite_product_relation;
public:
struct rel_spec {
--- ./src/muz/rel/dl_instruction.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/rel/dl_instruction.h 2015-05-25 14:23:35.961265724 -0600
@@ -46,7 +46,7 @@ namespace datalog {
//
// -----------------------------------
- class execution_context {
+ class __attribute__ ((visibility ("default"))) execution_context {
public:
typedef relation_base * reg_type;
typedef vector<reg_type> reg_vector;
@@ -297,7 +297,7 @@ namespace datalog {
//
// -----------------------------------
- class instruction_block {
+ class __attribute__ ((visibility ("default"))) instruction_block {
public:
struct instruction_observer {
virtual ~instruction_observer() {}
--- ./src/muz/rel/dl_relation_manager.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/muz/rel/dl_relation_manager.h 2015-05-25 14:24:20.742678760 -0600
@@ -37,7 +37,7 @@ namespace datalog {
class rule_set;
- class relation_manager {
+ class __attribute__ ((visibility ("default"))) relation_manager {
class empty_signature_relation_join_fn;
class default_relation_join_project_fn;
class default_relation_select_equal_and_project_fn;
--- ./src/nlsat/tactic/nlsat_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/nlsat/tactic/nlsat_tactic.cpp 2015-05-27 20:21:02.973376045 -0600
@@ -253,7 +253,7 @@ public:
}
};
-tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(nlsat_tactic, p));
}
--- ./src/nlsat/tactic/qfnra_nlsat_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/nlsat/tactic/qfnra_nlsat_tactic.cpp 2015-05-27 20:20:21.800652878 -0600
@@ -29,7 +29,7 @@ Notes:
#include"solve_eqs_tactic.h"
#include"elim_term_ite_tactic.h"
-tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p = p;
main_p.set_bool("elim_and", true);
main_p.set_bool("blast_distinct", true);
--- ./src/parsers/smt2/smt2parser.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/parsers/smt2/smt2parser.cpp 2015-05-26 21:31:00.545638185 -0600
@@ -2514,7 +2514,7 @@ namespace smt2 {
};
};
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) {
+__attribute__ ((visibility ("default"))) bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) {
smt2::parser p(ctx, is, interactive, ps);
return p();
}
--- ./src/parsers/smt/smtlib_solver.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/parsers/smt/smtlib_solver.h 2015-05-27 20:40:32.617053671 -0600
@@ -26,7 +26,7 @@ Revision History:
class cmd_context;
namespace smtlib {
- class solver {
+ class __attribute__ ((visibility ("default"))) solver {
context_params m_params;
ast_manager m_ast_manager;
cmd_context * m_ctx;
--- ./src/qe/qe_lite.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/qe/qe_lite.cpp 2015-05-27 20:28:17.108735925 -0600
@@ -2589,7 +2589,7 @@ public:
};
-tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
return alloc(qe_lite_tactic, m, p);
}
--- ./src/qe/qe_sat_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/qe/qe_sat_tactic.cpp 2015-05-27 20:29:02.424119746 -0600
@@ -707,7 +707,7 @@ namespace qe {
}
};
- tactic * mk_sat_tactic(ast_manager& m, params_ref const& p) {
+ __attribute__ ((visibility ("default"))) tactic * mk_sat_tactic(ast_manager& m, params_ref const& p) {
return alloc(sat_tactic, m, p);
}
--- ./src/qe/qe_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/qe/qe_tactic.cpp 2015-05-27 20:29:35.844452796 -0600
@@ -148,7 +148,7 @@ protected:
}
};
-tactic * mk_qe_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qe_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(qe_tactic, m, p));
}
--- ./src/qe/vsubst_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/qe/vsubst_tactic.cpp 2015-05-27 20:27:45.405265869 -0600
@@ -164,6 +164,6 @@ public:
virtual void cleanup(void) {}
};
-tactic * mk_vsubst_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_vsubst_tactic(ast_manager & m, params_ref const & p) {
return alloc(vsubst_tactic, p);
}
--- ./src/sat/dimacs.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/sat/dimacs.cpp 2015-05-26 21:31:32.830053088 -0600
@@ -126,7 +126,7 @@ void parse_dimacs_core(Buffer & in, sat:
}
}
-void parse_dimacs(std::istream & in, sat::solver & solver) {
+__attribute__ ((visibility ("default"))) void parse_dimacs(std::istream & in, sat::solver & solver) {
stream_buffer _in(in);
parse_dimacs_core(_in, solver);
}
--- ./src/sat/sat_solver.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/sat/sat_solver.h 2015-05-25 21:29:51.842508995 -0600
@@ -62,7 +62,7 @@ namespace sat {
void collect_statistics(statistics & st) const;
};
- class solver {
+ class __attribute__ ((visibility ("default"))) solver {
public:
struct abort_solver {};
protected:
--- ./src/sat/tactic/sat_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/sat/tactic/sat_tactic.cpp 2015-05-27 20:22:27.102666491 -0600
@@ -204,11 +204,11 @@ protected:
};
-tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(sat_tactic, m, p));
}
-tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
params_ref p_aux;
p_aux.set_uint("max_conflicts", 0);
tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux));
--- ./src/smt/params/dyn_ack_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/dyn_ack_params.h 2015-05-25 14:50:16.146129390 -0600
@@ -27,7 +27,7 @@ enum dyn_ack_strategy {
DACK_CR // congruence used during conflict resolution
};
-struct dyn_ack_params {
+struct __attribute__ ((visibility ("default"))) dyn_ack_params {
dyn_ack_strategy m_dack;
bool m_dack_eq;
double m_dack_factor;
--- ./src/smt/params/preprocessor_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/preprocessor_params.h 2015-05-25 14:49:38.269161530 -0600
@@ -30,7 +30,8 @@ enum lift_ite_kind {
LI_FULL
};
-struct preprocessor_params : public pattern_inference_params,
+struct __attribute__ ((visibility ("default"))) preprocessor_params :
+ public pattern_inference_params,
public bit_blaster_params,
public bv_simplifier_params,
public arith_simplifier_params {
--- ./src/smt/params/qi_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/qi_params.h 2015-05-25 14:51:24.516656169 -0600
@@ -28,7 +28,7 @@ enum quick_checker_mode {
MC_NO_SAT // instantiate unsatisfied and not-satisfied instances
};
-struct qi_params {
+struct __attribute__ ((visibility ("default"))) qi_params {
bool m_qi_ematching;
std::string m_qi_cost;
std::string m_qi_new_gen;
--- ./src/smt/params/smt_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/smt_params.h 2015-05-25 14:54:25.407175513 -0600
@@ -68,7 +68,8 @@ enum case_split_strategy {
CS_RELEVANCY_GOAL, // based on relevancy and the current goal
};
-struct smt_params : public preprocessor_params,
+struct __attribute__ ((visibility ("default"))) smt_params :
+ public preprocessor_params,
public dyn_ack_params,
public qi_params,
public theory_arith_params,
--- ./src/smt/params/theory_arith_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/theory_arith_params.h 2015-05-25 14:52:02.737596492 -0600
@@ -47,7 +47,7 @@ enum arith_pivot_strategy {
ARITH_PIVOT_LEAST_ERROR
};
-struct theory_arith_params {
+struct __attribute__ ((visibility ("default"))) theory_arith_params {
arith_solver_id m_arith_mode;
bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config
unsigned m_arith_blands_rule_threshold;
--- ./src/smt/params/theory_bv_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/params/theory_bv_params.h 2015-05-25 14:53:31.882460235 -0600
@@ -26,7 +26,7 @@ enum bv_solver_id {
BS_BLASTER
};
-struct theory_bv_params {
+struct __attribute__ ((visibility ("default"))) theory_bv_params {
bv_solver_id m_bv_mode;
bool m_bv_reflect;
bool m_bv_lazy_le;
--- ./src/smt/smt_solver.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/smt_solver.cpp 2015-05-26 21:32:18.201434945 -0600
@@ -132,7 +132,7 @@ public:
}
};
-solver_factory * mk_smt_solver_factory() {
+__attribute__ ((visibility ("default"))) solver_factory * mk_smt_solver_factory() {
return alloc(smt_solver_factory);
}
--- ./src/smt/tactic/ctx_solver_simplify_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/tactic/ctx_solver_simplify_tactic.cpp 2015-05-27 20:24:14.535093358 -0600
@@ -294,6 +294,6 @@ protected:
};
-tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(ctx_solver_simplify_tactic, m, p));
}
--- ./src/smt/tactic/smt_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/tactic/smt_tactic.cpp 2015-05-27 20:24:54.035941182 -0600
@@ -297,11 +297,11 @@ public:
}
};
-tactic * mk_smt_tactic(params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_smt_tactic(params_ref const & p) {
return alloc(smt_tactic, p);
}
-tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
+__attribute__ ((visibility ("default"))) tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
params_ref p = _p;
p.set_bool("auto_config", auto_config);
tactic * r = mk_smt_tactic(p);
--- ./src/smt/tactic/unit_subsumption_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/smt/tactic/unit_subsumption_tactic.cpp 2015-05-27 20:25:38.383402243 -0600
@@ -145,7 +145,7 @@ struct unit_subsumption_tactic : public
};
-tactic * mk_unit_subsumption_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_unit_subsumption_tactic(ast_manager & m, params_ref const & p) {
return alloc(unit_subsumption_tactic, m, p);
}
--- ./src/solver/solver.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/solver/solver.h 2015-05-26 20:50:54.504821052 -0600
@@ -25,7 +25,7 @@ Notes:
class solver;
-class solver_factory {
+class __attribute__ ((visibility ("default"))) solver_factory {
public:
virtual ~solver_factory() {}
virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0;
@@ -43,7 +43,7 @@ public:
- results based on check_sat_result API
- interruption (set_cancel)
*/
-class solver : public check_sat_result {
+class __attribute__ ((visibility ("default"))) solver : public check_sat_result {
public:
virtual ~solver() {}
/**
--- ./src/tactic/aig/aig_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/aig/aig_tactic.cpp 2015-05-27 20:26:15.188465191 -0600
@@ -121,6 +121,6 @@ protected:
}
};
-tactic * mk_aig_tactic(params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_aig_tactic(params_ref const & p) {
return clean(alloc(aig_tactic, p));
}
--- ./src/tactic/arith/add_bounds_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/add_bounds_tactic.cpp 2015-05-26 21:33:26.085058247 -0600
@@ -53,7 +53,7 @@ public:
}
};
-probe * mk_is_unbounded_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_unbounded_probe() {
return alloc(is_unbounded_probe);
}
@@ -187,6 +187,6 @@ protected:
}
};
-tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(add_bounds_tactic, m, p));
}
--- ./src/tactic/arith/degree_shift_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/degree_shift_tactic.cpp 2015-05-27 19:56:40.562075047 -0600
@@ -334,7 +334,7 @@ protected:
}
};
-tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) {
params_ref mul2power_p;
mul2power_p.set_bool("mul_to_power", true);
return and_then(using_params(mk_simplify_tactic(m), mul2power_p),
--- ./src/tactic/arith/diff_neq_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/diff_neq_tactic.cpp 2015-05-27 20:01:31.587727308 -0600
@@ -414,7 +414,7 @@ protected:
}
};
-tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(diff_neq_tactic, m, p));
}
--- ./src/tactic/arith/factor_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/factor_tactic.cpp 2015-05-27 19:54:33.852247369 -0600
@@ -347,7 +347,7 @@ public:
}
};
-tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(factor_tactic, m, p));
}
--- ./src/tactic/arith/fix_dl_var_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/fix_dl_var_tactic.cpp 2015-05-27 20:02:17.584041600 -0600
@@ -352,6 +352,6 @@ public:
}
};
-tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(fix_dl_var_tactic, m, p));
}
--- ./src/tactic/arith/fm_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/fm_tactic.cpp 2015-05-27 19:59:35.022069321 -0600
@@ -1699,7 +1699,7 @@ public:
}
};
-tactic * mk_fm_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_fm_tactic(ast_manager & m, params_ref const & p) {
params_ref s_p = p;
s_p.set_bool("arith_lhs", true);
s_p.set_bool("elim_and", true);
--- ./src/tactic/arith/lia2pb_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/lia2pb_tactic.cpp 2015-05-27 19:53:54.327420439 -0600
@@ -360,7 +360,7 @@ protected:
}
};
-tactic * mk_lia2pb_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_lia2pb_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(lia2pb_tactic, m, p));
}
--- ./src/tactic/arith/nla2bv_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/nla2bv_tactic.cpp 2015-05-27 20:00:55.277636854 -0600
@@ -469,7 +469,7 @@ public:
}
};
-tactic * mk_nla2bv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_nla2bv_tactic(ast_manager & m, params_ref const & p) {
return alloc(nla2bv_tactic, p);
}
--- ./src/tactic/arith/normalize_bounds_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/normalize_bounds_tactic.cpp 2015-05-27 19:57:59.867708356 -0600
@@ -206,6 +206,6 @@ protected:
}
};
-tactic * mk_normalize_bounds_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_normalize_bounds_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(normalize_bounds_tactic, m, p));
}
--- ./src/tactic/arith/pb2bv_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/pb2bv_tactic.cpp 2015-05-27 19:57:18.967991803 -0600
@@ -1017,7 +1017,7 @@ protected:
}
};
-tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(pb2bv_tactic, m, p));
}
@@ -1046,6 +1046,6 @@ struct is_pb_probe : public probe {
};
-probe * mk_is_pb_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_pb_probe() {
return alloc(is_pb_probe);
}
--- ./src/tactic/arith/probe_arith.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/probe_arith.cpp 2015-05-26 21:35:55.801200032 -0600
@@ -127,19 +127,19 @@ public:
}
};
-probe * mk_arith_avg_degree_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_arith_avg_degree_probe() {
return alloc(arith_degree_probe, true);
}
-probe * mk_arith_max_degree_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_arith_max_degree_probe() {
return alloc(arith_degree_probe, false);
}
-probe * mk_arith_avg_bw_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_arith_avg_bw_probe() {
return alloc(arith_bw_probe, true);
}
-probe * mk_arith_max_bw_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_arith_max_bw_probe() {
return alloc(arith_bw_probe, false);
}
@@ -356,27 +356,27 @@ public:
}
};
-probe * mk_is_qflia_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qflia_probe() {
return alloc(is_qflia_probe);
}
-probe * mk_is_qfauflia_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfauflia_probe() {
return alloc(is_qfauflia_probe);
}
-probe * mk_is_qflra_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qflra_probe() {
return alloc(is_qflra_probe);
}
-probe * mk_is_qflira_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qflira_probe() {
return alloc(is_qflira_probe);
}
-probe * mk_is_ilp_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_ilp_probe() {
return alloc(is_ilp_probe);
}
-probe * mk_is_mip_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_mip_probe() {
return alloc(is_mip_probe);
}
@@ -569,34 +569,34 @@ public:
}
};
-probe * mk_is_qfnia_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfnia_probe() {
return alloc(is_qfnia_probe);
}
-probe * mk_is_qfnra_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfnra_probe() {
return alloc(is_qfnra_probe);
}
-probe * mk_is_nia_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_nia_probe() {
return alloc(is_nia_probe);
}
-probe * mk_is_nra_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_nra_probe() {
return alloc(is_nra_probe);
}
-probe * mk_is_nira_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_nira_probe() {
return alloc(is_nira_probe);
}
-probe * mk_is_lia_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_lia_probe() {
return alloc(is_lia_probe);
}
-probe * mk_is_lra_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_lra_probe() {
return alloc(is_lra_probe);
}
-probe * mk_is_lira_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_lira_probe() {
return alloc(is_lira_probe);
}
--- ./src/tactic/arith/propagate_ineqs_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/propagate_ineqs_tactic.cpp 2015-05-27 19:55:55.638681517 -0600
@@ -59,7 +59,7 @@ protected:
virtual void set_cancel(bool f);
};
-tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(propagate_ineqs_tactic, m, p));
}
--- ./src/tactic/arith/purify_arith_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/purify_arith_tactic.cpp 2015-05-27 19:58:51.904530816 -0600
@@ -750,7 +750,7 @@ public:
}
};
-tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p) {
params_ref elim_rem_p = p;
elim_rem_p.set_bool("elim_rem", true);
--- ./src/tactic/arith/recover_01_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/arith/recover_01_tactic.cpp 2015-05-27 20:00:10.120255338 -0600
@@ -440,6 +440,6 @@ protected:
}
};
-tactic * mk_recover_01_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_recover_01_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(recover_01_tactic, m, p));
}
--- ./src/tactic/bv/bit_blaster_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/bv/bit_blaster_tactic.cpp 2015-05-27 20:18:24.474990532 -0600
@@ -160,6 +160,6 @@ protected:
};
-tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(bit_blaster_tactic, m, p));
}
--- ./src/tactic/bv/bv1_blaster_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/bv/bv1_blaster_tactic.cpp 2015-05-27 20:18:55.472523516 -0600
@@ -484,7 +484,7 @@ protected:
}
};
-tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(bv1_blaster_tactic, m, p));
}
@@ -497,6 +497,6 @@ public:
}
};
-probe * mk_is_qfbv_eq_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfbv_eq_probe() {
return alloc(is_qfbv_eq_probe);
}
--- ./src/tactic/bv/bv_size_reduction_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/bv/bv_size_reduction_tactic.cpp 2015-05-27 20:19:34.444421841 -0600
@@ -46,7 +46,7 @@ public:
virtual void set_cancel(bool f);
};
-tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(bv_size_reduction_tactic, m));
}
--- ./src/tactic/bv/max_bv_sharing_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/bv/max_bv_sharing_tactic.cpp 2015-05-27 20:17:45.765071357 -0600
@@ -325,7 +325,7 @@ public:
}
};
-tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(max_bv_sharing_tactic, m, p));
}
--- ./src/tactic/core/cofactor_term_ite_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/cofactor_term_ite_tactic.cpp 2015-05-27 20:08:09.138970060 -0600
@@ -76,6 +76,6 @@ public:
virtual void set_cancel(bool f) { m_elim_ite.set_cancel(f); }
};
-tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(cofactor_term_ite_tactic, m, p));
}
--- ./src/tactic/core/ctx_simplify_tactic.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/ctx_simplify_tactic.h 2015-05-27 20:03:56.208138802 -0600
@@ -21,7 +21,7 @@ Notes:
#include"tactical.h"
-class ctx_simplify_tactic : public tactic {
+class __attribute__ ((visibility ("default"))) ctx_simplify_tactic : public tactic {
struct imp;
imp * m_imp;
params_ref m_params;
--- ./src/tactic/core/der_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/der_tactic.cpp 2015-05-27 20:15:24.248334316 -0600
@@ -104,6 +104,6 @@ public:
}
};
-tactic * mk_der_tactic(ast_manager & m) {
+__attribute__ ((visibility ("default"))) tactic * mk_der_tactic(ast_manager & m) {
return alloc(der_tactic, m);
}
--- ./src/tactic/core/distribute_forall_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/distribute_forall_tactic.cpp 2015-05-27 20:14:50.356031719 -0600
@@ -144,6 +144,6 @@ public:
virtual void cleanup() {}
};
-tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p) {
return alloc(distribute_forall_tactic);
}
--- ./src/tactic/core/elim_term_ite_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/elim_term_ite_tactic.cpp 2015-05-27 20:10:00.795080097 -0600
@@ -188,6 +188,6 @@ public:
}
};
-tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(elim_term_ite_tactic, m, p));
}
--- ./src/tactic/core/elim_uncnstr_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/elim_uncnstr_tactic.cpp 2015-05-27 20:06:46.250578399 -0600
@@ -1065,6 +1065,6 @@ protected:
}
};
-tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(elim_uncnstr_tactic, m, p));
}
--- ./src/tactic/core/nnf_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/nnf_tactic.cpp 2015-05-27 20:09:02.550716688 -0600
@@ -122,11 +122,11 @@ public:
}
};
-tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
return alloc(nnf_tactic, p);
}
-tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
params_ref new_p(p);
new_p.set_sym("mode", symbol("full"));
TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
--- ./src/tactic/core/occf_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/occf_tactic.cpp 2015-05-27 20:07:23.342621208 -0600
@@ -240,7 +240,7 @@ protected:
}
};
-tactic * mk_occf_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_occf_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(occf_tactic, m));
}
--- ./src/tactic/core/propagate_values_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/propagate_values_tactic.cpp 2015-05-27 20:10:53.469886875 -0600
@@ -270,7 +270,7 @@ protected:
}
};
-tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(propagate_values_tactic, m, p));
}
--- ./src/tactic/core/reduce_args_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/reduce_args_tactic.cpp 2015-05-27 20:12:05.144181184 -0600
@@ -78,7 +78,7 @@ public:
virtual void set_cancel(bool f);
};
-tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(reduce_args_tactic, m));
}
--- ./src/tactic/core/simplify_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/simplify_tactic.cpp 2015-05-27 20:14:11.358135464 -0600
@@ -127,11 +127,11 @@ unsigned simplify_tactic::get_num_steps(
return m_imp->get_num_steps();
}
-tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(simplify_tactic, m, p));
}
-tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p) {
params_ref xp = p;
xp.set_bool("elim_and", true);
return using_params(mk_simplify_tactic(m, xp), xp);
--- ./src/tactic/core/solve_eqs_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/solve_eqs_tactic.cpp 2015-05-27 20:12:43.223149905 -0600
@@ -778,7 +778,7 @@ public:
}
};
-tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) {
+__attribute__ ((visibility ("default"))) tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) {
if (r == 0)
return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
else
--- ./src/tactic/core/split_clause_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/split_clause_tactic.cpp 2015-05-27 20:02:54.028121318 -0600
@@ -145,6 +145,6 @@ public:
}
};
-tactic * mk_split_clause_tactic(params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_split_clause_tactic(params_ref const & p) {
return clean(alloc(split_clause_tactic, p));
}
--- ./src/tactic/core/symmetry_reduce_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/symmetry_reduce_tactic.cpp 2015-05-27 20:11:30.275956898 -0600
@@ -651,6 +651,6 @@ void symmetry_reduce_tactic::cleanup() {
// no-op.
}
-tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p) {
return alloc(symmetry_reduce_tactic, m);
}
--- ./src/tactic/core/tseitin_cnf_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/core/tseitin_cnf_tactic.cpp 2015-05-27 20:13:22.139052687 -0600
@@ -922,11 +922,11 @@ public:
}
};
-tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(tseitin_cnf_tactic, m, p));
}
-tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool("elim_and", true);
simp_p.set_bool("blast_distinct", true);
--- ./src/tactic/fpa/fpa2bv_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/fpa/fpa2bv_tactic.cpp 2015-05-27 20:33:34.473415000 -0600
@@ -154,6 +154,6 @@ protected:
}
};
-tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(fpa2bv_tactic, m, p));
}
--- ./src/tactic/fpa/qffp_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/fpa/qffp_tactic.cpp 2015-05-27 20:32:34.046235727 -0600
@@ -26,7 +26,7 @@ Notes:
#include"qffp_tactic.h"
-tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool("arith_lhs", true);
simp_p.set_bool("elim_and", true);
@@ -49,7 +49,7 @@ tactic * mk_qffp_tactic(ast_manager & m,
return st;
}
-tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p) {
return mk_qffp_tactic(m, p);
}
@@ -93,10 +93,10 @@ public:
virtual ~is_qffp_probe() {}
};
-probe * mk_is_qffp_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qffp_probe() {
return alloc(is_qffp_probe);
}
-probe * mk_is_qffpbv_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qffpbv_probe() {
return alloc(is_qffp_probe);
}
--- ./src/tactic/portfolio/smt_strategic_solver.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/portfolio/smt_strategic_solver.cpp 2015-05-26 21:36:38.781795769 -0600
@@ -107,7 +107,7 @@ public:
}
};
-solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) {
+__attribute__ ((visibility ("default"))) solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) {
return alloc(smt_strategic_solver_factory, logic);
}
--- ./src/tactic/probe.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/probe.cpp 2015-05-26 21:39:27.167458841 -0600
@@ -31,7 +31,7 @@ public:
}
};
-probe * mk_memory_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_memory_probe() {
return alloc(memory_probe);
}
@@ -56,15 +56,15 @@ public:
}
};
-probe * mk_depth_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_depth_probe() {
return alloc(depth_probe);
}
-probe * mk_size_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_size_probe() {
return alloc(size_probe);
}
-probe * mk_num_exprs_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_num_exprs_probe() {
return alloc(num_exprs_probe);
}
@@ -186,63 +186,63 @@ public:
}
};
-probe * mk_const_probe(double v) {
+__attribute__ ((visibility ("default"))) probe * mk_const_probe(double v) {
return alloc(const_probe, v);
}
-probe * mk_not(probe * p) {
+__attribute__ ((visibility ("default"))) probe * mk_not(probe * p) {
return alloc(not_probe, p);
}
-probe * mk_and(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_and(probe * p1, probe * p2) {
return alloc(and_probe, p1, p2);
}
-probe * mk_or(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_or(probe * p1, probe * p2) {
return alloc(or_probe, p1, p2);
}
-probe * mk_implies(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_implies(probe * p1, probe * p2) {
return mk_or(mk_not(p1), p2);
}
-probe * mk_eq(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_eq(probe * p1, probe * p2) {
return alloc(eq_probe, p1, p2);
}
-probe * mk_neq(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_neq(probe * p1, probe * p2) {
return mk_not(mk_eq(p1, p2));
}
-probe * mk_le(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_le(probe * p1, probe * p2) {
return alloc(le_probe, p1, p2);
}
-probe * mk_ge(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_ge(probe * p1, probe * p2) {
return mk_le(p2, p1);
}
-probe * mk_lt(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_lt(probe * p1, probe * p2) {
return mk_not(mk_ge(p1, p2));
}
-probe * mk_gt(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_gt(probe * p1, probe * p2) {
return mk_lt(p2, p1);
}
-probe * mk_add(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_add(probe * p1, probe * p2) {
return alloc(add_probe, p1, p2);
}
-probe * mk_mul(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_mul(probe * p1, probe * p2) {
return alloc(mul_probe, p1, p2);
}
-probe * mk_sub(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_sub(probe * p1, probe * p2) {
return alloc(sub_probe, p1, p2);
}
-probe * mk_div(probe * p1, probe * p2) {
+__attribute__ ((visibility ("default"))) probe * mk_div(probe * p1, probe * p2) {
return alloc(div_probe, p1, p2);
}
@@ -308,11 +308,11 @@ public:
}
};
-probe * mk_is_propositional_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_propositional_probe() {
return alloc(is_propositional_probe);
}
-probe * mk_is_qfbv_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfbv_probe() {
return alloc(is_qfbv_probe);
}
@@ -350,7 +350,7 @@ public:
}
};
-probe * mk_is_qfaufbv_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_is_qfaufbv_probe() {
return alloc(is_qfaufbv_probe);
}
@@ -405,19 +405,19 @@ public:
}
};
-probe * mk_num_consts_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_num_consts_probe() {
return alloc(num_consts_probe, false, 0);
}
-probe * mk_num_bool_consts_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_num_bool_consts_probe() {
return alloc(num_consts_probe, true, 0);
}
-probe * mk_num_arith_consts_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_num_arith_consts_probe() {
return alloc(num_consts_probe, false, "arith");
}
-probe * mk_num_bv_consts_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_num_bv_consts_probe() {
return alloc(num_consts_probe, false, "bv");
}
@@ -442,15 +442,15 @@ public:
}
};
-probe * mk_produce_proofs_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_produce_proofs_probe() {
return alloc(produce_proofs_probe);
}
-probe * mk_produce_models_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_produce_models_probe() {
return alloc(produce_models_probe);
}
-probe * mk_produce_unsat_cores_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_produce_unsat_cores_probe() {
return alloc(produce_unsat_cores_probe);
}
@@ -482,6 +482,6 @@ public:
}
};
-probe * mk_has_pattern_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_has_pattern_probe() {
return alloc(has_pattern_probe);
}
--- ./src/tactic/probe.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/probe.h 2015-05-26 21:08:02.374860743 -0600
@@ -26,7 +26,7 @@ Revision History:
#include"goal.h"
-class probe {
+class __attribute__ ((visibility ("default"))) probe {
public:
class result {
double m_value;
--- ./src/tactic/sls/sls_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/sls/sls_tactic.cpp 2015-05-27 20:34:20.861714259 -0600
@@ -112,7 +112,7 @@ public:
}
};
-tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
clean(alloc(sls_tactic, m, p)));
}
@@ -157,7 +157,7 @@ tactic * mk_preamble(ast_manager & m, pa
mk_nnf_tactic(m, p));
}
-tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m, p));
t->updt_params(p);
return t;
--- ./src/tactic/smtlogics/qfbv_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/smtlogics/qfbv_tactic.cpp 2015-05-26 21:40:22.980038225 -0600
@@ -31,7 +31,7 @@ Notes:
#define MEMLIMIT 300
-tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
main_p.set_bool("elim_and", true);
main_p.set_bool("push_ite_bv", true);
--- ./src/tactic/smtlogics/qflia_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/smtlogics/qflia_tactic.cpp 2015-05-26 21:41:13.448040924 -0600
@@ -56,7 +56,7 @@ struct quasi_pb_probe : public probe {
}
};
-probe * mk_quasi_pb_probe() {
+__attribute__ ((visibility ("default"))) probe * mk_quasi_pb_probe() {
return mk_and(mk_not(mk_is_unbounded_probe()),
alloc(quasi_pb_probe));
}
@@ -168,7 +168,7 @@ static tactic * mk_bounded_tactic(ast_ma
mk_fail_if_undecided_tactic());
}
-tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
main_p.set_bool("elim_and", true);
main_p.set_bool("som", true);
--- ./src/tactic/smtlogics/qflra_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/smtlogics/qflra_tactic.cpp 2015-05-26 21:41:32.478533621 -0600
@@ -27,7 +27,7 @@ Notes:
#include"ctx_simplify_tactic.h"
#include"probe_arith.h"
-tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
params_ref pivot_p;
pivot_p.set_bool("arith.greatest_error_pivot", true);
--- ./src/tactic/smtlogics/qfnia_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/smtlogics/qfnia_tactic.cpp 2015-05-26 21:42:21.226672542 -0600
@@ -86,7 +86,7 @@ tactic * mk_qfnia_sat_solver(ast_manager
mk_fail_if_undecided_tactic());
}
-tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
return and_then(mk_qfnia_premable(m, p),
or_else(mk_qfnia_sat_solver(m, p),
mk_smt_tactic()));
--- ./src/tactic/smtlogics/qfnra_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/smtlogics/qfnra_tactic.cpp 2015-05-26 21:42:41.273084772 -0600
@@ -32,7 +32,7 @@ static tactic * mk_qfnra_sat_solver(ast_
mk_fail_if_undecided_tactic());
}
-tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
+__attribute__ ((visibility ("default"))) tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p;
p1.set_uint("seed", 11);
p1.set_bool("factor", false);
--- ./src/tactic/tactical.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/tactical.cpp 2015-05-27 20:05:08.698355823 -0600
@@ -1193,7 +1193,7 @@ public:
}
};
-tactic * clean(tactic * t) {
+__attribute__ ((visibility ("default"))) tactic * clean(tactic * t) {
return alloc(cleanup_tactical, t);
}
--- ./src/tactic/tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/tactic.cpp 2015-05-27 20:16:23.059653672 -0600
@@ -92,7 +92,7 @@ void skip_tactic::operator()(goal_ref co
core = 0;
}
-tactic * mk_skip_tactic() {
+__attribute__ ((visibility ("default"))) tactic * mk_skip_tactic() {
return alloc(skip_tactic);
}
@@ -111,7 +111,7 @@ public:
virtual tactic * translate(ast_manager & m) { return this; }
};
-tactic * mk_fail_tactic() {
+__attribute__ ((visibility ("default"))) tactic * mk_fail_tactic() {
return alloc(fail_tactic);
}
@@ -131,7 +131,7 @@ public:
}
};
-tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
+__attribute__ ((visibility ("default"))) tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
return alloc(report_verbose_tactic, msg, lvl);
}
@@ -150,7 +150,7 @@ public:
}
};
-tactic * mk_trace_tactic(char const * tag) {
+__attribute__ ((visibility ("default"))) tactic * mk_trace_tactic(char const * tag) {
return alloc(trace_tactic, tag);
}
@@ -169,7 +169,7 @@ public:
}
};
-tactic * mk_fail_if_undecided_tactic() {
+__attribute__ ((visibility ("default"))) tactic * mk_fail_if_undecided_tactic() {
return alloc(fail_if_undecided_tactic);
}
--- ./src/tactic/ufbv/macro_finder_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/ufbv/macro_finder_tactic.cpp 2015-05-27 20:30:48.255675430 -0600
@@ -158,6 +158,6 @@ public:
}
};
-tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) {
return alloc(macro_finder_tactic, m, p);
}
--- ./src/tactic/ufbv/quasi_macros_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/ufbv/quasi_macros_tactic.cpp 2015-05-27 20:30:14.305383897 -0600
@@ -165,6 +165,6 @@ public:
}
};
-tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p) {
return alloc(quasi_macros_tactic, m, p);
}
--- ./src/tactic/ufbv/ufbv_tactic.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/tactic/ufbv/ufbv_tactic.cpp 2015-05-27 20:31:35.227928102 -0600
@@ -31,11 +31,11 @@ Notes:
#include"ufbv_tactic.h"
-tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)));
}
-tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
params_ref no_elim_and(p);
no_elim_and.set_bool("elim_and", false);
@@ -59,7 +59,7 @@ tactic * mk_ufbv_preprocessor_tactic(ast
mk_trace_tactic("ufbv_post"));
}
-tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {
+__attribute__ ((visibility ("default"))) tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p(p);
main_p.set_bool("mbqi", true);
main_p.set_uint("mbqi.max_iterations", UINT_MAX);
--- ./src/util/debug.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/debug.cpp 2015-05-27 20:38:30.761777865 -0600
@@ -49,7 +49,7 @@ static void init_debug_table() {
}
}
-void finalize_debug() {
+__attribute__ ((visibility ("default"))) void finalize_debug() {
dealloc(g_enabled_debug_tags);
g_enabled_debug_tags = 0;
}
--- ./src/util/env_params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/env_params.h 2015-05-25 21:32:54.140833230 -0600
@@ -21,7 +21,7 @@ Notes:
class param_descrs;
-struct env_params {
+struct __attribute__ ((visibility ("default"))) env_params {
static void updt_params();
static void collect_param_descrs(param_descrs & p);
/*
--- ./src/util/gparams.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/gparams.h 2015-05-25 21:33:37.488344147 -0600
@@ -21,7 +21,7 @@ Notes:
#include"params.h"
-class gparams {
+class __attribute__ ((visibility ("default"))) gparams {
struct imp;
static imp * g_imp;
public:
--- ./src/util/memory_manager.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/memory_manager.h 2015-05-25 15:55:55.094764811 -0600
@@ -41,12 +41,12 @@ Revision History:
#endif
-class out_of_memory_error : public z3_error {
+class __attribute__ ((visibility ("default"))) out_of_memory_error : public z3_error {
public:
out_of_memory_error();
};
-class memory {
+class __attribute__ ((visibility ("default"))) memory {
public:
static bool is_out_of_memory();
static void initialize(size_t max_size);
--- ./src/util/params.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/params.h 2015-05-25 21:32:12.480186537 -0600
@@ -30,7 +30,7 @@ typedef cmd_arg_kind param_kind;
class params;
class param_descrs;
-class params_ref {
+class __attribute__ ((visibility ("default"))) params_ref {
static params_ref g_empty_params_ref;
params * m_params;
@@ -108,7 +108,7 @@ inline std::ostream & operator<<(std::os
return out;
}
-class param_descrs {
+class __attribute__ ((visibility ("default"))) param_descrs {
struct imp;
imp * m_imp;
public:
--- ./src/util/prime_generator.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/prime_generator.h 2015-05-27 21:42:00.354673852 -0600
@@ -31,7 +31,7 @@ public:
/**
\brief Prime generator
*/
-class prime_generator {
+class __attribute__ ((visibility ("default"))) prime_generator {
svector<uint64> m_primes;
void process_next_k_numbers(uint64 k);
public:
@@ -40,7 +40,7 @@ public:
void finalize();
};
-class prime_iterator {
+class __attribute__ ((visibility ("default"))) prime_iterator {
unsigned m_idx;
prime_generator * m_generator;
bool m_global;
--- ./src/util/rational.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/rational.h 2015-05-27 20:37:40.974749748 -0600
@@ -21,7 +21,7 @@ Revision History:
#include"mpq.h"
-class rational {
+class __attribute__ ((visibility ("default"))) rational {
mpq m_val;
static rational m_zero;
static rational m_one;
--- ./src/util/statistics.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/statistics.h 2015-05-25 21:30:59.206085111 -0600
@@ -22,7 +22,7 @@ Notes:
#include<iostream>
#include"vector.h"
-class statistics {
+class __attribute__ ((visibility ("default"))) statistics {
typedef std::pair<char const *, unsigned> key_val_pair;
svector<key_val_pair> m_stats;
typedef std::pair<char const *, double> key_d_val_pair;
--- ./src/util/symbol.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/symbol.cpp 2015-05-26 21:43:35.820764343 -0600
@@ -62,13 +62,13 @@ public:
internal_symbol_table* g_symbol_table = 0;
-void initialize_symbols() {
+__attribute__ ((visibility ("default"))) void initialize_symbols() {
if (!g_symbol_table) {
g_symbol_table = alloc(internal_symbol_table);
}
}
-void finalize_symbols() {
+__attribute__ ((visibility ("default"))) void finalize_symbols() {
dealloc(g_symbol_table);
g_symbol_table = 0;
}
--- ./src/util/symbol.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/symbol.h 2015-05-26 21:10:11.425568323 -0600
@@ -28,7 +28,7 @@ Revision History:
template<typename T>
class symbol_table;
-class symbol {
+class __attribute__ ((visibility ("default"))) symbol {
char const * m_data;
template<typename T>
--- ./src/util/timeout.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/timeout.cpp 2015-05-26 21:44:07.681240845 -0600
@@ -46,13 +46,13 @@ public:
}
};
-void set_timeout(long ms) {
+__attribute__ ((visibility ("default"))) void set_timeout(long ms) {
if (g_timeout)
delete g_timeout;
g_timeout = new scoped_timer(ms, new g_timeout_eh());
}
-void register_on_timeout_proc(void (*proc)()) {
+__attribute__ ((visibility ("default"))) void register_on_timeout_proc(void (*proc)()) {
g_on_timeout = proc;
}
--- ./src/util/trace.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/trace.cpp 2015-05-26 21:44:29.192537050 -0600
@@ -33,7 +33,7 @@ static str_hashtable& get_enabled_trace_
return *g_enabled_trace_tags;
}
-void finalize_trace() {
+__attribute__ ((visibility ("default"))) void finalize_trace() {
dealloc(g_enabled_trace_tags);
g_enabled_trace_tags = 0;
}
--- ./src/util/util.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/util.cpp 2015-05-27 20:36:53.697521406 -0600
@@ -21,21 +21,21 @@ Revision History:
static unsigned g_verbosity_level = 0;
-void set_verbosity_level(unsigned lvl) {
+__attribute__ ((visibility ("default"))) void set_verbosity_level(unsigned lvl) {
g_verbosity_level = lvl;
}
-unsigned get_verbosity_level() {
+__attribute__ ((visibility ("default"))) unsigned get_verbosity_level() {
return g_verbosity_level;
}
static std::ostream* g_verbose_stream = &std::cerr;
-void set_verbose_stream(std::ostream& str) {
+__attribute__ ((visibility ("default"))) void set_verbose_stream(std::ostream& str) {
g_verbose_stream = &str;
}
-std::ostream& verbose_stream() {
+__attribute__ ((visibility ("default"))) std::ostream& verbose_stream() {
return *g_verbose_stream;
}
--- ./src/util/warning.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/warning.cpp 2015-05-27 20:36:28.859502919 -0600
@@ -70,7 +70,7 @@ void send_warnings_to_stdout(bool flag)
g_use_std_stdout = flag;
}
-void enable_warning_messages(bool flag) {
+__attribute__ ((visibility ("default"))) void enable_warning_messages(bool flag) {
g_warning_msgs = flag;
}
@@ -159,7 +159,7 @@ void print_msg(std::ostream * out, const
};
}
-void warning_msg(const char * msg, ...) {
+__attribute__ ((visibility ("default"))) void warning_msg(const char * msg, ...) {
if (g_warning_msgs) {
va_list args;
va_start(args, msg);
--- ./src/util/z3_exception.h.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/z3_exception.h 2015-05-25 21:30:27.551633818 -0600
@@ -21,7 +21,7 @@ Notes:
#include<string>
-class z3_exception {
+class __attribute__ ((visibility ("default"))) z3_exception {
public:
virtual ~z3_exception() {}
virtual char const * msg() const = 0;
@@ -29,7 +29,7 @@ public:
bool has_error_code() const;
};
-class z3_error : public z3_exception {
+class __attribute__ ((visibility ("default"))) z3_error : public z3_exception {
unsigned m_error_code;
public:
z3_error(unsigned error_code);
Reference in New Issue View Git Blame Copy Permalink