z3prover/z3उच्च-प्रदर्शन SMT सॉल्वर स्वचालित प्रमेय सिद्ध करने, बाधा समाधान, और प्रोग्राम सत्यापन के लिए। कई सिद्धांतों और औपचारिक विश्लेषण के लिए भाषा बाइंडिंग का समर्थन करता है।
# Z3 Z3 Microsoft Research का एक प्रमेय प्रमाणक (theorem prover) है। यह [MIT लाइसेंस](https://github.com/z3prover/z3/blob/master/LICENSE.txt) के अंतर्गत लाइसेंस प्राप्त है। Windows बाइनरी वितरणों में [C++ रनटाइम रीडिस्ट्रिब्यूटेबल्स](https://visualstudio.microsoft.com/license-terms/vs2022-cruntime/) शामिल हैं यदि आप Z3 से परिचित नहीं हैं, तो आप [यहाँ](https://github.com/Z3Prover/z3/wiki#background) से शुरुआत कर सकते हैं। स्थिर और नाइटली रिलीज़ के लिए पूर्व-निर्मित बाइनरीज़ [यहाँ](https://github.com/Z3Prover/z3/releases) उपलब्ध हैं। Z3 को [CMake][3], [vcpkg][4], या [Bazel][5] का उपयोग करके बनाया जा सकता है। यह [कई प्रोग्रामिंग भाषाओं के लिए बाइंडिंग][6] प्रदान करता है। Z3 के विभिन्न स्थिर रिलीज़ों के नोट्स के लिए [रिलीज़ नोट्स](https://github.com/z3prover/z3/blob/master/RELEASE_NOTES.md) देखें। [](https://microsoft.github.io/z3guide/) ## बिल्ड स्थिति ### पुल रिक्वेस्ट और पुश वर्कफ़्लो | WASM बिल्ड | Windows बिल्ड | CI | परिमित-क्षेत्र रिग्रेशन | | ------------|---------------|----------------------|-------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ci.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/finite-field.yml) | | डिटरमिनिज़्म लिंटर | सॉल्वर डिटरमिनिज़्म | पल्स नेटिव चेकर बिल्ड | |---------------------|---------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-report.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-build.yml) | ### निर्धारित वर्कफ़्लो | Android बिल्ड | नाइटली बिल्ड | क्रॉस बिल्ड | F* मास्टर बिल्ड | | ---------------|---------------|-------------|------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nightly.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/cross-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml) | | MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready | |-------------|---------------|----------------|---------------|----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build-clang-cl.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/build-z3-cache.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/mark-prs-ready-for-review.yml) | | Clang-Tidy Warning Report | |----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/clang-tidy-warning-report.yml) | ### मैनुअल और रिलीज़ वर्कफ़्लो | Documentation | Release Build | WASM Release | Pyodide Wheel (PyPI) | |---------------|---------------|--------------|---------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/docs.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wasm-release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide-pypi.yml) | ### विशेषीकृत वर्कफ़्लो | Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit | |--------------------|---------------|----------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/nightly-validation.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/copilot-setup-steps.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/agentics-maintenance.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nfv-formal-audit-dispatcher.yml) | ### फ़ॉलो-अप / टिप्पणी वर्कफ़्लो | Determinism Linter PR Comment | Solver Determinism PR Comment | Pulse Checker Regressions | |--------------------------------|---------------------------------|--------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-regressions.yml) | ### एजेंटिक वर्कफ़्लो | API सुसंगतता | कोड सरलीकरणकर्ता | रिलीज़ नोट्स | वर्कफ़्लो सुझाव | अकादमिक उद्धरण | | -------------|-----------------|---------------|---------------------|-------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/api-coherence-checker.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-simplifier.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release-notes-updater.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/workflow-suggestion-agent.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/academic-citation-tracker.lock.yml) | | इश्यू बैकलॉग | मेमोरी सुरक्षा रिपोर्ट | SMTLIB बेंचमार्क खोजकर्ता | F* NFV PR ऑडिट | | --------------|----------------------|-------------------------|-----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/issue-backlog-processor.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety-report.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/smtlib-benchmark-finder.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-nfv-audit.lock.yml) | | A3 पायथन विश्लेषण | कोड परंपराएँ | आँकड़ों की तुलना विसंगति रिपोर्टर | CSA विश्लेषण | टैक्टिक-से-सरलीकरणकर्ता | |----------------------|-------------------|----------------------------------|----------------|------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/a3-python.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-conventions-analyzer.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/compare-stats-anomaly-reporter.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/csa-analysis.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/tactic-to-simplifier.lock.yml) | [3]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-cmake [4]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-vcpkg [5]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-bazel [6]: https://raw.githubusercontent.com/z3prover/z3/master/#z3-bindings ## CMake का उपयोग करके Z3 का निर्माण CMake, Z3 के लिए पसंदीदा और सबसे पूर्ण सुविधाओं वाला बिल्ड सिस्टम है। एक बुनियादी रिलीज़ बिल्ड है: ```bash cmake -S . -B build -DCMAKE_BUILD_TYPE=Release cmake --build build --parallel $(nproc) ``` [README-CMake.md](https://github.com/z3prover/z3/blob/master/README-CMake.md) में बिल्ड विकल्प, भाषा बाइंडिंग, इंस्टॉलेशन, और किसी अन्य CMake प्रोजेक्ट से Z3 का उपयोग करने के निर्देश देखें। Z3 C++20 का उपयोग करता है। Windows पर, Visual Studio का अनुशंसित संस्करण इसलिए VS2019 या बाद का है; Ninja या Visual Studio जनरेटर के साथ CMake Visual Studio Command Prompt से Z3 को बिल्ड करता है। **सुरक्षा सुविधाएँ (MSVC)**: Visual Studio/MSVC के साथ बिल्ड करते समय, Z3 के लिए डिफ़ॉल्ट रूप से कुछ सुरक्षा सुविधाएँ सक्षम होती हैं: - Control Flow Guard (`/guard:cf`) - फ़ंक्शन एंट्री पॉइंट के अलावा अन्य स्थानों पर कॉल को रोककर आपके कोड से समझौता करने के प्रयासों का पता लगाने के लिए डिफ़ॉल्ट रूप से सक्षम, जिससे हमलावरों के लिए कंट्रोल फ्लो रीडायरेक्शन के माध्यम से मनमाना कोड निष्पादित करना अधिक कठिन हो जाता है - Address Space Layout Randomization (`/DYNAMICBASE`) - मेमोरी लेआउट रैंडमाइज़ेशन के लिए डिफ़ॉल्ट रूप से सक्षम, `/GUARD:CF` लिंकर विकल्प के लिए आवश्यक - यदि आवश्यक हो तो इन्हें `cmake -S . -B build -DZ3_ENABLE_CFG=OFF` का उपयोग करके अक्षम किया जा सकता है सिस्टम प्रीफ़िक्स में इंस्टॉल करने के लिए `sudo cmake --install build` का उपयोग करें (या कस्टम प्रीफ़िक्स के लिए कॉन्फ़िगर समय पर `-DCMAKE_INSTALL_PREFIX=` सेट करें)। अनइंस्टॉल करने के लिए, अपने प्लेटफ़ॉर्म के पैकेज मैनेजर से परामर्श करें, या, चूँकि CMake इंस्टॉल की गई फ़ाइलों को `build/install_manifest.txt` में ट्रैक करता है, उन फ़ाइलों को सीधे हटा दें। ## vcpkg का उपयोग करके Z3 बिल्ड करना vcpkg एक पूर्ण प्लेटफ़ॉर्म पैकेज मैनेजर है। vcpkg के साथ Z3 इंस्टॉल करने के लिए, निष्पादित करें: ```bash 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](https://bazel.build/) का उपयोग करके बनाया जा सकता है। यह Ubuntu पर Clang के साथ काम करने के लिए ज्ञात है (लेकिन अन्य कंपाइलरों के साथ अन्यत्र भी काम कर सकता है): ``` bazel build //... ``` ## निर्भरताएँ Z3 की स्वयं बहुत कम निर्भरताएँ हैं। यह C++ रनटाइम लाइब्रेरीज़ का उपयोग करता है, जिसमें मल्टी-थ्रेडिंग के लिए pthreads भी शामिल है। वैकल्पिक रूप से मल्टी-प्रिसिजन पूर्णांकों के लिए GMP का उपयोग करना संभव है, लेकिन Z3 में अपनी स्वयं की स्व-निहित मल्टी-प्रिसिजन कार्यक्षमता शामिल है। Z3 को बनाने के लिए Python आवश्यक है। Java, .NET, OCaml और Julia API बनाने के लिए संबंधित टूलचेन इंस्टॉल करना आवश्यक है। ## Z3 बाइंडिंग्स Z3 में विभिन्न प्रोग्रामिंग भाषाओं के लिए बाइंडिंग्स हैं। ### ``.NET`` आप [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/) से नवीनतम रिलीज़ Z3 के लिए NuGet पैकेज इंस्टॉल कर सकते हैं। CMake के साथ, ``-DZ3_BUILD_DOTNET_BINDINGS=ON`` विकल्प का उपयोग करें। उदाहरणों के लिए [``examples/dotnet``](https://github.com/z3prover/z3/blob/master/examples/dotnet) देखें। ### ``C`` ये सदैव सक्षम रहते हैं। उदाहरणों के लिए [``examples/c``](https://github.com/z3prover/z3/blob/master/examples/c) देखें। ### ``C++`` ये सदैव सक्षम रहते हैं। उदाहरणों के लिए [``examples/c++``](https://github.com/z3prover/z3/blob/master/examples/c%2B%2B) देखें। ### ``Java`` CMake के साथ, ``-DZ3_BUILD_JAVA_BINDINGS=ON`` विकल्प का उपयोग करें। IDE सेटअप निर्देशों (Eclipse, IntelliJ IDEA, Visual Studio Code) और समस्या-निवारण के लिए, [Java IDE Setup Guide](https://github.com/z3prover/z3/blob/master/doc/JAVA_IDE_SETUP.md) देखें। उदाहरणों के लिए [``examples/java``](https://github.com/z3prover/z3/blob/master/examples/java) देखें। ### ``Go`` CMake के साथ, ``-DZ3_BUILD_GO_BINDINGS=ON`` विकल्प का उपयोग करें। ध्यान दें कि Go बाइंडिंग्स CGO का उपयोग करती हैं और बनाने के लिए Go टूलचेन (Go 1.20 या बाद का) आवश्यक है। उदाहरणों के लिए [``examples/go``](https://github.com/z3prover/z3/blob/master/examples/go) देखें और पूर्ण API दस्तावेज़ीकरण के लिए [``src/api/go/README.md``](https://github.com/z3prover/z3/blob/master/src/api/go/README.md) देखें। ### ``OCaml`` CMake के साथ, ``-DZ3_BUILD_OCAML_BINDINGS=ON`` विकल्प का उपयोग करें। उदाहरणों के लिए [``examples/ml``](https://github.com/z3prover/z3/blob/master/examples/ml) देखें। ### ``Python`` आप निम्नलिखित कमांड का उपयोग करके pypi से नवीनतम रिलीज़ के लिए Z3 का Python रैपर इंस्टॉल कर सकते हैं: ```bash pip install z3-solver ``` CMake के साथ, ``-DZ3_BUILD_PYTHON_BINDINGS=ON`` विकल्प का उपयोग करें। ध्यान दें कि कुछ प्लेटफ़ॉर्म पर यह आवश्यक है कि Python पैकेज निर्देशिका (अधिकांश वितरणों पर ``site-packages`` और Debian-आधारित वितरणों पर ``dist-packages``) इंस्टॉल प्रीफ़िक्स के अंतर्गत हो। यदि आप एक गैर-मानक प्रीफ़िक्स का उपयोग करते हैं, तो आप इंस्टॉलेशन के लिए उपयोग की जाने वाली Python पैकेज निर्देशिका बदलने के लिए ``-DCMAKE_INSTALL_PYTHON_PKG_DIR=`` विकल्प का उपयोग कर सकते हैं। उदाहरण के लिए: ```bash cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/home/leo -DZ3_BUILD_PYTHON_BINDINGS=ON -DCMAKE_INSTALL_PYTHON_PKG_DIR=/home/leo/lib/python3.x/site-packages ``` यदि आपको गैर-मानक प्रीफ़िक्स में इंस्टॉल करने की आवश्यकता है, तो एक बेहतर तरीका [Python वर्चुअल एनवायरनमेंट](https://virtualenv.readthedocs.org/en/latest/) का उपयोग करना और वहाँ Z3 इंस्टॉल करना है। Windows पर, Visual C++ नेटिव कमांड बिल्ड एनवायरनमेंट के अंदर बिल्ड करना याद रखें। ध्यान दें कि ``build/python/z3`` डायरेक्टरी उस स्थान से सुलभ होनी चाहिए जहाँ Python का उपयोग Z3 के साथ किया जाता है और इसके लिए आवश्यक है कि ``libz3.dll`` पाथ में हो। ```bash virtualenv venv source venv/bin/activate cmake -S . -B build -DCMAKE_INSTALL_PREFIX=$VIRTUAL_ENV -DZ3_BUILD_PYTHON_BINDINGS=ON cmake --build build --parallel $(nproc) cmake --install build # You will find Z3 and the Python bindings installed in the virtual environment venv/bin/z3 -h ... python -c 'import z3; print(z3.get_version_string())' ... ``` उदाहरणों के लिए [``examples/python``](https://github.com/z3prover/z3/blob/master/examples/python) देखें। ### ``Julia`` Julia पैकेज [Z3.jl](https://github.com/ahumenberger/Z3.jl) Z3 के C API को रैप करता है। इसका एक पिछला संस्करण C++ API को रैप करता था: Julia बाइंडिंग्स को अपडेट करने और बनाने की जानकारी [src/api/julia](https://github.com/z3prover/z3/blob/master/src/api/julia) में पाई जा सकती है। ### ``WebAssembly`` / ``TypeScript`` / ``JavaScript`` संबंधित TypeScript टाइपिंग्स के साथ एक WebAssembly बिल्ड npm पर [z3-solver](https://www.npmjs.com/package/z3-solver) के रूप में प्रकाशित है। इन बाइंडिंग्स को बनाने की जानकारी [src/api/js](https://github.com/z3prover/z3/blob/master/src/api/js) में पाई जा सकती है। ### Smalltalk (``Pharo`` / ``Smalltalk/X``) प्रोजेक्ट [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) Z3 के C API के लिए एक Smalltalk इंटरफ़ेस प्रदान करता है। अधिक जानकारी के लिए, [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) देखें। ### AIX [AIX के लिए बिल्ड सेटिंग्स यहाँ वर्णित हैं।](https://github.com/Z3Prover/z3/pull/8113) ## सिस्टम अवलोकन  ## इंटरफ़ेस * डिफ़ॉल्ट इनपुट फ़ॉर्मेट [SMTLIB2](http://smtlib.cs.uiowa.edu) है * अन्य नेटिव फ़ॉरेन फ़ंक्शन इंटरफ़ेस: * [C++ API](https://z3prover.github.io/api/html/namespacez3.html) * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) ([pydoc फ़ॉर्मेट](https://z3prover.github.io/api/html/z3.html) में भी उपलब्ध) * [Rust](https://github.com/prove-rs/z3.rs) * C * OCaml * [Julia](https://github.com/ahumenberger/Z3.jl) * [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (Pharo और Smalltalk/X का समर्थन करता है) ## पावर टूल्स * [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) जिसे वर्तमान में ETH Zurich द्वारा विकसित किया जा रहा है # फ़ज़ बग दर्ज करने की नीति Z3 फ़ज़र्स के लिए एक लोकप्रिय लक्ष्य है। z3 और SMT सॉल्वरों में बग खोजने पर कई (सर्वोत्तम) पेपर प्रकाशित हुए हैं और निस्संदेह बग फ़ाइल/फ़िक्स अनुपात फ़ज़ टूल्स के मूल्य के लिए प्रकाशनों में साक्ष्य स्थापित करने में महत्वपूर्ण भूमिका निभाता है। दुर्भाग्य से, फ़ज़ बग्स को संबोधित करना ज़रूरी नहीं कि z3 के उन उपयोगों को आगे बढ़ाए जहाँ यह उपयोगकर्ताओं के लिए सबसे अधिक मायने रखता है, और उन्हें संबोधित करने के प्रयास ऐसी गतिविधियों से समय दूर ले जाते हैं। निदान और फ़िक्स के लिए कोडिंग एजेंट्स की तेज़ी से बढ़ती गुणवत्ता के साथ अब यह एक उचित अपेक्षा है कि फ़ज़ बग रिपोर्ट निदान और फ़िक्स पर ठोस प्रयास करें। प्रयासों को उस पर केंद्रित करने में मदद करने के लिए जो मायने रखता है, केवल रीप्रो से अधिक विश्लेषण के बिना फ़ज़ बग्स को बिना किसी और विचार के बंद किया जा सकता है।
