के लिए एसएमटी सॉल्वर मैं सी कोड के प्रतीकात्मक निष्पादन में कुछ प्रयोगों की योजना बना रहा हूं, ऑफ-द-शेल्फ एसएमटी सॉल्वर का उपयोग करके, और सोच रहा हूं कि कौन सा सॉल्वर उपयोग करना है; उदा। एसएमटी प्रतियोगिता प्रवेशकर्ता, और केवल ओपन-सोर्स सिस्टम लेते हुए, इसे बीवर, बूलेक्टर, सीवीसी 3, ओपनएसएमटी, सैटेन, सोनोलर, एसटीपी, वेरिट तक सीमित कर दिया गया है; जो अभी भी एक लंबी सूची है।बिट वेक्टर अंकगणितीय
इसे थोड़ा संकीर्ण करने की कोशिश कर रहा है, मुझे लगता है कि कुछ सिस्टम बिट वेक्टर अंकगणितीय को संभालने की क्षमता का विज्ञापन करते हैं, जबकि अन्य केवल सामान्य पूर्णांक अंकगणितीय को संभालने की क्षमता का विज्ञापन करते हैं। सिद्धांत रूप में, पूर्व सी के लिए सही है, जहां वेरिएबल्स मशीन शब्द हैं, असंबद्ध पूर्णांक नहीं। अभ्यास में यह कितना अंतर करता है? यदि आप इस तरह की नौकरी के लिए एक सामान्य पूर्णांक प्रणाली का उपयोग करने का प्रयास करते हैं तो क्या होता है? क्या निम्न परिदृश्यों में से कोई एक लागू होता है?
थोड़ा सा वेक्टर सिस्टम थोड़ा अधिक कुशल है, लेकिन आप या तो कोई समस्या नहीं कर सकते हैं।
आप थोड़ी-थोड़ी tweaking के साथ एक सामान्य पूर्णांक प्रणाली का उपयोग कर सकते हैं।
हस्ताक्षर int के लिए एक सामान्य पूर्णांक प्रणाली ठीक है (क्योंकि अतिप्रवाह का परिणाम अपरिभाषित है) लेकिन हस्ताक्षरित के लिए गलत जवाब देगा।
एक सामान्य पूर्णांक प्रणाली मशीन शब्द अंकगणितीय के लिए बिल्कुल सही नहीं है, और मैं केवल उन प्रणालियों को अपनी छोटी सूची को कम कर सकता हूं जो बिट वेक्टर अंकगणित प्रदान करते हैं।
कुछ और ...?
मैं संभव के रूप में विशिष्ट एक सवाल पूछने की कोशिश की है, लेकिन अगर किसी को भी इस सूची में नीचे संकुचन के लिए किसी अन्य मापदंड सुझाव दे सकते हैं, कि बहुत अच्छा होगा!