diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,7 @@ +# 1.2.1 (June 2021) + +* Include test suite data in the Hackage tarball. + # 1.2 (June 2021) This is primarily a bugfix release, but also adds support diff --git a/test/responses/err-behav-continue.exp b/test/responses/err-behav-continue.exp new file mode 100644 --- /dev/null +++ b/test/responses/err-behav-continue.exp @@ -0,0 +1,1 @@ +Right (RspErrBehavior "continued-execution") diff --git a/test/responses/err-behav-continue.rsp b/test/responses/err-behav-continue.rsp new file mode 100644 --- /dev/null +++ b/test/responses/err-behav-continue.rsp @@ -0,0 +1,1 @@ +(:error-behavior continued-execution) diff --git a/test/responses/err-behav-unrec.exp b/test/responses/err-behav-unrec.exp new file mode 100644 --- /dev/null +++ b/test/responses/err-behav-unrec.exp @@ -0,0 +1,12 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Unrecognized response from solver: + bad :error-behavior value +in response to command: + (get-info :error-behavior) + +Attempting to parse input for test resp: +Just "(:error-behavior freak-out)\n" + +in response to commands for test resp: +test cmd diff --git a/test/responses/err-behav-unrec.rsp b/test/responses/err-behav-unrec.rsp new file mode 100644 --- /dev/null +++ b/test/responses/err-behav-unrec.rsp @@ -0,0 +1,1 @@ +(:error-behavior freak-out) diff --git a/test/responses/error_bad.exp b/test/responses/error_bad.exp new file mode 100644 --- /dev/null +++ b/test/responses/error_bad.exp @@ -0,0 +1,4 @@ +Left Solver reported an error: + this is bad +in response to command: + test cmd diff --git a/test/responses/error_bad.rsp b/test/responses/error_bad.rsp new file mode 100644 --- /dev/null +++ b/test/responses/error_bad.rsp @@ -0,0 +1,1 @@ +(error "this is bad") diff --git a/test/responses/minisat_verbose_success.exp b/test/responses/minisat_verbose_success.exp new file mode 100644 --- /dev/null +++ b/test/responses/minisat_verbose_success.exp @@ -0,0 +1,1 @@ +Right AckSuccess diff --git a/test/responses/minisat_verbose_success.rsp b/test/responses/minisat_verbose_success.rsp new file mode 100644 --- /dev/null +++ b/test/responses/minisat_verbose_success.rsp @@ -0,0 +1,2 @@ +minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy. +success diff --git a/test/responses/minisat_verbose_success.strict.exp b/test/responses/minisat_verbose_success.strict.exp new file mode 100644 --- /dev/null +++ b/test/responses/minisat_verbose_success.strict.exp @@ -0,0 +1,8 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Parse exception: Failed reading: empty +Attempting to parse input for test resp: +Just "minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.\nsuccess\n" + +in response to commands for test resp: +test cmd diff --git a/test/responses/name.exp b/test/responses/name.exp new file mode 100644 --- /dev/null +++ b/test/responses/name.exp @@ -0,0 +1,1 @@ +Right (RspName "fancy solver #12") diff --git a/test/responses/name.rsp b/test/responses/name.rsp new file mode 100644 --- /dev/null +++ b/test/responses/name.rsp @@ -0,0 +1,1 @@ +(:name "fancy solver #12") diff --git a/test/responses/rsnunk-bad.exp b/test/responses/rsnunk-bad.exp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-bad.exp @@ -0,0 +1,12 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Unrecognized response from solver: + bad :reason-unknown value +in response to command: + reason? + +Attempting to parse input for test resp: +Just "(:reason-unknown foo bar baz)\n" + +in response to commands for test resp: +test cmd diff --git a/test/responses/rsnunk-bad.rsp b/test/responses/rsnunk-bad.rsp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-bad.rsp @@ -0,0 +1,1 @@ +(:reason-unknown foo bar baz) diff --git a/test/responses/rsnunk-incomplete.exp b/test/responses/rsnunk-incomplete.exp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-incomplete.exp @@ -0,0 +1,1 @@ +Right RspRsnIncomplete diff --git a/test/responses/rsnunk-incomplete.rsp b/test/responses/rsnunk-incomplete.rsp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-incomplete.rsp @@ -0,0 +1,1 @@ +(:reason-unknown incomplete) diff --git a/test/responses/rsnunk-memout.exp b/test/responses/rsnunk-memout.exp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-memout.exp @@ -0,0 +1,1 @@ +Right RspOutOfMemory diff --git a/test/responses/rsnunk-memout.rsp b/test/responses/rsnunk-memout.rsp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-memout.rsp @@ -0,0 +1,1 @@ +(:reason-unknown memout) diff --git a/test/responses/rsnunk-sexp.exp b/test/responses/rsnunk-sexp.exp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-sexp.exp @@ -0,0 +1,1 @@ +Right (RspUnkReason (SApp [SAtom "foo",SAtom "bar",SAtom "baz"])) diff --git a/test/responses/rsnunk-sexp.rsp b/test/responses/rsnunk-sexp.rsp new file mode 100644 --- /dev/null +++ b/test/responses/rsnunk-sexp.rsp @@ -0,0 +1,1 @@ +(:reason-unknown (foo bar baz)) diff --git a/test/responses/sat.exp b/test/responses/sat.exp new file mode 100644 --- /dev/null +++ b/test/responses/sat.exp @@ -0,0 +1,1 @@ +Right AckSat diff --git a/test/responses/sat.rsp b/test/responses/sat.rsp new file mode 100644 --- /dev/null +++ b/test/responses/sat.rsp @@ -0,0 +1,1 @@ +sat diff --git a/test/responses/success.exp b/test/responses/success.exp new file mode 100644 --- /dev/null +++ b/test/responses/success.exp @@ -0,0 +1,1 @@ +Right AckSuccess diff --git a/test/responses/success.rsp b/test/responses/success.rsp new file mode 100644 --- /dev/null +++ b/test/responses/success.rsp @@ -0,0 +1,1 @@ +success diff --git a/test/responses/unknown.exp b/test/responses/unknown.exp new file mode 100644 --- /dev/null +++ b/test/responses/unknown.exp @@ -0,0 +1,1 @@ +Right AckUnknown diff --git a/test/responses/unknown.rsp b/test/responses/unknown.rsp new file mode 100644 --- /dev/null +++ b/test/responses/unknown.rsp @@ -0,0 +1,1 @@ +unknown diff --git a/test/responses/unsat.exp b/test/responses/unsat.exp new file mode 100644 --- /dev/null +++ b/test/responses/unsat.exp @@ -0,0 +1,1 @@ +Right AckUnsat diff --git a/test/responses/unsat.rsp b/test/responses/unsat.rsp new file mode 100644 --- /dev/null +++ b/test/responses/unsat.rsp @@ -0,0 +1,1 @@ +unsat diff --git a/test/responses/unsupported.exp b/test/responses/unsupported.exp new file mode 100644 --- /dev/null +++ b/test/responses/unsupported.exp @@ -0,0 +1,2 @@ +Left unsupported command: + test cmd diff --git a/test/responses/unsupported.rsp b/test/responses/unsupported.rsp new file mode 100644 --- /dev/null +++ b/test/responses/unsupported.rsp @@ -0,0 +1,1 @@ +unsupported diff --git a/test/responses/version.exp b/test/responses/version.exp new file mode 100644 --- /dev/null +++ b/test/responses/version.exp @@ -0,0 +1,1 @@ +Right (RspVersion "1.8") diff --git a/test/responses/version.rsp b/test/responses/version.rsp new file mode 100644 --- /dev/null +++ b/test/responses/version.rsp @@ -0,0 +1,1 @@ +(:version "1.8") diff --git a/what4.cabal b/what4.cabal --- a/what4.cabal +++ b/what4.cabal @@ -1,6 +1,6 @@ -Cabal-version: 2.2 +Cabal-version: 2.4 Name: what4 -Version: 1.2 +Version: 1.2.1 Author: Galois Inc. Maintainer: jhendrix@galois.com, rdockins@galois.com Copyright: (c) Galois, Inc 2014-2021 @@ -22,6 +22,10 @@ to ensure type-correct manipulation of symbolic values. data-files: solverBounds.config + +Extra-source-files: + test/responses/*.exp + test/responses/*.rsp Extra-doc-files: README.md