Jest to polecenie lpsbinary, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
lpsbinary - zamień skończone zmienne sortowania na wektory zmiennych boolowskich w LPS
STRESZCZENIE
lpsbinarny [OPCJA]... [W PLIKU [PLIK WYJŚCIOWY]]
OPIS
Zamień zmienne sortowania skończonego na wektory zmiennych boolowskich w LPS w INFILE i
zapisz wynik do OUTFILE. Jeśli INFILE nie jest obecny, używane jest standardowe wejście. Jeśli OUTFILE nie jest
obecne, używane jest standardowe wyjście
OPCJE
OPCJA może być jednym z następujących:
-QNUM, --qlimit=NUM
ograniczyć wyliczanie kwantyfikatorów do NUM zmiennych. (Domyślnie NUM=1000, NUM=0 dla
Nieograniczony).
-rIMIĘ, --przepisujący=IMIĘ
użyj strategii przepisywania NAZWA: 'jitty' jitty przepisywanie (domyślnie) 'jittyc' skompilowane
jitty przepisywanie 'jittyp' jitty przepisywanie z prover
--czasy[=FILE]
dołącz pomiary czasu do pliku FILE. Pomiary są zapisywane z błędem standardowym, jeśli
nie podano żadnego PLIKU
Opcje standardowe:
-q, --cichy
nie wyświetlaj komunikatów ostrzegawczych
-v, --gadatliwy
wyświetlaj krótkie komunikaty pośrednie
-d, --odpluskwić
wyświetlaj szczegółowe komunikaty pośrednie
--poziom-logarytmowania=POZIOM
wyświetlaj komunikaty pośrednie do poziomu włącznie
-h, --help
wyświetl informacje pomocy
--wersja
wyświetl informacje o wersji
Użyj lpsbinary online, korzystając z usług onworks.net
