ນີ້ແມ່ນຄໍາສັ່ງ mace4 ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍໆບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
mace4 - ຄົ້ນຫາ countermodel finite ຂອງຄໍາສັ່ງທໍາອິດຄໍາສັ່ງ
ສະຫຼຸບສັງລວມ
ມ້າມ4 [ທາງເລືອກໃນການ] ໄຟລ໌ປ້ອນຂໍ້ມູນ > output-file
ລາຍລະອຽດ
ຫນ້າຄູ່ມືນີ້ເອກະສານສັ້ນໆກ່ຽວກັບ ມ້າມ4 ຄໍາສັ່ງ.
ໂຄງການ ມ້າມ4 ຄົ້ນຫາສໍາລັບໂຄງສ້າງຈໍາກັດທີ່ພໍໃຈຄໍາສັ່ງທໍາອິດແລະສົມຜົນ
ຖະແຫຼງການ, ປະເພດດຽວກັນຂອງຄໍາຖະແຫຼງທີ່ prover9(1) ຍອມຮັບ. ຖ້າຄໍາຖະແຫຼງການແມ່ນ
ການປະຕິເສດການຄາດເດົາບາງຢ່າງ, ໂຄງສ້າງໃດໆທີ່ພົບເຫັນໂດຍ ມ້າມ4 ແມ່ນກົງກັນຂ້າມກັບຕົວຢ່າງ
ການໂຕ້ຖຽງ. ມ້າມ4 ສາມາດເປັນສ່ວນເສີມທີ່ມີຄຸນຄ່າ prover9(1), ຊອກຫາຕົວຢ່າງກົງກັນຂ້າມ
ກ່ອນ (ຫຼືໃນເວລາດຽວກັນກັບ) ການນໍາໃຊ້ prover9(1) ການຄົ້ນຫາສໍາລັບຫຼັກຖານ. ມັນຍັງສາມາດເປັນ
ໃຊ້ເພື່ອຊ່ວຍແກ້ບັນຫາການປ້ອນຂໍ້ຄວາມ ແລະສູດສຳລັບ prover9(1).
OPTIONS
ສະຫຼຸບຂອງທາງເລືອກແມ່ນລວມຢູ່ຂ້າງລຸ່ມນີ້. ຕົວເລືອກຕ່າງໆຈະແທນທີ່ການຕັ້ງຄ່າທຽບເທົ່າທີ່ລະບຸໄວ້ໃນ
ໄຟລ໌ປ້ອນຂໍ້ມູນ. ເພື່ອຕັ້ງ ຫຼືລຶບທຸງ, ທ່ານຕ້ອງໃຫ້ 1 ຫຼື 0 ເປັນຄ່າ.
-ຊ່ວຍ ສິ່ງນີ້ບອກ ມ້າມ4 ເພື່ອພິມບົດສະຫຼຸບຂອງຕົວເລືອກແຖວຄໍາສັ່ງເຫຼົ່ານີ້.
-n n ນີ້ເຮັດໃຫ້ຂະຫນາດໂດເມນເລີ່ມຕົ້ນສໍາລັບການຄົ້ນຫາ. ຄ່າເລີ່ມຕົ້ນແມ່ນ 2. ຖ້າທ່ານ
ຍັງໃຫ້ -N ທາງເລືອກ, ມ້າມ4 ຈະ iterate ຂະ ຫນາດ ໂດ ເມນ ຂຶ້ນ ໂດຍ ຜ່ານ ການ -N ມູນຄ່າ,
ການນໍາໃຊ້ການເພີ່ມຂຶ້ນໂດຍ -I ຄ່າ. ຖ້າບໍ່ດັ່ງນັ້ນ, ມ້າມ4 ຈະຄົ້ນຫາພຽງແຕ່ສໍາລັບ
-n ມູນຄ່າ.
-N n ນີ້ເຮັດໃຫ້ຂະຫນາດໂດເມນທີ່ສິ້ນສຸດສໍາລັບການຄົ້ນຫາ. ຄ່າເລີ່ມຕົ້ນແມ່ນ 10.
-i n ນີ້ເຮັດໃຫ້ການເພີ່ມຂະຫນາດໂດເມນສໍາລັບການຄົ້ນຫາ. ຄ່າເລີ່ມຕົ້ນແມ່ນ 1.
-q n ທຸງນີ້ overrides ພາຣາມິເຕີ iterate. ມັນບອກວ່າຈະພະຍາຍາມຂະຫນາດທີ່ເປັນຕົ້ນຕໍ
ຕົວເລກ, ຈາກ -n ຂຶ້ນຜ່ານ -N.
-m n ຢຸດການຄົ້ນຫາໃນເວລາທີ່ nໂຄງສ້າງ th ໄດ້ພົບເຫັນ. ຄ່າເລີ່ມຕົ້ນແມ່ນ 1.
-t n ຢຸດການຊອກຫາຫຼັງຈາກ n ວິນາທີ.
-s n ອະນຸຍາດໃຫ້ຫຼາຍທີ່ສຸດ n ວິນາທີສໍາລັບແຕ່ລະຂະຫນາດໂດເມນ. ພາລາມິເຕີສາມາດນໍາໃຊ້ໄດ້ (ຮ່ວມກັນ
ກັບ -t) ເພື່ອກໍານົດເວລາລວມ.
-b n ຢຸດການຄົ້ນຫາເມື່ອ (ປະມານ) n megabytes ຂອງຫນ່ວຍຄວາມຈໍາໄດ້ຖືກນໍາໃຊ້.
-V n ກົດລະບຽບແມ່ນຈໍາເປັນສໍາລັບການຈໍາແນກຕົວແປຈາກຄ່າຄົງທີ່ຢູ່ໃນຂໍ້ແລະ
ສູດທີ່ມີຕົວແປຟຣີ. ຖ້າທຸງນີ້ຈະແຈ້ງ, ຕົວແປເລີ່ມຕົ້ນດ້ວຍ (ຕ່ໍາກວ່າ
case) `u' ຜ່ານ `z'. ຖ້າທຸງນີ້ຖືກຕັ້ງ, ຕົວແປໃນປະໂຫຍກເລີ່ມຕົ້ນດ້ວຍ (ເທິງ
case) `A' ຜ່ານ `Z' ຫຼື `_'.
-P n ຖ້າທຸງນີ້ຖືກຕັ້ງ, ໂຄງສ້າງທັງຫມົດທີ່ພົບເຫັນຈະຖືກພິມອອກໃນຮູບແບບ 'ມາດຕະຖານ',
ຊຶ່ງຫມາຍຄວາມວ່າພວກເຂົາເຫມາະສົມເປັນວັດສະດຸປ້ອນກັບໂຄງການ LADR ອື່ນໆເຊັ່ນ: isofilter(1)
ແລະ ຮູບແບບການພົວພັນ(1).
-p n ຖ້າທຸງນີ້ຖືກຕັ້ງ, ແລະຖ້າ -P ແມ່ນຈະແຈ້ງ, ໂຄງສ້າງທັງຫມົດທີ່ພົບເຫັນແມ່ນພິມອອກ
ໃນຮູບແບບຕາຕະລາງ.
-R n ຖ້າທຸງນີ້ຖືກຕັ້ງ, ໂຄງສ້າງວົງຈະຖືກນໍາໃຊ້ກັບການຄົ້ນຫາ. ການດໍາເນີນງານ
{+,-,*} ຖືວ່າເປັນວົງແຫວນຂອງຈຳນວນເຕັມ (mod domain_size). ວິທີການນີ້ເຮັດໃຫ້
ຂໍ້ຈໍາກັດທີ່ເຄັ່ງຄັດໃນການຄົ້ນຫາ, ອະນຸຍາດໃຫ້ມີໂຄງສ້າງຂະຫນາດໃຫຍ່ຫຼາຍ
ສືບສວນ.
-v n ຖ້າທຸງນີ້ຖືກຕັ້ງ, ໄຟລ໌ຜົນຜະລິດໄດ້ຮັບຂໍ້ມູນກ່ຽວກັບການຄົ້ນຫາ,
ລວມທັງຕົວແບບບາງສ່ວນເບື້ອງຕົ້ນ (ສ່ວນຂອງຕົວແບບທີ່ສາມາດກໍານົດໄດ້
ກ່ອນທີ່ຈະ backtracking ເລີ່ມຕົ້ນ) ແລະເວລາແລະສະຖິຕິອື່ນໆສໍາລັບແຕ່ລະຂະຫນາດໂດເມນ.
(ມັນບໍ່ໄດ້ໃຫ້ຮ່ອງຮອຍຂອງ backtracking, ສະນັ້ນມັນບໍ່ໄດ້ບໍລິໂພກຫຼາຍໄຟລ໌
ຊ່ອງ.)
-T n ຖ້າທຸງຕິດຕາມຖືກຕັ້ງ, ຂໍ້ມູນລາຍລະອຽດກ່ຽວກັບການຄົ້ນຫາ, ລວມທັງການຕິດຕາມ
ຂອງການມອບຫມາຍແລະ backtracking ທັງຫມົດ, ຖືກພິມອອກເປັນຜົນຜະລິດມາດຕະຖານ. ທຸງນີ້
ເຮັດໃຫ້ຜົນຜະລິດຫຼາຍ, ດັ່ງນັ້ນມັນຄວນຈະຖືກນໍາໃຊ້ໃນການຄົ້ນຫາຂະຫນາດນ້ອຍເທົ່ານັ້ນ.
ນອກຈາກນີ້ຍັງມີທາງເລືອກຂັ້ນສູງຈໍານວນຫນຶ່ງ, ເຊິ່ງຖືກນໍາໃຊ້ສໍາລັບການທົດລອງ
ວິທີການຄົ້ນຫາ. ພວກເຂົາສາມາດຖືກລະເລີຍໂດຍຜູ້ໃຊ້ເກືອບທັງຫມົດ. ສໍາລັບຄໍາອະທິບາຍເຫຼົ່ານີ້
ທາງເລືອກ, ເບິ່ງຕົ້ນສະບັບ ມ້າມ4 ຄູ່ມື.
ໃຊ້ mac4 ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
