Skip to content

Commit 484d564

Browse files
sim642sim642
committed
Lisa toyatp
1 parent c4e904e commit 484d564

19 files changed

+939
-0
lines changed

‎src/toyatp/README.md

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
# Automaatsed teoreemitõestajad (toyatp)
2+
3+
## Z3 paigaldamine
4+
Hakkame kasutama [Z3](https://github.com/Z3Prover/z3/wiki) teeki.
5+
Selle OCaml-i versiooni paigaldamiseks toimi järgnevalt:
6+
1. Navigeeri käsureal kloonitud projekti repositooriumi kausta.
7+
2. Käivita: `eval $(opam env)`
8+
3. Käivita: `opam update`
9+
4. Käivita: `opam install z3`
10+
* NB! Z3 kompileerimine võtab tükk aega.
11+
12+
Kui tekib mingi probleem, küsi Zulip-is!
13+
14+
15+
## Iseseisvaks läbitöötamiseks
16+
Tööta iseseisvalt läbi järgmised näited siin `src/toyatp/` kaustas:
17+
1. [`Sat`](./sat.ml)
18+
2. [`Smt`](./smt.ml)
19+
3. [`Magic`](./magic.ml)
20+
21+
Neis ise midagi lahendada pole vaja, vaid lihtsalt aru saada antud Z3 teeki kasutavast OCaml-i koodist, milles on rohkelt kommentaare.
22+
Vaata ka vastavaid teste `test/toyatp/` kaustas.
23+
24+
Kui midagi jääb endiselt segaseks, küsi Zulip-is!
25+
26+
27+
## Kodutööks
28+
Olles tuttav Z3 kasutamisega, lahenda kodutööna järgmised ülesanded siin `src/toyatp/` kaustas:
29+
* [`Bool`](./bool.ml)
30+
* [`Zebra`](./zebra.ml)
31+
32+
Lahendust kontrollivad testid on samuti `test/toyatp/` kasutas.
33+
**Esita oma lahendused Moodle'isse!**
34+
35+
Kui tekib raskusi, küsi Zulip-is!

‎src/toyatp/bool.ml

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
(** Bool keele kehtestatavuse kontrollija.
2+
Vt. Toylangs.Bool. *)
3+
open Z3
4+
open Toylangs.Bool
5+
6+
let ctx = mk_context [
7+
("model", "true");
8+
]
9+
let solver = Solver.mk_simple_solver ctx
10+
11+
12+
(** Abifunktsioon Bool keele muutujast Z3 muutuja nime tegemiseks. *)
13+
let string_of_char (c: char): string =
14+
String.make 1 c
15+
16+
(** Abifunktsioon Z3 muutuja nimest Bool keele muutuja tegemiseks. *)
17+
let char_of_string (s: string): char =
18+
assert (String.length s = 1);
19+
s.[0]
20+
21+
22+
(** Teisendab Bool keele avaldise Z3 avaldiseks.
23+
Vihje: string_of_char. *)
24+
let rec eval_expr (e: t): Expr.expr =
25+
failwith "TODO"
26+
27+
28+
(** Kehtestatavuse kontrolli tulemus. *)
29+
type verdict =
30+
| Satisfiable of env (** Kehtestatav. Andmetena kaasas keskkond, milles Bool keele avaldis on tõene. *)
31+
| Unsatisfiable (** Mitte-kehtestatav. *)
32+
| Unknown (** Z3 ei oska lahendada. *)
33+
34+
(** Abifunktsioon Z3 mudelist Bool keele keskkonna tegemiseks. *)
35+
let env_of_model (model: Model.model): env =
36+
List.fold_left (fun acc fd ->
37+
let x = char_of_string (Symbol.get_string (FuncDecl.get_name fd)) in
38+
let e = Option.get (Model.get_const_interp model fd) in
39+
let b = Sat.bool_of_expr e in
40+
if b then
41+
CharSet.add x acc (* kui tõene, siis lisatakse keskkonna hulka *)
42+
else
43+
acc (* kui väär, siis ei lisata keskkonna hulka *)
44+
) CharSet.empty (Model.get_const_decls model)
45+
46+
(** Kontrollib, kas Bool keele avaldis on kehtestatav.
47+
Vihje: eval_expr.
48+
Vihje: match-i Solver.check tulemust.
49+
Vihje: env_of_model. *)
50+
let check (e: t): verdict =
51+
failwith "TODO"

‎src/toyatp/dune

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
(library
2+
(name toyatp)
3+
(libraries z3 zarith toylangs))

‎src/toyatp/magic.ml

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
(** Maagilise ruudu ülesanded.
2+
3+
Failides/moodulites Sat ja Smt olid võrdlemisi lihtsad SAT ja SMT ülesanded.
4+
Siin on näide veidi keerulisemast ülesandest, mida saab SMT solveri abil lahendada.
5+
Praktikas võib olla mõistlikum spetsifiseerida ülesanne SMT-na ja lahendada see efektiivse SMT solveriga
6+
selle asemel, et ise üritada konkreetse ülesande jaoks välja mõelda efektiivne algoritm.
7+
8+
Olgu n naturaalarv, siis n×n maagiliseks ruuduks nimetatakse ruudukujulist tabelit,
9+
mille kõikide ridade, veergude ja diagonaalide summa on sama (nimetatakse maagiliseks konstandiks)
10+
ning elementideks on paarikaupa erinevad naturaalarvud 1, 2, 3, ..., n².
11+
12+
Vt. https://en.wikipedia.org/wiki/Magic_square. *)
13+
14+
open Z3
15+
16+
let ctx = mk_context [
17+
("model", "true");
18+
]
19+
let solver = Solver.mk_simple_solver ctx
20+
21+
(** Koostada 3×3 maagiline ruut. *)
22+
module Magic3Example =
23+
struct
24+
let ((x11, x12, x13), (x21, x22, x23), (x31, x32, x33)) =
25+
(* Loome Z3 muutujad ruudu kõigi lahtrite jaoks.
26+
Neist koosnev ruut näeks välja selline:
27+
x11 x12 x13
28+
x21 x22 x23
29+
x31 x32 x33 *)
30+
let x11 = Arithmetic.Integer.mk_const_s ctx "x11" in
31+
let x12 = Arithmetic.Integer.mk_const_s ctx "x12" in
32+
let x13 = Arithmetic.Integer.mk_const_s ctx "x13" in
33+
let x21 = Arithmetic.Integer.mk_const_s ctx "x21" in
34+
let x22 = Arithmetic.Integer.mk_const_s ctx "x22" in
35+
let x23 = Arithmetic.Integer.mk_const_s ctx "x23" in
36+
let x31 = Arithmetic.Integer.mk_const_s ctx "x31" in
37+
let x32 = Arithmetic.Integer.mk_const_s ctx "x32" in
38+
let x33 = Arithmetic.Integer.mk_const_s ctx "x33" in
39+
(* Loome Z3 muutuja maagilise konstandi jaoks.
40+
See abimuutuja võimaldab lihtsamini vajalikke võrdusi kirja panna. *)
41+
let magic = Arithmetic.Integer.mk_const_s ctx "magic" in
42+
43+
(* Loome maagilise konstandiga võrdused ridade, veergude ja diagonaalide jaoks. *)
44+
let c_rows = [
45+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x12; x13]) magic;
46+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x21; x22; x23]) magic;
47+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x31; x32; x33]) magic;
48+
]
49+
in
50+
let c_cols = [
51+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x21; x31]) magic;
52+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x12; x22; x32]) magic;
53+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x13; x23; x33]) magic;
54+
]
55+
in
56+
let c_diags = [
57+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x22; x33]) magic;
58+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x13; x22; x31]) magic;
59+
]
60+
in
61+
62+
(* List kõigist ruudu muutujatest. *)
63+
let xs = [x11; x12; x13; x21; x22; x23; x31; x32; x33] in
64+
(* Loome Z3 avaldise, mis väljendab, et kõik ruudu muutujad on paarikaupa erinevad. *)
65+
let c_distinct = Boolean.mk_distinct ctx xs in
66+
67+
(* Abidefinitsioonid konstantide 1 ja 9 jaoks. *)
68+
let one = Arithmetic.Integer.mk_numeral_i ctx 1 in
69+
let nine = Arithmetic.Integer.mk_numeral_i ctx 9 in
70+
(* Loome Z3 avaldised, mis väljendavad, et iga lahtri väärtus on intervallis [1, 9]. *)
71+
let c_ranges = List.map (fun x ->
72+
Boolean.mk_and ctx [
73+
Arithmetic.mk_ge ctx x one;
74+
Arithmetic.mk_le ctx x nine;
75+
]
76+
) xs
77+
in
78+
79+
(* Tingimused c_distinct ja c_ranges koos tähendavad, et lahtrite väärtused on mingi permutatsioon arvudest 1, 2, 3, ..., 9. *)
80+
81+
(* Käivitame Z3 solveri kõigi vajalike tingimustega. *)
82+
let cs = c_distinct :: c_ranges @ c_rows @ c_cols @ c_diags in
83+
let status = Solver.check solver cs in
84+
assert (status = SATISFIABLE); (* Siin näites peaks olema kehtestatav. *)
85+
86+
let model = Option.get (Solver.get_model solver) in
87+
(* Õngitseme mudelist välja meie lahtrite Z3 muutujate väärtused OCaml-i täisarvudena. *)
88+
let int_of_model x = Smt.int_of_expr (Option.get (Model.get_const_interp_e model x)) in
89+
let x11' = int_of_model x11 in
90+
let x12' = int_of_model x12 in
91+
let x13' = int_of_model x13 in
92+
let x21' = int_of_model x21 in
93+
let x22' = int_of_model x22 in
94+
let x23' = int_of_model x23 in
95+
let x31' = int_of_model x31 in
96+
let x32' = int_of_model x32 in
97+
let x33' = int_of_model x33 in
98+
(* Tagastame maagilise ruudu testi jaoks. *)
99+
((x11', x12', x13'), (x21', x22', x23'), (x31', x32', x33'))
100+
end
101+
102+
(** Tõestada, et 2×2 maagilist ruutu pole võimalik koostada. *)
103+
module Magic2Example =
104+
struct
105+
let status =
106+
(* Loome Z3 muutujad ruudu kõigi lahtrite jaoks.
107+
Neist koosnev ruut näeks välja selline:
108+
x11 x12
109+
x21 x22 *)
110+
let x11 = Arithmetic.Integer.mk_const_s ctx "x11" in
111+
let x12 = Arithmetic.Integer.mk_const_s ctx "x12" in
112+
let x21 = Arithmetic.Integer.mk_const_s ctx "x21" in
113+
let x22 = Arithmetic.Integer.mk_const_s ctx "x22" in
114+
(* Loome Z3 muutuja maagilise konstandi jaoks. *)
115+
let magic = Arithmetic.Integer.mk_const_s ctx "magic" in
116+
117+
(* Loome maagilise konstandiga võrdused ridade, veergude ja diagonaalide jaoks. *)
118+
let c_rows = [
119+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x12]) magic;
120+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x21; x22]) magic;
121+
]
122+
in
123+
let c_cols = [
124+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x21]) magic;
125+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x12; x22]) magic;
126+
]
127+
in
128+
let c_diags = [
129+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x11; x22]) magic;
130+
Boolean.mk_eq ctx (Arithmetic.mk_add ctx [x12; x21]) magic;
131+
]
132+
in
133+
134+
(* List kõigist ruudu muutujatest. *)
135+
let xs = [x11; x12; x21; x22] in
136+
(* Loome Z3 avaldise, mis väljendab, et kõik ruudu muutujad on paarikaupa erinevad. *)
137+
let c_distinct = Boolean.mk_distinct ctx xs in
138+
139+
(* Abidefinitsioonid konstantide 1 ja 4 jaoks. *)
140+
let one = Arithmetic.Integer.mk_numeral_i ctx 1 in
141+
let four = Arithmetic.Integer.mk_numeral_i ctx 4 in
142+
(* Loome Z3 avaldised, mis väljendavad, et iga lahtri väärtus on intervallis [1, 4]. *)
143+
let c_ranges = List.map (fun x ->
144+
Boolean.mk_and ctx [
145+
Arithmetic.mk_ge ctx x one;
146+
Arithmetic.mk_le ctx x four;
147+
]
148+
) xs
149+
in
150+
151+
(* Käivitame Z3 solveri kõigi vajalike tingimustega. *)
152+
let cs = c_distinct :: c_ranges @ c_rows @ c_cols @ c_diags in
153+
let status = Solver.check solver cs in
154+
(* Siin näites peaks tulemus olema UNSATISFIABLE,
155+
mis tähendab, et maagilist ruutu pole võimalik koostada. *)
156+
(* Tagastame solveri tulemuse testi jaoks.
157+
Kui tulemus on mitte-kehtestatav, siis Z3 mingit mudelit anda ei saa. *)
158+
status
159+
end

