It seems to me that implementing convert(...) in every ValHandler subclasses defeats the purpose of the Default type-class.

I'm willing to make a PR for this.

In my project, i want to translate expressions to Z3 and use the solver to check their validity / satisfiability.

I have a Z3AST init (and (= i 0) (= b false)) and a Z3AST pre (<= i 42). Now, as a test, I want to prove that init implies pre, so I call my Z3Context like this: z3Context.mkImplies(init, fpre)

However, this throws an unexpected exception:

Sort mismatch at argument #1 for function (declare-fun => (Bool Bool) Bool) supplied sort is Bool

Indeed, when debugging, I can see that getSort of both Z3ASTs is Bool, but for init, the value isBoolSort is false. I suspect this could point to the cause of the bug, but I'm stuck here. Can this be solved somehow?

Hi,

I've followed the setup steps for Linux with an a priori compilation of the latest Z3 branch for my architecture (64 bits). Some of the tests succeed, but:

lacramioara@ubuntu:/media/ubuntuPart2/Tools/ScalaZ3-master$ scala -cp scalaz3.jar Fibonacci.scala

gives me:

java.lang.UnsatisfiedLinkError: /tmp/SCALAZ3_155c903ca7e7b3e2124cba9a911813b/lib-bin/libscalaz3.so: /tmp/SCALAZ3_155c903ca7e7b3e2124cba9a911813b/lib-bin/libscalaz3.so: wrong ELF class: ELFCLASS32 (Possible cause: architecture word width mismatch)
at java.lang.ClassLoader$NativeLibrary.load(Native Method)
\vdots

Can you please help me with a piece of advice? I add that my jvm is on 64 bits.

Thanks,
Lacramioara

PS
I can successfully make use of the functionalities of ScalaZ3 from inside sbt, either with test or with run. So my guess is that the problem is with building the jar...

Hope that this message reaches you well! Any thoughts/plans/roadmaps on Scala 3/dotty support?

Hello guys,

I think there is a bug in the ScalaZ3 library on Scala 2.10. For example running the follwoing example in the interpreter will lead to an exception.

z3.scala.version

The exception which is thrown is related to Java Reflection (I think)

java.lang.NoClassDefFoundError: scala/reflect/ClassManifest
    at .(:8)
    at .()
    at .(:7)
    at .()
    at $print()
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:601)
    at scala.tools.nsc.interpreter.IMain$ReadEvalPrint.call(IMain.scala:731)
    at scala.tools.nsc.interpreter.IMain$Request.loadAndRun(IMain.scala:980)
    at scala.tools.nsc.interpreter.IMain.loadAndRunReq$1(IMain.scala:570)
    at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:601)
    at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:565)
    at scala.tools.nsc.interpreter.ILoop.reallyInterpret$1(ILoop.scala:745)
    at scala.tools.nsc.interpreter.ILoop.interpretStartingWith(ILoop.scala:790)
    at scala.tools.nsc.interpreter.ILoop.command(ILoop.scala:702)
    at scala.tools.nsc.interpreter.ILoop.processLine$1(ILoop.scala:566)
    at scala.tools.nsc.interpreter.ILoop.innerLoop$1(ILoop.scala:573)
    at scala.tools.nsc.interpreter.ILoop.loop(ILoop.scala:576)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply$mcZ$sp(ILoop.scala:867)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply(ILoop.scala:822)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply(ILoop.scala:822)
    at scala.tools.nsc.util.ScalaClassLoader$.savingContextLoader(ScalaClassLoader.scala:135)
    at scala.tools.nsc.interpreter.ILoop.process(ILoop.scala:822)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:83)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:96)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:105)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)
Caused by: java.lang.ClassNotFoundException: scala.reflect.ClassManifest
    at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
    at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
    at java.security.AccessController.doPrivileged(Native Method)
    at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
    ... 29 more

But when I run the same example with Scala 2.9 I will get this expected result:
res0: String = Z3 4.3 (build 1, rev. 0), ScalaZ3 4.0.a (in dev.)

How to reproduce the bug

