convert smt to expr

[agle]

• supports predicates and bvexprs that can be generated by bincaml
• will not support all bvops defined in smtlib, we could extend it but it will need some translation into the IR (e.g. we don't define greater-than operators, so convert to not-lessthan).
• expands expr gen property test to generate predicates
• removes associative binary operators from Ops.AllOps.binary so they are only present in Ops.AllOps.intrin -- make their representation canonical