- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 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
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
(set-logic UF)
; https://smtlib.cs.uiowa.edu/logics.shtml
; UF for the extension allowing free sort and function symbols
(set-option :produce-proofs true)
(declare-sort M_list)
(declare-fun m_node (M_list M_list) M_list)
; один хер какой порядок, можно переписать (a, b) на (b, a)
(assert
(forall ( (a M_list) (b M_list) )
(=
(m_node a b)
(m_node b a)
)
)
)
; если есть (a (b c)) то можно переписать на (с (a b))
(assert
(forall ( (a M_list) (b M_list) (c M_list) )
(=
(m_node a (m_node b c) )
(m_node c (m_node a b) )
)
)
)
; Можно создавать или удалять повторы, (a a) <=> a
(assert
(forall ( (a M_list))
(=
(m_node a a)
a
)
)
)
; Чтоб узнать, выводима ли такая-то хернь
(declare-fun m_node_select (M_list M_list) Bool)
(assert
(forall ( (a M_list) (b M_list) )
(m_node_select
a (m_node a b)
)
)
)
; проверяем, можно ли сконструировать (a a) из (c ((b d) a))
(assert
(not (forall ( (a M_list) (b M_list) (c M_list) (d M_list) )
(m_node_select
(m_node a a)
(m_node c (m_node (m_node b d) a) )
)
))
)
(check-sat)
(get-proof)
Follow us!