• In Mac OSX (Mountain Lion) -and probably other OSes too-
• Install JDK 7, Scala 2.10 and Z3 4.3 (I couldn't find version 3.2 of the solver)
• Install Scala^Z3 as mentioned in this webpage (http://lara.epfl.ch/w/ScalaZ3)
• Open the terminal, and write this:

    LD_LIBRARY_PATH=${Z3_LIB_PATH} scala -classpath scalaz3.jar
  

  Where ${Z3_LIB_PATH} is the path to Z3 lib and scalaz3.jar is the path to the scala^z3 jar

• Run this into your REPL:

    z3.scala.version

And Boom! the exception will be thrown!

Thanks for taking care of this :)
Amanj

The z3JarFile is just a string, and if the Z3 project wasn't compiled yet, unamangedJars will contain the right path to com.microsoft.z3.jar but the file won't be there, and compilation will simply fail. It would work the next time though, if somehow Z3 was built at least once and the jar is there.
A potential fix might be to make the z3JarFile be a task that dependsOn z3.value
— @dragos

See #59 (comment)

The Z3 docs describe support for floats that has been added over the past few years, and which may resolve outstanding issues - namely #75 - and would expand the capabilities of the library.

This appears to be implemented in Z3's backend as a float system built upon BitVector arithmetic, presumably alongside tactics for linearization.

This appears to be unsupported in any of the current DSLs for SMTLIB present in the Scala ecosystem, as well as within the Haskell and Rust ecosystems (barring broken partial implementations), and may allow this library to gain a larger audience alongside the added utility.

The purpose of z3-turnkey is to provide a JAR artifact that:

1. ships its own native libraries,
2. can use them without administrative privileges, and
3. can be obtained using Maven.

If this works, this could allow us to distribute ScalaZ3 via Maven or Bintray, without requiring that users manually build it themselves or download one of our pre-built artifacts.

Is there a reason why ScalaZ3 needs to use hand-written JNI code instead of JNR-FFI? Removing the need to package custom native code would allow cross-platform ScalaZ3 JARs to be published on Maven; users would only have to ensure that an appropriate version of the libz3 was on their runtime includes path.

The current version of Z3Context has no mkEnumType method, or EnumSort class.
The Java API has a corresponding method,
and so does the underlying Native class used by ScalaZ3 (at least when I compiled it):

    protected static native long INTERNALmkEnumerationSort(long var0, long var2, int var4, long[] var5, long[] var6, long[] var7);

Is there another preferred way to create an enum type?

Hello there,

i was trying to use this api for z3 in scala. I'm using windows 7 x64. I've compiled the thing as you mention, except for the scalaz3.dll part.

when i run sbt test, all tests fail, and when i use the .jar in scala projects i keep getting the following error:

"java.lang.UnsatisfiedLinkError: C:\Users\camon\AppData\Local\Temp\SCALAZ3_d43487e7c44667ed98849de6247386\lib-bin\scalaz3.dll: Can't find dependent libraries"

I would appreciate your help,

Thanks in advance

Regards
Tiago

It's now inside github:
https://github.com/Z3Prover/z3

Hello,

I'm using MacOSX 10.6 and have a version of Z3 4.1.2 compiled from the source code available at: http://z3.codeplex.com/

I have cloned the ScalaZ3 git repo (oct. 10) and followed the instructions in the README file.
I had to place the lib and include files in a folder called "4.0" and not "4.1.2" in order to get through the following steps:

$ sbt update
$ sbt package

Then I get some errors when I run the tests:

$ DYLD_LIBRARY_PATH=z3/x64/4.0/lib/ sbt test
[info] == load-lib ==
[info]
[info] == copy-test-resources ==
[info] == copy-test-resources ==
[info]
[info] == test-start ==
[info] == test-start ==
[info]
[info] == IntArith ==
[info] IntArith:
[info] - Comfusy-like
[info] == IntArith ==
[info]
[info] == TheoryExtension ==
[info] TheoryExtension:
Problem 0, should be solved by simplifying only (no model).
Problem 1.
[info] - Theory extension
[info] == TheoryExtension ==
[info]
[info] == NQueens ==
[info] NQueens:
Total number of models: 92
[info] - NQueens
[info] == NQueens ==
[info]
[info] == Core ==
[info] Core:
[info] - Core
[info] == Core ==
[info]
[info] == ADTs ==
[info] ADTs:
[info] - ADTs
[info] == ADTs ==
[info]
[info] == ForComprehension ==
[info] ForComprehension:
[info] - ForComprehension
[info] == ForComprehension ==
[info]
[info] == Calendar ==
[info] Calendar:
[info] - Calendar
[info] == Calendar ==
[info]
[info] == QuickPA ==
[info] QuickPA:
Sat?
-> sat
Unsat?
-> unsat
WARNING: invalid function application, sort mismatch on argument at position 1
Invalid memory access of location 0x0 rip=0x11294a526

Segmentation fault

Hello,
I am trying to replicate some examples seen online and I cannot find checkAndGetAllModels or an equivalent way to iterate over all models produced by a solver.
Is this still supported in the current version?
Can you help me out with trying to iterate over all possible models of a set of constraints?

Thank you in advance!

Hello all,

I'm trying to build ScalaZ3 but I'm struggling with some errors in the sbt package command. I followed closely all the steps in the README file.

Z3

I'm currently using the unstable version of Z3. I successfully (?) compiled it using

CXX=clang++ CC=clang python scripts/mk_make.py
cd build ; make

Although I saw some warnings coming up, it ended without errors.

I then run sudo make install to finish the installation.

ScalaZ3

I downloaded ScalaZ3-2.9.x and created the path z3/4.3-osx-64b/include and z3/4.3-osx-64b/lib inside it. I then copied z3 include and lib files to them, as ordered.

After that, I ran sbt package and got the following output:

Note: I'm using sbt 0.12.4

bcandeias:ScalaZ3-2.9.x$ sbt package

[info] Loading project definition from /Users/bcandeias/apps/ScalaZ3-2.9.x/project
[info] Set current project to ScalaZ3 (in build file:/Users/bcandeias/apps/ScalaZ3-2.9.x/)
[info] Generating library checksum
[info] Compiling C sources ...
[info] $ gcc -o /Users/bcandeias/apps/ScalaZ3-2.9.x/lib-bin/libscalaz3.dylib -dynamiclib -I/Library/Java/JavaVirtualMachines/jdk1.7.0_40.jdk/Contents/Home/jre/../include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/bcandeias/apps/ScalaZ3-2.9.x/z3/4.3-osx-64b/include -L/Users/bcandeias/apps/ScalaZ3-2.9.x/z3/4.3-osx-64b/lib -g -lc -lz3 -fPIC -O2 -fopenmp /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/casts.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_thycallbacks.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_Z3Wrapper.c
[info] Wrote checksum cc18447f2ae7368241d1ba2ada01aa9 as part of /Users/bcandeias/apps/ScalaZ3-2.9.x/src/main/java/z3/LibraryChecksum.java.
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:24:86: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jsorts = (*env)->GetLongArrayElements(env, sorts, NULL); if(jsorts == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:25:92: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jsortsN = (*env)->GetLongArrayElements(env, sortNames, NULL); if(jsortsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:28:86: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jdecls = (*env)->GetLongArrayElements(env, decls, NULL); if(jdecls == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:29:92: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jdeclsN = (*env)->GetLongArrayElements(env, declNames, NULL); if(jdeclsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:40:15: warning: assigning to 'const jbyte *' (aka 'const signed char *') from 'const char *' converts between pointers to integer types with different sign [-Wpointer-sign]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]               ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:40:79: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]                                                                               ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:93:86: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jsorts = (*env)->GetLongArrayElements(env, sorts, NULL); if(jsorts == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:94:92: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jsortsN = (*env)->GetLongArrayElements(env, sortNames, NULL); if(jsortsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:97:86: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jdecls = (*env)->GetLongArrayElements(env, decls, NULL); if(jdecls == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:98:92: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jdeclsN = (*env)->GetLongArrayElements(env, declNames, NULL); if(jdeclsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:109:15: warning: assigning to 'const jbyte *' (aka 'const signed char *') from 'const char *' converts between pointers to integer types with different sign [-Wpointer-sign]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]               ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:109:79: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]                                                                               ^
[error] 2 warnings and 10 errors generated.
[info] Updating {file:/Users/bcandeias/apps/ScalaZ3-2.9.x/}ScalaZ3...
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_Z3Wrapper.c:1:10: fatal error: 'z3_Z3Wrapper.h' file not found
[error] #include "z3_Z3Wrapper.h"
[error]          ^
[error] 1 error generated.
[info] Resolving org.scalatest#scalatest_2.9.3;1.9.1 ...
[info] Done updating.
[info] Compiling 28 Scala sources and 14 Java sources to /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/classes...
[info] Preparing JNI headers...
[info] $ javah -classpath /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/classes -d /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c z3.Z3Wrapper
[error] Cannot find annotation method 'bytes()' in type 'scala.reflect.ScalaSignature': class file for scala.reflect.ScalaSignature not found
[error] Error: Class scala.ScalaObject could not be found.
[info] Packaging /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/scalaz3_2.9.3-2.0.jar ...
[info] Done packaging.
[success] Total time: 56 s, completed 3/Fev/2014 22:43:08

The file target/scala-2.9.3/scalaz3_2.9.3-2.0.jarwas created, tough.

Then running DYLD_LIBRARY_PATH=z3/4.3-osx-64b/lib sbt test I get

bcandeias:ScalaZ3-2.9.x$ DYLD_LIBRARY_PATH=z3/4.3-osx-64b/lib sbt test

[info] Loading project definition from /Users/bcandeias/apps/ScalaZ3-2.9.x/project
[info] Set current project to ScalaZ3 (in build file:/Users/bcandeias/apps/ScalaZ3-2.9.x/)
[info] Generating library checksum
[info] Wrote checksum cc18447f2ae7368241d1ba2ada01aa9 as part of /Users/bcandeias/apps/ScalaZ3-2.9.x/src/main/java/z3/LibraryChecksum.java.
[info] Quantifiers:
Exception in thread "Thread-1" java.io.EOFException
    at java.io.ObjectInputStream$BlockDataInputStream.peekByte(ObjectInputStream.java:2597)
    at java.io.ObjectInputStream.readObject0(ObjectInputStream.java:1316)
    at java.io.ObjectInputStream.readObject(ObjectInputStream.java:370)
    at sbt.React.react(ForkTests.scala:98)
    at sbt.ForkTests$$anonfun$apply$2$Acceptor$2$.run(ForkTests.scala:66)
    at java.lang.Thread.run(Thread.java:724)
[info] Passed: : Total 0, Failed 0, Errors 0, Passed 0, Skipped 0
[info] No tests to run for test:test
[success] Total time: 3 s, completed 3/Fev/2014 22:48:20

Does anyone know what's going on? Am I doing something wrong?

Thanks in advance!

Perhaps built on top of either:

• https://typelevel.org/cats-tagless/ + https://typelevel.org/cats-effect/
• https://zio.dev

I have issues working with long values because the provided 'mkInt' function accepts only ints, despite long values being supported by the Z3 java api.

Upstream commit Z3Prover/z3#efc893263a4fe107b3c62cea02aaa355b2f34ec8 has merged /z3_mk_abs.patch into mainline Z3.
This may allow the Build.scala implementation to be simplified, and may remove a major blocker on #78 - Replace custom build of Z3 with z3-turnkey.

Hey,
I want to pass a list of assumption literals in solver.checkAssumptions (in order to get the Unsat Core).
I have Z3 version 4.4.1 on my machine and I have tried with both scalaz3_2.10-3.0.jar and scalaz3-unix-64b-2.1.1.jar.

Supposedly I have 4 propositional literals - a,b,c,d and I want to pass all of them to solver.checkAssumptions. Surprisingly, this works :

solver.checkAssumptions(a,b,c,d)

but, assuming alist = List(a,b,c,d) :

solver.checkAssumptions(alist) throws the following error :

scala> solver.checkAssumptions(alist) 
<console>:22: error: type mismatch;
 found   : List[z3.scala.Z3AST] 
 required: z3.scala.Z3AST  
              solver.checkAssumptions(alist)

I checked the code for checkAssumptions in Z3Solver and it says :

def checkAssumptions(assumptions: Z3AST*) : Option[Boolean] = {

which implies I should be able to pass a list/Seq/array of assumptions right? Could anyone help?

Hello, Thank you for the awesome API.

I am completely new to z3 and I am trying to perform a constraint satisfying problem.
This is what I want to achieve:

a * 2.5 < 5
1 < a < 3.5

But I am not able to find any way to represent a which should be a floating point number.
Can someone help me here.

Also, are there any examples that I can refer to, for scalaZ3.
Any help would be much appreciated!

Hello,

I'm having a problem with the final step of the installation guide. Packaging seems to work correclty (at least I don't see any errors):

> package
[info] Generating library checksum
[info] Generating library checksum
[info] Wrote checksum 61f7962552d79e96a73fe47615a6b35d as part of /Users/georgii/workspace/scalogno/ScalaZ3/src/main/java/z3/LibraryChecksum.java.
[info] Wrote checksum 61f7962552d79e96a73fe47615a6b35d as part of /Users/georgii/workspace/scalogno/ScalaZ3/src/main/java/z3/LibraryChecksum.java.
[info] Compiling C sources ...
[info] $ install_name_tool -id @loader_path/libz3.dylib /Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib
[info] $ gcc -o /Users/georgii/workspace/scalogno/ScalaZ3/lib-bin/libscalaz3.dylib -dynamiclib -install_name /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib -I/Library/Java/JavaVirtualMachines/jdk1.7.0_51.jdk/Contents/Home/jre/../include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/include -L/Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib -g -lc -Wl,-rpath,/var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/ -lz3 -fPIC -O2 -fopenmp /Users/georgii/workspace/scalogno/ScalaZ3/src/c/casts.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/extra.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/z3_thycallbacks.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/z3_Z3Wrapper.c
[info] Updating {file:/Users/georgii/workspace/scalogno/ScalaZ3/}ScalaZ3...
[info] Resolving org.fusesource.jansi#jansi;1.4 ...
[info] Done updating.
[info] Compiling 29 Scala sources and 14 Java sources to /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/classes...
[info] Preparing JNI headers...
[info] $ javah -classpath /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/classes:/Users/georgii/.sbt/boot/scala-2.10.2/lib/scala-library.jar -d /Users/georgii/workspace/scalogno/ScalaZ3/src/c z3.Z3Wrapper
[info] Bundling files:
[info]  - /Users/georgii/workspace/scalogno/ScalaZ3/lib-bin/libscalaz3.dylib -> lib-bin/libscalaz3.dylib
[info]  - /Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib -> lib-bin/libz3.dylib
[info] Packaging /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.1.jar ...
[info] Done packaging.
[success] Total time: 19 s, completed Jun 13, 2014 12:54:05 PM

But then tests don't work at all:

> test
[info] Compiling 10 Scala sources to /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/test-classes...
[warn] /Users/georgii/workspace/scalogno/ScalaZ3/src/test/scala/z3/scala/ADTs.scala:111: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] /Users/georgii/workspace/scalogno/ScalaZ3/src/test/scala/z3/scala/IntArith.scala:43: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] two warnings found
[info] Sets:
[error] Uncaught exception when running z3.Sets: java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
[trace] Stack trace suppressed: run last test:test for the full output.
[info] ForComprehension:
[error] Uncaught exception when running z3.ForComprehension: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Calendar:
[error] Uncaught exception when running z3.Calendar: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] SatSolver:
[error] Uncaught exception when running z3.SatSolver: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] ADTs:
[error] Uncaught exception when running z3.ADTs: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Core:
[error] Uncaught exception when running z3.Core: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Quantifiers:
[error] Uncaught exception when running z3.Quantifiers: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] IntArith:
[error] Uncaught exception when running z3.IntArith: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] NQueens:
[error] Uncaught exception when running z3.NQueens: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Arrays:
[error] Uncaught exception when running z3.Arrays: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[error] Error: Total 10, Failed 0, Errors 10, Passed 0
[error] Error during tests:
[error]     z3.Core
[error]     z3.NQueens
[error]     z3.Quantifiers
[error]     z3.Arrays
[error]     z3.Sets
[error]     z3.ForComprehension
[error]     z3.ADTs
[error]     z3.Calendar
[error]     z3.SatSolver
[error]     z3.IntArith
[error] (test:test) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 7 s, completed Jun 13, 2014 12:54:47 PM

