blob: e2bf9d1440eb2556e877ec9261b1989f508bb2f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
(set-logic ALL)
(declare-sort S 0)
(declare-var f Bool)
(declare-var u (-> S Bool))
(declare-var new_f Bool)
(declare-var new_u (-> S Bool))
(define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x)))))
(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not
(u x)) (not f))))))
(define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x)))
(constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u)))
(check-synth)
|
