From 593416e78e7dad99137c7499a17352201ed953d4 Mon Sep 17 00:00:00 2001
From: Romain Beguet <beguet@adacore.com>
Date: Fri, 22 Dec 2023 12:06:31 +0100
Subject: [PATCH] Expose procedure for deallocating a Clause.

---
 src/adasat-dpll.adb |  2 ++
 src/adasat.adb      | 14 ++++++++++++++
 src/adasat.ads      | 10 +++-------
 3 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/adasat-dpll.adb b/src/adasat-dpll.adb
index bc87d89..adde15f 100644
--- a/src/adasat-dpll.adb
+++ b/src/adasat-dpll.adb
@@ -4,6 +4,8 @@
 --  SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 --
 
+with Ada.Unchecked_Deallocation;
+
 with AdaSAT.Vectors;
 with AdaSAT.Internals; use AdaSAT.Internals;
 
diff --git a/src/adasat.adb b/src/adasat.adb
index d0d71d5..596de75 100644
--- a/src/adasat.adb
+++ b/src/adasat.adb
@@ -5,8 +5,13 @@
 --
 
 with Ada.Strings.Unbounded;
+with Ada.Unchecked_Deallocation;
 
 package body AdaSAT is
+
+   procedure Free_Clause is new Ada.Unchecked_Deallocation
+     (Literal_Array, Clause);
+
    ---------
    -- "+" --
    ---------
@@ -80,4 +85,13 @@ package body AdaSAT is
       end loop;
       return To_String (Res);
    end Image;
+
+   ----------
+   -- Free --
+   ----------
+
+   procedure Free (C : in out Clause) is
+   begin
+      Free_Clause (C);
+   end Free;
 end AdaSAT;
diff --git a/src/adasat.ads b/src/adasat.ads
index 00e303f..a2f035b 100644
--- a/src/adasat.ads
+++ b/src/adasat.ads
@@ -4,8 +4,6 @@
 --  SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 --
 
-with Ada.Unchecked_Deallocation;
-
 --  The root package of the AdaSAT library. Defines the base data structures
 --  that are used everywhere else.
 --  You should instantiate the `AdaSAT.DPLL` package with your own theory or
@@ -61,6 +59,9 @@ package AdaSAT is
    function Image (M : Model) return String;
    --  Returns a string representation of the model
 
+   procedure Free (C : in out Clause);
+   --  Free memory allocated for the given clause
+
 private
 
    type Literal is new Integer;
@@ -72,9 +73,4 @@ private
    --
    --  Note that while both literals and variables are "just" integers, we
    --  cannot mix them up in our code thanks to Ada's strong type system.
-
-   procedure Free is new Ada.Unchecked_Deallocation
-     (Literal_Array, Clause);
-   --  We declare this here to make it available to each child package
-   --  of AdaSAT.
 end AdaSAT;