Exceptions are all same, here's one of them:

[error] Uncaught exception when running z3.Arrays: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
sbt.ForkMain$ForkError: Could not initialize class z3.Z3Wrapper
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at z3.scala.Z3Context.<init>(Z3Context.scala:31)
    at z3.Arrays$$anonfun$1.apply$mcV$sp(Arrays.scala:10)
    at z3.Arrays$$anonfun$1.apply(Arrays.scala:9)
    at z3.Arrays$$anonfun$1.apply(Arrays.scala:9)
    at org.scalatest.FunSuite$$anon$1.apply(FunSuite.scala:1265)
    at org.scalatest.Suite$class.withFixture(Suite.scala:1974)
    at z3.Arrays.withFixture(Arrays.scala:6)
    at org.scalatest.FunSuite$class.invokeWithFixture$1(FunSuite.scala:1262)
    at org.scalatest.FunSuite$$anonfun$runTest$1.apply(FunSuite.scala:1271)
    at org.scalatest.FunSuite$$anonfun$runTest$1.apply(FunSuite.scala:1271)
    at org.scalatest.SuperEngine.runTestImpl(Engine.scala:198)
    at org.scalatest.FunSuite$class.runTest(FunSuite.scala:1271)
    at z3.Arrays.runTest(Arrays.scala:6)
    at org.scalatest.FunSuite$$anonfun$runTests$1.apply(FunSuite.scala:1304)
    at org.scalatest.FunSuite$$anonfun$runTests$1.apply(FunSuite.scala:1304)
    at org.scalatest.SuperEngine$$anonfun$org$scalatest$SuperEngine$$runTestsInBranch$1.apply(Engine.scala:260)
    at org.scalatest.SuperEngine$$anonfun$org$scalatest$SuperEngine$$runTestsInBranch$1.apply(Engine.scala:249)
    at scala.collection.immutable.List.foreach(List.scala:318)
    at org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:249)
    at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:326)
    at org.scalatest.FunSuite$class.runTests(FunSuite.scala:1304)
    at z3.Arrays.runTests(Arrays.scala:6)
    at org.scalatest.Suite$class.run(Suite.scala:2303)
    at z3.Arrays.org$scalatest$FunSuite$$super$run(Arrays.scala:6)
    at org.scalatest.FunSuite$$anonfun$run$1.apply(FunSuite.scala:1310)
    at org.scalatest.FunSuite$$anonfun$run$1.apply(FunSuite.scala:1310)
    at org.scalatest.SuperEngine.runImpl(Engine.scala:362)
    at org.scalatest.FunSuite$class.run(FunSuite.scala:1310)
    at z3.Arrays.run(Arrays.scala:6)
    at org.scalatest.tools.ScalaTestFramework$ScalaTestRunner.run(ScalaTestFramework.scala:214)
    at sbt.RunnerWrapper$1.runRunner2(FrameworkWrapper.java:220)
    at sbt.RunnerWrapper$1.execute(FrameworkWrapper.java:233)
    at sbt.ForkMain$Run.runTest(ForkMain.java:239)
    at sbt.ForkMain$Run.runTestSafe(ForkMain.java:211)
    at sbt.ForkMain$Run.runTests(ForkMain.java:187)
    at sbt.ForkMain$Run.run(ForkMain.java:251)
    at sbt.ForkMain.main(ForkMain.java:97)

