cvc3 - ക്ലൗഡിൽ ഓൺലൈനിൽ

പട്ടിക:

NAME

cvc3 - ഓട്ടോമാറ്റിക് SMT സിദ്ധാന്തം തെളിയിക്കുന്നു

സിനോപ്സിസ്

cvc3 [ഓപ്ഷൻ]... [ഫയലിന്റെ പേര്]

വിവരണം

HVAC3 നിരവധി തരംതിരിച്ച (ടൈപ്പ് ചെയ്‌ത) ഫസ്റ്റ്-ഓർഡർ ലോജിക്കിനുള്ള ഒരു ഓട്ടോമേറ്റഡ് വാലിഡിറ്റി ചെക്കറാണ്
ബിൽറ്റ്-ഇൻ സിദ്ധാന്തങ്ങൾ, ക്വാണ്ടിഫയറുകൾക്കുള്ള ചില പിന്തുണ, ഭാഗിക പ്രവർത്തനങ്ങൾ, കൂടാതെ
ഉപവിഭാഗങ്ങൾ പ്രവചിക്കുക. എന്ന സിദ്ധാന്തങ്ങളാണ് നിലവിലുള്ള അന്തർനിർമ്മിത സിദ്ധാന്തങ്ങൾ

· സ്വതന്ത്ര (അഥവാ വ്യാഖ്യാനിക്കപ്പെടാത്ത) പ്രവർത്തനത്തിനും പ്രവചന ചിഹ്നങ്ങൾക്കും മേൽ തുല്യത,

യഥാർത്ഥവും പൂർണ്ണസംഖ്യാ രേഖീയ ഗണിതവും (രേഖീയമല്ലാത്ത ഗണിതത്തിന് ചില പിന്തുണയോടെ),

· ബിറ്റ് വെക്‌ടറുകൾ,

· ശ്രേണികൾ,

· ട്യൂപ്പിൾസ്,

· രേഖകള്,

· ഉപയോക്തൃ-നിർവചിക്കപ്പെട്ട ഇൻഡക്റ്റീവ് ഡാറ്റാടൈപ്പുകൾ.

CVC3 CVC-യിലെ ഫയലുകളിൽ പ്രവർത്തിക്കുന്നു അവതരണം ഇൻപുട്ട് ഭാഷ അഥവാ SMTLIB ഇൻപുട്ട്
ഭാഷ. കമാൻഡ് ലൈനിൽ ഇൻപുട്ട് ഫയലൊന്നും നൽകിയിട്ടില്ലെങ്കിൽ, CVC3 സ്റ്റാൻഡേർഡ് ഇൻപുട്ട് വായിക്കുന്നു.

ഓപ്ഷനുകൾ

ഏറ്റവും കൂടുതൽ ഉപയോഗിക്കുന്ന ചില ഓപ്ഷനുകൾ മാത്രം ചുവടെ നൽകിയിരിക്കുന്നു. കൂടുതൽ വിവരങ്ങൾക്ക്, കാണുക
CVC3-ന്റെ അന്തർനിർമ്മിത സഹായം (cvc3 -ഹെൽപ്പ്) അല്ലെങ്കിൽ CVC3 വെബ്സൈറ്റ്.

-സഹായം]
CVC3 നിയന്ത്രിക്കുന്നതിനുള്ള എല്ലാ ഓപ്ഷനുകളും ലിസ്റ്റ് ചെയ്യുക. ബൂളിയൻ ഓപ്ഷനുകൾ അടയാളപ്പെടുത്തിയിരിക്കുന്നു (ബി). അവർ
ഉപയോഗിച്ച് പ്രിഫിക്‌സ് ചെയ്‌ത് പ്രവർത്തനക്ഷമമാക്കുന്നു + കൂടെ പ്രിഫിക്‌സ് ചെയ്‌ത് പ്രവർത്തനരഹിതമാക്കി -. സഹായത്തിൽ
ഔട്ട്പുട്ട്, ദി നിലവിലുള്ളത് ക്രമീകരണം നൽകിയിരിക്കുന്നു. ഉദാഹരണത്തിന്, ഔട്ട്പുട്ട് ലിസ്റ്റുകൾ

(ബി) -ഇന്ററാക്ടീവ് ഇന്ററാക്ടീവ് മോഡ്

ഇന്ററാക്ടീവ് മോഡ് പ്രവർത്തനരഹിതമാക്കിയതായി സൂചിപ്പിക്കുന്നു. സംവേദനാത്മക മോഡ് പ്രവർത്തനക്ഷമമാക്കാൻ, the
ഓപ്ഷൻ + സംവേദനാത്മക അതിനാൽ ഉപയോഗിക്കുന്നു. മറ്റ് ഓപ്ഷനുകൾ അടയാളപ്പെടുത്തിയിരിക്കുന്നു (കൾ) സ്ട്രിങ്ങിനായി
വാദങ്ങൾ, അല്ലെങ്കിൽ (i) പൂർണ്ണസംഖ്യ ആർഗ്യുമെന്റുകൾക്കായി.

-പതിപ്പ്
CVC3 പതിപ്പ് പ്രിന്റ് ചെയ്‌ത് പുറത്തുകടക്കുക.

-ലംഗ് (അവതരണം|smtlib|ആന്തരിക) ഉപയോഗിച്ച ഇൻപുട്ട് ഭാഷ തിരഞ്ഞെടുക്കുക. സ്ഥിരസ്ഥിതിയാണ്
അവതരണം.

+int[eractive]
സംവേദനാത്മക മോഡ് പ്രവർത്തനക്ഷമമാക്കുക. കമാൻഡുകൾ സാധാരണ ഇൻപുട്ടിൽ നിന്ന് വായിക്കുകയും പ്രോസസ്സ് ചെയ്യുകയും ചെയ്യുന്നു
ഉടനെ.

+ സ്ഥിതിവിവരക്കണക്കുകൾ റൺ-ടൈം സ്ഥിതിവിവരക്കണക്കുകൾ അച്ചടിക്കുക.

-ടൈം ഔട്ട് t
ശേഷം CVC3 സ്വയമേവ അവസാനിപ്പിക്കുക t സെക്കൻഡ്.

onworks.net സേവനങ്ങൾ ഉപയോഗിച്ച് cvc3 ഓൺലൈനായി ഉപയോഗിക്കുക