neuppl / rsdd

Performant and safe knowledge compilation in rust
https://neuppl.github.io/rsdd-docs/
MIT License
23 stars 9 forks source link

Adds Logical S-expression serialization, sketches out `bottomup_formula_to_bdd` #159

Closed mattxwang closed 1 year ago

mattxwang commented 1 year ago

Part of #155.

Usage:

$ cat bloop.sexp 
(And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y))))
$ cargo run --bin bottomup_formula_to_bdd --features="cli" -- -f bloop.sexp
{"nodes":[{"topvar":1,"low":"False","high":"True"},{"topvar":0,"low":{"Ptr":{"index":0,"compl":true}},"high":{"Ptr":{"index":0,"compl":false}}}],"roots":[{"Ptr":{"index":1,"compl":true}}]}

Or, for a manual ordering,

$ cat bloop.sexp 
(And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y))))
$ cat bloop.json
{ "order": ["Y", "X"] }
$ cargo run --bin bottomup_formula_to_bdd --features="cli" -- -f bloop.sexp -v --ordering manual -c bloop.json
=== METADATA ===
variable mapping: {"X": 0, "Y": 1}
variable ordering: [1, 0]
=== STATS ===
compilation time: 0.0033s
recursive calls: 9
{"nodes":[{"topvar":0,"low":"False","high":"True"},{"topvar":1,"low":{"Ptr":{"index":0,"compl":true}},"high":{"Ptr":{"index":0,"compl":false}}}],"roots":[{"Ptr":{"index":1,"compl":true}}]}