Any help really appreciated!

Add a method mkNumeral(String, Sort) in the Z3Context to be able to create arbitrary precision integers and real numbers based on their string representation (reals are written as rational fractions with arbitrary precision integers as numerators and denominators). Current state of the Z3Context only allows Int constants and and fractions of integers for Real constants.

Also, add support for get methods for numeral values of Real sort, especially those which return string representations.

Sir could u just send me a basic binder test case in play (scala) ASAP ...

Hi,

So I've downloaded the fixed version, compiled it using "sbt package", and obtained a compilation error regarding a missing ";", i fixed the compilation error, sent you a pull request.

After fixing the compilation error I got the same error as before regarding not being able to find the dependent libraries.

Once again I would appreciate your help

Best,
Tiago

First, congrats on the good work. The latest version of master is easily built with Cygwin and sbt. It also compiles under Visual Studio with minor changes to casts.h and z3_Z3Wrapper.c. However it doesn't run. I suspect the reason is that it is missing the import library that tells the O/S to load libz3.dll.

In the past I used a separate fork to link this in. With things working so well using sbt, I'd prefer to use the official fork now.

It appears the necessary libz3.lib that needs to be linked with the Windows version can be generated from Cygwin using the command:

dlltool -D libz3.dll -d z3.def -l libz3.lib