‎src/toyatp/sat.ml

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
(** Lausearvutuse kehtestatavuse ülesanded ehk SAT.
2+
3+
SAT ülesanded on arvutiteaduses olulisel kohal,
4+
sest nende lahendamine on NP-täielik.
5+
St, SAT ülesannete lahendamine on "raske" ja
6+
teised "rasked" arvutiteaduse ülesanded on taandatavad SAT ülesande lahendamisele.
7+
8+
Vt. https://en.wikipedia.org/wiki/Boolean_satisfiability_problem. *)
9+
10+
(** Vaatamata ülesannete keerukusele on praktikas olemas väga efektiivsed SAT lahendajad (solverid).
11+
Me kasutame siin populaarset Z3 solverit.
12+
Vt. https://github.com/Z3Prover/z3/wiki. *)
13+
14+
(** Z3 mooduli avamine võimaldab kasutada tema alammooduleid (Boolean, Solver, ...) ilma,
15+
et iga kord Z3 ette kirjutada. *)
16+
open Z3
17+
18+
(** Z3 solveri kasutamiseks on vaja luua kontekst. *)
19+
let ctx = mk_context [
20+
("model", "true"); (* Z3 seadistus mudelite loomiseks, vt SatExample. *)
21+
]
22+
let solver = Solver.mk_simple_solver ctx
23+
24+
(** Abifunktsioon Z3 avaldise OCaml-i tõeväärtuseks teisendamiseks.
25+
Vaja SatExample-is mudelist väärtuste kätte saamiseks. *)
26+
let bool_of_expr e =
27+
match Boolean.get_bool_value e with
28+
| L_TRUE -> true
29+
| L_FALSE -> false
30+
| L_UNDEF -> failwith "bool_of_expr: L_UNDEF"
31+
32+
(** Olgu meil lausearvutuse muutujad P, Q ja R.
33+
Olgu meil lausearvutuse valemid:
34+
1. P → Q,
35+
2. R ↔ ¬Q,
36+
3. ¬P ∨ R.
37+
38+
Kas need kolm valemit on samaaegselt kehtestatavad?
39+
St, kas leidub muutujate väärtustus, mille korral kõik kolm valemit on tõesed?
40+
Kui, siis milline muutujate väärtustus seda näitab? *)
41+
module SatExample =
42+
struct
43+
let (p, q, r) =
44+
(* Loome tõeväärtuse tüüpi Z3 muutujad. *)
45+
let p = Boolean.mk_const_s ctx "p" in
46+
let q = Boolean.mk_const_s ctx "q" in
47+
let r = Boolean.mk_const_s ctx "r" in
48+
49+
(* Loome Z3 avaldised nende kolme valemi jaoks. *)
50+
(* Boolean moodulis mk_ algusega funktsioonid, millega Z3 avaldispuu tippe saab luua.
51+
Kuna Z3 on C++ teek, siis tema avaldispuid ei saa mugavalt OCaml-i konstruktoritega luua.
52+
Samuti peab iga tipu loomisel andma kõigepealt ctx argumendi. *)
53+
let c1 = Boolean.mk_implies ctx p q in
54+
let c2 = Boolean.mk_iff ctx r (Boolean.mk_not ctx q) in
55+
(* Disjunktsiooni loomise funktsioon mk_or ei võta kahte argumenti,
56+
vaid listi disjunktidest, sest neid saab olla ka rohkem. *)
57+
let c3 = Boolean.mk_or ctx [(Boolean.mk_not ctx p); r] in
58+
59+
(* Käivitame Z3 solveri kolmele valemile vastavate avaldistega.
60+
Z3 lahendab SAT ülesande, mis ongi vastus meie küsimusele,
61+
kas need kolm valemit on samaaegselt kehtestatavad. *)
62+
let status = Solver.check solver [c1; c2; c3] in
63+
(* Solveri tulemus saab olla:
64+
1. SATISFIABLE (kehtestatav),
65+
2. UNSATISFIABLE (mitte-kehtestatav ehk samaselt väär) või
66+
3. UNKNOWN (kui millegipärast peaks ülesanne olema Z3 jaoks liiga keeruline). *)
67+
assert (status = SATISFIABLE); (* Siin näites peaks olema kehtestatav. *)
68+
69+
(* Kui valemid on kehtestatavad, siis Z3 annab meile vastava väärtustuse,
70+
mida Z3 kutsub mudeliks.
71+
Mudel antakse viimase Solver.check-i kohta, sest Z3 solveril on oma sisemine olek. *)
72+
let model = Option.get (Solver.get_model solver) in
73+
(* Õngitseme mudelist välja meie kolme Z3 muutuja väärtused OCaml-i tõeväärtustena. *)
74+
let bool_of_model x = bool_of_expr (Option.get (Model.get_const_interp_e model x)) in
75+
let p' = bool_of_model p in
76+
let q' = bool_of_model q in
77+
let r' = bool_of_model r in
78+
(* Tagastame testi jaoks kolm tõeväärtust. *)
79+
(p', q', r')
80+
end
81+
82+
(** Olgu meil lausearvutuse muutujad P ja Q.
83+
Kas kehtib samaväärsus
84+
P ∧ Q ≡ ¬(¬P ∨ ¬Q)
85+
?
86+
87+
Siin ei huvita meid, kas leiduvad muutujate väärtused, mille korral samaväärsuse pooled on samad,
88+
vaid hoopis, kas kõigi võimalike väärtustuste korral on samaväärsuse pooled samad.
89+
Kuigi Z3 lahendab kehtestatavuse esimest ülesannet,
90+
siis saab seda tegelikult kasutada ka teise tõestamisülesande lahendamiseks. *)
91+
module ProofExample =
92+
struct
93+
let status =
94+
(* Loome tõeväärtuse tüüpi Z3 muutujad. *)
95+
let p = Boolean.mk_const_s ctx "p" in
96+
let q = Boolean.mk_const_s ctx "q" in
97+
98+
(* Loome Z3 avaldised samaväärsuse vasaku ja parema poole jaoks. *)
99+
(* Konjunktsiooni loomise funktsioon mk_and on samuti listi argumendiga. *)
100+
let lhs = Boolean.mk_and ctx [p; q] in
101+
let rhs = Boolean.mk_not ctx (Boolean.mk_or ctx [Boolean.mk_not ctx p; Boolean.mk_not ctx q]) in
102+
103+
(* Loome Z3 avaldise samaväärsuse enda jaoks.
104+
Siin võib võrduse loomise funktsiooni mk_eq asemel kasutada ka mk_iff. *)
105+
let c = Boolean.mk_eq ctx lhs rhs in
106+
107+
(* Lausearvutuses kehtib fakt:
108+
valem on samaselt tõene parajasti siis, kui tema eitus ei ole kehtestatav.
109+
St, kui ei leidu väärtustust samaväärsuse ümberlükkamiseks, siis ta peab kehtima. *)
110+
(* Seega loome Z3 avaldise samaväärsuse eituse jaoks. *)
111+
let c' = Boolean.mk_not ctx c in
112+
(* Ja käivitame Z3 solveri, et kontrollida, kas eitus on kehtestatav. *)
113+
let status = Solver.check solver [c'] in
114+
(* Siin näites peaks tulemus olema UNSATISFIABLE,
115+
mis tähendab, et samaväärsus kehtib. *)
116+
(* Tagastame solveri tulemuse testi jaoks.
117+
Kui tulemus on mitte-kehtestatav, siis Z3 mingit mudelit anda ei saa. *)
118+
status
119+
end

0 commit comments

Comments
 (0)