Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
101 commits
Select commit Hold shift + click to select a range
b5b04ed
Do not consider guards for sharing flips
ellieyhcheng Mar 23, 2021
031c65f
Squeezed vars uses new var when there's dependency conflicts
ellieyhcheng Apr 2, 2021
63e4f0f
Implement sbk encoding of discretes
ellieyhcheng Jun 22, 2021
592689f
Add bayesian networks
ellieyhcheng Jun 24, 2021
e95abab
Reorganize bayesian networks to benchmarks/bayesian-networks
ellieyhcheng Jun 24, 2021
ef09f92
Sang Beame Kautz encoding sorts probabilities high to low
ellieyhcheng Jun 25, 2021
515e149
Folds deterministic branches away and determinism in guard flips
ellieyhcheng Jun 25, 2021
2a1ab2e
Merge from upstream
ellieyhcheng Jun 29, 2021
504350b
Merge with stash
ellieyhcheng Jun 29, 2021
d7cfdd4
Merge stash
ellieyhcheng Jun 29, 2021
75a260f
SBK encoding orders flips by most used in different branches
ellieyhcheng Jul 3, 2021
5b08814
Add benchmarks
ellieyhcheng Jul 18, 2021
aa4de3c
use SBK only when there's shared flips
ellieyhcheng Jul 19, 2021
58e0bd0
Hoist complement flips
ellieyhcheng Jul 22, 2021
5cc320f
Merge remote-tracking branch 'upstream/master'
ellieyhcheng Jul 23, 2021
7d7be93
Reorder sbk flips to have hoisted flip at the end & use rounded equal…
ellieyhcheng Jul 26, 2021
4060122
Flip-hoisting v3
ellieyhcheng Aug 8, 2021
b101d2f
Count number of flips
ellieyhcheng Aug 9, 2021
56162ae
Count flips uses some tail recursion
ellieyhcheng Aug 10, 2021
5a42c4e
Merge branch 'master' of https://github.com/SHoltzen/dice
ellieyhcheng Aug 10, 2021
2166c60
Collects dataflow facts for cross-table hoisting
ellieyhcheng Aug 17, 2021
edc80ee
Add hoisting for across-table
ellieyhcheng Aug 22, 2021
ba6bbbc
Rename flip-hoisting and fix cross table bug
ellieyhcheng Aug 22, 2021
5516498
Clear warnings
ellieyhcheng Aug 22, 2021
ed41423
Fix bug where hoisted flips are missing
ellieyhcheng Aug 24, 2021
a91a1da
Fix cross table missing out flips because conflicting hoists
ellieyhcheng Aug 26, 2021
6aa7ffe
Count parameters and skipping compilation commands
ellieyhcheng Aug 27, 2021
e36e5a9
Cross table doesn't create extra variables
ellieyhcheng Aug 28, 2021
cdab19e
Split regular hoisting and cross-table hoisting to avoid being too gr…
ellieyhcheng Aug 29, 2021
40c4e1f
SBK encoding doesn't generate for 1.0
ellieyhcheng Sep 2, 2021
71f3280
Param count doesn't count 1.0 or 0.0
ellieyhcheng Sep 3, 2021
855400b
Flip limit
ellieyhcheng Sep 4, 2021
0506f66
Global hoisting only hoists tables next to each other
ellieyhcheng Sep 5, 2021
54bd418
Separate global and local matching
ellieyhcheng Sep 5, 2021
70734c2
Typo in global hoist
ellieyhcheng Sep 5, 2021
35ee59b
Global hoist still tracks all param matches
ellieyhcheng Sep 5, 2021
b51ffe5
Forgot to match Non for Flips
ellieyhcheng Sep 5, 2021
c4dd906
Don't push up shared flips during global
ellieyhcheng Sep 8, 2021
ea0eb9b
But still need to pass up the same flip
ellieyhcheng Sep 8, 2021
4b2268b
And match the right flip
ellieyhcheng Sep 8, 2021
da366db
Cross table documentation
ellieyhcheng Sep 9, 2021
73c10f1
merge from upstream
ellieyhcheng Nov 9, 2021
86c4385
Update float usage
ellieyhcheng Nov 9, 2021
2d18725
rename flip-hoisting and cross table to local hoisting and global hoi…
ellieyhcheng Nov 9, 2021
9b3e544
LogicalFormula Definitions
ellieyhcheng Dec 2, 2021
6b57a78
Additional pass to convert to logical formula
ellieyhcheng Dec 27, 2021
860f6a7
Add weights mapping
ellieyhcheng Dec 27, 2021
7276b77
Compile from logical formula to bdd
ellieyhcheng Dec 31, 2021
02827d3
Temp 1
ellieyhcheng Jan 6, 2022
ad6ef60
Compile to unweighted CNF
ellieyhcheng Jan 21, 2022
f4d1fa9
Tup 1
ellieyhcheng Jan 21, 2022
3c1c907
Bug fix generating CNF
ellieyhcheng Jan 24, 2022
2d1daca
Output cnf for sharpsat format
ellieyhcheng Jan 26, 2022
f79a73b
Call sharpSAT and output probability
ellieyhcheng Feb 3, 2022
a74bb4a
Remove redundant constants
ellieyhcheng Feb 6, 2022
44bbeec
Bubble up tuples in CG->LF pass
ellieyhcheng Feb 7, 2022
328adc3
CNF decisions
ellieyhcheng Feb 7, 2022
8fca521
Don't add line if var isn't used
ellieyhcheng Feb 7, 2022
690e94e
Don't try to add weight to var if it's not used
ellieyhcheng Feb 8, 2022
f1b79a5
Resolve merge
ellieyhcheng Feb 8, 2022
0533653
Assume unaccounted for vars are prob = 1
ellieyhcheng Feb 9, 2022
768cd14
Unfinished get table probs
ellieyhcheng Feb 9, 2022
c0449d9
CNF queries sharpSAT-td for each row of the joint probability table
ellieyhcheng Feb 11, 2022
55026a2
Computing subset marginals 1
ellieyhcheng Feb 15, 2022
4462579
Random marginal but type still glitch
ellieyhcheng Feb 17, 2022
3fec969
Generate tseitin encoding clauses directly
ellieyhcheng Feb 18, 2022
34c09d9
Logical formula size
ellieyhcheng Feb 22, 2022
e55ee5b
Average decision count
ellieyhcheng Feb 22, 2022
fce360b
More efficient generation of CNFs by reusing compiled sub-CNFs
ellieyhcheng Mar 1, 2022
7635d19
Compute time elapsed for CNF and for SharpSAT-td
ellieyhcheng Mar 1, 2022
b1c9527
SharpSAT-td should run flowcutter for 1 min
ellieyhcheng Mar 2, 2022
f8abbac
In place LF trees
ellieyhcheng Mar 7, 2022
17b02d9
Calculate LF to BDD time
ellieyhcheng Mar 8, 2022
587b2c4
Propagate tuple to the top when converting to BDD from LF
ellieyhcheng Mar 9, 2022
f3f1b27
Cache CNF printing
ellieyhcheng Mar 14, 2022
818991a
Used Buffer to print CNF
ellieyhcheng Mar 14, 2022
1e05b14
Don't use physical equality
ellieyhcheng Mar 17, 2022
0e28369
True needs to be a var that must be true
ellieyhcheng Apr 6, 2022
078da62
Streamline from_external_prog and bubble up Tuple rather than extract…
ellieyhcheng May 9, 2022
a7c232c
CG->LF bug fix
ellieyhcheng May 10, 2022
652a8b3
Remove print statements
ellieyhcheng May 11, 2022
bcc72b4
LF->CNF bottleneck bug fix by caching var names only and threading cn…
ellieyhcheng May 11, 2022
c20e1e4
Fix weird git diff artifacts
ellieyhcheng May 11, 2022
63ac36e
Flowcutter timeout flag
ellieyhcheng May 11, 2022
d3dcc48
Calculate Total CNF decisions not average
ellieyhcheng May 11, 2022
7acdce6
Lets do not share flips locally
ellieyhcheng May 11, 2022
460ba6a
Smarter append
ellieyhcheng May 11, 2022
9f84379
call SharpSAT-td only if not skipping table
ellieyhcheng May 12, 2022
f114651
Flip hoisting bug fix for negating flips
ellieyhcheng May 12, 2022
4eacfab
Calculate compilation time
ellieyhcheng May 17, 2022
a79983f
Remove flip-hoisting down pass redundant sorting
ellieyhcheng May 18, 2022
1a1b9eb
Increase max flips to 100000
ellieyhcheng May 18, 2022
bc1a794
Timings of up and down pass for flip hoisting
ellieyhcheng May 18, 2022
f64839b
Speed up global hoist
ellieyhcheng May 18, 2022
fa2dc01
revert
ellieyhcheng May 18, 2022
ea2c61a
Merge branch 'temp' of https://github.com/ellieyhcheng/dice into temp
ellieyhcheng May 18, 2022
53d406d
revert global
ellieyhcheng May 18, 2022
1314233
Merge branch 'temp' of https://github.com/ellieyhcheng/dice into temp
ellieyhcheng May 18, 2022
a43c8b4
Remove unused functions and debugging output
ellieyhcheng Jun 15, 2022
341a151
Merge pull request #1 from ellieyhcheng/temp
ellieyhcheng Jun 15, 2022
cd0da6a
merge from upstream
ellieyhcheng Nov 4, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions bench/dicebench.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ let run_benches () =
| Parser.Error ->
fprintf stderr "%a: syntax error\n" print_position buf;
failwith (Format.sprintf "Error parsing %s" contents) in
(parsed, Compiler.compile_program ~eager_eval:true (snd (Passes.from_external_prog parsed)))
(parsed, Compiler.compile_program ~eager_eval:true (snd (Passes.from_external_prog false (Passes.expand_recursion parsed) false false None false false)))
))) in
print_endline (Format.sprintf "Benchmark\tTime (s)\t#Paths (log10)\tBDD Size");
List.iter benches ~f:(fun (name, bench) ->
Expand Down Expand Up @@ -60,8 +60,8 @@ let bench_caesar inline_functions =
List.iter lst ~f:(fun len ->
let t0 = Unix.gettimeofday () in
let caesar = gen_caesar (List.init len ~f:(fun _ -> Random.int_incl 0 25)) in
let res = (if inline_functions then Passes.inline_functions caesar else caesar)
|> Passes.from_external_prog
let prog = (if inline_functions then Passes.inline_functions caesar else caesar) in
let res = Passes.from_external_prog false prog false false None false false
|> snd
|> Compiler.compile_program ~eager_eval:true in
let sz = 0 in
Expand Down Expand Up @@ -99,8 +99,8 @@ let bench_caesar_error inline_functions =
List.iter lst ~f:(fun len ->
let t0 = Unix.gettimeofday () in
let caesar = gen_caesar_error (List.init len ~f:(fun _ -> Random.int_incl 0 25)) in
let res = (if inline_functions then Passes.inline_functions caesar else caesar)
|> Passes.from_external_prog
let prog = (if inline_functions then Passes.inline_functions caesar else caesar) in
let res = Passes.from_external_prog false prog false false None false false
|> snd
|> Compiler.compile_program ~eager_eval:true in
(* let sz = Cudd.Bdd.size res.body.z in *)
Expand Down Expand Up @@ -135,7 +135,7 @@ let bench_diamond inline_functions =
let caesar = gen_diamond (len + 1) in
let inlined = if inline_functions then Passes.inline_functions caesar else caesar in
let t0 = Unix.gettimeofday () in
let res = Passes.from_external_prog inlined
let res = Passes.from_external_prog false inlined false false None false false
|> snd
|> Compiler.compile_program ~eager_eval:true in
let sz = VarState.state_size res.ctx.man [res.body.state] in
Expand Down Expand Up @@ -174,7 +174,7 @@ let bench_ladder inline_functions =
let caesar = gen_ladder (len + 1) in
let inlined = if inline_functions then Passes.inline_functions caesar else caesar in
let t0 = Unix.gettimeofday () in
let res = Passes.from_external_prog inlined
let res = Passes.from_external_prog false inlined false false None false false
|> snd
|> Compiler.compile_program ~eager_eval:true in
let sz = VarState.state_size res.ctx.man [res.body.state] in
Expand Down
25 changes: 25 additions & 0 deletions benchmarks/bayesian-networks/BN_28.dice

Large diffs are not rendered by default.

55 changes: 55 additions & 0 deletions benchmarks/bayesian-networks/BN_78.dice

Large diffs are not rendered by default.

55 changes: 55 additions & 0 deletions benchmarks/bayesian-networks/BN_79.dice

Large diffs are not rendered by default.

38 changes: 38 additions & 0 deletions benchmarks/bayesian-networks/alarm-alt.dice

Large diffs are not rendered by default.

38 changes: 38 additions & 0 deletions benchmarks/bayesian-networks/alarm-safer.dice

Large diffs are not rendered by default.

Loading