The required input file z3.def may be available from Microsoft RISE z3, but if not, the Artemis project (https://github.com/cs-au-dk/Artemis) has a usable version in the contrib/Z3/dll folder.

So, please solve this issue by:

1. locating and adding the file z3.def to your branch;
2. adding the call dlltool -D libz3.dll -d z3.def -l libz3.lib to sbt; and
3. including libz3.lib when linking scalaz3.dll under Cygwin

a) I have

1. sbt - 0.13.2
2. scala - 2.10.3
3. Z3 - 4.4.1
   ...on my machine. I am aware these are outdated versions but its for a specific project.

Now, I followed the steps mentioned here. But the JAR file it generated was - 'sbl_2.10-0.1-SNAPSHOT.jar'. It does not match with the pattern mentioned in the para.

b) Also, running simple "import z3.model._" in scala interpreter gives the following error :
<console>:7: error: not found: value z3

Can anyone help?

Hello,

as far as I can tell, the garbage collector can only collect AST nodes, when the corresponding Context is deleted. This seams to be true for other Z3Object subclasses as well, but I am mentioning AST nodes explicitly, because this is the greatest issue for me.

The reason is that Z3Object instances get added to a Z3RefCountQueue object once they are created and this queue is not cleared until the context, which created the objects, is deleted. Hence, there is always a reference to an object, which might not be needed at all.

