Example Gradle Project

[lorenzleutgeb]

I am trying to use JavaSMT within a project that is built with Gradle, and am having difficulties, especially with the Z3 dependencies. I already posted a question on StackOverflow, and would be very glad if you could help me out.

However, independently from my project, I think it would be beneficial to add an example setup using Gradle to JavaSMT.

[kfriedberger]

Thank you for your interest in JavaSMT.
We will take a look soon and report back.
An example setup for Gradle would be a great idea to extend our documentation.

[baierd]

Gradle searches for a pom.xml per default and it fails because some of our artifacts don't have any (or no useful ones).
You can however tell Gradle to search for artifacts directly.
To do this you need to add a metadataSource to your repo like so:

repositories {
    jcenter()
    mavenCentral {
        metadataSources {
            artifact()
        }
    }
}

[baierd]

I've added a Gradle example project that includes Z3.
Currently it resides on the branch Gradle-Example-Project in the doc folder if you want to check it out.
It will be merged into the master once its finished.
Everyone feel free to comment it as i am new to Gradle.
I'll add a few more examples/tests etc. in the upcoming weeks.

[lorenzleutgeb]

I left comments on f2b6c1d, mainly because the example project in its current form is incompatible with the most recent release of Gradle.

[lorenzleutgeb]

Off Topic: Congratulations on acceptance of your paper at CAV2021! In fact, my interest in JavaSMT is motivated by the development of ATLAS, which is covered in another CAV2021 paper!

[baierd]

Thank you very much!

The incompatibilities should be fixed now. If you find anything else please feel free to comment again!

Would you say that the Gradle example is helpful for your work, or would a more advanced example be more helpful?
If the later is the case, please give some details as to how and what would be helpful.

[kfriedberger]

Is there anything left to do? Otherwise we could merge this and apply potential fixes later.

[baierd]

From my point of view we can merge it.

[baierd]

I have updated the Gradle example project some more:

• All SMT-Solvers are now included. In the case of Yices2 this includes the Yices2-JavaSMT version needed to run it.
• A small readme was added, explaining the commands needed to build/test/run the project.
• A jar can now be build from the project.

@kfriedberger I've added a comment explaining how to run the project only with Yices2. Does this suffice or do i need to create another project just for Yices2?

[baierd]

I've added tests for Boolector and Yices2. Now all available solvers get tested when building the project. However, since parts of the tests rely on our examples, and in the current release of JavaSMT some of the needed methods are private, we need to make a small release or disable the tests.

The rest of the Gradle example is done and can be reviewed and merged.

[breandan]

I have encountered a number of issues configuring this project with Gradle. First, it seems like there are two outdated artifacts on Maven Central. For Z3, when I copy the default snippet for the Gradle Kotlin DSL into my build script as follows:

implementation("org.sosy-lab:javasmt-solver-z3:4.8.14")

This produces the error:

Execution failed for task ':kspTestKotlinJvm'.
> Error while evaluating property 'filteredArgumentsMap' of task ':kspTestKotlinJvm'
   > Could not resolve all files for configuration ':jvmTestCompileClasspath'.
      > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.14.
        Required by:
            project :
         > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.14.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.14/javasmt-solver-z3-4.8.14.pom
               > Cannot invoke "String.hashCode()" because "version" is null
         > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.14.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.14/javasmt-solver-z3-4.8.14.pom
               > Cannot invoke "String.hashCode()" because "version" is null

I have tried different variations, including:

// val libZ3Version = "4.8.14"
// implementation("org.sosy-lab:javasmt-solver-z3:$libZ3Version")
// implementation("org.sosy-lab:javasmt-solver-z3:libz3:$libZ3Version:so")
// implementation("org.sosy-lab:javasmt-solver-z3:libz3java:$libZ3Version:so")

In particular, configuring the type and classifier options for the solver libraries using Gradle is not straightforward. For Z3, I receive the error:

