search

tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

Satisfiability Assertions #263

Closed sidprasad closed 3 months ago

sidprasad commented 3 months ago

Adding support for assertions about the satisfiability (or unsatisfiability) for assertions. These take the form:

assert <predicatename> is sat
assert <predicatename> is unsat
assert <predicatename> is forge_error
tnelson commented 3 months ago

@sidprasad Looks good. I made some minor revisions; if they look OK to you, go ahead and merge in.

I believe the answer to the comment I deleted is "yes", assuming it meant that both options were valid (not that they might be valid together).