TP-modelisation/TP2/enigme/enigme-Predicats-Thm01_1.smt2
2023-06-10 20:56:24 +02:00

30 lines
517 B
Plaintext
Executable file

;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
(declare-datatypes () ((tuple0 (Tuple0))))
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun da () Bool)
;; da_def
(assert (= da (and b (not c))))
(declare-fun db () Bool)
;; db_def
(assert (= db (=> a c)))
(declare-fun dc () Bool)
;; dc_def
(assert (= dc (and (not c) (or a b))))
(assert
;; Thm01
;; File "enigme.mlw", line 13, characters 7-12
(not (and da (and db dc))))
(check-sat)