C2po develop

[cgjohannsen]

Major rewrite of c2po, adding REPL capability. Allows for granular control of the compiler and extra analysis.

[aaurandt]

Nothing obvious sticks out other than the few minor changes required when computing the minimal bounds. I will try to pull and play with these changes to C2PO early next week, and provide further feedback.

[aaurandt]

I find it a little annoying that we now have to specify --spec to input the spec into C2PO. Is there ever an option where we won't be providing a .c2po file as input into C2PO?

I fixed some problems with check-sat. Should we add a few tests for this? Also, should there be something printed to the console when enabling SAT checking? If I recall correctly, there was previously a message printed indicating the results.

I also fixed some other option errors. I think I fixed them all, but you may want to double check.

@cgjohannsen Will we release this as 4.2.0? If so, I can update the version numbers in C2PO/R2U2.

[cgjohannsen]

The issue with omitting the '--spec' option is that when c2po runs in interactive or script mode it doesn't take as .c2po file as input. So 'python3 c2po.py -i' launches into interactive mode and shouldn't take any file as input. Same for when proving a script as in 'python3 c2po.py -s script.cmd'.

As for sat checking messaging, the check_sat command has a '--print' option that will print the output but it's off by default. I figure the best behavior is to only warn the user when their spec is unsat or unknown.

And I say we do a minor version bump like you suggest, so to 4.2.0.

Thanks for the help on this!