blob: d3ca69e965792e3fb63f40d4d8ea45639d144275 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --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 AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
((Start Bool))
((Start Bool ((and Start Start) (not Start) a b c d))))
(declare-var a Bool)
(declare-var b Bool)
(declare-var c Bool)
(declare-var d Bool)
(constraint
(= (parity a b c d)
(and (AIG a b c d)
(not (and (and (not (and a b)) (not (and (not a) (not b))))
(and (not (and (not c) (not d))) (not (and c d))))))))
(check-synth)
; Solution:
;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
;(not
; (and
; (and (not (and (not a) b)) (not (and d (not c))))
; (and (not (and (not b) a)) (not (and (not d) c))))))
|
