Skip to content

Commit ba08f43

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #524 from sosy-lab/yices-2.7.0
Update Yices to version v2.7.0+X, preparing for upcoming v2.8.0.
2 parents f5a7ab3 + 661c824 commit ba08f43

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+2105
-4539
lines changed

‎.appveyor.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ build_script:
4545
Copy-Item -Path "lib\java\runtime-mathsat\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
4646
Copy-Item -Path "lib\java\runtime-bitwuzla\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
4747
Copy-Item -Path "lib\java\runtime-cvc5\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
48+
Copy-Item -Path "lib\java\runtime-yices2\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
4849
4950
test_script:
5051
- ant unit-tests

‎.idea/JavaSMT.iml‎

Lines changed: 9 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎README.md‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -61,20 +61,20 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
6161

6262
JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
6363

64-
| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
65-
| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- |
66-
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic |
67-
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated |
68-
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | |
69-
| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
70-
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ | | |
71-
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | |
72-
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries |
73-
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
74-
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
75-
| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ | | |
76-
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
77-
| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | | | | | an older version of Z3 that still provides interpolation support |
64+
| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
65+
|-------------------------------------------------------------------------|:-------------------:|:-------------------:|:------------------:|:------------------:|:-------------------------------------------------------:|:------------------:|:----------------------------------------------------------------------------|
66+
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic |
67+
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated |
68+
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | |
69+
| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
70+
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ | | |
71+
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | |
72+
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries |
73+
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
74+
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
75+
| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ | | |
76+
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
77+
| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | | | | | an older version of Z3 that still provides interpolation support |
7878

7979
We support a reasonable list of operating systems and versions.
8080
- Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
@@ -114,19 +114,19 @@ If something specific is missing, please [look for or file an issue](https://git
114114

115115
#### Multithreading Support
116116

117-
| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
118-
| --- |:---:|:---:|
119-
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | |
120-
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | |
121-
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: |
122-
| [CVC5](https://cvc4.github.io/) | :question: | |
123-
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | |
124-
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :question: | |
125-
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | |
126-
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | |
127-
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | |
128-
| [Yices2](https://yices.csl.sri.com/) | | |
129-
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | |
117+
| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
118+
|-------------------------------------------------------------------------|:-------------------------:|:------------------------:|
119+
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | |
120+
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | |
121+
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: |
122+
| [CVC5](https://cvc4.github.io/) | :heavy_check_mark: | |
123+
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | |
124+
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | |
125+
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | |
126+
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | |
127+
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | |
128+
| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | |
129+
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | |
130130

131131
Interruption using a [ShutdownNotifier][] may be used to interrupt a solver from any thread.
132132
Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_.

‎build/build-maven-publish.xml‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -266,10 +266,13 @@ SPDX-License-Identifier: Apache-2.0
266266
<!-- get revision from dependencies -->
267267
<ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
268268
<property name="stage.solver" value="yices2"/>
269-
<property name="stage.revision" value="${libyices2j.revision}"/>
269+
<property name="stage.revision" value="${yices.revision}"/>
270+
<property name="libDir.x64" value="lib/java/runtime-yices2/x64"/>
270271
<!-- prepare the pom-file -->
271272
<generate-solver-pom-file/>
272273
<!-- then publish the file -->
273-
<stage-solver-file filename="libyices2j" classifier="libyices2j" fileending="so"/>
274+
<stage-solver-file filename="yices" fileending="jar"/>
275+
<stage-solver-file filename="libyices2java" classifier="libyices2java-x64" filedirectory="${libDir.x64}" fileending="so"/>
276+
<stage-solver-file filename="yices2java" classifier="yices2java-x64" filedirectory="${libDir.x64}" fileending="dll"/>
274277
</target>
275278
</project>

0 commit comments

Comments
 (0)