Theoretically, these 2 logics have some difference in Z3. But when I try to code, it seems that there is no difference between them. For example, the code below should have showed the difference:
from z3 import *
# create variables
x = Real('x')
y = Real('y')
# create solver
solver = SolverFor("QF_NRA")
# add constraints
solver.add(x * y == 1)
solver.add(x + y >= 3)
# check satisfiability
print(solver.check())
# print model
if solver.check() == sat:
m = solver.model()
print(m)
# create solver
solver = SolverFor("QF_LRA")
# add constraints
solver.add(x * y == 1)
solver.add(x + y >= 3)
# check satisfiability
print(solver.check())
# print model
if solver.check() == sat:
m = solver.model()
print(m)
However, these 2 logics finally have their solutions. I am confused and wonder whether they are different or not.
I have asked chatGPT but I am not satisfied. I want to know if there is difference. If so, please give me an example to show their obvious difference.
In z3, solvers are really portfolios. When you pick a solver for a logic, you don't really "limit" what it can do, but you're hinting what engine might work the best for your problem.
So, in your example both solvers can handle the problem, but they might have performance differences. i.e., one can go faster while the other is slower. Exactly when this happens relies on your formula and a lot of internal factors, and it is usually not possible to predict ahead of time. Furthermore, these characteristics change over time as z3 itself evolves.
Having said that, there's definitely a difference between NRA and LRA, i.e., when you allow for quantifiers. Here's an example:
from z3 import *
s = SolverFor("NRA")
x, y, z = Reals('x y z')
s.add(x < y)
s.add(y * y < x)
s.add(ForAll(z, z * x != y))
print(s.check())
This prints unsat. But if you change it to SolverFor("LRA"), it goes into a (seemingly) infinite loop.