search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

sat command #1146

Open AlisonElaine opened 3 years ago

AlisonElaine commented 3 years ago

Is just the 'sat' command defined somewhere? (I'm looking to use the command from the SAW manual defined.. sat : ProofScript SatResult -> Term -> TopLevel SatResult). I found the 'prove' command in the ProofScript.hs in SAWServer, but was unable to track down a similiar call for the 'sat' command. I might just be missing where it is located- any help is appreciated. Thanks!

atomb commented 3 years ago

I'm not entirely sure if I know which of two questions you're asking, so I'll answer them both!

In SAWScript, the sat command is defined in SAWScript/Builtins.hs. In general, you can find the name of the Haskell function that implements any SAWScript command by looking in SAWScript/Interpreter.hs.

For the SAW server, all of the available commands are defined in saw-remote-api/saw-remote-api/Main.hs. This includes SAW/prove, but there's currently no equivalent to the SAWScript sat command. We do plan to add bindings to that function at some point soon, but haven't done it yet.