search

gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

Fix slow integration of new paths into the tree #11

Closed gernst closed 2 years ago

gernst commented 2 years ago

path + "." and constraints + [.] are too costly

gernst commented 2 years ago

Turns out the reason is another one: z3.Not(_) is slow (likely hash-consing). Fixed by computing negated constraints only when the sampler is instantiated.