Improve MRSolver interface

[m-yac]

This PR cleans up the Mr. Solver interface and introduces a new type of Mr. Solver assumption.

The interface now consists of:

• mr_solver_prove t1 t2 which asks Mr. Solver to prove t1 |= t2, throwing an error and exiting if it cannot, or adding a new assumption to the Mr. Solver context if it can. For refinements of the form f1 ... |= f2 ..., the assumption is added as an opaque assumption, which means calls to f1 on the LHS will now only be unfolded if a matching f2 cannot be found on the RHS. (Specifically, if we have such an opaque assumption and encounter f1 args1 >>= k1 |= f2 args2 >>= k2, we now prove that f1 args1 |= f2 args2 is provable from our assumption, then continue proving k1 |= k2.) Otherwise, for refinements of the form f1 ... |= rhs, the assumption is added as a rewrite assumption, which has the old behavior: always replacing calls of f1 on the LHS with rhs.
• mr_solver_test t1 t2 which is like the above, but does not add the result as an assumption. This is useful for testing that a refinement holds in isolation, e.g. for reflexivity or no-errors proofs.
• mr_solver_query t1 t2 which asks Mr. Solver to prove t1 |= t2, but unlike the above returns a boolean as to whether it could or could not. Calls to this function will never fail, and never add any assumptions.
• mr_solver_set_debug_level i sets the debug level of Mr. Solver until its next invocation.

Additionally, the first three have new console output which indicate when and when not assumptions are added to scope.

Finally, a change to the way memoization works in monadification was needed to make sure examples which use opaque assumptions work properly.

[eddywestbrook]

Looks good!