(Minimal) Boolean Formula Synthesis using SyGuS

bf.sygus

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2
(set-logic ALL)

(synth-fun f ((x Bool) (y Bool) (z Bool)) Bool
    ((Start Bool)) (
    (Start Bool (
        x y z
        (not Start)
        (and Start Start)
        (or Start Start)
    ))
))

(declare-var x Bool)
(declare-var y Bool)
(declare-var z Bool)

(define-fun toint ((b Bool)) Int (ite b 1 0))
(define-fun f2 ((x Int) (y Int) (z Int)) Int
    (toint (f (not (= x 0)) (not (= y 0)) (not (= z 0)))))

; 00011111,  x1 | (x2 & x3),  5
; Solution:  (or x (and y z))  ==  x | (y & z)
(constraint (= (f2 0 0 0)  0 ))
(constraint (= (f2 0 0 1)  0 ))
(constraint (= (f2 0 1 0)  0 ))
(constraint (= (f2 0 1 1)  1 ))
(constraint (= (f2 1 0 0)  1 ))
(constraint (= (f2 1 0 1)  1 ))
(constraint (= (f2 1 1 0)  1 ))
(constraint (= (f2 1 1 1)  1 ))

(check-synth)