Skip to content

Commit f7a20a4

Browse files
committed
Add BDD memory management via preserve and sweep operations
Implemented commands for preserving, unpreserving, and sweeping Binary Decision Diagrams (BDDs). Enhanced the interpreter, parser, lexer, and documentation to support these features, and added comprehensive tests for validation.
1 parent 52afb54 commit f7a20a4

File tree

14 files changed

+450
-40
lines changed

14 files changed

+450
-40
lines changed

.idea/dictionaries/project.xml

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ add_executable(${PROJECT_NAME}
7171
src/walker_bdd_manip.cpp
7272
src/token.h
7373
src/walker_bdd_substitute.cpp
74+
src/walker_sweep.cpp
7475
)
7576
target_link_libraries(${PROJECT_NAME} abseil::abseil)
7677

@@ -90,6 +91,7 @@ add_executable(tests
9091
src/token.h
9192
tests/test_lexer.cpp
9293
src/walker_bdd_substitute.cpp
94+
src/walker_sweep.cpp
9395
)
9496
target_link_libraries(tests PRIVATE Catch2::Catch2WithMain abseil::abseil)
9597
add_test(NAME bdd_engine_tests COMMAND tests)

README.md

Lines changed: 97 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,6 @@
55
C++ Implementation of Reduced Ordered [Binary Decision Diagrams](https://en.wikipedia.org/wiki/Binary_decision_diagram)
66
for Propositional Formulae Manipulation.
77

8-
## Todo
9-
10-
*Meta Features*
11-
12-
- Implement garbage sweeping of unreachable BDD nodes
13-
- Web GUI using WASM
14-
158
# Language
169

1710
## Grammar
@@ -27,16 +20,21 @@ statements:
2720
statement:
2821
| "bvar" IDENTIFIER* ";"
2922
| "set" IDENTIFIER "=" expression ";"
30-
| function_name expression* ";"
23+
| function_call ";"
3124
| expression ";"
3225
33-
function_name
34-
| "display_tree"
35-
| "display_graph"
36-
| "is_sat"
37-
| "source"
26+
function_call
27+
| "display_tree" expression
28+
| "display_graph" expression
29+
| "is_sat" expression
30+
| "source" FILENAME
3831
| "clear_cache"
39-
32+
| "preserve" IDENTIFIER*;
33+
| "preserve_all";
34+
| "unpreserve" IDENTIFIER*;
35+
| "unpreserve_all";
36+
| "sweep";
37+
4038
expression:
4139
| "sub" "{" (IDENTIFIER ":" expression ("," IDENTIFIER ":" expression)*)? "}" expression
4240
| equality
@@ -91,12 +89,12 @@ execution will not continue after the error.
9189

9290
## Statements
9391

94-
A statement is either
92+
Statements are used to
9593

96-
- a BDD variable declaration
97-
- an assignment
98-
- a function call
99-
- an expression statement
94+
- Declare symbolic variables
95+
- Do assignments
96+
- Call functions for BDD queries or memory management
97+
- Evaluate expressions
10098

10199
### Symbolic Variable Declaration
102100

@@ -110,6 +108,9 @@ This will create two symbolic variables `x` and `y`.
110108

111109
The order in which symbolic variables are declared is important as this is their order within the BDDs.
112110

111+
The BDD order cannot be changed without restarting the REPL or reloading the script since that would invalidate existing
112+
BDDs.
113+
113114
### Assignments
114115

115116
We can assign BDDs to any non-symbolic variables using the `set` keyword.
@@ -120,7 +121,7 @@ set b = !x | y;
120121
set c = a & b;
121122
```
122123

123-
### Built-in Functions
124+
### BDD Query Functions
124125

125126
We have a few built-in functions to query about the BDDs:
126127

@@ -155,6 +156,8 @@ satisfiable or not.
155156

156157
This reachability check is done with breath-first search (BFS)
157158

159+
### Loading and Running Scripts
160+
158161
#### Run a script file
159162

160163
```
@@ -170,7 +173,9 @@ The filename should only consist of the following characters:
170173
- Underscore (`_`)
171174
- Dot (`.`)
172175

173-
### Clearing Caches
176+
### Memory Management and Garbage Collection
177+
178+
#### clear_cache
174179

175180
The interpreter has caches for:
176181

@@ -190,6 +195,76 @@ clear_cache;
190195

191196
Will clear all of these caches.
192197

198+
#### preserve
199+
200+
Marks one or more BDDs as protected from garbage collection. When you preserve a BDD, it will not be deleted during a
201+
sweep operation, even if there are no other references to it.
202+
203+
```
204+
set a = x & y; // Create a BDD
205+
preserve a; // Mark 'a' as preserved
206+
sweep; // 'a' will be kept in memory
207+
```
208+
209+
You can preserve multiple BDDs by listing them:
210+
211+
```
212+
preserve a b c; // Preserve BDDs named 'a', 'b', and 'c'
213+
```
214+
215+
#### preserve_all
216+
217+
Marks all currently existing BDDs as preserved. This is useful when you want to ensure that your entire working set is
218+
protected from garbage collection.
219+
220+
```
221+
set a = x & y;
222+
set b = x | z;
223+
preserve_all; // Both 'a' and 'b' are now preserved
224+
sweep; // Nothing will be deleted
225+
```
226+
227+
#### unpreserve
228+
229+
Removes the preservation mark from one or more BDDs, making them eligible for garbage collection during the next sweep.
230+
231+
```
232+
preserve_all; // Preserve all BDDs
233+
unpreserve b; // Make 'b' eligible for deletion
234+
sweep; // 'b' will be deleted
235+
```
236+
237+
#### unpreserve_all
238+
239+
Removes the preservation mark from all BDDs, making all of them eligible for garbage collection.
240+
241+
```
242+
preserve_all;
243+
unpreserve_all; // No BDDs are preserved anymore
244+
sweep; // All unpreserved BDDs will be deleted
245+
```
246+
247+
#### sweep
248+
249+
Performs garbage collection, removing all non-preserved BDDs from memory. This helps manage memory usage by cleaning up
250+
BDDs that are no longer needed.
251+
252+
Sweep automatically calls `clear_cache` to ensure the caches are valid.
253+
254+
```
255+
set a = x & y;
256+
set b = a | z;
257+
preserve a;
258+
sweep; // 'b' will be deleted, but 'a' remains
259+
```
260+
261+
#### Notes
262+
263+
- The garbage collector always preserves the TRUE and FALSE nodes (BDD IDs 0 and 1)
264+
- When sweeping, all intermediate BDD nodes that are only referenced by deleted BDDs will also be removed
265+
- Attempting to preserve a non-existent BDD or a symbolic variable will result in an error message
266+
- Preserving a BDD preserves all nodes in its structure, including shared nodes used by other BDDs
267+
193268
### Expression Statements
194269

195270
An expression statement is simply an expression that is evaluated.
@@ -355,6 +430,7 @@ The project is a tree-walk interpreter, so it has three internal parts:
355430
- `walker_bdd_substitute.cpp` implements the run-time substitution of variables in BDDs
356431
- `walker_bdd_manip.cpp` implements the run-time construction and manipulation of BDDs
357432
- `walker_bdd_view.cpp` implements queries about the BDDs, such as satisfiability and display functions
433+
- `walker_sweep.cpp` implements memory management operations such as sweeping and cache clearing
358434

359435
The REPL and overall application are implemented by the following
360436

src/ast.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,10 @@ std::string stmt_repr(const stmt& statement) {
5555
for (const auto& arg : s.arguments) {
5656
result += expr_repr(*arg) + ", ";
5757
}
58-
result.pop_back(); // Remove last space
59-
result.pop_back(); // Remove last comma
58+
if (!s.arguments.empty()) {
59+
result.pop_back(); // Remove last space
60+
result.pop_back(); // Remove last comma
61+
}
6062
result += "))";
6163
return result;
6264
} else if constexpr (std::is_same_v<T, decl_stmt>) {

src/config.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,5 @@ constexpr bool print_tokens = false; // Set to true to print tokens
66
constexpr bool print_ast = false; // Set to true to print AST
77
constexpr auto warning_level = absl::LogSeverity::kWarning;
88

9-
constexpr bool use_colours = true; // Set to true to enable coloured parser errors
9+
// Set to true to enable coloured parser errors
10+
constexpr bool use_colours = true;

src/lexer.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,15 @@ const std::unordered_map<std::string, token::Type> keyword_map = {
1111
{"display_graph", token::Type::GRAPH_DISPLAY},
1212
{"is_sat", token::Type::IS_SAT},
1313
{"source", token::Type::SOURCE},
14-
{"clear_cache", token::Type::CLEAR_CACHE},
14+
{"sub", token::Type::SUBSTITUTE},
1515
{"exists", token::Type::EXISTS},
1616
{"forall", token::Type::FORALL},
17-
{"sub", token::Type::SUBSTITUTE},
17+
{"clear_cache", token::Type::CLEAR_CACHE},
18+
{"preserve", token::Type::PRESERVE},
19+
{"preserve_all", token::Type::PRESERVE_ALL},
20+
{"unpreserve", token::Type::UNPRESERVE},
21+
{"unpreserve_all", token::Type::UNPRESERVE_ALL},
22+
{"sweep", token::Type::SWEEP},
1823
};
1924

2025
constexpr bool is_lexeme_char(const char c) {
@@ -108,7 +113,7 @@ lex_result_t scan_to_tokens(const std::string& source) {
108113
tokens.emplace_back(token::Type::ID, std::to_string(number),
109114
number);
110115
} else {
111-
return std::unexpected<LexerException>(LexerException(
116+
return std::unexpected(LexerException(
112117
"Unexpected character: " + std::string(1, c),
113118
__func__));
114119
}

src/parser.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,11 @@ stmt parse_statement(const_span& sp) {
4747
case token::Type::IS_SAT:
4848
case token::Type::SOURCE:
4949
case token::Type::CLEAR_CACHE:
50+
case token::Type::PRESERVE:
51+
case token::Type::PRESERVE_ALL:
52+
case token::Type::UNPRESERVE:
53+
case token::Type::UNPRESERVE_ALL:
54+
case token::Type::SWEEP:
5055
return parse_func_call(sp);
5156
default: // assume expr statement
5257
return parse_expr_stmt(sp);

src/token.h

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,22 @@ struct token {
4141
GRAPH_DISPLAY,
4242
IS_SAT,
4343
SOURCE,
44-
CLEAR_CACHE,
4544

4645
// Special Keywords for quantifiers
4746
EXISTS,
4847
FORALL,
4948

49+
// Special Keywords for memory management
50+
CLEAR_CACHE,
51+
PRESERVE,
52+
UNPRESERVE,
53+
PRESERVE_ALL,
54+
UNPRESERVE_ALL,
55+
SWEEP,
5056
};
5157

5258
Type type;
53-
std::string lexeme; // the text of the token
59+
std::string lexeme; // the text of the token
5460
std::optional<uint32_t> token_value{}; // optional value for number tokens
5561

5662
token(const Type type, const std::string& lexeme,
@@ -62,7 +68,9 @@ struct token {
6268
std::string repr() const {
6369
return "Token(" + std::to_string(static_cast<int>(type)) + ", " +
6470
lexeme +
65-
(token_value.has_value() ? ", " + std::to_string(token_value.value()) : "") +
71+
(token_value.has_value()
72+
? ", " + std::to_string(token_value.value())
73+
: "") +
6674
")";
6775
}
6876
};

src/walker.cpp

Lines changed: 64 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ void Walker::walk_func_call_stmt(const func_call_stmt& statement) {
181181
auto filename =
182182
std::get<identifier>(*statement.arguments[0]).name.lexeme;
183183

184-
// Read all of the file into the buffer
184+
// Read all the file into the buffer
185185
std::string buffer;
186186
std::ifstream f(filename);
187187
if (!f.is_open()) {
@@ -225,6 +225,69 @@ void Walker::walk_func_call_stmt(const func_call_stmt& statement) {
225225
out << "Cleared all caches" << '\n';
226226
break;
227227
}
228+
case token::Type::PRESERVE: {
229+
for (const auto& arg : statement.arguments) {
230+
if (!std::holds_alternative<identifier>(*arg)) {
231+
throw ExecutionException(
232+
"Invalid argument type for preserve", __func__);
233+
}
234+
if (const auto& id = std::get<identifier>(*arg).name.lexeme;
235+
globals.contains(id)) {
236+
if (std::holds_alternative<Bdd_ptype>(globals[id])) {
237+
std::get<Bdd_ptype>(globals[id]).preserved = true;
238+
out << "Preserved BDD: " << id << '\n';
239+
} else {
240+
out << "Variable is not a BDD: " << id << '\n';
241+
}
242+
} else {
243+
out << "Variable not found: " << id << '\n';
244+
}
245+
}
246+
break;
247+
}
248+
case token::Type::PRESERVE_ALL: {
249+
for (auto& [name, value] : globals) {
250+
if (std::holds_alternative<Bdd_ptype>(value)) {
251+
std::get<Bdd_ptype>(value).preserved = true;
252+
out << "Preserved BDD: " << name << '\n';
253+
}
254+
}
255+
break;
256+
}
257+
case token::Type::UNPRESERVE: {
258+
for (const auto& arg : statement.arguments) {
259+
if (!std::holds_alternative<identifier>(*arg)) {
260+
throw ExecutionException(
261+
"Invalid argument type for unpreserve", __func__);
262+
}
263+
if (const auto& id = std::get<identifier>(*arg).name.lexeme;
264+
globals.contains(id)) {
265+
if (std::holds_alternative<Bdd_ptype>(globals[id])) {
266+
std::get<Bdd_ptype>(globals[id]).preserved = false;
267+
out << "Unpreserved BDD: " << id << '\n';
268+
} else {
269+
out << "Variable is not a BDD: " << id << '\n';
270+
}
271+
} else {
272+
out << "Variable not found: " << id << '\n';
273+
}
274+
}
275+
break;
276+
}
277+
case token::Type::UNPRESERVE_ALL: {
278+
for (auto& [name, value] : globals) {
279+
if (std::holds_alternative<Bdd_ptype>(value)) {
280+
std::get<Bdd_ptype>(value).preserved = false;
281+
out << "Unpreserved BDD: " << name << '\n';
282+
}
283+
}
284+
break;
285+
}
286+
case token::Type::SWEEP: {
287+
sweep();
288+
out << "Swept all non-preserved BDDs" << '\n';
289+
break;
290+
}
228291
default:
229292
throw ExecutionException("Unknown function call", __func__);
230293
}

0 commit comments

Comments
 (0)