Skip to content
This repository has been archived by the owner on Aug 12, 2024. It is now read-only.

Commit

Permalink
Implement context as controlled type
Browse files Browse the repository at this point in the history 
ref #24
  • Loading branch information
@jklmnn
jklmnn committed Dec 7, 2021
1 parent f67c7be commit 93d169e
Show file tree
Hide file tree
Showing 3 changed files with 115 additions and 73 deletions.
10 changes: 5 additions & 5 deletions tests/z3-tests.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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");
Expand All @@ -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);
Expand Down
98 changes: 67 additions & 31 deletions z3.adb
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
with Interfaces.C.Extensions;
with Ada.Strings.Hash;
with Ada.Unchecked_Deallocation;
with z3_optimization_h;
with System;

Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------

Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------
Expand All @@ -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;

------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -648,15 +684,15 @@ 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
-- 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 => Context,
Context => Z3.Context (Context),
Objectives => Int_Maps.Empty_Map,
Backtracking_Count => 0);
end Create;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -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;

------------------------------------------------------------------------------------------------
Expand Down
Loading

0 comments on commit 93d169e

Please sign in to comment.