Boolector
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It supports the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a rich C and Python API and supports incremental solving, both with the SMT-LIB commands push and pop, and as solving under assumptions. The documentation of its API can be found here.
Now that’s the definition, but we as developers don’t really care about that. Let me just make it simple. Boolector is something of a solver that check on random values of variable with provided constraints (like x>0 or x<100) and assert it as SAT (satisfiable: fancy way of saying possible) or UNSAT (Well I have smart audience!) or other.
To install it on Linux :
# Download and build Boolector
git clone https://github.com/boolector/boolector
cd boolector
# Download and build Lingeling
./contrib/setup-lingeling.sh
# Download and build BTOR2Tools
./contrib/setup-btor2tools.sh
# Configure Boolector
./configure.sh
chmod -R o+rw .
#Build Boolector
cd build/
make
#Global Installation
sudo make install If you see an error for libstdc++:
sudo yum install glibc-static libstdc++-static -y;Then
try:=>($locate boolector.h)(should show you the path if not, no worries)
#For globalisation of all header files
setenv CPATH "/usr/local/include/boolector/:$PATH"
Now create a directory dir_name
$ mkdir dir_name
$ cd dir_name
$ code . (to open visual studio code)
Press Ctrl+Shift+P
type cmake:Quick Start
Select C++ Version (if installed otherwise you would have to install SIMPLE)
Type in project name pr_name
Now, two files will be created, one name main.cpp and CMakeList.txt
in CMakeList.txt
add these two statements
find_package will look for package Boolector in your local system.
target_link_library will link libraries of boolector in Boolector package with your target (pr_name).
find_package(Boolector)
target_link_libraries(<your_target> Boolector::boolector)
Let’s write our very first helloworld program.
Save it
Now let’s go back to our terminal. Get in our dir_name.
$ cd dir_name
create a new directoy.
$ mkdir build/
$ cd build/
Compile our project
$ cmake ..
$ make
Execute Object File
$ ./HelloWorldZ
Voila!!
For next part click here.
