notes from weekend thinking about java 21, Sojourn, babel, graal,

[Groostav]

some general points:

• i dont want everything running in process for OASIS.
• TornadoVM seems like a really good way of "use the GPU if you can, dont if you cant"
  -> also, in cloud world, we get one beefy GPU machine and run there
• GRPC seems like a good way to connect a constraint solver to OASIS, since it lets us represent this problem as an externality
• GRAAL's Truffle Framework provides the tools to get babel running more quickly

regarding constraint solvers, 2023 competition just closed: https://smt-comp.github.io/2023/results.html

• Z3 is also so 5 years ago; CVC5 seems like a good winner, https://cvc5.github.io/, also the beijing guys did a thing: https://z3-plus-plus.github.io/, and bitwuzla: https://bitwuzla.github.io/download.html

so the work that needs to be done:

• you need a converter to SMTlib2. I think the best approach here is a simple visitor on our existing babel nodes. This makes it hard to avoid exposing ANTLR. But so what?

  • the existing approach of using the Z3 API is both bug-prone and not portable. SMTLIB2 gives you something much more portable and much easier to reason about.

• once you have an SMTLIB2 converter, it needs to be wired to Z3 and/or CVC2 and/or bitwulza

• I want more performance, and I think I initially want to skip anything scary. Write an ANTLR visitor that encodes to a long[] instruction sequence. Dont think too hard about a formal IR, just make it go fast.

• from there, it should also be ~simple to write a Vector-API evaluator.

• more performance: use truffle, either with the truffle APi directly, or generate LLVM-IR and hand that over.

  • truffle:
    • pros: its designed to do exactly what im asking for, and the sample very precisely fits my use case. I can alsmot certainly hack something elegant together
    • cons: its using another specific API.
  • LLVM-IR:
    • pros: I feel like i have a good handle on this. It should be trivial to port whatever long[] emulation i have above to LLVM-IR, assuming that long[] is an SSA machine.
    • cons: this effectively couples us to our own babel-IR, which I dont want. Cleaner to just generate things directly off the AST.
    • con2: getting LLVM-IR running as an expression may be difficult. it will likely require a bunch of pointless window dressing.

• regarding torandoVM, if your on GRAAL it should be pretty straightforward. In this way you probably dont want to be in-process, instead using GRPC.

[Groostav]

Z3 online: https://jfmc.github.io/z3-play/

---

their arithmatic example:

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)

(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized complete solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

which crashes the solver!

also division example:

(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)

I've included these here to remind myself just how simple an SMTLIB converter should be

[Groostav]

Im looking for "Nonlinear real Arithmatic" (*NRA).

math with "mixed" integers and reals is called "mixed" or "IR" => NIRA or NRIA

"QF" is "quantifier free" and is fine as long as we can unroll sum & prod loops

looking at QFNRIA and QFNRA,

---

Im not sure if "uninterpreted functions" would be useful in our modelling. My gut says it would, but i havent worked throught he logic yet.

https://en.wikipedia.org/wiki/Uninterpreted_function