Synthesis

Once the SMT-LIB2 specification is generated, synthesis is as simple as passing the specification to an SMT solver and requesting it to check satisfiability (“does a transition function and initial state exist such that the specification is true”) and produce a model (the satisfying function and initial state).

In particular, our implementation used Microsoft’s Z3 Theorem Prover as the backing SMT solver, as it was able to handle the recursive exec-dfa DFA simulation function used for evaluating input examples. Using CVC5 and encoding the specification as a syntax-guided synthesis (SyGuS) problem was considered; however, CVC5 was not able to handle the exec-dfa function.

Interpreting Models from Z3

One disadvantage to Z3 is that the output transition function, while technically correct, is often longer and more arcane than needed. This is a consequence of Z3 being a general-purpose SMT solver, not optimized for synthesis problems, so it outputs “a” solution, not necessarily the “best” solution. Regardless, this satisfies the goal of this project to produce a closed-form function for the transition relation. A post-processing simplification step can be applied to translate Z3’s output into a more reasonable form. For example, the output for Automaton A2 is:

(define-fun T ((x!0 Int) (x!1 String)) Int
    (let ((a!1 (or (and (<= 1 x!0) (not (<= 2 x!0)) (= x!1 "1"))
                   (and (<= 1 x!0) (not (<= 2 x!0)) (not (= x!1 "1")))
                   (and (not (<= 1 x!0)) (= x!1 "1"))
                   (and (not (<= 1 x!0)) (not (= x!1 "1")))))
          (a!2 (or (and (<= 1 x!0) (<= 2 x!0) (not (= x!1 "1")))
                   (and (<= 1 x!0) (<= 2 x!0) (= x!1 "1")))))
      (ite a!1 0 (ite a!2 1 3))))

Simplifying by applying logical equivalences (e.g., (and (<= 1 x!0) (not (<= 2 x!0))) <=> (= 1 x!0)), this can be reduced to:

(define-fun T ((x!0 Int) (x!1 String)) Int
    (let ((a!1 (or (and (= 1 x!0))
                   (and (< x!0 1))))
          (a!2 (or (and (<= 2 x!0)))))
      (ite a!1 0 (ite a!2 1 3))))

which further simplifies to:

(define-fun T ((x!0 Int) (x!1 String)) Int
    (let ((a!1 (<= x!0 1))
          (a!2 (>= x!0 2)))
      (ite a!1 0 (ite a!2 1 3))))

and finally, as a!1 is always true, to:

(define-fun T ((x!0 Int) (x!1 String)) Int
    ;; ite is "If-Then-Else"
	(ite (<= x!0 1) 0   ; States 0 and 1 always to go 0
                    1)) ; State 2 (the only other valid state) goes to state 1
                                     

which is the expected result, as A2 only accepts single character strings.

Unsatisfiable Automata

Two automata featured in our gallery, Automata A2 and A3, are actually unsatisfiable. This discovery demonstrated the importance of including positive and negative input examples: we had been working with A2 and A3 for several weeks and did not notice their unsatisfiability until our tooling reported it.

However, the drawn automata for A2 and A3 are still mostly correct, so we implemented the following scheme to handle unsatisfiable automata: if the SMT solver reports that the desired automaton is unsatisfiable, add an “extra” state to the specification. The synthesizer can append this extra state to the automaton to come up with an implementation that satisfies the given input examples.