blob: aea7e32f3c1c60be082ef9edaa35e884450cfd14 (
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
37
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi-prereg-inst --sygus-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) (StartAnd Bool) (Vars Bool) (Constants 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)))))))))
|