This became an issue while I was using Scala^Z3 for symbolic execution. During such executions I build lots of formulas for unsatisfiable paths, which are not needed in subsequent steps.
Since this led to severe problems regarding memory consumption, I had to switch to the Java-API, which is included in the master branch of Z3 at Codeplex (https://z3.codeplex.com/SourceControl/latest).

This API circumvents this problem by not keeping references from the context to the objects it created and overwrites Object.finalize() to get the reference counting in the C-API work correctly. So, the garbage collector can collect all formulas for unsatisfiable paths and the reference count of objects gets decremented correctly by the finalizer.

I think this should also work for this API.

There is no support for Real, or at least the z3 api for real is not accessibile from the wrapper.

OS X version 10.7.4 - 64 bit
Scala 2.9.1
Z3 4.0 - 64 bit
sbt 0.7.7

The compiler was first complaining for missing __in and __out. I added them in one of the header files.

Then I receive the following error:

[info] == gcc-osx == [info] Compiling C library [info] gcc -o /Users/rax/git/ScalaZ3/lib-bin/libscalaz3.jnilib -dynamiclib -I/System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/rax/git/ScalaZ3/z3/x64/4.0/include -L/Users/rax/git/ScalaZ3/z3/x64/4.0/lib -g -lc -lz3 -fPIC -O2 -fopenmp /Users/rax/git/ScalaZ3/src/c/z3_thycallbacks.c /Users/rax/git/ScalaZ3/src/c/extra.c /Users/rax/git/ScalaZ3/src/c/casts.c /Users/rax/git/ScalaZ3/src/c/z3_Z3Wrapper.c [error] Undefined symbols for architecture x86_64: [error] "_Z3_trace_off", referenced from: [error] _Java_z3_Z3Wrapper_traceOff in ccUdOQlM.o [error] "_Z3_trace_to_stdout", referenced from: [error] _Java_z3_Z3Wrapper_traceToStdout in ccUdOQlM.o [error] "_Z3_trace_to_stderr", referenced from: [error] _Java_z3_Z3Wrapper_traceToStderr in ccUdOQlM.o [error] "_Z3_trace_to_file", referenced from: [error] _Java_z3_Z3Wrapper_traceToFile in ccUdOQlM.o [error] ld: symbol(s) not found for architecture x86_64 [error] collect2: ld returned 1 exit status [info] == gcc-osx ==

I'm on OS X, and the C compilation fails when GCC 5 is used. I tracked down the cause to the change of standard from GNU89 to GNU11, affecting the semantics of inline functions.

A quick "fix" is to pass the flag -std=gnu89 to GCC. I assume the alternative is to rename inline functions to "extern inline" ones, which should be equivalent to the old "inline" functions in C99 semantics that are used now by default (according to this document).

We should check whether something changed in the interface for theory plugins. Note that the BAPA plugin appears to work fine (Linux 32bit).

Using Java version openjdk version "1.8.0_242" on Debian, I get this error:

[info] ForComprehension:
null
java.lang.NullPointerException
        at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1847)
        at java.lang.Runtime.loadLibrary0(Runtime.java:871)
        at java.lang.System.loadLibrary(System.java:1124)
        at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:110)
        at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:49)
        at z3.scala.Z3Context.<init>(Z3Context.scala:23)
        at z3.scala.Z3Context.<init>(Z3Context.scala:45)
        at z3.scala.dsl.package$.findAll(package.scala:245)
        at z3.scala.ForComprehension.$anonfun$new$1(ForComprehension.scala:14)
        at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
        at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
        at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
        at org.scalatest.Transformer.apply(Transformer.scala:22)
        at org.scalatest.Transformer.apply(Transformer.scala:20)
        at org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:186)
        at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
        at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
        at org.scalatest.FunSuite.withFixture(FunSuite.scala:1560)

