Question about chained application in python API.

[jparsert]

If I wanted to add the assertion (assert (= (* a a) b)) via the python API I would write something like this:
s = z3.Solver() s.add(a * a == b)
Now, consider the following assertion: (assert (= (* a a a) b)) or (assert (= (* a) b)). How would I add them in the Python API?

[LeventErkok]

Probably easiest to simply use Product:

z3/src/api/python/z3/z3.py

Lines 8829 to 8852 in 5a9b0dd

	def Product(*args):
	"""Create the product of the Z3 expressions.
	>>> a, b, c = Ints('a b c')
	>>> Product(a, b, c)
	a*b*c
	>>> Product([a, b, c])
	a*b*c
	>>> A = IntVector('a', 5)
	>>> Product(A)
	a__0*a__1*a__2*a__3*a__4
	"""
	args = _get_args(args)
	if len(args) == 0:
	return 1
	ctx = _ctx_from_ast_arg_list(args)
	if ctx is None:
	return _reduce(lambda a, b: a * b, args, 1)
	args = _coerce_expr_list(args, ctx)
	if is_bv(args[0]):
	return _reduce(lambda a, b: a * b, args, 1)
	else:
	_args, sz = _to_ast_array(args)
	return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)

You can also use a python reduce expression to achieve the same, if you're willing to always put the arguments in a list:

$ python
Python 3.9.9 (main, Nov 21 2021, 03:23:44)
[Clang 13.0.0 (clang-1300.0.29.3)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> import functools
>>> x, y = Ints('x y')
>>> s = Solver()
>>> s.add(functools.reduce(lambda a, b: a*b, [x, y, x, x], 1) == x)
>>> print(s.sexpr())

This prints:

(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (* 1 x y x x) x))

And, tangentially, the stack-overflow forum https://stackoverflow.com/questions/tagged/z3py and https://stackoverflow.com/questions/tagged/z3 are more suitable for these sorts of questions.