Ročníkový projekt

Meno študenta: Vitalii Serhiienko
Mail: serhiienko3@uniba.sk

Meno školiteľa: Petra Hozzová
Mail: kubincova21@uniba.sk

Informácie o projekte

Názov projektu: Implementácia parsera pre formát SyGuS v solveri Vampire
Jazyk SyGuS slúži na špecifikáciu programov pre syntézu. Okrem špecifikácie vstupno-výstupnej relácie podporuje aj dodatočné obmedzenia pre hľadaný program.

Ciele:

Cieľom projektu je rozšíriť podporu vstupných formátov solvera Vampire o jazyk SyGuS tak, aby Vampire korektne parsoval vstupy v tomto formáte.
T.j. aby logickou formulou reprezentoval vstupno-výstupnú reláciu zadanú vo vstupe, a aby podporoval aj vybrané dodatočné obmedzenia zadané vo vstupe.