NetworkVerification / nv

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

Forall expression #62

Closed nickgian closed 4 years ago

nickgian commented 4 years ago

Adds a forall expression of type (a->bool)->(b->bool)->dict[a,b]->bool. forall p f m has the following semantics: forall (k,v) in m. p k => f v

There might be other similar primitives that are useful. Implemented for simulator, but I didn't do something about the SMT, perhaps a warning that it won't work with SMT should be inserted.

Also refactored some bad code in compiled simulation.