ASCII Digits
ASCII Digits accepts all binary strings that represent digits zero through 9 in ASCII. This automaton is intended to be an extreme case: it contains 12 states (instead of the usual three or four), as well as free text not associated with the automaton itself.
Annotated Image
Program Specification
;;;
;;; Preamble
;;;
(set-logic ALL)
;;;
;;; State Definitions
;;;
(define-fun is-state ((q Int)) Bool
(and (< (- 1) q) (< q 13)))
(define-fun is-accepting ((q Int)) Bool
(or (= q 5)))
(declare-fun IS () Int)
(assert (is-state IS))
(assert (not (= 0 IS)))
;;;
;;; Transition Definitions
;;;
(declare-fun T (Int String) Int)
;; All transitions must go to a valid state
(assert (forall ((q Int) (symb String))
(=> (is-state q) (is-state (T q symb)))))
;; It must not be possible to leave the zero state
(assert (forall ((symb String)) (= 0 (T 0 symb))))
;; Defined transitions
(assert (= 3 (T 1 "0")))
(assert (= 2 (T 4 "1")))
(assert (= 5 (T 2 "0")))
(assert (= 2 (T 4 "0")))
(assert (= 5 (T 2 "1")))
(assert (= 4 (T 7 "0")))
(assert (= 4 (T 7 "1")))
(assert (= 6 (T 3 "0")))
(assert (= 5 (T 8 "0")))
(assert (= 5 (T 8 "1")))
(assert (= 7 (T 9 "0")))
(assert (= 11 (T 6 "1")))
(assert (= 8 (T 12 "0")))
(assert (= 12 (T 10 "0")))
(assert (= 10 (T 9 "1")))
(assert (= 9 (T 11 "1")))
;; Negative transitions
(assert (forall ((symb String))
(=> (not (or (= symb "0")))
(= 0 (T 1 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0") (= symb "1")))
(= 0 (T 2 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0")))
(= 0 (T 3 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "1") (= symb "0")))
(= 0 (T 4 symb)))))
(assert (forall ((symb String))
(=> (not (or false))
(= 0 (T 5 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "1")))
(= 0 (T 6 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0") (= symb "1")))
(= 0 (T 7 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0") (= symb "1")))
(= 0 (T 8 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0") (= symb "1")))
(= 0 (T 9 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0")))
(= 0 (T 10 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "1")))
(= 0 (T 11 symb)))))
(assert (forall ((symb String))
(=> (not (or (= symb "0")))
(= 0 (T 12 symb)))))
;;;
;;; Examples
;;;
(define-fun-rec exec-dfa ((q Int) (input String)) Bool
(ite (= 0 (str.len input))
(is-accepting q)
(exec-dfa (T q (str.at input 0)) (str.substr input 1 (- (str.len input) 1)))))
;; Positive
(assert (exec-dfa IS "00110001"))
;; Negative
;;;
;;; Postamble
;;;
(check-sat)
(get-model)Synthesized Program
sat
(
(define-fun IS () Int
1)
(define-fun T ((x!0 Int) (x!1 String)) Int
(let ((a!1 (or (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(not (<= 7 x!0))
(= x!1 "0")
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(not (<= 6 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(not (<= 8 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(not (<= 9 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(not (<= 10 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(not (<= 12 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(not (<= 11 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (not (<= 1 x!0)) (= x!1 "1"))
(and (not (<= 1 x!0)) (not (= x!1 "0")) (not (= x!1 "1")))
(and (<= 1 x!0)
(not (<= 2 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(not (<= 4 x!0))
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(not (<= 6 x!0))
(= x!1 "0")
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(not (<= 6 x!0))
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(not (<= 12 x!0))
(= x!1 "0")
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(not (<= 7 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(not (<= 11 x!0))
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(<= 12 x!0)
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(<= 12 x!0)
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(not (<= 5 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(not (<= 4 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))
(and (not (<= 1 x!0)) (= x!1 "0") (not (= x!1 "1")))
(and (<= 1 x!0) (not (<= 2 x!0)) (= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(not (<= 3 x!0))
(not (= x!1 "0"))
(not (= x!1 "1")))))
(a!2 (or (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(not (<= 9 x!0))
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(not (<= 9 x!0))
(= x!1 "0")
(not (= x!1 "1")))))
(a!3 (or (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(not (<= 8 x!0))
(= x!1 "1"))
(and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(not (<= 8 x!0))
(= x!1 "0")
(not (= x!1 "1")))))
(a!4 (ite (and (<= 1 x!0)
(not (<= 2 x!0))
(= x!1 "0")
(not (= x!1 "1")))
3
21)))
(let ((a!5 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(not (<= 5 x!0))
(= x!1 "1"))
2
a!4)))
(let ((a!6 (ite (and (<= 1 x!0)
(<= 2 x!0)
(not (<= 3 x!0))
(= x!1 "0")
(not (= x!1 "1")))
5
a!5)))
(let ((a!7 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(not (<= 5 x!0))
(= x!1 "0")
(not (= x!1 "1")))
2
a!6)))
(let ((a!8 (ite (and (<= 1 x!0) (<= 2 x!0) (not (<= 3 x!0)) (= x!1 "1"))
5
a!7)))
(let ((a!9 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(not (<= 4 x!0))
(= x!1 "0")
(not (= x!1 "1")))
6
(ite a!3 4 a!8))))
(let ((a!10 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(not (<= 10 x!0))
(= x!1 "0")
(not (= x!1 "1")))
7
(ite a!2 5 a!9))))
(let ((a!11 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(not (<= 7 x!0))
(= x!1 "1"))
11
a!10)))
(let ((a!12 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(<= 12 x!0)
(= x!1 "0")
(not (= x!1 "1")))
8
a!11)))
(let ((a!13 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(not (<= 11 x!0))
(= x!1 "0")
(not (= x!1 "1")))
12
a!12)))
(let ((a!14 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(not (<= 10 x!0))
(= x!1 "1"))
10
a!13)))
(let ((a!15 (ite (and (<= 1 x!0)
(<= 2 x!0)
(<= 3 x!0)
(<= 4 x!0)
(<= 5 x!0)
(<= 6 x!0)
(<= 7 x!0)
(<= 8 x!0)
(<= 9 x!0)
(<= 10 x!0)
(<= 11 x!0)
(not (<= 12 x!0))
(= x!1 "1"))
9
a!14)))
(ite a!1 0 a!15))))))))))))))
)