STL to SMT-LIB compiler based on definitions from "A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation"
Tseitin transformation returns the (and (or ... )). When we nest, we get (and (or (and (or ...)))), effectively defeating the purpose of our transformation in the first place. How do we work around this?
roberthsheng
commented
1 year ago
Tseitin transformation returns the (and (or ... )). When we nest, we get (and (or (and (or ...)))), effectively defeating the purpose of our transformation in the first place. How do we work around this?