Skip to content

Commit

Permalink
Merge branch 'topic/free_clause' into 'master'
Browse files Browse the repository at this point in the history
Expose procedure for deallocating a Clause.

See merge request eng/libadalang/adasat!21
  • Loading branch information
raph-amiard committed Jan 3, 2024
2 parents 64a3da5 + 593416e commit 01e9a19
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 7 deletions.
2 changes: 2 additions & 0 deletions src/adasat-dpll.adb
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
14 changes: 14 additions & 0 deletions src/adasat.adb
Original file line number Diff line number Diff line change
Expand Up @@ -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);

---------
-- "+" --
---------
Expand Down Expand Up @@ -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;
10 changes: 3 additions & 7 deletions src/adasat.ads
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand All @@ -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;

0 comments on commit 01e9a19

Please sign in to comment.