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;