I would like to delve into the capability of SMT solvers to deal with trascendental and infinitesimal elements.
Thus, I just read the paper on computing in real closed fields https://www.cl.cam.ac.uk/~gp351/infinitesimals.pdf and I would like to practise some of its examples, such as (pg 13):
msqrt2, sqrt2 = MkRoots([-2, 0, 1])
print(sqrt2)
>> root(x^2 + -2, (0, +oo), {})
However, the link to the code they offer (http://z3.codeplex.com/wikipage?title=CADE24) is not active. Also, in Z3-Py, declarations like MkRoots do not exist.
Any idea? In case this paper is out-to-date, how are trascendentals and infinitesimals treated in Z3 nowadays?
The paper also states that MetiTarski "uses the nlsat nonlinear solver in Z3", which confuses me, since I thought MetiTarski (https://www.cl.cam.ac.uk/~lp15/papers/Arith/) was a separated automatic theorem prover). Indeed, they talk about MetiTarski in related work but do not mention Z3 (also, in MetiTarski's paper https://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf Z3 is neither mentioned).
Would you recommend any other SMT-paradigm interesting for this? Any tools to prove benchmars as the one above? Any other reading? I already know dReal, but the aforementioned paper says that "their methods are incomplete even for ∃RCF", so I would be interested in complete methods if possible.
Z3's RCF related functions are in the z3.z3rcf module path, so simply import that first:
from z3 import *
from z3.z3rcf import *
msqrt2, sqrt2 = MkRoots([-2, 0, 1])
print(sqrt2)
This prints:
root(x^2 + -2, (0, +oo), {})
MetiTarski does indeed use z3: It's download page even mentions this dependency explicitly: https://www.cl.cam.ac.uk/~lp15/papers/Arith/download.html
My understanding is that reasoning with transcendentals is beyond the capability of current SMT solvers. (dReal is all about approximations, not exact solutions.) If your goal is to work on transcendentals, then your best bet is to use theorem provers. I believe there has been significant amount of work in ACL2, Coq, and Isabelle; and google results in many hits. Expecting a lot of automation would be unreasonable though, so you should be prepared to writing proofs by hand and hopefully these systems are mature enough to help you along with custom tactics and as they branch to z3 for "simpler" subgoals.