Implement reference counting for optimize

ref #24
Componolit · Nov 22, 2021 · 49c9dc7 · 49c9dc7
1 parent 37a4304
commit 49c9dc7
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 7 deletions.
diff --git 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
@@ -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;