Jordan England
Reputation: 45
Does Z3py support Linear Temporal logic LTL?
Does Z3py support Linear Temporal logic LTL? If yes, can you provide an example of simple explain.
Upvotes: 0
Views: 766
Answers (1)
Nikolaj Bjorner
Reputation: 8359
Z3 does not support LTL or other temporal or modal logics. The input accepted by Z3 is first-order logic with theories, such as arithmetic.
Upvotes: 3
Related Questions
- Z3Py: Why are the following assumptions not satisfiable?
- multiple constraints in z3py if conditional
- Defining constraints in Z3 using Boolean operators
- z3py: How do I set the used logic in z3py?
- Can Z3 effectively solve constraints with a max operation?
- Representing temporal constraints in SMT-LIB
- z3py: How to check trace information when using z3 python api
- z3: Is it possible to adjust the branching heuristics in Z3?
- z3py: Can the switch of the orders of constraints affect the performance of the Z3 SMT solver?
- z3 Solver solution issues