Ito ang command na mace4 na maaaring patakbuhin sa OnWorks na libreng hosting provider gamit ang isa sa aming maramihang libreng online na workstation gaya ng Ubuntu Online, Fedora Online, Windows online emulator o MAC OS online emulator
PROGRAMA:
NAME
mace4 - naghahanap ng mga may hangganang countermodel ng mga first-order na pahayag
SINOPSIS
tungkod4 [pagpipilian] input-file > output-file
DESCRIPTION
Ang manu-manong pahinang ito ay nagdodokumento ng maikling tungkod4 utos.
Ang programa tungkod4 naghahanap ng mga may hangganang istruktura na nagbibigay-kasiyahan sa first-order at equational
mga pahayag, ang parehong uri ng pahayag na iyon salawikain9(1) tinatanggap. Kung ang pahayag ay ang
pagtanggi sa ilang haka-haka, anumang istrukturang natagpuan ng tungkod4 ay mga kontrahalimbawa sa
haka-haka tungkod4 ay maaaring maging isang mahalagang pandagdag sa salawikain9(1), naghahanap ng mga kontra-halimbawa
bago (o kasabay ng) paggamit salawikain9(1) para maghanap ng patunay. Pwede rin naman
ginagamit upang tumulong sa pag-debug ng mga sugnay at formula ng input para sa salawikain9Na (1).
Opsyon
Ang isang buod ng mga opsyon ay kasama sa ibaba. In-override ng mga opsyon ang katumbas na setting na ibinigay sa
ang input file. Para magtakda o mag-clear ng flag, dapat kang magbigay ng 1 o 0 bilang value.
-tulong Sinasabi nito tungkod4 upang mag-print ng buod ng mga opsyon sa command-line na ito.
-n n Nagbibigay ito ng panimulang laki ng domain para sa paghahanap. Ang default na halaga ay 2. Kung ikaw
magbigay din ng -N pagpipilian, tungkod4 uulitin ang mga laki ng domain sa pamamagitan ng -N halaga,
gamit ang increment na ibinigay ng -I halaga. kung hindi, tungkod4 maghahanap lamang ng
-n halaga.
-N n Nagbibigay ito ng pangwakas na laki ng domain para sa paghahanap. Ang default ay 10.
-i n Nagbibigay ito ng pagtaas ng laki ng domain para sa paghahanap. Ang default ay 1.
-q n Ino-override ng flag na ito ang parameter iterate. Sinasabi nito na subukan ang mga sukat na prime
mga numero, mula sa -n hanggang sa -N.
-m n Itigil ang paghahanap kapag ang nang istraktura ay natagpuan. Ang default ay 1.
-t n Itigil ang paghahanap pagkatapos n segundo.
-s n Pahintulutan nang higit pa n segundo para sa bawat laki ng domain. Maaaring gamitin ang parameter (magkasama
sa -t) upang magbigay ng pangkalahatang limitasyon sa oras.
-b n Itigil ang paghahanap kung kailan (tungkol sa) n megabytes ng memorya ang ginamit.
-V n Ang isang panuntunan ay kinakailangan para sa pagkilala sa mga variable mula sa mga constant sa mga sugnay at
mga formula na may mga libreng variable. Kung malinaw ang flag na ito, magsisimula ang mga variable sa (lower
kaso) `u' hanggang `z'. Kung nakatakda ang flag na ito, ang mga variable sa mga clause ay magsisimula sa (upper
case) `A' hanggang `Z' o `_'.
-P n Kung ang flag na ito ay nakatakda, ang lahat ng mga istraktura na matatagpuan ay naka-print sa `standard' form,
na nangangahulugan na ang mga ito ay angkop bilang input sa iba pang mga programa ng LADR tulad ng isofilter(1)
at interpformatNa (1).
-p n Kung nakatakda ang flag na ito, at kung -P ay malinaw, ang lahat ng mga istraktura na matatagpuan ay naka-print
sa isang tabular na anyo.
-R n Kung nakatakda ang flag na ito, may ilalapat na istraktura ng singsing sa paghahanap. Ang mga operasyon
Ang {+,-,*} ay ipinapalagay na singsing ng mga integer (mod domain_size). Ang pamamaraang ito ay naglalagay
isang mahigpit na hadlang sa paghahanap, na nagbibigay-daan sa mas malalaking istruktura
sinisiyasat.
-v n Kung nakatakda ang flag na ito, ang output file ay makakatanggap ng impormasyon tungkol sa paghahanap,
kabilang ang paunang bahagyang modelo (ang bahagi ng modelo na maaaring matukoy
bago magsimula ang backtracking) at timing at iba pang istatistika para sa bawat laki ng domain.
(Hindi ito nagbibigay ng bakas ng backtracking, kaya hindi ito kumukonsumo ng maraming file
space.)
-T n Kung nakatakda ang trace flag, detalyadong impormasyon tungkol sa paghahanap, kabilang ang isang bakas
ng lahat ng mga takdang-aralin at backtracking, ay naka-print sa karaniwang output. Ang watawat na ito
nagdudulot ng maraming output, kaya dapat itong gamitin lamang sa maliliit na paghahanap.
Mayroon ding maraming mga advanced na opsyon, na ginagamit para sa pag-eeksperimento sa
mga paraan ng paghahanap. Maaari silang balewalain ng halos lahat ng mga gumagamit. Para sa mga paglalarawan ng mga ito
mga pagpipilian, tingnan ang orihinal tungkod4 manu-manong
Gumamit ng mace4 online gamit ang mga serbisyo ng onworks.net
