Improve adding theories

[RobinWebbers]

Problem

Currently, a lot of code effort is required to add new theories to Liquid Fixpoint. It would be nicer if we could leverage most of the system to do this for us. This would remove clutter from having 50 names in the code base for the functions, as well as their accompanying types.

Proposed solution

Have a directive in Liquid Fixpoint syntax to bind a LF function to an underlying SMTLIB2 function. Something like the rust #[...]

#[smt="smt_set_emp"]
constant Set_empty : func(1, [int; Set_Set @(0)])

Then just prepend a file containing all these definitions when solving a liquid fixpoint file (to avert having to do actual package managing). Of course the syntax of the annotation may be different, but this is also extendible without parser changes for other purposes.