module M = Map.Make(String) type term = V of string F of string * term list let find m = (* gaseste substitutia lui v in m *) let rec findm = function F (f, tl) -> F (f, List.map findm tl) V s -> try findm (M.find s m) with Not_found -> V s in findm let unify = (* returneaza unificatorul *) let rec unifm m t1 t2 = match (find m t1, find m t2) with (V v, t) (t, V v) -> subst v t m (F (f1, a1), F (f2, a2)) -> ... in unifm M.empty
2. Exersați scrierea unor formule în logica predicatelor, și folosiți demonstratorul Z3 dezvoltat la Microsoft pentru a determina dacă sunt realizabile, și a obține în acest caz un model.
Formulele sunt descrise în extensia unui format standard, SMT-LIB 2.0. Sintactic, scriem o serie de S-expresii, adică fie un atom (identificator), fie o listă de expresii între paranteze ( ). Formulele pot fi introduse interactiv direct în pagina indicată.
Pentru a scrie formule, vom folosi următoarele declarații:
(declare-sort U)declara un univers U de valori neinterpretate. Se poate lucra cu mai multe tipuri disjuncte de valori, dar, ca în logica propozițională clasică vom folosi unul singur.
(declare-fun numefct (lista-tipuri-argumente) tip-rezultat)de exemplu (declare-fun f (U U) U) definește o funcție de două argumente, cu valori în același univers. Tot aceeași sintaxă o folosim și pentru predicate, specificând tipul rezultat Bool : (declare-fun frate (U U) Bool) declară predicatul binar (relația) frate.
(declare-const nume tip)declară o instanța (constantă sau variabilă) cu numele si tipul dat (din nou, vom folosi doar universul U).
Fiecare operator se scrie tot sub forma de S-expresie: (not expresie), (=> expresie expresie), cu oricate argumente pentru and și or: (and expr1 expr2 ... exprN).
Cuantificatorul universal se poate scrie sub forma (forall ((x U)) expresie), ceea ce il si declară pe x pentru a putea fi folosit în expresie.
O formulă e specificată cu (assert formula) . Realizabilitatea formulei, se verifică cu comanda (check-sat), iar comanda (get-model) afișează un model, dacă există.