;; exemple 12.5 ;; types énumératifs (declare-datatypes () ((Titre shining player easyrider apocalypsenow) (Nom kubrick altman hopper nicholson robbins coppola) (Cinema champo odeon))) ;; la relation `Film' (define-fun Film ((x Titre) (y Nom) (z Nom)) Bool (ite (and (= x shining) (= y kubrick) (= z nicholson)) true (ite (and (= x player) (= y altman) (= z robbins)) true (ite (and (= x easyrider) (= y hopper) (= z nicholson)) true (ite (and (= x easyrider) (= y hopper) (= z hopper)) true (ite (and (= x apocalypsenow) (= y coppola) (= z hopper)) true false)))))) ;; la relation `Seance' (define-fun Seance ((x Cinema) (y Titre)) Bool (ite (and (= x champo) (= y shining)) true (ite (and (= x champo) (= y easyrider)) true (ite (and (= x champo) (= y player)) true (ite (and (= x odeon) (= y easyrider)) true false))))) (push) (declare-const x Titre) (echo ";; équation (12)") (assert (exists ((r Nom) (i Nom)) (Film x r i))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Cinema) (echo ";; équation (13)") (assert (exists ((t Titre) (i Nom)) (and (Film t hopper i) (Seance x t)))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Cinema) (echo ";; équation (14)") (assert (exists ((t Titre)) (and (Film t kubrick hopper) (Seance x t)))) (check-sat-using (then qe smt)) (pop) (push) (declare-const x Nom) (echo ";; équation (15)") (assert (exists ((t Titre)) (or (Film t kubrick x) (Film t coppola x)))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Nom) (echo ";; équation (16)") (assert (exists ((t Titre)) (Film t x x))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Nom) (declare-const y Cinema) (echo ";; équation (17)") (assert (exists ((t Titre) (i Nom)) (and (Film t x i) (Seance y t)))) (check-sat-using (then qe smt)) (get-value (x y)) (pop) (push) (declare-const x Nom) (echo ";; équation (18)") (assert (forall ((c Cinema)) (=> (exists ((t Titre)) (Seance c t)) (exists ((t Titre) (i Nom)) (and (Film t x i) (Seance c t)))))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Nom) (echo ";; équation (21)") (assert (and (exists ((t Titre)) (Film t hopper x)) (not (exists ((t Titre)) (Film t kubrick x))))) (check-sat-using (then qe smt)) (get-value (x)) (pop) (push) (declare-const x Nom) (echo ";; équation (22)") (assert (exists ((t Titre) (r Nom)) (and (Film t r x) (forall ((t2 Titre) (r2 Nom)) (=> (Film t2 r2 x) (= t t2)))))) (check-sat-using (then qe smt)) (get-value (x)) (exit)