alias
Reputation: 30428
associativity of => and chainability of =
Leonardo: According to http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf, section 3.7.1, => is right associative and = is chainable. However, it looks like the online version of Z3 does not support such uses. Is there an option I need to set to get this behavior?
Thanks..
Upvotes: 2
Views: 104
Answers (1)
Leonardo de Moura
Reputation: 21475
No, Z3 3.1 (and older versions) do not support these two 'features'. I will add them to Z3 3.2.
Upvotes: 1
Related Questions
- z3 cannot prove transitive identity
- Counterexample output of Z3
- Encoding self-dependent relations in Z3
- equivalence checking with Z3
- Z3 invariant check
- Does Z3 have a feature for facilitating the matching of subformulas in chains of associative / commutative operators?
- How to prove that the Z3 group satisfies the associative law using Z3-SMT-LIB
- Provide simple axioms to Z3
- set operations over Z3 expressions
- About the array theory in Z3