search

NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Resolve #73 #74

Closed alberdingk-thijm closed 2 years ago

alberdingk-thijm commented 2 years ago

This PR changes ConstantSet.compare back to String.compare from String.numeric_compare, which bumps the speed of encoding back up significantly and resolves #73. To make this change, we have to change how we determine the relevant SMT terms for each input expression: instead of searching through the declared constants, we store the full set of variables for each input. Right now, this is done at partitioning time, which unfortunately means that the type information of the attribute is not used to reconstitute the input hyp routes back together. As a further modification, we should change this to properly use the transformations to map the values back.

alberdingk-thijm commented 2 years ago

Later commits have now resolved the issue with mapping back hypotheses, so this PR is all done. Has definitely exposed some other things that should be fixed later, but for now we have some improvements.