diff --git a/tests/z3-tests.adb b/tests/z3-tests.adb index d5765f2..5f8a59e 100644 --- a/tests/z3-tests.adb +++ b/tests/z3-tests.adb @@ -7,7 +7,7 @@ package body Z3.Tests is subtype LLI is Long_Long_Integer; subtype LLU is Long_Long_Unsigned; - Ctx : constant Context := New_Context; + Ctx : Context; function Simp (V : Bool_Type) return Bool_Type is begin @@ -271,7 +271,7 @@ package body Z3.Tests is procedure Incompatible_Context is - C1 : constant Context := New_Context; + C1 : Context; Result : constant Bool_Type := Bool (True, Ctx) = Bool (False, C1); begin pragma Unreferenced (Result); @@ -589,12 +589,12 @@ package body Z3.Tests is Optimize.Maximize (Int ("X", Ctx)); Optimize.Check (Result); Assert (Result = Result_True, "Invalid result"); - Assert (Optimize.Upper (Int ("X", Ctx)) = Int (LLU'(19), Ctx), "Invalid optimize value"); + Assert (Int (Optimize.Upper (Int ("X", Ctx))) = Int (LLU'(19), Ctx), "Invalid optimize value"); Optimize.Pop; Optimize.Maximize (Int ("X", Ctx)); Optimize.Check (Result); Assert (Result = Result_True, "Invalid result"); - Assert (Optimize.Upper (Int ("X", Ctx)) = Int (LLU'(99), Ctx), "Invalid optimize value"); + Assert (Int (Optimize.Upper (Int ("X", Ctx))) = Int (LLU'(99), Ctx), "Invalid optimize value"); Optimize.Push; Optimize.Reset; Assert_Exception (Optimize_Invalid_Pop'Access, "Too many pops not detected"); @@ -617,7 +617,7 @@ package body Z3.Tests is Optimize.Maximize (Objective); Optimize.Check (Result); Assert (Result = Result_True, "Invalid result"); - Assert (Optimize.Upper (Objective) = Int (LLU'(88), Ctx), "Invalid maximiize value"); + Assert (Int (Optimize.Upper (Objective)) = Int (LLU'(88), Ctx), "Invalid maximiize value"); declare Constant_Count : constant Natural := Optimize.Get_Number_Of_Values; Constants : Int_Array (1 .. Constant_Count); diff --git a/z3.adb b/z3.adb index 50436d0..06b865c 100644 --- a/z3.adb +++ b/z3.adb @@ -1,5 +1,6 @@ with Interfaces.C.Extensions; with Ada.Strings.Hash; +with Ada.Unchecked_Deallocation; with z3_optimization_h; with System; @@ -33,26 +34,26 @@ is ------------------------------------------------------------------------------------------------ - function Bool (Name : String; Context : Z3.Context) return Bool_Type + function Bool (Name : String; Context : Z3.Context'Class) return Bool_Type is begin return (Data => Const (Name => Name, Sort => z3_api_h.Z3_mk_bool_sort (Context.Data), Context => Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Bool; ------------------------------------------------------------------------------------------------ - function Bool (Value : Boolean; Context : Z3.Context) return Bool_Type + function Bool (Value : Boolean; Context : Z3.Context'Class) return Bool_Type is begin if Value then return (Data => z3_api_h.Z3_mk_true (Context.Data), - Context => Context); + Context => Z3.Context (Context)); end if; return (Data => z3_api_h.Z3_mk_false (Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Bool; ------------------------------------------------------------------------------------------------ @@ -168,7 +169,42 @@ is ------------------------------------------------------------------------------------------------ - function New_Context return Context is ((Data => z3_api_h.Z3_mk_context (z3_api_h.Z3_mk_config))); + overriding + procedure Initialize (Ctx : in out Context) + is + begin + Ctx.Config := z3_api_h.Z3_mk_config; + Ctx.Data := z3_api_h.Z3_mk_context (Ctx.Config); + Ctx.Ref_Count := new Natural; + Ctx.Ref_Count.all := 1; + end Initialize; + + overriding + procedure Finalize (Ctx : in out Context) + is + use type z3_api_h.Z3_config; + procedure Free is new Ada.Unchecked_Deallocation (Natural, Reference_Counter); + begin + if Ctx.Ref_Count.all > 0 then + Ctx.Ref_Count.all := Ctx.Ref_Count.all - 1; + end if; + if Ctx.Ref_Count.all > 0 then + return; + end if; + z3_api_h.Z3_del_context (Ctx.Data); + Ctx.Data := null; + z3_api_h.Z3_del_config (Ctx.Config); + Ctx.Config := null; + Free (Ctx.Ref_Count); + Ctx.Ref_Count := null; + end Finalize; + + overriding + procedure Adjust (Ctx : in out Context) + is + begin + Ctx.Ref_Count.all := Ctx.Ref_Count.all + 1; + end Adjust; ------------------------------------------------------------------------------------------------ @@ -238,25 +274,25 @@ is ------------------------------------------------------------------------------------------------ - function Int (Name : String; Context : Z3.Context) return Int_Type + function Int (Name : String; Context : Z3.Context'Class) return Int_Type is begin return (Data => Const (Name => Name, Sort => z3_api_h.Z3_mk_int_sort (Context.Data), Context => Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Int; ------------------------------------------------------------------------------------------------ function Int (Value : Long_Long_Integer; - Context : Z3.Context) return Int_Type + Context : Z3.Context'Class) return Int_Type is begin return (Data => z3_api_h.Z3_mk_int64 (c => Context.Data, v => Value, ty => z3_api_h.Z3_mk_int_sort (Context.Data)), - Context => Context); + Context => Z3.Context (Context)); end Int; ------------------------------------------------------------------------------------------------ @@ -280,13 +316,13 @@ is ------------------------------------------------------------------------------------------------ function Int (Value : Long_Long_Unsigned; - Context : Z3.Context) return Int_Type + Context : Z3.Context'Class) return Int_Type is begin return (Data => z3_api_h.Z3_mk_unsigned_int64 (c => Context.Data, v => Interfaces.C.Extensions.unsigned_long_long (Value), ty => z3_api_h.Z3_mk_int_sort (Context.Data)), - Context => Context); + Context => Z3.Context (Context)); end Int; ------------------------------------------------------------------------------------------------ @@ -421,23 +457,23 @@ is ------------------------------------------------------------------------------------------------ - function Create (Context : Z3.Context) return Solver + function Create (Context : Z3.Context'Class) return Solver is begin return (Data => z3_api_h.Z3_mk_solver (Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Create; ------------------------------------------------------------------------------------------------ function Create (Logic : Solver_Logic; - Context : Z3.Context) return Solver + Context : Z3.Context'Class) return Solver is 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 => Context); + Context => Z3.Context (Context)); end Create; ------------------------------------------------------------------------------------------------ @@ -648,7 +684,7 @@ is ------------------------------------------------------------------------------------------------ - function Create (Context : Z3.Context) return Optimize + function Create (Context : Z3.Context'Class) return Optimize is Opt : constant z3_api_h.Z3_optimize := z3_optimization_h.Z3_mk_optimize (Context.Data); begin @@ -656,7 +692,7 @@ is z3_optimization_h.Z3_optimize_inc_ref (Context.Data, Opt); z3_optimization_h.Z3_optimize_push (Context.Data, Opt); return Optimize'(Data => Opt, - Context => Context, + Context => Z3.Context (Context), Objectives => Int_Maps.Empty_Map, Backtracking_Count => 0); end Create; @@ -880,13 +916,13 @@ is ------------------------------------------------------------------------------------------------ function Big_Int (Value : String; - Context : Z3.Context) return Int_Type is (Big_Int (Value, 10, Context)); + Context : Z3.Context'Class) return Int_Type is (Big_Int (Value, 10, Context)); ------------------------------------------------------------------------------------------------ function Big_Int (Value : String; Base : Positive; - Context : Z3.Context) return Int_Type + Context : Z3.Context'Class) return Int_Type is Position : Long_Long_Integer := 0; Result : Int_Type; @@ -953,41 +989,41 @@ is function Bit_Vector (Name : String; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type + Context : Z3.Context'Class) return Bit_Vector_Type is begin return (Data => Const (Name => Name, Sort => z3_api_h.Z3_mk_bv_sort (Context.Data, Interfaces.C.unsigned (Size)), Context => Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Bit_Vector; ------------------------------------------------------------------------------------------------ function Bit_Vector (Value : Long_Long_Unsigned; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type + Context : Z3.Context'Class) return Bit_Vector_Type is begin return (Data => z3_api_h.Z3_mk_unsigned_int64 (c => Context.Data, v => Interfaces.C.Extensions.unsigned_long_long (Value), ty => z3_api_h.Z3_mk_bv_sort (Context.Data, Interfaces.C.unsigned (Size))), - Context => Context); + Context => Z3.Context (Context)); end Bit_Vector; ------------------------------------------------------------------------------------------------ function Bit_Vector (Value : Long_Long_Integer; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type + Context : Z3.Context'Class) return Bit_Vector_Type is begin return (Data => z3_api_h.Z3_mk_int64 (c => Context.Data, v => Value, ty => z3_api_h.Z3_mk_bv_sort (Context.Data, Interfaces.C.unsigned (Size))), - Context => Context); + Context => Z3.Context (Context)); end Bit_Vector; ------------------------------------------------------------------------------------------------ @@ -1184,31 +1220,31 @@ is ------------------------------------------------------------------------------------------------ function Real (Name : String; - Context : Z3.Context) return Real_Type + Context : Z3.Context'Class) return Real_Type is begin return (Data => Const (Name => Name, Sort => z3_api_h.Z3_mk_real_sort (Context.Data), Context => Context.Data), - Context => Context); + Context => Z3.Context (Context)); end Real; ------------------------------------------------------------------------------------------------ function Real (Numerator : Integer; - Context : Z3.Context) return Real_Type is (Real (Numerator, 1, Context)); + Context : Z3.Context'Class) return Real_Type is (Real (Numerator, 1, Context)); ------------------------------------------------------------------------------------------------ function Real (Numerator : Integer; Denominator : Integer; - Context : Z3.Context) return Real_Type + Context : Z3.Context'Class) return Real_Type is begin return (Data => z3_api_h.Z3_mk_real (c => Context.Data, num => Interfaces.C.int (Numerator), den => Interfaces.C.int (Denominator)), - Context => Context); + Context => Z3.Context (Context)); end Real; ------------------------------------------------------------------------------------------------ diff --git a/z3.ads b/z3.ads index 5e70291..2e1659f 100644 --- a/z3.ads +++ b/z3.ads @@ -1,5 +1,6 @@ with z3_api_h; with Ada.Iterator_Interfaces; +with Ada.Finalization; private with Ada.Containers; private with Ada.Containers.Indefinite_Hashed_Maps; @@ -13,7 +14,7 @@ package Z3 is -- GCOV_EXCL_LINE type Long_Long_Unsigned is mod 2 ** 64; - type Context is private; + type Context is new Ada.Finalization.Controlled with private; type Result is (Result_True, Result_False, Result_Undef); type Expr_Kind is (Kind_Any, @@ -40,8 +41,6 @@ package Z3 is -- GCOV_EXCL_LINE Sort_Real, Sort_Unknown); - function New_Context return Context; - type Expr_Type is tagged private with Default_Iterator => Iterate, Iterator_Element => Expr_Type'Class, @@ -77,11 +76,12 @@ package Z3 is -- GCOV_EXCL_LINE type Bool_Type is new Expr_Type with private; type Bool_Array is array (Natural range <>) of Bool_Type; - function Bool (Name : String; Context : Z3.Context) return Bool_Type; - function Bool (Value : Boolean; Context : Z3.Context) return Bool_Type; + function Bool (Name : String; Context : Z3.Context'Class) return Bool_Type; + function Bool (Value : Boolean; Context : Z3.Context'Class) return Bool_Type; function Bool (Expr : Expr_Type'Class) return Bool_Type with Pre => Sort (Expr) = Sort_Bool; function Same_Context (Terms : Bool_Array) return Boolean; + overriding function Simplified (Value : Bool_Type) return Bool_Type; @@ -132,12 +132,12 @@ package Z3 is -- GCOV_EXCL_LINE type Real_Type is new Arith_Type with private; function Real (Name : String; - Context : Z3.Context) return Real_Type; + Context : Z3.Context'Class) return Real_Type; function Real (Numerator : Integer; - Context : Z3.Context) return Real_Type; + Context : Z3.Context'Class) return Real_Type; function Real (Numerator : Integer; Denominator : Integer; - Context : Z3.Context) return Real_Type with + Context : Z3.Context'Class) return Real_Type with Pre => Denominator /= 0; function Real (Expr : Expr_Type'Class) return Real_Type with Pre => Sort (Expr) in Sort_Int | Sort_Real; @@ -149,20 +149,20 @@ package Z3 is -- GCOV_EXCL_LINE type Int_Type is new Arith_Type with private; type Int_Array is array (Natural range <>) of Int_Type; - function Int (Name : String; Context : Z3.Context) return Int_Type; + function Int (Name : String; Context : Z3.Context'Class) return Int_Type; function Int (Value : Long_Long_Integer; - Context : Z3.Context) return Int_Type; + Context : Z3.Context'Class) return Int_Type; function Int (Value : Long_Long_Unsigned; - Context : Z3.Context) return Int_Type; + Context : Z3.Context'Class) return Int_Type; function Int (Expr : Expr_Type'Class) return Int_Type with Pre => Sort (Expr) in Sort_Int | Sort_Real; function Big_Int (Value : String; - Context : Z3.Context) return Int_Type; + Context : Z3.Context'Class) return Int_Type; function Big_Int (Value : String; Base : Positive; - Context : Z3.Context) return Int_Type with + Context : Z3.Context'Class) return Int_Type with Pre => Base >= 2 and Base <= 16; function Same_Context (Values : Int_Array) return Boolean; @@ -235,16 +235,16 @@ package Z3 is -- GCOV_EXCL_LINE function Bit_Vector (Name : String; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type; + Context : Z3.Context'Class) return Bit_Vector_Type; function Bit_Vector (Value : Long_Long_Unsigned; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type with + Context : Z3.Context'Class) return Bit_Vector_Type with Pre => Size > Value'Size; function Bit_Vector (Value : Long_Long_Integer; Size : Natural; - Context : Z3.Context) return Bit_Vector_Type with + Context : Z3.Context'Class) return Bit_Vector_Type with Pre => Size >= Value'Size; function Bit_Vector (Value : Int_Type'Class; @@ -369,16 +369,16 @@ package Z3 is -- GCOV_EXCL_LINE Logic_QF_FD : constant Solver_Logic; Logic_SMTPD : constant Solver_Logic; - function Create (Context : Z3.Context) return Solver; - - function Create (Logic : Solver_Logic; - Context : Z3.Context) 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 + function Create (Context : Z3.Context'Class) return Solver; + + function Create (Logic : Solver_Logic; + Context : Z3.Context'Class) return Solver; + + procedure Assert (Solver : in out Z3.Solver; + Fact : Bool_Type'Class) with Pre => Same_Context (Solver, Fact); function Check (Solver : Z3.Solver) return Result; @@ -389,7 +389,7 @@ package Z3 is -- GCOV_EXCL_LINE function "+" (Optimize : Z3.Optimize) return String; - function Create (Context : Z3.Context) return Optimize; + function Create (Context : Z3.Context'Class) return Optimize; procedure Set_Timeout (Optimize : in out Z3.Optimize; Timeout : Natural := 1000); @@ -434,15 +434,22 @@ package Z3 is -- GCOV_EXCL_LINE private - type Config is - record - Data : z3_api_h.Z3_config; - end record; + type Reference_Counter is access Natural; - type Context is - record - Data : z3_api_h.Z3_context; - end record; + type Context is new Ada.Finalization.Controlled with record + Data : z3_api_h.Z3_context; + Config : z3_api_h.Z3_config; + Ref_Count : Reference_Counter; + end record; + + overriding + procedure Initialize (Ctx : in out Context); + + overriding + procedure Finalize (Ctx : in out Context); + + overriding + procedure Adjust (Ctx : in out Context); type Expr_Type is tagged record @@ -460,11 +467,10 @@ private type Bit_Vector_Type is new Arith_Type with null record; - type Solver is tagged limited - record - Data : z3_api_h.Z3_solver; - Context : Z3.Context; - end record; + type Solver is tagged limited record + Data : z3_api_h.Z3_solver; + Context : Z3.Context; + end record; package ICS renames Interfaces.C.Strings;