mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Bugfix for theory_fpa construction and destruction.
This commit is contained in:
parent
689ed9fa12
commit
5995c753d3
|
@ -142,7 +142,8 @@ namespace smt {
|
|||
m_trail_stack(*this),
|
||||
m_fpa_util(m_converter.fu()),
|
||||
m_bv_util(m_converter.bu()),
|
||||
m_arith_util(m_converter.au())
|
||||
m_arith_util(m_converter.au()),
|
||||
m_is_initialized(false)
|
||||
{
|
||||
params_ref p;
|
||||
p.set_bool("arith_lhs", true);
|
||||
|
@ -151,10 +152,24 @@ namespace smt {
|
|||
|
||||
theory_fpa::~theory_fpa()
|
||||
{
|
||||
ast_manager & m = get_manager();
|
||||
dec_ref_map_values(m, m_conversions);
|
||||
dec_ref_map_values(m, m_wraps);
|
||||
dec_ref_map_values(m, m_unwraps);
|
||||
if (m_is_initialized) {
|
||||
ast_manager & m = get_manager();
|
||||
dec_ref_map_values(m, m_conversions);
|
||||
dec_ref_map_values(m, m_wraps);
|
||||
dec_ref_map_values(m, m_unwraps);
|
||||
}
|
||||
else {
|
||||
SASSERT(m_conversions.empty());
|
||||
SASSERT(m_wraps.empty());
|
||||
SASSERT(m_unwraps.empty());
|
||||
}
|
||||
|
||||
m_is_initialized = false;
|
||||
}
|
||||
|
||||
void theory_fpa::init(context * ctx) {
|
||||
smt::theory::init(ctx);
|
||||
m_is_initialized = true;
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
|
|
|
@ -148,6 +148,7 @@ namespace smt {
|
|||
obj_map<sort, func_decl*> m_wraps;
|
||||
obj_map<sort, func_decl*> m_unwraps;
|
||||
obj_map<expr, expr*> m_conversions;
|
||||
bool m_is_initialized;
|
||||
|
||||
virtual final_check_status final_check_eh();
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
|
@ -169,9 +170,11 @@ namespace smt {
|
|||
virtual void finalize_model(model_generator & mg);
|
||||
|
||||
public:
|
||||
theory_fpa(ast_manager& m);
|
||||
theory_fpa(ast_manager & m);
|
||||
virtual ~theory_fpa();
|
||||
|
||||
virtual void init(context * ctx);
|
||||
|
||||
virtual void display(std::ostream & out) const;
|
||||
|
||||
protected:
|
||||
|
|
Loading…
Reference in a new issue