ScalaZ3
ScalaZ3 copied to clipboard
epfl-lara
DSL in Scala for Constraint Solving with Z3 SMT Solver
The [Z3 docs describe support for floats](https://microsoft.github.io/z3guide/docs/theories/IEEE%20Floats/) that has been added over the past few years, and which may resolve outstanding issues - namely #75 - and would expand the...
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.(Z3Wrapper.java:49) at z3.scala.Z3Context.(Z3Context.scala:23) at...
Hope that this message reaches you well! Any thoughts/plans/roadmaps on Scala 3/dotty support?
I removed `getAbsFunDecl` (and the corresponding test suite) which crashes because the AST kind is `Z3UnknownAST`. Is that ok?
The purpose of [z3-turnkey](https://github.com/tudo-aqua/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...
The current version of `Z3Context` has no `mkEnumType` method, or `EnumSort` class. The [Java API has a corresponding method](https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#a4374b521f4ce4c9fae1bff928aaf4a8a), and so does the underlying `Native` class used by `ScalaZ3` (at...
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:...
``` $ scala -cp jars/scalaz3-unix-x64-2.13.jar Welcome to Scala 2.13.0 (Java HotSpot(TM) 64-Bit Server VM, Java 11.0.2). Type in expressions for evaluation. Or try :help. scala> new z3.Z3Wrapper WARNING: An illegal...
Perhaps built on top of either: - https://typelevel.org/cats-tagless/ + https://typelevel.org/cats-effect/ - https://zio.dev