Update SMTInterpol and add new theories#648
Conversation
Disable tests that use integer/bv conversions from Smtlib 2.7. Support has been added in recently, but 2.5-1388-ga5a4ab0c is too old
# Conflicts: # lib/ivy.xml
|
@kfriedberger You can build the binaries from my fork here. It includes a script to patch the version numbers for us, and the PR for SMTInterpol has been updated for the latest Ultimate release. The process should look something like this: git clone git@github.com:daniel-raffler/ultimate.git
cd ultimate
git checkout smtinterpol-dependency
cd releaseScripts
./patchVersion 0.3.1.20260413
cd ../trunk/source/BA_MavenParentUltimate
mvn install source:jar(The version string for The last line will build Ultimate and then install all packages to your local Maven repository. You can then pull it from there into your Ivy repo. I simply changed daniel@notebook:~/workspace/ivy$ svn diff ivysettings.xml
Index: ivysettings.xml
===================================================================
--- ivysettings.xml (revision 3248)
+++ ivysettings.xml (working copy)
@@ -11,8 +11,7 @@
</filesystem>
<chain name="extern">
<ibiblio name="maven2" m2compatible="true"/>
- <ibiblio name="jcenter" m2compatible="true" root="https://jcenter.bintray.com/" />
- <!-- <ibiblio name="restlet" m2compatible="true" root="https://maven.restlet.org/" /> -->
+ <ibiblio name="local" m2compatible="true" root="file://${user.home}/.m2/repository"/>
</chain>
</resolvers>
</ivysettings>Now the Maven packages can be copied to Ivy like this: ant install -Dorganisation=de.uni_freiburg.informatik.ultimate -Dmodule=de.uni_freiburg.informatik.ultimate.lib.lassoranker -Drevision=0.3.1.20260413Note that this will also pull some dependencies into the Ivy repository, which should probably be added separately: daniel@notebook:~/workspace/ivy$ svn status repository/
? repository/ch.qos.reload4j
? repository/com.sun.xml.bind/jaxb-osgi
M repository/commons-io/commons-io/ivy-2.16.1.xml
M repository/commons-io/commons-io/ivy-2.16.1.xml.md5
M repository/commons-io/commons-io/ivy-2.16.1.xml.sha1
? repository/de.uni_freiburg.informatik.ultimate
? repository/net.sf.trove4j
M repository/org.glassfish.hk2/osgi-resource-locator/ivy-1.0.3.xml
M repository/org.glassfish.hk2/osgi-resource-locator/ivy-1.0.3.xml.md5
M repository/org.glassfish.hk2/osgi-resource-locator/ivy-1.0.3.xml.sha1
? repository/org.osgi/org.osgi.service.prefs
? repository/org.osgi/osgi.annotationAlso note that the Ultimate packages are now under |
kfriedberger
left a comment
kfriedberger
left a comment
There was a problem hiding this comment.
Nice work.
Lets update JavaSMT now, and handle conflicts CPAchecker with LassoRanker later, as soon as JavaSMT is released.
| fsym = theory.getFunction(fun, paramSorts); | ||
| } catch (SMTLIBException e) { | ||
| // fsym = null | ||
| } |
There was a problem hiding this comment.
Is ignoring the exception really the best way to go?
There was a problem hiding this comment.
Good point! I've rewritten the function, and we're now checking for collisions before trying to declare the new symbol
| fsym = theory.getFunction(fun, paramSorts); | ||
| } catch (SMTLIBException e) { | ||
| // fsym = null | ||
| } |
There was a problem hiding this comment.
Is ignoring the exception really the best way to go?
| fsym = environment.getTheory().getFunction(fun, paramSorts); | ||
| } catch (SMTLIBException e) { | ||
| // fsym = null | ||
| } |
There was a problem hiding this comment.
Is ignoring the exception really the best way to go?
|
Completely unchecked and potentially untrue statement: wasn't the problem with updating SMTInterpol that it requires Java 21? |
|
Seems to work well on Java 17: https://github.com/sosy-lab/java-smt/actions/runs/24358593939/job/71132099693 |
No, it's just Ultimate (i.e LassoRanker, Eliminator, etc) that requires Java 21. This should be fine, though, as I believe CPAchecker is also using Java 21 The new SMTInterpol version only requires Java 8 |
|
Awesome! Thank you both for the clarification and also for the update! |
3 participants
Hello,
this PR updates SMTInterpol to the latest Maven release (= version
2.5-1388) and adds support for bitvectors and quantifiersUpdating SMTInterpol has been blocked for several years by conflicts with LassoRanker, see issue #468. However, there is now a PR (link) for Ultimate that makes SMTInterpol a regular dependency of LassoRanker, which fixes most of the conflicts. The remaining clashes are mostly in JavaCUP and some of the utility classes of SMTInterpol/Ultimate. Neither are likely to change in the future, and I couldn't find any issues when trying the new version with Benchcloud (See here: both columns use SMTInterpol
2.5-1388, the left uses LassoRanker from the PR, on the right we're using the current version, which causes crashes due to conflicting classes in the jars)