Z3

Z3 माइक्रोसॉफ्ट रिसर्च का एक प्रमेय सिद्धकर्ता है। यह MIT लाइसेंस के अंतर्गत लाइसेंस प्राप्त है। Windows बाइनरी वितरण में C++ runtime redistributables शामिल हैं।

यदि आप Z3 से परिचित नहीं हैं, तो आप यहाँ से शुरू कर सकते हैं।

स्थिर और नाइटली रिलीज़ के लिए पूर्व-निर्मित बाइनरी यहाँ उपलब्ध हैं।

Z3 को Visual Studio, Makefile, CMake, vcpkg, या Bazel का उपयोग करके बनाया जा सकता है। यह कई प्रोग्रामिंग भाषाओं के लिए बाइंडिंग्स प्रदान करता है।

Z3 के विभिन्न स्थिर रिलीज़ों पर नोट्स के लिए रिलीज़ नोट्स देखें।

बिल्ड स्थिति

पुल रिक्वेस्ट और पुश वर्कफ़्लोज़

WASM बिल्ड	Windows बिल्ड	CI	OCaml बाइंडिंग

अनुसूचित वर्कफ़्लोज़

Open Bugs	Android बिल्ड	Pyodide Wheel (PyPI)	Nightly बिल्ड	Cross बिल्ड

MSVC Static	MSVC Clang-CL	Build Z3 Cache	मेमोरी सुरक्षा	PRs को तैयार चिह्नित करें

मैनुअल और रिलीज़ वर्कफ़्लोज़

दस्तावेज़ीकरण	रिलीज़ बिल्ड	WASM रिलीज़	NuGet बिल्ड

विशेषीकृत वर्कफ़्लोज़

Nightly सत्यापन	Copilot सेटअप	Agentics रखरखाव

एजेंटिक वर्कफ़्लोज़

API सामंजस्य	कोड सरलीकरणकर्ता	रिलीज़ नोट्स	वर्कफ़्लो सुझाव	अकादमिक उद्धरण

Issue बैकलॉग	मेमोरी सुरक्षा रिपोर्ट	QF-S बेंचमार्क	Specbot क्रैश विश्लेषक	SMTLIB बेंचमार्क खोजक

TPTP बेंचमार्क

Visual Studio कमांड प्रॉम्प्ट का उपयोग करके Windows पर Z3 बनाना

32-बिट बिल्ड के लिए, इसके साथ शुरू करें:

python scripts/mk_make.py

या इसके बजाय, 64-बिट बिल्ड के लिए:

python scripts/mk_make.py -x

फिर चलाएँ:

cd build
nmake

Z3 C++20 का उपयोग करता है। इसलिए Visual Studio का अनुशंसित संस्करण VS2019 या बाद का है।

सुरक्षा सुविधाएँ (MSVC): Visual Studio/MSVC के साथ निर्माण करते समय, Z3 के लिए डिफ़ॉल्ट रूप से कुछ सुरक्षा सुविधाएँ सक्षम होती हैं:

कंट्रोल फ़्लो गार्ड (/guard:cf) - फ़ंक्शन एंट्री पॉइंट्स के अलावा अन्य स्थानों पर कॉल को रोककर आपके कोड से समझौता करने के प्रयासों का पता लगाने के लिए डिफ़ॉल्ट रूप से सक्षम, जिससे हमलावरों के लिए कंट्रोल फ़्लो रीडायरेक्शन के माध्यम से मनमाना कोड निष्पादित करना अधिक कठिन हो जाता है
एड्रेस स्पेस लेआउट रैंडमाइज़ेशन (/DYNAMICBASE) - मेमोरी लेआउट रैंडमाइज़ेशन के लिए डिफ़ॉल्ट रूप से सक्षम, /GUARD:CF लिंकर विकल्प द्वारा आवश्यक
यदि आवश्यक हो तो इन्हें python scripts/mk_make.py --no-guardcf (Python बिल्ड) या cmake -DZ3_ENABLE_CFG=OFF (CMake बिल्ड) का उपयोग करके अक्षम किया जा सकता है

make और GCC/Clang का उपयोग करके Z3 बनाना

निष्पादित करें:

python scripts/mk_make.py
cd build
make
sudo make install

नोट: डिफ़ॉल्ट रूप से g++ का उपयोग C++ कंपाइलर के रूप में किया जाता है यदि यह उपलब्ध है। यदि आप Clang का उपयोग करना पसंद करते हैं, तो mk_make.py के आह्वान को इसमें बदलें:

