Fixed the dependent library problem on W7 x64

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver

Apache License 2.0

122 stars 34 forks source link

Fixed the dependent library problem on W7 x64 #36

Closed tvcsantos closed 10 years ago

tvcsantos commented 10 years ago

So I pulled the last version and found a compilation error, there was a missing ";", no big deal. Fixed that, tried again and got the same error from the missing dependent library. Investigated a little further and found out that scalaz3.dll also depends on another dll, "msvcr120d.dll", a debug dll from visual studio 2013.

Patched "Build.scala" file to add the extra dll in "sbt packageBin" to the jar file.

Patched "Z3Wrapper.java" to load the extra dll

Thanks

Best, Tiago

colder commented 10 years ago

Thanks for the PR! I will fix the ; immediately. Regarding the rest:

@MikaelMayer Was msvcr120d required in your Windows build as well? And/or do you know how to make it optional? It would be best if we had to package as little as possible.

tvcsantos commented 10 years ago

Hey @colder, probably (but I'm not sure on this), who has Visual Studio 2013 installed will not need the dll, because it will exist in system32 folder.

Also I think there is another option, that will avoid packaging the msvcr120d.dll. Since msvcr120d.dll, is a debug version of the msvcr120.dll, if scalaz3.dll is compiled in release mode, instead of debug mode, scalaz3 will depend on the msvcr120 instead, and this one already exists in system32 folder

Another thing, probably this is not the place, but I would like your help if possible. Is it possible with the API, to create parametric datatypes like the following:

(declare-datatypes (T) ((Ref (mk-ref (inner T)))))

I've searched your documentation, the paper on the tool, the C API, the python API, the source of the "leon" project, but I can't seem to find an example of a parametric datatype.

Thanks once again

colder commented 10 years ago

@camon You can create generic datatypes in the sense that T will be an uninterpreted kind, but different instantiations of this datatype will not be compatible and have to be declared spearately.

What we do in Leon is we declare datatypes on demand, which allows us to do, for instance:

if List[T] is used, then we declare the List_T datatype where T is an uninterpreted kind.
if List[Int] is used, we specialize and declare List_Int where T becomes the Int kind.

This declaration is done here: https://github.com/epfl-lara/leon/blob/master/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala#L251

(a ClassType is an ADT + valuation for type parameters)

Hope this helps,