About available first-order logic semantics.

[zqzqz]

Does Sally support exists and forall operators? I tried a simple example but it throws parser error at the location of "exists".

(define-state-type my_state
  ((x Real) (y Real))
)

(define-states initial_states my_state
  (and (= x 1) (= y 2))
)

(define-transition transition my_state
  (and (= next.x (+ state.x 1)) (= next.y (+ state.y 2)))
)

(define-transition-system T my_state
   ;; Initial states
   initial_states
   ;; Transition
   transition
)

(query T (
        exists
        ((z Real))
        ((and (> y z) (> z x)))
))

[dddejan]

Sally does not support quantifiers at the moment.

Most SMT solvers we work with do not support quantifiers (Yices2, MathSAT, OpenSMT) and we try to stay in decidable quantifier-free fragments. If there was an appealing use-case we could add support through Z3 but this could only be used for BMC and k-induction.