I am playing with the CVC5 example at https://github.com/cvc5/cvc5/blob/main/examples/api/python/pythonic/linear_arith.py.
from cvc5.pythonic import *
slv = SolverFor('QF_LIRA')
x = Int('x')
y = Real('y')
slv += And(x >= 3 * y, x <= y, -2 < x)
slv.push()
print(slv.check(y-x <= 2/3))
slv.pop()
slv.push()
slv += y-x == 2/3
print(slv.check())
slv.pop()
It works as it is supposed to work.
However, whenever I try to print the content of the formula (i.e., print(slv)), it raises the following error: Cannot print: Kind.CONST_INTEGER
The same happens with literals that compound the formula: i.e., print(x >= 3); but not with variables: print(x) returns x.
I would like to have this printing capability, since Z3 allows it and I am trying my (originally-in-Z3-made) implementation with different SMT sovlers. Any idea?
Note that print(slv) does return info ([]), when it is empty. I tried using str(), but the error persists and indeed I guess print() uses str() before printing.
PS: I am using CVC5, should I use CVC4 or is CVC5 mature enough?
I think this is a bug. You should report it to the CVC5 folks at https://github.com/cvc5/cvc5/issues. (i.e., they should be able to handle this case just fine.)
In the interim, you can use the following workaround:
print(slv.sexpr())
which prints:
(and (let ((_let_1 (to_real x))) (and (>= _let_1 (* 3.0 y)) (<= _let_1 y) (> x (- 2)))))
which takes a bit of squinting to see that this is what you asserted, but it should do the trick.