Use Patricia trees #207
Use Patricia trees #207
Conversation
N1ark
force-pushed
the
patricia-optims
branch
from
a4dceb7 to
bf3c390
Compare
giltho
left a comment
giltho
left a comment
There was a problem hiding this comment.
Looks good, though I'd also expose a way of doing States.PMap with patricia trees as well
| let v2, st = get_or_make v2 st in | ||
| merge v1 v2 st; | ||
| (* Here we choose to pass down the equality (rather than simplifying to true), | ||
| so that the underlying solver can do trivial SAT checks using these equalities. |
There was a problem hiding this comment.
Should "trivial_truthiness" go through analyses? It would avoid that problem?
There was a problem hiding this comment.
that's done in #208 hehe! though i dont think i removed this there so when you review it pls add a comment to remind me
There was a problem hiding this comment.
I don't see any modifications of trivial_truthiness in #208?
There was a problem hiding this comment.
ahh i misread that ! was thinking of the trivial_model_check or whatever it's called (better names needed maybe)
it's already handled in the trivial_truthiness, since here https://github.com/soteria-tools/soteria/blob/disjoint-analysis/soteria/lib/bv_values/bv_solver.ml#L21 it calls the fallback, which is analyses.simplify!
reallyyyy what we want is that BvSolver's PC is an analysis itself i think, which is at the bottom of the stack and for which:
- add_constraint... adds the constraint
- simplify checks the PC for a value and its negation
i think that would be quite elegant :)
There was a problem hiding this comment.
regardless of that change though this comment should go and i can now return true for equalities !!! so yayyy
|
yup will do tmw |
|
I believe this is ready to be merged as soon as you add Patricia trees for states then? |
|
can you actually just check the PR f83778d like it works but i am not super super convinced of how I did it so I'd like your opinion |
|
About to go to sleep and skiing tomorrow so I can't postpone sleep, but will do tomorrow! I had a very very quick look and saw you have S_PatriciaTree instead of S_patricia_tee somewhere :p |
* Use `Bimap` in `Fun_ctx` * Use Patricia trees where possible * Ignore failures in soteria-c `--benchmark` * Update shell.nix * Patricia trees of values * Tentative: add `Patricia_tree` to `pmap` * `Typo_in_module_name` :P * drive-by: Nicer frontend error message * Unexpose some `PMap` stuff
Fixes #170
Use the patricia-tree where possible. Unfortunately, there are a few places where we use hashconsed values over
Hashtbl/Hashset, whichPatricia_treedoesn't have an equivalent for.For where we used maps/sets I still did the switch; most notably:
Var.Map/Var.SetBv_solverandC_solverTree_borrowBenchmarks:
This one is over 50132 executions of
Rtree_block.Make.MemVal.merge, which itself callsTree_borrow.merge, which merges two integer maps. The new implementation usesidempotent_union, which is faster as it reuses subtrees