diff --git a/z3.adb b/z3.adb index 987e927..fd66088 100644 --- a/z3.adb +++ b/z3.adb @@ -727,12 +727,36 @@ is -- ISSUE: Componolit/AZ3#9 z3_optimization_h.Z3_optimize_inc_ref (Context.Data, Opt); z3_optimization_h.Z3_optimize_push (Context.Data, Opt); - return Optimize'(Data => Opt, - Context => Z3.Context (Context), - Objectives => Int_Maps.Empty_Map, - Backtracking_Count => 0); + return Optimize'(Ada.Finalization.Controlled with Data => Opt, + Context => Z3.Context (Context), + Objectives => Int_Maps.Empty_Map, + Backtracking_Count => 0); end Create; + overriding + procedure Initialize (Opt : in out Optimize) + is + use type z3_api_h.Z3_optimize; + begin + if Opt.Data /= null then + z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data); + end if; + end Initialize; + + overriding + procedure Adjust (Opt : in out Optimize) + is + begin + z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data); + end Adjust; + + overriding + procedure Finalize (Opt : in out Optimize) + is + begin + z3_optimization_h.Z3_optimize_inc_ref (Opt.Context.Data, Opt.Data); + end Finalize; + function "+" (Optimize : Z3.Optimize) return String is begin diff --git a/z3.ads b/z3.ads index 03bebab..16bd57c 100644 --- a/z3.ads +++ b/z3.ads @@ -367,7 +367,7 @@ package Z3 is -- GCOV_EXCL_LINE Logic_QF_FD : constant Solver_Logic; Logic_SMTPD : constant Solver_Logic; - type Solver is new Ada.Finalization.Controlled with private; + type Solver (<>) is new Ada.Finalization.Controlled with private; function Create (Context : Z3.Context'Class) return Solver; @@ -385,7 +385,7 @@ package Z3 is -- GCOV_EXCL_LINE procedure Reset (Solver : in out Z3.Solver); - type Optimize is tagged limited private; + type Optimize (<>) is new Ada.Finalization.Controlled with private; function "+" (Optimize : Z3.Optimize) return String; @@ -529,13 +529,22 @@ private package Int_Maps is new Ada.Containers.Indefinite_Hashed_Maps (Z3.Arith_Type'Class, Objective_Data, Hash, "="); - type Optimize is tagged limited record + type Optimize is new Ada.Finalization.Controlled with record Data : z3_api_h.Z3_optimize; Context : Z3.Context; Objectives : Int_Maps.Map; Backtracking_Count : Natural; end record; + overriding + procedure Initialize (Opt : in out Optimize); + + overriding + procedure Adjust (Opt : in out Optimize); + + overriding + procedure Finalize (Opt : in out Optimize); + function To_Z3_ast_array (Value : Bool_Array) return Z3_ast_array with Pre => Same_Context (Value), -- GCOV_EXCL_LINE Post => Value'Length = To_Z3_ast_array'Result'Length;