blob: a836c9726acf2bac9d7ab4aa759eecd24c14d811 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
(set-logic BV)
(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
(xor (not (xor a b)) (not (xor c d))))
(synth-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
((Start Bool ((not StartAnd) Vars Constants))
(StartAnd Bool ((and Start Start)))
(Vars Bool (a b c d))
(Constants Bool (true false))))
(declare-var a Bool)
(declare-var b Bool)
(declare-var c Bool)
(declare-var d Bool)
(constraint
(= (parity a b c d)
(not (and (NAND a b c d)
(not
(and
(not (and (not (and d (not (and d a)))) (not (and a (not (and d a))))))
(not (and (not (and (not (and true c)) (not (and true b)))) (not (and b c))))))))))
(check-synth)
; Solution:
;(define-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
;(not
; (and
; (not (and (not (and (not (and c true)) b)) (not (and (not (and b c)) c))))
; (not (and (not (and a d)) (not (and (not (and a true)) (not (and true d)))))))))
|
