Home
last modified time | relevance | path

Searched refs:Boolector (Results 1 – 25 of 61) sorted by relevance

123

/dports/math/boolector/boolector-3.2.2/
H A DREADME.md2 …//dev.azure.com/Boolector/Boolector/_apis/build/status/Boolector.boolector?branchName=master)](htt…
4 # Boolector chapter
32 To build Boolector from source you need:
53 You can build Boolector with support for
60 Boolector has one other external dependency,
71 # Download and build Boolector
81 # Build Boolector
98 Then, from Boolector's root directory configure and build Boolector as follows:
107 Then build Boolector and issue:
123 project to link against Boolector.
[all …]
H A DCOMPILING_WINDOWS.md1 # Boolector installation steps on Windows
89 ## Building Boolector
91 ### Configuring Boolector's build environment argument
151 ### Obtaining Boolector argument
155 * `git clone https://github.com/Boolector/boolector`
158 ### Building Boolector argument
160 The following steps will allow you to build Boolector from the above clone:
170 # Download, patch and build Boolector's dependencies
184 # Build Boolector
201 ### Testing Boolector argument
[all …]
H A DTHANKS11 + Jannis Harder for fixing instructions and scripts for building Boolector for
15 - setting up a patch set for building Boolector for Windows in 2019
18 - fixing instructions and scripts for building Boolector for 64-bit Windows
20 - providing a Dockerfile for Boolector in 2020
21 - fixes/additions in Boolector's C and Python API in 2019 and 2020
H A Dazure-pipelines.yml50 displayName: 'Configure Boolector'
54 displayName: 'Build Boolector'
109 displayName: 'Configure Boolector'
113 displayName: 'Build Boolector'
/dports/math/boolector/boolector-3.2.2/doc/
H A Dpyboolector.rst1 Boolector Python API documentation
21 First, we create a Boolector instance:
35 :func:`~pyboolector.Boolector.Set_opt`.
38 :func:`~pyboolector.Boolector.Assert`.
47 :func:`~pyboolector.Boolector.Assume`.
52 :func:`~pyboolector.Boolector.Sat`.
64 :data:`~pyboolector.Boolector.SAT`,
70 :func:`~pyboolector.Boolector.Parse`.
102 :func:`~pyboolector.Boolector.Sat`,
292 Boolector can be configured either via :func:`~pyboolector.Boolector.Set_opt`,
[all …]
H A Dboolector.rst6 .. autoclass:: pyboolector.Boolector
12 :func:`~pyboolector.Boolector.Sat`.
17 :func:`~pyboolector.Boolector.Sat`.
22 :func:`~pyboolector.Boolector.Sat`.
27 :func:`~pyboolector.Boolector.Sat`.
35 The Boolector instance this node is associated with.
39 :exclude-members: Boolector, BoolectorNode
H A Dcboolector.rst1 Boolector C API documentation
21 First, we create a Boolector instance:
42 Boolector's internal design is motivated by hardware design.
129 Boolector supports printing models in its own format ("btor") or in
187 Boolector can be configured either via :c:func:`boolector_set_opt`,
211 like the original Boolector run.
242 Boolector instance by id and a given node's id.
256 Boolector's API, however, provides a richer set of operators for
267 Boolector simplifies expressions and the expression DAG by means of
277 Boolector not only simplifies expressions during construction
[all …]
H A Dindex.rst1 Welcome to Boolector's API documentation!
9 Boolector supports BTOR_, `SMT-LIB v1`_, and `SMT-LIB v2`_
12 This is the documentation of Boolector's public **C interface** and
14 For further information and the latest version of Boolector, please refer
/dports/math/boolector/boolector-3.2.2/contrib/docker/
H A DDOCKER.md1 # Using Boolector with Docker
3 Boolector has support for executing Boolector "input files" (e.g., `.smt2`)
16 git clone https://github.com/Boolector/boolector.git
29 UPSTREAM=https://github.com/Boolector/boolector/archive
43 # Assuming you're at the root of a Boolector clone
47 Alternatively, to see Boolector's help:
55 Boolector via your Docker `run` command.
68 # Assuming you're at the root of a Boolector clone
77 ## Using Docker to work with Boolector's Python API
79 The Boolector Docker image has been built with support for Boolector's Python
[all …]
H A DDockerfile8 # To make Boolector work under `musl`, Boolector is "patched" using the #
10 # Boolector to the minimum amount of libc that is exposed via MinGW. #
12 # For our purposes, restricting Boolector to the MinGW runtime also means #
13 # that Boolector builds and runs under `musl`. #
56 ARG UPSTREAM=https://github.com/Boolector/boolector/archive
59 # Which Boolector branch to build?
74 # Grab our Boolector tar (output is going to be "boolector-${BRANCH}".tar.gz)
102 # Validate our build of Boolector
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/what4-1.1/src/What4/Solver/
H A DBoolector.hs19 module What4.Solver.Boolector
20 ( Boolector(..)
48 data Boolector = Boolector deriving Show type
73 instance SMT2.SMTLib2Tweaks Boolector where
74 smtlib2tweaks = Boolector
83 SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction boolectorFeatures
92 -> (SMT2.Session t Boolector -> IO a)
95 withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction boolectorFeatures
102 instance SMT2.SMTLib2GenericSolver Boolector where
122 instance OnlineSolver (SMT2.Writer Boolector) where
[all …]
/dports/math/boolector/boolector-3.2.2/src/api/python/
H A Dpyboolector.pyx5 # This file is part of Boolector.
112 cdef Boolector btor
163 cdef Boolector btor
190 cdef Boolector btor
274 cdef public Boolector btor
634 cdef class Boolector: class
635 """ Boolector
695 btor = Boolector()
965 return Boolector(self)
1023 # Boolector options
[all …]
/dports/math/boolector/boolector-3.2.2/cmake/
H A DBoolectorConfig.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DCheckNoExportDynamic.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A Dgoogletest-download.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DCheckTimeUtils.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindCryptoMiniSat.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindLingeling.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindMiniSat.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindBtor2Tools.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindCaDiCaL.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DFindPicoSAT.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
H A DCheckSignals.cmake1 # Boolector: Satisfiablity Modulo Theories (SMT) solver.
5 # This file is part of Boolector.
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Provers/
H A DBoolector.hs14 module Data.SBV.Provers.Boolector(boolector) where
24 name = Boolector
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/what4-1.1/src/What4/
H A DSolver.hs36 , Boolector(..)
90 import What4.Solver.Boolector

123