I would like to write proof obligations in SMT format where some functions have some common generic properties (i.e. associativity and commutativity).
One simple solution would be to include the corresponding axioms in the proof obligations. I suppose that means that the reasoning on these properties will strongly depend on the quantifier instantiation algorithms. Other techniques, such as rewriting, could be more efficient, and I am wondering if Z3 implements such techniques to that effect. The existence of the values such as Z3_OP_PR_REFLEXIVITY and Z3_OP_PR_COMMUTATIVITY in the API is an sign that this might be the case.
My first question is then:
- Does Z3 has means to handle generic properties for user-defined symbols other than through quantifier instantiation of user-defined axioms?
If the answer is positive, then:
Which such generic properties would be?
Since, as far as I know, the SMT-LIB standard has not fixed such attributes for user-defined symbols (only theory symbols), what would be the SMT syntax for declaring that a user-defined symbol has a given property?