The tests work fine with openjdk 11.0.6 2020-01-14.

Thanks for the project.
I had been using it successfully on windows 32-bit. But recently I moved to x64.

On compiling the src on x64 I am getting errors.

Build Command:

D:\OpenSourceProjects\ScalaZ3\psuter-ScalaZ3-6c233b2> gcc -shared -o lib-bin\scalaz3.dll -D_JNI_IMPLEMENTATION_ -Wl,--kill-at -I "D:\ProgramFiles\Java\jdk1.6.0_31\include" -I "D:\ProgramFiles\Java\jdk1.6.0_31\include\win32" -I z3\x64\3.2\include src\c\*.h src\c\*.c z3\x64\3.2\bin\z3.lib 

Errors:

C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x2be): undefined reference to `Z3_parse_smtlib2_string'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x319): undefined reference to `Z3_parse_smtlib_string'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x6d1): undefined reference to `Z3_parse_smtlib2_file'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x71e): undefined reference to `Z3_parse_smtlib_file'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x7): undefined reference to `Z3_mk_config'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x45): undefined reference to `Z3_del_config'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0xdf): undefined reference to `Z3_set_param_value'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x11b): undefined reference to `Z3_mk_context'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x159): undefined reference to `Z3_del_context'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x189): undefined reference to `Z3_soft_check_cancel
'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x1f8): undefined reference to `Z3_trace_to_file'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x228): undefined reference to `Z3_trace_to_stderr'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x258): undefined reference to `Z3_trace_to_stdout'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x288): undefined reference to `Z3_trace_off'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x2a4): undefined reference to `Z3_toggle_warning_me
..............
...[Many such similar errors...omitted for clarity]
..............
collect2: ld returned 1 exit status

Few things about my setup

• I have already created JNI header files by running the following command

  javah -classpath D:\OpenSourceProjects\ScalaZ3\psuter-ScalaZ3-6c233b2\target\scala_2.9.1\classes -d D:\OpenSourceProjects\ScalaZ3\psuter-ScalaZ3-6c233b2\src\c z3.Z3Wrapper
  

