Open Groostav opened 1 year ago
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
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.
some general points:
regarding constraint solvers, 2023 competition just closed: https://smt-comp.github.io/2023/results.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?
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.
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.