विजेता - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

विजेता - एसएमटी सॉल्वर का उपयोग करके सत्यापन शर्तों को पूरा करने का प्रयास

SYNOPSIS

विजेता [इकाई]

वर्णन

RSI विजेता कमांड ViCToR के चारों ओर एक आवरण है (VCT) जो इसके उपयोग को सरल करता है। विजेता
SPARK सत्यापन शर्तों का SMTlib में अनुवाद करता है और उन्हें SMT सॉल्वर को फीड करता है।
ऐसे ही एक एसएमटी सॉल्वर के साथ स्पार्क जहाज, ऑल्ट-एर्गो, लेकिन अन्य सॉल्वरों का उपयोग करना संभव है
जैसे सीवीसी3.

विजेता का इच्छित उपयोग सिम्पलिफायर द्वारा छोड़े गए सच्चे कुलपतियों का निर्वहन करना है और नहीं
सरलीकरण को बदलें। कृपया यह भी ध्यान दें कि वीआईसीटीओआर को एक प्रयोगात्मक माना जाता है
फिलहाल विशेषता।

यह मैनुअल पृष्ठ केवल सारांशित करता है विजेता कमांड लाइन झंडे, कृपया पूर्ण देखें
अधिक जानकारी के लिए VictorWrapper मैनुअल।

विकल्प

ये विकल्प सामान्य जीएनयू कमांड लाइन सिंटैक्स का बिल्कुल पालन नहीं करते हैं क्योंकि विकल्प शुरू होते हैं
सामान्य दो के बजाय एक एकल पानी का छींटा।

-h, -मदद
कमांड-लाइन सहायता दिखाता है।

-टी =सेकंड
इसके बाद कई सेकंड (डिफ़ॉल्ट रूप से 5) का उपयोग करके श्रीमती सॉल्वर का टाइम-आउट करें अलिमित। सेवा मेरे
टाइम-आउट अक्षम करें 0 निर्दिष्ट करें।

-एम =मेगाबाइट
एसएमटी सॉल्वर को वर्चुअल मेमोरी के कई एमआईबी (डिफ़ॉल्ट रूप से कोई सीमा नहीं) का उपयोग करके सीमित करें
अलिमित.

-v किसी भी siv फ़ाइल की उपस्थिति पर ध्यान न दें और vcg फ़ाइलों को ही संसाधित करें। डिफ़ॉल्ट रूप से, दिया गया
a यूनिट जैसे फू, विक्टर पहले foo.siv को प्रोसेस करने का प्रयास करेगा और फिर वापस आ जाएगा
foo.vcg के लिए।

—लगाना सादा मोड - समय और संस्करणों को दबाएं।

-सॉल्वर =सॉल्वर
एक वैकल्पिक एसएमटी सॉल्वर निर्दिष्ट करता है। डिफ़ॉल्ट रूप से हम alt-ergo का उपयोग करते हैं। alt में से एक हो सकता है-
ergo, cvc3, yices या z3. ऑल्ट-एर्गो सॉल्वर स्पार्क के साथ वितरित किया जाता है। सीवीसी3
सॉल्वर डेबियन का हिस्सा है। Yices और z3 सॉल्वर मालिकाना हैं।

onworks.net सेवाओं का उपयोग करके ऑनलाइन विजेता का उपयोग करें