• I have the copied files from Z3-3.2\include and Z3-3.2\x64 to z3\x64\3.2\include and z3\x64\3.2\bin directories respectively. (Note that the compilation succeeds if I copy the files from Z3-3.2\bin, but then the generated dll is for 32 bit platform)
• I have MinGW binaries in the PATH.

Is anything else needs to be done for compiling the src on windows x64
Please let me know if you need any more information about my installation setup to resolve the problem.

Hi,

I'm using the may release scalaz3-win-64b-2.1.1.jar

I get the following exception when trying to run a small example on Windows 8, x64:

Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\Users\AppData\Local\Temp\SCALAZ3_63b836a3598d68208352cc915673bed\lib-bin\libz3.dll: Can't find dependent libraries.

Here is the content of SCALAZ3_63b836a3598d68208352cc915673bed\lib-bin:

07/10/2014 11:49 AM 8,164,352 libz3.dll
07/10/2014 11:49 AM 173,056 Microsoft.Z3.dll
07/10/2014 11:49 AM 608,080 msvcp100.dll
07/10/2014 11:49 AM 829,264 msvcr100.dll
07/10/2014 11:49 AM 56,832 scalaz3.dll
07/10/2014 11:49 AM 57,168 vcomp100.dll
07/10/2014 11:49 AM 8,268,800 z3.exe
07/10/2014 11:49 AM 242,993 z3.pyc
07/10/2014 11:49 AM 6,828 z3consts.pyc
07/10/2014 11:49 AM 152,911 z3core.pyc
07/10/2014 11:49 AM 39,815 z3printer.pyc
07/10/2014 11:49 AM 256 z3test.pyc
07/10/2014 11:49 AM 11,040 z3types.pyc

I tried deleting this directory, but I get the same error.

Let me know what other information you need.

It's all in the title.

We should look into the representation of models of arrays, including functions to access default values etc.

When I try to use the scalaz3-osx-64b-2.1.1.jar binary on OSX, I run into UnsatisfiedLinkError exceptions:

scala -classpath /Users/joshrosen/Downloads/scalaz3-osx-64b-2.1.1.jar
Welcome to Scala version 2.11.2 (Java HotSpot(TM) 64-Bit Server VM, Java 1.7.0_65).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import z3.scala._
import z3.scala._

scala> import z3.scala.dsl._
import z3.scala.dsl._

scala>     val ctx = new Z3Context("MODEL" -> true)
java.lang.UnsatisfiedLinkError: /private/var/folders/0k/2qp2p2vs7bv033vljnb8nk1c0000gn/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib: dlopen(/private/var/folders/0k/2qp2p2vs7bv033vljnb8nk1c0000gn/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib, 1): Library not loaded: /usr/local/lib/gcc/x86_64-apple-darwin13.2.0/4.8.2/libgomp.1.dylib
  Referenced from: /private/var/folders/0k/2qp2p2vs7bv033vljnb8nk1c0000gn/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib
  Reason: image not found
  at java.lang.ClassLoader$NativeLibrary.load(Native Method)
  at java.lang.ClassLoader.loadLibrary1(ClassLoader.java:1965)
  at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1890)
  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1880)
  at java.lang.Runtime.loadLibrary0(Runtime.java:849)
  at java.lang.System.loadLibrary(System.java:1088)
  at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
  at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
  at z3.scala.Z3Config.<init>(Z3Config.scala:6)
  at z3.scala.Z3Context.<init>(Z3Context.scala:31)
  ... 33 elided

Maybe this is due to the GCC -> Clang change in 10.9?

There are 3 native libraries that need to be loaded by ScalaZ3, with the following dependencies:

libz3java --> libz3 <-- libscalaz3

These dependencies are part of the dynamically-loaded libraries, and are resolved by the OS. Even if the JVM has the right java.library.path, Mac OS will fail to resolve the dependency from libz3java to libz3. The other dependency, from libscalaz3 to libz3 is properly resolved because the dylib list the dependency as @loaderpath:

$ otool -L /tmp/../libscalaz3.dylib 
/tmp/../libscalaz3.dylib:
	/tmp/../libscalaz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.0.0)
!!!	@loader_path/libz3.dylib (compatibility version 0.0.0, current version 0.0.0)

Somebody knew something, because this is explicitly set in the Mac part of this build. But it's not done for libz3java.

The z3 java library, instead:

$ otool -L /tmp/../libz3java.dylib
/tmp/../libz3java.dylib:
	libz3java.dylib (compatibility version 0.0.0, current version 0.0.0)
	libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 400.9.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.0.0)

The workaround seems to be to install Z3 in a place that's part of DYLD_LIBRARY_PATH, though relying on this environment variable is discouraged for security reasons.