Implement reference counting for solver

ref #24

tests/z3-tests.adb

@@ -760,7 +760,7 @@ package body Z3.Tests is
       pragma Unreferenced (T);
       procedure Test_Create (Logic : Solver_Logic)
       is
-         Ignore_Solver : constant Solver := Create (Logic, Ctx);
+         Ignore_Solver : constant Solver := Create (Ctx, Logic);
       begin
          null;
       end Test_Create;

z3.adb

@@ -457,23 +457,59 @@ is
 
    ------------------------------------------------------------------------------------------------
 
+   overriding
+   procedure Initialize (Solv : in out Solver)
+   is
+      use type z3_api_h.Z3_solver;
+   begin
+      if Solv.Data /= null then
+         z3_api_h.Z3_solver_inc_ref (c => Solv.Context.Data,
+                                     s => Solv.Data);
+      end if;
+   end Initialize;
+
+   overriding
+   procedure Adjust (Solv : in out Solver)
+   is
+   begin
+      z3_api_h.Z3_solver_inc_ref (c => Solv.Context.Data,
+                                  s => Solv.Data);
+   end Adjust;
+
+   overriding
+   procedure Finalize (Solv : in out Solver)
+   is
+   begin
+      z3_api_h.Z3_solver_dec_ref (c => Solv.Context.Data,
+                                  s => Solv.Data);
+   end Finalize;
+
    function Create (Context : Z3.Context'Class) return Solver
    is
+      Solver : constant Z3.Solver :=
+         Z3.Solver'(Ada.Finalization.Controlled with Data    => z3_api_h.Z3_mk_solver (Context.Data),
+                                                     Context => Z3.Context (Context));
    begin
-      return (Data    => z3_api_h.Z3_mk_solver (Context.Data),
-              Context => Z3.Context (Context));
+      z3_api_h.Z3_solver_inc_ref (c => Solver.Context.Data,
+                                  s => Solver.Data);
+      return Solver;
    end Create;
 
    ------------------------------------------------------------------------------------------------
 
-   function Create (Logic   : Solver_Logic;
-                    Context : Z3.Context'Class) return Solver
+   function Create (Context : Z3.Context'Class;
+                    Logic   : Solver_Logic) return Solver
    is
+      Z3_Logic : constant z3_api_h.Z3_symbol :=
+         z3_api_h.Z3_mk_string_symbol (Context.Data, z3_api_h.Z3_string (Logic));
+      Solver : constant Z3.Solver :=
+         Z3.Solver'(Ada.Finalization.Controlled with Data    => z3_api_h.Z3_mk_solver_for_logic
+                                                                   (Context.Data, Z3_Logic),
+                                                     Context => Z3.Context (Context));
    begin
-      return (Data    => z3_api_h.Z3_mk_solver_for_logic
-                           (Context.Data,
-                            z3_api_h.Z3_mk_string_symbol (Context.Data, z3_api_h.Z3_string (Logic))),
-              Context => Z3.Context (Context));
+      z3_api_h.Z3_solver_inc_ref (c => Solver.Context.Data,
+                                  s => Solver.Data);
+      return Solver;
    end Create;
 
    ------------------------------------------------------------------------------------------------

z3.ads

@@ -335,8 +335,6 @@ package Z3 is  --  GCOV_EXCL_LINE
               and Size (Left) = Size (Right);
 
    --  Solver
-   type Solver is tagged limited private;
-
    type Solver_Logic is private;
 
    Logic_AUFLIA    : constant Solver_Logic;
@@ -369,13 +367,15 @@ package Z3 is  --  GCOV_EXCL_LINE
    Logic_QF_FD     : constant Solver_Logic;
    Logic_SMTPD     : constant Solver_Logic;
 
-   function Same_Context (Solver : Z3.Solver;
-                          Fact   : Bool_Type'Class) return Boolean;
+   type Solver is new Ada.Finalization.Controlled with private;
 
    function Create (Context : Z3.Context'Class) return Solver;
 
-   function Create (Logic   : Solver_Logic;
-                    Context : Z3.Context'Class) return Solver;
+   function Create (Context : Z3.Context'Class;
+                    Logic   : Solver_Logic) return Solver;
+
+   function Same_Context (Solver : Z3.Solver;
+                          Fact   : Bool_Type'Class) return Boolean;
 
    procedure Assert (Solver : in out Z3.Solver;
                      Fact   :        Bool_Type'Class) with
@@ -467,11 +467,20 @@ private
 
    type Bit_Vector_Type is new Arith_Type with null record;
 
-   type Solver is tagged limited record
-      Data : z3_api_h.Z3_solver;
+   type Solver is new Ada.Finalization.Controlled with record
       Context : Z3.Context;
+      Data : z3_api_h.Z3_solver;
    end record;
 
+   overriding
+   procedure Initialize (Solv : in out Solver);
+
+   overriding
+   procedure Finalize (Solv : in out Solver);
+
+   overriding
+   procedure Adjust (Solv : in out Solver);
+
    package ICS renames Interfaces.C.Strings;
 
    type Solver_Logic is new ICS.chars_ptr;