ผู้ชนะ - ออนไลน์ในคลาวด์

โครงการ:

ชื่อ

ผู้ชนะ - พยายามใช้เงื่อนไขการตรวจสอบโดยใช้ตัวแก้ไข SMT

เรื่องย่อ

ผู้มีชัย [หน่วย]

DESCRIPTION

เทศกาล ผู้มีชัย คำสั่งเป็นตัวห่อหุ้มรอบ ViCToR (ปรึกษา) ซึ่งทำให้การใช้งานง่ายขึ้น ViCToR
แปลเงื่อนไขการตรวจสอบ SPARK เป็น SMTlib และป้อนไปยังโปรแกรมแก้ไข SMT
SPARK มาพร้อมกับตัวแก้ไข SMT ตัวหนึ่ง ทางเลือกอื่นแต่สามารถใช้ตัวแก้ปัญหาอื่นได้
เช่น ซีวีซี3.

จุดประสงค์ของการใช้ชัยชนะคือการปลดปล่อย VC ที่แท้จริงที่เหลืออยู่โดย Simplifier ไม่ใช่
แทนที่ Simplifier โปรดทราบว่า ViCToR ถือเป็นการทดลอง
คุณลักษณะในขณะนี้

หน้าคู่มือนี้สรุปเฉพาะ ผู้มีชัย แฟล็กบรรทัดคำสั่ง โปรดดูแบบเต็ม
คู่มือ VictorWrapper สำหรับข้อมูลเพิ่มเติม

OPTIONS

ตัวเลือกเหล่านี้ไม่ค่อยเป็นไปตามไวยากรณ์บรรทัดคำสั่งของ GNU ปกติเนื่องจากตัวเลือกเริ่มต้นด้วย
เส้นประเดียวแทนที่จะเป็นสองเส้นปกติ

-h, -ช่วยด้วย
แสดงวิธีใช้บรรทัดคำสั่ง

-t =วินาที
หมดเวลาตัวแก้ปัญหา SMT หลังจากผ่านไปหลายวินาที (โดยค่าเริ่มต้น 5) โดยใช้ ulimit. ไปยัง
ปิดใช้งานการหมดเวลา ระบุ 0

-ม=เมกะไบต์
จำกัด ตัวแก้ปัญหา SMT ให้กับหน่วยความจำเสมือน MiB จำนวนมาก (โดยค่าเริ่มต้นไม่ จำกัด ) โดยใช้
ulimit.

-v ละเว้นการมีอยู่ของไฟล์ siv และประมวลผลไฟล์ vcg เท่านั้น โดยค่าเริ่มต้น ให้
a หน่วย เช่น foo ผู้ชนะจะพยายามประมวลผล foo.siv ก่อนแล้วค่อยถอยกลับ
ไปยัง foo.vcg

-ที่ราบ โหมดธรรมดา — หยุดการกำหนดเวลาและเวอร์ชัน

-ตัวแก้=โซลเวอร์
ระบุตัวแก้ไข SMT ทางเลือก โดยค่าเริ่มต้นเราใช้ alt-ergo สามารถเป็นหนึ่งใน alt-
ergo, cvc3, yices หรือ z3 ตัวแก้ปัญหา alt-ergo แจกจ่ายด้วย SPARK cvc3
ตัวแก้เป็นส่วนหนึ่งของเดเบียน ตัวแก้ yices และ z3 เป็นกรรมสิทธิ์

ใช้ victor ออนไลน์โดยใช้บริการ onworks.net