Jest to polecenie cvc3, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu darmowych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online Windows lub emulator online MAC OS
PROGRAM:
IMIĘ
cvc3 - automatyczne dowodzenie twierdzenia SMT
STRESZCZENIE
CVC3 [opcja] ... [filename]
OPIS
CVC3 to automatyczne narzędzie do sprawdzania poprawności dla logiki pierwszego rzędu z wieloma sortowaniem (wpisywane) z
wbudowane teorie, w tym pewne wsparcie dla kwantyfikatorów, funkcji częściowych i
podtypy predykatów. Obecne teorie wbudowane to teorie
· równość nad wolną (inaczej nieinterpretowaną) funkcją i symbolami predykatów,
· arytmetyka liniowa rzeczywista i całkowita (z pewnym wsparciem dla arytmetyki nieliniowej),
· wektory bitowe,
· tablice,
· krotki,
· zapisy,
· indukcyjne typy danych zdefiniowane przez użytkownika.
CVC3 operuje na plikach w CVC Prezentacja Wkład Wybierz język albo SMTLIB wkład
język. Jeśli w wierszu poleceń nie podano pliku wejściowego, CVC3 czyta standardowe wejście.
OPCJE
Poniżej podano tylko kilka najczęściej używanych opcji. Aby uzyskać więcej informacji, zobacz
Wbudowana pomoc CVC3 (CVC3 -Pomoc) lub w witrynie CVC3.
-Wsparcie]
Wymień wszystkie opcje sterowania CVC3. Opcje logiczne są zaznaczone (B). Oni
są włączane przez przedrostek + i wyłączone przez przedrostek z -. W pomocy
wyjście, aktualne ustawienie jest podane. Na przykład listy wyjściowe
(b) -interaktywny tryb interaktywny
Wskazuje, że tryb interaktywny jest wyłączony. aby włączyć tryb interaktywny,
opcja +interaktywny jest zatem używany. Inne opcje są zaznaczone (S) na sznurek
argumenty, lub (I) dla argumentów całkowitych.
-wersja
Wydrukuj wersję CVC3 i wyjdź.
-długie (presentation|smtlib|wewnętrzny) Wybierz używany język wprowadzania. Wartość domyślna to
presentation.
+inter[aktywny]
Włącz tryb interaktywny. Polecenia są odczytywane ze standardowego wejścia i przetwarzane
natychmiast.
+statystyki Drukuj statystyki czasu wykonywania.
-koniec czasu t
Automatycznie zakończ CVC3 po t towary drugiej jakości.
Korzystaj z cvc3 online za pomocą usług onworks.net