multiplication is variadic

[ffrohn]

This allows for creating multiplication-terms with more than two arguments with Z3. Currently, such terms can be created with CVC5, but not with Z3 (I didn't try other solvers).

[yoni206]

Thanks! Could you please include a test for this new feature?
Perhaps the best place would be to add a test here?
https://github.com/stanford-centaur/smt-switch/blob/master/tests/test-int.cpp

This would also clarify the status with the other solvers.

[yoni206]

Perhaps we could try this without catching? This will tell us what solvers have problems with that, and then we can fix it for those solvers?

Ideally we would like to be uniform w.r.t. back-end solvers, as much as possible.

[ffrohn]

I'm not sure what you mean. If an exception is thrown, then the FAIL in the catch-block is executed, and the solver's error message is shown:

FAIL() << "creating mult-term failed: " << e.what();

For example, if I execute the test in the master branch on my machine, then I get:

$SMT_SWITCH/tests/test-int.cpp:58: Failure
Failed
creating mult-term failed: Can't apply * to 3 terms.
[  FAILED  ] ParameterizedSolverIntTests/IntTests.Mult/4, where GetParam() = Z3(logging=0) (1 ms)

Since all CI checks pass with my fix, I guess that Z3 is the only solver that can't handle variadic multiplication.

I guess it would also work as desired without catching (I'm not very familiar with gtest and how it handles exceptions), but then we cannot provide a custom error message ("creating mult-term failed: "...).

[yoni206]

Sorry, you are right, I missed the fact that the message goes to FAIL(). So if z3 is the only solver for which this does not work, could you perhaps try to make it work for that too? It should support it so it is unclear why this does not work:

smt-switch/z3/src/z3_solver.cpp

Line 99 in f4bd379

{ Mult, Z3_mk_mul },

[ffrohn]

With my fix (a757315), it does work with Z3 (which is the reason why the CI checks passed after my last commit 61b4855). The problem was that z3_solver only tries to build a variadic term if the corresponding operation is marked as variadic in ops.h, which was not the case for Mult.

[yoni206]

Thanks for this change and for the discussion!