Supplied String module notation 'org.sosy-lab:javasmt-solver-z3:libz3:4.8.14:so' is invalid.

Has anyone been successful in configuring the third-party SMT solvers with Gradle? It would be helpful to provide a version of the Getting Started Guide for the Gradle Kotlin DSL.

[lorenzleutgeb]

@breandan, I think you you need to swap the version number with what comes after.

Has anyone been successful in configuring the third-party SMT solvers with Gradle?

I managed to get it to work in another project.

It would be helpful to provide a version of the Getting Started Guide for the Gradle Kotlin DSL.

Definitely.

[baierd]

@lorenzleutgeb should be right. Please try to use version 4.8.10 for Z3. I currently don't know why i chose version 4.8.14 in Gradle. If this does not help, please report back and i'll take a closer look.

[breandan]

Thank you for your replies. I tried both 4.8.10 and 4.8.14 using the example from @lorenzleutgeb's project:

        implementation("org.sosy-lab:javasmt-solver-z3:4.8.10:com.microsoft.z3@jar")
        implementation("org.sosy-lab:javasmt-solver-z3:4.8.10:com.microsoft.z3@jar")
        implementation("org.sosy-lab:javasmt-solver-z3:4.8.10:libz3@so")
        implementation("org.sosy-lab:javasmt-solver-z3:4.8.10:libz3java@so")
        implementation("org.sosy-lab:java-smt:3.11.0")

Unfortunately, both versions returned the following error:

* What went wrong:
Execution failed for task ':kspTestKotlinJvm'.
> Error while evaluating property 'filteredArgumentsMap' of task ':kspTestKotlinJvm'
   > Could not resolve all files for configuration ':jvmTestCompileClasspath'.
      > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.10.
        Required by:
            project :
         > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.10.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.10/javasmt-solver-z3-4.8.10.pom
               > java.lang.NullPointerException (no error message)
         > Could not resolve org.sosy-lab:javasmt-solver-z3:4.8.10.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.10/javasmt-solver-z3-4.8.10.pom
               > java.lang.NullPointerException (no error message)

I have pasted below the output from running ./gradlew --version:

------------------------------------------------------------
Gradle 7.4.2
------------------------------------------------------------

Build time:   2022-03-31 15:25:29 UTC
Revision:     540473b8118064efcc264694cbcaa4b677f61041

Kotlin:       1.5.31
Groovy:       3.0.9
Ant:          Apache Ant(TM) version 1.10.11 compiled on July 10 2021
JVM:          17.0.1 (JetBrains s.r.o. 17.0.1+12-b164.8)
OS:           Mac OS X 12.3.1 aarch64

Please let me know if you need any further information to diagnose.

edit: It just occurs to me that since I am running aarch64 this might be the reason why it doesn't work. However I do have an compiled version of Z3 I can run from the command line. Is there a way to drive a natively-installed Z3 using java-smt?

[kfriedberger]

You can use a natively-installed version of Z3.
JavaSMT needs to find the JAR-file for Z3, i.e., you need provide Z3 (in form of a JAR and a native library) via the library-path for Java, and/or provide an implementation of a loading-mechanism when creating the context for JavaSMT, see

java-smt/src/org/sosy_lab/java_smt/SolverContextFactory.java

Line 138 in 28e9304

* @param pLoader The loading mechanism (loading method) in this class can be injected by the user

).

[breandan]

@kfriedberger Thanks, I appreciate the info. However, I would prefer to avoid interacting with native libraries and all the FFI stuff. Shouldn't there be a way to bypass all of that and generate SMT-LIB 2.0 syntax directly, without needing any extra JARs? I just want to output the constraints to a file, feed it to Z3 via z3 constraints.txt, then read the output...

[kfriedberger]

JavaSMT does not provide a way to use process- or pipe-based interaction with SMT solvers (which seems to be your intent), but only provides interaction via native APIs. This was a design-decision that comes from the early times of JavaSMT and it has several benefits, for example, control over the SMT solver in terms of runtime, cancelation, and resource limits.

