Support for :sat in Python SAW

[smithnormform]

In Python SAW one can call :prove from Cryptol. The following example illustrates how one can use this command:

import unittest
from saw_client             import *
from saw_client.crucible    import *
from saw_client.proofscript import *

class ProveTest(unittest.TestCase):
    def test(self):
        connect(reset_server=True)
        if __name__ == "__main__": view(LogResults(verbose_failure=True))

        thm  = cry_f("\(x : [8]) -> x + 1 != 0")
        x    = prove(thm, ProofScript([z3([])]))
        thm2 = cry_f("{x.get_counterexample()[0][1]} == 0xff")
        y    = prove(thm2, ProofScript([z3([])]))
        print(y.is_valid())

if __name__ == "__main__":
    unittest.main()

However, there's no Python support for Cryptol's :sat command. In fact, currently Python SAW lacks the type SatResult found in native SAW. It doesn't seem like a solution should be too bad though:

1. In saw_client/__init__.py add a class SatResult with two methods get_example and is_satisfiable similar to ProofResult.
2. In saw_client/__init__.py add a function sat similar to prove.
3. In saw_client/commands.py add a class SAT(SAWCommand) similar to Prove(SAWCommand).

[weaversa]

I agree it would be nice to have better coverage between Python and the commands in SAW. If you're in need of an immediate solution, you can negate (~) your property and prove should act identical to sat.

[smithnormform]

It will act identical as long as the function is total. Otherwise, prove seems to find an easy, error-producing counterexample. Maybe this discussion is relevant. In my case, I could artificially make my function total, but I'm not sure if we should always force totality so users can use sat.