Bu, Ubuntu Online, Fedora Online, Windows çevrimiçi emülatörü veya MAC OS çevrimiçi emülatörü gibi birden fazla ücretsiz çevrimiçi iş istasyonumuzdan birini kullanarak OnWorks ücretsiz barındırma sağlayıcısında çalıştırılabilen cvc3 komutudur.
Program:
ADI
cvc3 - otomatik SMT teoremi ispatlayıcısı
SİNOPSİS
cvc3 [seçenek] ... [Dosya]
TANIM
CVC3 ile çok sıralı (yazılı) birinci dereceden mantık için otomatik bir geçerlilik denetleyicisidir.
niceleyiciler için bazı destek, kısmi işlevler ve
yüklem alt türleri. Mevcut yerleşik teoriler,
· serbest (diğer adıyla yorumlanmamış) fonksiyon ve yüklem sembolleri üzerinde eşitlik,
· gerçek ve tamsayılı doğrusal aritmetik (doğrusal olmayan aritmetik için bir miktar destekle),
· bit vektörleri,
· diziler,
· demetler,
· kayıtlar,
· kullanıcı tanımlı endüktif veri türleri.
CVC3, CVC'deki dosyalar üzerinde çalışır Sunum Giriş Dil ya da SMTLIB giriş
dilim. Komut satırında herhangi bir girdi dosyası verilmezse, CVC3 standart girdiyi okur.
SEÇENEKLER
Aşağıda en sık kullanılan seçeneklerden sadece birkaçı verilmiştir. Daha fazla ayrıntı için bkz.
CVC3'ün yerleşik yardımı (cvc3 -Yardım) veya CVC3 web sitesi.
-Yardım]
CVC3'ü kontrol etmek için tüm seçenekleri listeleyin. Boole seçenekleri işaretlendi (B). Onlar
ön eki ile etkinleştirilir + ve ön eki ile devre dışı bırakıldı -. yardımda
çıktı, akım ayar verilir. Örneğin, çıktı listeleri
(b) -etkileşimli Etkileşimli mod
Etkileşimli modun devre dışı olduğunu gösterir. etkileşimli modu etkinleştirmek için,
seçenek +etkileşimli bu nedenle kullanılmaktadır. Diğer seçenekler işaretlenmiştir (S) dize için
argümanlar veya (i) tamsayı argümanları için.
-version
CVC3 sürümünü yazdırın ve çıkın.
-dil (sunum|smtlib|iç) Kullanılan giriş dilini seçin. Varsayılan
sunum.
+int[eraktif]
Etkileşimli modu etkinleştirin. Komutlar standart girdiden okunur ve işlenir
hemen.
+istatistikler Çalışma zamanı istatistiklerini yazdırın.
-zaman aşımı t
CVC3'ü otomatik olarak sonlandır t saniye.
onworks.net hizmetlerini kullanarak cvc3'ü çevrimiçi kullanın