In general, dumping and reading single SMTLIB-formatted queries (ASSERT only, no PUSH or POP) is already supported for most included SMT solvers. A user can dump SMTLIB from one SMT solver (e.g. SMTInterpol) and read the String into another SMT solver like Z3. However, to use JavaSMT in the way you have described, the user needs to implement the process-based interaction on his own. Also note, that there can be minor variations in the SMT solvers' implementation of the SMTLIB standard.

[baierd]

@breandan i am running arch64 as well, that should not be a problem. Did you change anything besides the dependency versions? Also what version of Gradle are you running?

I'm gonna take a closer look.

[baierd]

I can't recreate your problem despite being on Arch64 myself and having the same Gradle version as you @breandan. I've even tried including the imports as described by @lorenzleutgeb and couldn't find a problem (btw. you have 1 import twice ;D). Did you try other solvers besides Z3?

[breandan]

@baierd Thank you for investigating. I am not sure what the issue is, but it seems like Gradle does not like the POM format? Here is the result from running ./gradlew build --scan: https://scans.gradle.com/s/63mnuv66cofam

[baierd]

@breandan could you try replacing the dot in org.sosy-lab with a / and report back? (org/sosy-lab)

If that does not help, could you copy & paste your repositories section from the build.gradle file here?

[breandan]

As advised, I tried replacing the . with /:

implementation("org/sosy-lab:javasmt-solver-z3:4.8.10:com.microsoft.z3@jar")
implementation("org/sosy-lab:javasmt-solver-z3:4.8.10:libz3@so")
implementation("org/sosy-lab:javasmt-solver-z3:4.8.10:libz3java@so")

This still produces the same error:

> Error while evaluating property 'filteredArgumentsMap' of task ':kspKotlinJvm'
   > Could not resolve all files for configuration ':jvmCompileClasspath'.
      > Could not resolve org/sosy-lab:javasmt-solver-z3:4.8.10.
        Required by:
            project :
         > Could not resolve org/sosy-lab:javasmt-solver-z3:4.8.10.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.10/javasmt-solver-z3-4.8.10.pom
               > Cannot invoke "String.hashCode()" because "version" is null
         > Could not resolve org/sosy-lab:javasmt-solver-z3:4.8.10.
            > Could not parse POM https://repo.maven.apache.org/maven2/org/sosy-lab/javasmt-solver-z3/4.8.10/javasmt-solver-z3-4.8.10.pom
               > Cannot invoke "String.hashCode()" because "version" is null

Here is the repositories section of my build.gradle.kts file:

repositories {
  mavenCentral()
}

If you want to create a sample project containing a build.gradle[.kts] template I would be happy to try and reproduce it. Thanks!

[baierd]

Ah i think i know whats causing the problem. Please try using the following repository options:

repositories {
  mavenCentral {
    metadataSources {
      mavenPom()
    }
  }
  mavenCentral {
    metadataSources {
      artifact()
    }
  }
}

This way it looks for a useable POM first and if it can't find any (your error) it simply uses the artifact that the dependency points to.
If this does not work please report back again with a sample project and i'll try to figure it out there.

[breandan]

After updating the repositories section, it now compiles but switching the solver to Z3, produces the following error:

java.lang.UnsatisfiedLinkError: no z3 in java.library.path: /Users/breandan/Library/Java/Extensions:/Library/Java/Extensions:/Network/Library/Java/Extensions:/System/Library/Java/Extensions:/usr/lib/java:.
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)
at java.base/java.lang.System.loadLibrary(System.java:1989)
at org.sosy_lab.common.NativeLibraries.loadLibrary(NativeLibraries.java:200)
at com.google.common.collect.ImmutableList.forEach(ImmutableList.java:422)
at org.sosy_lab.java_smt.basicimpl.AbstractSolverContext.loadLibrariesWithFallback(AbstractSolverContext.java:128)
at org.sosy_lab.java_smt.solvers.z3.Z3SolverContext.create(Z3SolverContext.java:123)
at org.sosy_lab.java_smt.SolverContextFactory.generateContext0(SolverContextFactory.java:254)
at org.sosy_lab.java_smt.SolverContextFactory.generateContext(SolverContextFactory.java:203)
... 3 more

