Make kotlin extension API

[Groostav]

As a JVM developer willing to use non-java JVM languages (eg kotlin, scala, clojure, ...) I want to use Z3 with my application in a more fluent and less error prone fashion than mangled method calls, so that I can more quickly build my application and experience less complex-expression-fatigue related bugs.

The java API is not perfect. It exposes a large bulk of the functionality of Z3, but it does so in a way which conforms to many java idioms, which are likely not idioms familiar to Z3 users, and they are very verbose.

My suggestion:

Using only the existing types we can write a set of kotlin extension functions that would make writing static expressions in Z3 much easier.

The four below uses could be identical:

smt-lib:

(declare-const x Real)
(declare-const y Real)

(assert (> (+ x y) 5))
(assert (> x 1))
(assert (> y 1))

(check-sat)
(get-model)

python:

x = Real('x')
y = Real('y')
s = Solver()

s.add(x + y > 5, x > 1, y > 1)

print(s.check())
print(s.model())

java:

Context ctx = new Context()

val x = ctx.mkRealConst("x")
val y = ctx.mkRealConst("y")
Solver s = ctx.mkSolver()

s.add(ctx.mkGt(ctx.mkAdd(x, y), ctx.mkReal("5")))
s.add(ctx.mkGt(x, ctx.mkInt(1))
s.add(ctx.mkGt(y, ctx.mkInt(1))

System.out.println(s.check())
System.out.println(s.getModel())

kotlin:

with(Context()){
  x = Real("x")
  y = Real("y")
  s = Solver()

  s.add(x + y gt 5, x gt 1, y gt 1)

  println(s.check())
  println(s.model())
}

Some notes about the kotlin example:

• operator fun A.compareTo(a: A) defines >, >=, <, and <=, and is overloadable, but its return type must be int in accordance with java's Comparable interface. This means we could get even closer adherence to the python like api, but it would involve picking-up a mutability (and thus thread-safety) fight.

---

as an aside: Every time I log bugs on libs (such as #1327) I feel guilty because I'm asking a group which owes me nothing to do something, albeit something that will likely benefit everybody. As I learn more about Z3 maybe ill eventually be able to pickup issues like that.

But I'm pretty knowledgeable about kotlin, so maybe I can offer you guys this feature instead. I could do it as a pull request against this repository, or as a separate repository, if you guys think it would be valuable.

[NikolajBjorner]

Contributions are very welcome.

The biggest consideration for contributors is whether the features are stable or get maintained and responsiveness with respect to bug fixes.

Functionality that bit-rots gets cut. There is limited bandwidth to deal with stale features. API features are occasionally added. It helps when there is a systematic and straight-forward way to expose these features for new interfaces.

There are some APIs to Z3 that are not part of this repository. E.g., there is/were some Haskell bindings. There is also some interest in usable JavaScript bindings (see #1298).

Regarding the Java idioms, they are similar to the .Net conventions. The example you list above resembles the Python bindings API, which is considerably more user friendly for scripting. Some of these features can be carried over to the Java bindings based on popular demand, but overall there are no plans to change the overall way the bindings are exposed. An application that needs something efficient should bypass the Java/.Net bindings that creates objects for every expression. Unfortunately, it is too error prone (every expression becomes a ulong or IntPtr) to use such bindings so it is not something that is worth exposing for general consumption.

[delcypher]

@Groostav

Contributions are welcome. To avoid bit rot you would need to also contribute some examples using the Kotlin bindings and also have them tested in CI.

I can give you advise on doing this as I've already added support for the python, Java, C# build systems to the new CMake based build system and these are tested in TravisCI.

I have no experience with Kotlin itself though so I won't be much help there.

[Groostav]

Hey guys, I have not given up on this issue I was just taking some time to ponder my response.

[Groostav]

Alright so I've done a little bit of groundwork and it looks pretty good:

given the python for a mod function:

mod = z3.Function('mod', z3.RealSort(),z3.RealSort(), z3.RealSort())
quot = z3.Function('quot', z3.RealSort(),z3.RealSort(), z3.IntSort())

s = z3.Solver()

X, k = z3.Reals('X k')

s.add(Implies(k != 0, 0 <= mod(X,k)),
      Implies(k > 0, mod(X,k) < k),
      Implies(k < 0, mod(X,k) < -k),
      Implies(k != 0, k*quot(X,k) + mod(X,k) == X))

we get the equivalent kotlin:

val z3 = Context()
z3 {
  val mod = BinaryFunction("mod", Real, Real, Real)
  val quot = BinaryFunction("quot", Real, Real, Real)

  val s = Solver()

  val (X, k) = Reals("X", "k")

  s += listOf(
          (0.0 neq k) implies (0.0 lt mod(X, k)),
          (k gt 0.0) implies (mod(X, k) lt k),
          (k lt 0.0) implies (mod(X, k) lt -k),
          k * quot(X, k) + mod(X, k) eq X
  )
}

a maybe 60%-of-what-I-want-to-implement version can be found here: https://github.com/Groostav/sojourn-CVG/blob/master/src/main/kotlin/com/empowerops/sojourn/Z3Extensions.kt

You'll notice its just a whole bunch of extension functions at this point, and thats how I play to keep it.

Note that I could overload equals and compareTo operators to allow you to write things like mod(X, k) >= k) but these operators have some invariants in their type signatures, meaning I would have to play some games with state on a context-object-wrapper, which, while very tempting, seemed like a bridge too far.

Regarding testing:

Contributions are welcome. To avoid bit rot you would need to also contribute some examples using the Kotlin bindings and also have them tested in CI.

Happy to do this. Strangely enough I'm pretty familiar with every other major CI service except travis, though I suspect its many of the same things, and JetBrains has put a great deal of effort into making kotlinc wrap javac elegantly.

[NikolajBjorner]

no traction