@@ -161,7 +161,7 @@ This reachability check is done with breath-first search (BFS)
161
161
source <filename>
162
162
```
163
163
164
- Loads the entire file into memory, scans it, parses it and executes it. The file is expected to be a valid script.
164
+ Loads the entire file into memory, scans it, parses it, and executes it. The file is expected to be a valid script.
165
165
166
166
The filename should only consist of the following characters:
167
167
@@ -267,12 +267,15 @@ Quantification is used to eliminate variables from a BDD.
267
267
- ` exists x P ` is equivalent to ` (sub {x: true} P) | (sub {x: false} P) `
268
268
- ` forall x P ` is equivalent to ` (sub {x: true} P) & (sub {x: false} P) `
269
269
270
- Note that these operations are implemented directly and are thus more efficient than using substitutions to achieve the same effect.
270
+ Note that these operations are implemented directly and are thus more efficient than using substitutions to achieve the
271
+ same effect.
271
272
272
273
The quantification operations can support multiple variables with a single operation:
274
+
273
275
- e.g. ` exists (x y) P ` is equivalent to ` exists x (exists y P) `
274
276
275
- This is more efficient than performing multiple quantification operations in a row, as it does a single traversal of the BDD
277
+ This is more efficient than performing multiple quantification operations in a row, as it does a single traversal of the
278
+ BDD
276
279
277
280
### Propositional Logic Operations
278
281
@@ -345,9 +348,11 @@ The project is a tree-walk interpreter, so it has three internal parts:
345
348
- A call to the ` parse ` function returns an ` expected ` object that either has the parsed ASTs or a list of parse
346
349
errors.
347
350
- ` ast.h ` contains the abstract syntax tree (AST) node types
351
+ - ` ast.cpp ` implements a method to stringify the ASTs for debugging purposes
348
352
- A tree-walk interpreter
349
353
- ` walker.h ` contains the interface for the interpreter, including the run-time BDD graph
350
354
- ` walker.cpp ` implements the execution of statements
355
+ - ` walker_bdd_substitute.cpp ` implements the run-time substitution of variables in BDDs
351
356
- ` walker_bdd_manip.cpp ` implements the run-time construction and manipulation of BDDs
352
357
- ` walker_bdd_view.cpp ` implements queries about the BDDs, such as satisfiability and display functions
353
358
@@ -357,6 +362,7 @@ The REPL and overall application are implemented by the following
357
362
- ` colours.h ` contains the colour codes for terminal output
358
363
- ` main.cpp ` contains the main function
359
364
- ` repl.h/cpp ` contains the REPL interface/implementation
365
+ - ` engine_exceptions.h ` contains the custom exceptions for the lexer, parser, and walker
360
366
361
367
# Building and Dependencies
362
368
@@ -387,7 +393,7 @@ We can run benchmarks with `./tests "[!-benchmark]"` to get the benchmark result
387
393
388
394
### REPL Usage
389
395
390
- The default way to use the application is as a REPL. The REPL will read a line of input, parse it and execute it. The
396
+ The default way to use the application is as a REPL. The REPL will read a line of input, parse it, and execute it. The
391
397
REPL will print the result of the execution.
392
398
393
399
To be able to use up and down arrow keys to use previous commands, use ` rlwrap ` to run the binary.
@@ -399,7 +405,7 @@ rlwrap ./bdd_engine
399
405
### Script Usage
400
406
401
407
We can also pass a script file to the binary. The script file should be a valid script. The script file will be loaded
402
- into memory, scanned, parsed and executed.
408
+ into memory, scanned, parsed, and executed.
403
409
404
410
``` bash
405
411
./bdd_engine --source < script_file.bdd>
0 commit comments