CXX=clang++ CC=clang python scripts/mk_make.py

ध्यान दें कि Clang < 3.7 OpenMP का समर्थन नहीं करता है।

आप Cygwin और Mingw-w64 क्रॉस-कंपाइलर का उपयोग करके Windows के लिए Z3 भी बना सकते हैं। उस स्थिति में, सुनिश्चित करें कि Cygwin के अपने Python का उपयोग करें, न कि Python की किसी Windows स्थापना का।

64-बिट बिल्ड (Cygwin64 से) के लिए, Z3 के स्रोतों को इसके साथ कॉन्फ़िगर करें:

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

32-बिट बिल्ड समान रूप से काम करना चाहिए (लेकिन परीक्षण नहीं किया गया है); Cygwin32 के भीतर से 32/64 बिट बिल्ड के लिए भी यही सच है।

डिफ़ॉल्ट रूप से, यह z3 निष्पादन योग्य फ़ाइलों को PREFIX/bin पर, लाइब्रेरी को PREFIX/lib पर, और इन्क्लूड फ़ाइलों को PREFIX/include पर स्थापित करेगा, जहाँ PREFIX स्थापना उपसर्ग mk_make.py स्क्रिप्ट द्वारा अनुमानित किया जाता है। यह अधिकांश Linux वितरणों के लिए सामान्यतः /usr होता है, और FreeBSD और macOS के लिए /usr/local। स्थापना उपसर्ग बदलने के लिए --prefix= कमांड-लाइन विकल्प का उपयोग करें। उदाहरण के लिए:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

Z3 को अनइंस्टॉल करने के लिए, उपयोग करें:

sudo make uninstall

Z3 को साफ़ करने के लिए, आप बिल्ड निर्देशिका को हटा सकते हैं और mk_make.py स्क्रिप्ट को फिर से चला सकते हैं।

CMake का उपयोग करके Z3 बनाना

Z3 में CMake का उपयोग करके एक बिल्ड सिस्टम है। विवरण के लिए README-CMake.md फ़ाइल पढ़ें। OCaml बाइंडिंग बनाने को छोड़कर, अधिकांश बिल्ड कार्यों के लिए इसकी अनुशंसा की जाती है।

vcpkg का उपयोग करके Z3 बनाना

vcpkg एक पूर्ण प्लेटफ़ॉर्म पैकेज मैनेजर है। vcpkg के साथ Z3 स्थापित करने के लिए, निष्पादित करें:

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Bazel का उपयोग करके Z3 बनाना

Z3 को Bazel का उपयोग करके बनाया जा सकता है। यह Clang के साथ Ubuntu पर काम करने के लिए जाना जाता है (लेकिन अन्य कंपाइलरों के साथ कहीं और भी काम कर सकता है):

bazel build //...

निर्भरताएँ

Z3 में स्वयं केवल कुछ निर्भरताएँ हैं। यह C++ रनटाइम लाइब्रेरी का उपयोग करता है, जिसमें मल्टी-थ्रेडिंग के लिए pthreads शामिल हैं। वैकल्पिक रूप से मल्टी-प्रेसिजन पूर्णांकों के लिए GMP का उपयोग करना संभव है, लेकिन Z3 में अपनी स्व-निहित मल्टी-प्रेसिजन कार्यक्षमता है। Z3 बनाने के लिए Python आवश्यक है। Java, .NET, OCaml और Julia APIs बनाने के लिए प्रासंगिक टूलचेन स्थापित करना आवश्यक है।

Z3 बाइंडिंग्स

Z3 में विभिन्न प्रोग्रामिंग भाषाओं के लिए बाइंडिंग्स हैं।

`.NET`

आप nuget.org से नवीनतम रिलीज़ Z3 के लिए एक NuGet पैकेज स्थापित कर सकते हैं।

इन्हें बनाने में सक्षम करने के लिए mk_make.py के साथ --dotnet कमांड लाइन फ़्लैग का उपयोग करें।

उदाहरणों के लिए examples/dotnet देखें।

`C`

ये हमेशा सक्षम रहते हैं।

उदाहरणों के लिए examples/c देखें।

`C++`

ये हमेशा सक्षम रहते हैं।

उदाहरणों के लिए examples/c++ देखें।

`Java`

इन्हें बनाने में सक्षम करने के लिए mk_make.py के साथ --java कमांड लाइन फ़्लैग का उपयोग करें।