I have Z3 version 4.8.15 - 64 bit installed and can run z3 from the command line. Thank you again!

[baierd]

Now try version 4.8.10 please.
We are a little behind in releases currently. But i will try to update Z3 this week!

[d-costa]

I'm facing the same problem as breandan:

The SMT solver Z3 is not available on this machine because of missing libraries (no z3 in java.library.path: [/usr/java/packages/lib, /usr/lib64, /lib64, /lib, /usr/lib]).

But I can see these files in build/dependencies:

• javasmt-solver-z3-4.8.10-com.microsoft.z3.jar
• libz3.so
• libz3java.so

build.gradle.kts:

repositories {
    mavenCentral {
        metadataSources {
            mavenPom()
        }
    }
    mavenCentral {
        metadataSources {
            artifact()
        }
    }
}
dependencies {
    implementation("org.sosy-lab:java-smt:3.12.0")
    runtimeOnly("org.sosy-lab:javasmt-solver-z3:4.8.10:com.microsoft.z3@jar")
    runtimeOnly("org.sosy-lab:javasmt-solver-z3:4.8.10:libz3@so")
    runtimeOnly("org.sosy-lab:javasmt-solver-z3:4.8.10:libz3java@so")

    implementation(files("build/dependencies/*.jar"))
}
configurations {
    register("javaSMTConfig").configure {
        extendsFrom(runtimeOnly.get())
    }
}
tasks.register<Copy>("copyDependencies") {
    dependsOn("cleanDownloadedDependencies")
    from(configurations["javaSMTConfig"])
    into("build/dependencies")
    rename(".*(lib[^-]*)-?.*.so", "\$1.so")
}
tasks.register<Delete>("cleanDownloadedDependencies") {
    delete(file("build/dependencies"))
}
tasks.compileKotlin {
    dependsOn("copyDependencies")
}
tasks.clean {
    dependsOn("cleanDownloadedDependencies")
}

Edit: Found the issue. This script now works by replacing

configurations {
    register("javaSMTConfig").configure {
        extendsFrom(runtimeOnly.get())
    }
}

with

configurations {
    register("javaSMTConfig").configure {
        dependencies.addAll(runtimeOnly.get().dependencies.filter { it.group == "org.sosy-lab" })
        dependencies.addAll(implementation.get().dependencies.filter { it.group == "org.sosy-lab" })
    }
}

and replacing

implementation(files("build/dependencies/*.jar"))

with

implementation(fileTree("dir" to "build/dependencies", "include" to "*.jar"))

Maybe it is worth considering adding an example of a kotlin build script to the Example-Gradle-Project?

[baierd]

@breandan all versions up to and including 4.8.15 are now available (thanks to @kfriedberger).

@d-costa thank you for your input! I'll update the Gradle example project with your solutions!

[baierd]

@d-costa i've added a Kotlin example similar to the existing Gradle example. Could you take a look/try it out and report back? Its located parallel to the existing example in doc/Example-Gradle-Project-Kotlin

[d-costa]

@baierd works fine on my end! I took the liberty of fixing the tests (#268).
TLDR: the SudokuTest class needed to be in test/java instead of test/kotlin.

By the way, is there a reason why you changed DuplicatesStrategy.INCLUDE to DuplicatesStrategy.EXCLUDE?

[baierd]

Thank you very much for that!

@d-costa no there is no real reason. I tried different options and that stuck. Would it be more in line with Kotlin to use DuplicatesStrategy.INCLUDE?