How to use Ints.abs with Java Bindings?

[lorenzleutgeb]

Hi!

Obviously, Z3 supports some abs (absolute value) function, as exhibited here:

(declare-const x Int)
(assert (= x -1))

(declare-const y Int)
(assert (= y (abs x)))

(check-sat)

(echo "Next line is expected to be '((y 1))'.")
(get-value (y))

sat
Next line is expected to be '((y 1))'.
((y 1))

I suspect abs to be the one defined in SMT-LIB Ints.

After this successful test I'd like to re-create above example program using the Java API, but I fail to achieve this. I am looking for something like com.microsoft.z3.Context#mkFuncApp(String, Expr) or similar, but I can only find #mkFuncDecl(...), which not only results in a function call, but also creates a function declaration, which is not what I want.

Put differently, and a little more generally: How does one call, but not declare, a function via the Java API?

I found com.microsoft.z3.FuncDecl#apply, but how would I get an instance of FuncDecl that represents the declaration of abs?

Note that I did not add

(assert (= y 1))

on purpose, because then we wouldn't see abs work...

[NikolajBjorner]

The java API does not expose the "abs" function. It is really just treated as a shorthand for (if (>= x 0) x (- x)) so you can define an auxiliary function "abs" in Java that produces this term.

[lorenzleutgeb]

OK, that would have been my workaround. Thanks for clarifying.