IDE सेटअप निर्देशों (Eclipse, IntelliJ IDEA, Visual Studio Code) और समस्या निवारण के लिए, Java IDE सेटअप गाइड देखें।

उदाहरणों के लिए examples/java देखें।

`Go`

इन्हें बनाने में सक्षम करने के लिए mk_make.py के साथ --go कमांड लाइन फ़्लैग का उपयोग करें। ध्यान दें कि Go बाइंडिंग्स CGO का उपयोग करती हैं और निर्माण के लिए Go टूलचेन (Go 1.20 या बाद का) की आवश्यकता होती है।

CMake के साथ, -DZ3_BUILD_GO_BINDINGS=ON विकल्प का उपयोग करें।

उदाहरणों के लिए examples/go और पूर्ण API दस्तावेज़ीकरण के लिए src/api/go/README.md देखें।

`OCaml`

इन्हें बनाने में सक्षम करने के लिए mk_make.py के साथ --ml कमांड लाइन फ़्लैग का उपयोग करें।

उदाहरणों के लिए examples/ml देखें।

`Python`

आप नवीनतम रिलीज़ के लिए Z3 के Python रैपर को pypi से इस कमांड का उपयोग करके स्थापित कर सकते हैं:

   pip install z3-solver

इन्हें बनाने में सक्षम करने के लिए mk_make.py के साथ --python कमांड लाइन फ़्लैग का उपयोग करें।

ध्यान दें कि कुछ प्लेटफ़ॉर्म पर यह आवश्यक है कि Python पैकेज निर्देशिका (अधिकांश वितरणों पर site-packages और Debian-आधारित वितरणों पर dist-packages) स्थापना उपसर्ग के अंतर्गत हो। यदि आप एक गैर-मानक उपसर्ग का उपयोग करते हैं तो आप Python पैकेज निर्देशिका बदलने के लिए --pypkgdir विकल्प का उपयोग कर सकते हैं। उदाहरण के लिए:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

यदि आपको वास्तव में गैर-मानक उपसर्ग में स्थापित करने की आवश्यकता है, तो एक बेहतर तरीका Python वर्चुअल एनवायरनमेंट का उपयोग करना और वहां Z3 स्थापित करना है। Python पैकेज Python3 के लिए भी काम करते हैं। Windows के अंतर्गत, Visual C++ नेटिव कमांड बिल्ड एनवायरनमेंट के अंदर निर्माण करना याद रखें। ध्यान दें कि build/python/z3 निर्देशिका वहाँ से पहुँच योग्य होनी चाहिए जहाँ Z3 के साथ Python का उपयोग किया जाता है और इसे पथ में libz3.dll की आवश्यकता होती है।

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# आप Z3 और Python बाइंडिंग्स को वर्चुअल एनवायरनमेंट में स्थापित पाएंगे
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

उदाहरणों के लिए examples/python देखें।

`Julia`

Julia पैकेज Z3.jl Z3 के C API को रैप करता है। इसका पिछला संस्करण C++ API को रैप करता था: Julia बाइंडिंग्स को अपडेट करने और बनाने की जानकारी src/api/julia में पाई जा सकती है।

`WebAssembly` / `TypeScript` / `JavaScript`

एक WebAssembly बिल्ड संबंधित TypeScript टाइपिंग के साथ npm पर z3-solver के रूप में प्रकाशित किया गया है। इन बाइंडिंग्स को बनाने की जानकारी src/api/js में पाई जा सकती है।

Smalltalk (`Pharo` / `Smalltalk/X`)

प्रोजेक्ट MachineArithmetic Z3 के C API के लिए एक Smalltalk इंटरफ़ेस प्रदान करता है। अधिक जानकारी के लिए, MachineArithmetic/README.md देखें।

AIX

AIX के लिए बिल्ड सेटिंग्स यहाँ वर्णित हैं।

सिस्टम अवलोकन

System Diagram

इंटरफ़ेस

डिफ़ॉल्ट इनपुट प्रारूप SMTLIB2 है
अन्य देशी विदेशी फ़ंक्शन इंटरफ़ेस:
C++ API
.NET API
Java API
Python API (also available in pydoc format)
Rust
C
OCaml
Julia
Smalltalk (supports Pharo and Smalltalk/X)

पावर टूल्स

Axiom Profiler वर्तमान में ETH Zurich द्वारा विकसित किया जा रहा है

z3 z3-5.1.0

श्रेणियाँ