বিজয়ী - ক্লাউডে অনলাইন

কার্যক্রম:

NAME এর

বিজয়ী - এসএমটি সমাধানকারী ব্যবহার করে যাচাইকরণের শর্তগুলি ডিসচার্জ করার চেষ্টা করে

সাইনোপিসিস

বিজেতা [ইউনিট]

বর্ণনাঃ

সার্জারির বিজেতা কমান্ড হল ViCToR এর চারপাশে একটি মোড়ক (vct) যা এর ব্যবহারকে সহজ করে। ভিসিটোআর
SPARK যাচাইকরণের শর্তগুলিকে SMTlib-এ অনুবাদ করে এবং একটি SMT সমাধানকারীকে ফিড করে৷
স্পার্ক এমন একটি এসএমটি সলভার সহ জাহাজে করে, alt-ergo, কিন্তু অন্য সমাধানকারী ব্যবহার করা সম্ভব
যেমন cvc3.

বিজয়ীর উদ্দেশ্যমূলক ব্যবহার হল সরলকারীর দ্বারা অবশিষ্ট সত্য ভিসিগুলিকে ডিসচার্জ করা এবং না
সিম্পলিফায়ার প্রতিস্থাপন করুন। অনুগ্রহ করে আরও মনে রাখবেন যে ViCtoR একটি পরীক্ষামূলক বলে মনে করা হয়
এই মুহূর্তে বৈশিষ্ট্য।

এই ম্যানুয়াল পৃষ্ঠা শুধুমাত্র সারসংক্ষেপ বিজেতা কমান্ড-লাইন পতাকা, অনুগ্রহ করে সম্পূর্ণ দেখুন
আরও তথ্যের জন্য VictorWrapper ম্যানুয়াল।

বিকল্প

এই বিকল্পগুলি স্বাভাবিক GNU কমান্ড লাইন সিনট্যাক্স অনুসরণ করে না কারণ বিকল্পগুলি দিয়ে শুরু হয়
সাধারণ দুটির পরিবর্তে একটি একক ড্যাশ।

-h, -হেল্প
কমান্ড লাইন সাহায্য দেখায়।

-t=সেকেন্ডস
এসএমটি সলভারকে টাইম-আউট করার অনেক সেকেন্ড পরে (ডিফল্ট 5) ব্যবহার করে সীমা। থেকে
টাইম-আউট অক্ষম করুন নির্দিষ্ট করুন 0।

-m=মেগাবাইট
এসএমটি সমাধানকারীকে ভার্চুয়াল মেমরির এই অনেক MiB পর্যন্ত সীমাবদ্ধ করুন (ডিফল্টভাবে সীমা নেই)
সীমা.

-v কোনো siv ফাইলের উপস্থিতি উপেক্ষা করুন এবং শুধুমাত্র vcg ফাইলগুলি প্রক্রিয়া করুন। ডিফল্টরূপে, দেওয়া
a UNIT পর্যন্ত যেমন foo, ভিক্টর প্রথমে foo.siv প্রক্রিয়া করার চেষ্টা করবে এবং তারপরে ফিরে আসবে
foo.vcg-তে।

-সমতল প্লেইন মোড — টাইমিং এবং ভার্সন দমন করুন।

- সমাধানকারী =সমাধান
একটি বিকল্প SMT সমাধানকারী নির্দিষ্ট করে। ডিফল্টরূপে আমরা alt-ergo ব্যবহার করি। Alt-এর একটি হতে পারে-
ergo, cvc3, yices বা z3. Alt-ergo সলভার স্পার্কের সাথে বিতরণ করা হয়। cvc3
সমাধানকারী ডেবিয়ানের অংশ। yices এবং z3 সমাধানকারী মালিকানাধীন।

onworks.net পরিষেবা ব্যবহার করে ভিক্টর অনলাইন ব্যবহার করুন