Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

xsts-cli: zip package, discussion #333

Open
AdamZsofi opened this issue Jan 21, 2025 · 2 comments
Open

xsts-cli: zip package, discussion #333

AdamZsofi opened this issue Jan 21, 2025 · 2 comments
Assignees
Labels
xsts Issue is XSTS specific (not core or XCFA or other formalisms)

Comments

@AdamZsofi
Copy link
Member

AdamZsofi commented Jan 21, 2025

Based on the "binary" we submit at SV-COMP, I created a similar package for xsts-cli. I mainly plan to use it with Semantifyr. It is bash script only for now.

First, I would like to just manually upload this theta-xsts.zip to the latest theta release. Later, we can add it to the CI, similar to Theta.zip, add a batch script, etc..

Whichever tools used the jar so far are free to continue to do so, this is just an extra option.

Semantifyr used the docker image so far, but I need to be able to use my local Theta to debug, and it is much simpler and nicer to have a bash script (and everything packaged in one) inbetween Semantifyr and the Theta jar. I will open a PR about this in Semantifyr soon.

Please discuss, do you have anything to change/add, do you mind if I upload this zip besides the current release?
@mondokm @leventeBajczi and anyone else.

Shell script

theta-start.sh.txt

( related: #332 )

Content

.
|-- CONTRIBUTORS.md
|-- GENERAL_README.md
|-- LIB_LICENSES.md
|-- LICENSE
|-- README.md
|-- cross_with.cex
|-- example
|   |-- choices.prop
|   |-- choices.xsts
|   `-- readme.txt
|-- lib
|   |-- Download-VCredist.ps1
|   |-- README.md
|   |-- com.microsoft.z3.jar
|   |-- com.microsoft.z3legacy.jar
|   |-- cvc5.jar
|   |-- hu.bme.mit.delta-0.0.1-all.jar
|   |-- javasmt.jar
|   |-- libcvc5.so.1
|   |-- libcvc5jni.so
|   |-- libcvc5parser.so
|   |-- libcvc5parser.so.1
|   |-- libmpfr.dylib
|   |-- libmpfr_java-1.0.so
|   |-- libmpfr_java-1.4.jnilib
|   |-- libpoly.so.0
|   |-- libpolyxx.so.0
|   |-- libtheta-llvm.so
|   |-- libz3.dll
|   |-- libz3.dylib
|   |-- libz3.so
|   |-- libz3java.dll
|   |-- libz3java.dylib
|   |-- libz3java.so
|   |-- libz3javalegacy.dll
|   |-- libz3javalegacy.dylib
|   |-- libz3javalegacy.so
|   |-- libz3legacy.dll
|   |-- libz3legacy.dylib
|   |-- libz3legacy.so
|   |-- mpfr64.dll
|   |-- mpfr_java-1.0-linux64.jar
|   |-- mpfr_java-1.0-windows64.jar
|   |-- mpfr_java-1.0.jar
|   |-- mpfr_java.dll
|   |-- mpir64.dll
|   `-- refinery-store-0.1.jar
|-- theta-smtlib.jar
|-- theta-start.sh
`-- theta-xsts-cli.jar
@AdamZsofi AdamZsofi added the xsts Issue is XSTS specific (not core or XCFA or other formalisms) label Jan 21, 2025
@mondokm
Copy link
Contributor

mondokm commented Jan 22, 2025

Great idea, I approve

@AdamZsofi
Copy link
Member Author

Uploaded manually to the v6.8.6 release - I'll use it for a while before doing anything else, but I'll leave this issue open until it is also added to CI.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
xsts Issue is XSTS specific (not core or XCFA or other formalisms)
Projects
None yet
Development

No branches or pull requests

2 participants