Note

This project is currently in low maintenance mode. We will still fix bugs and accept pull requests, but we will not actively develop new features.

LogicBlocks - A Interface Library for SAT/SMT Abstractions written in C++

A interface library for the abstraction of several methods of interaction with SAT/SMT Solvers developed by the Chair for Design Automation at the Technical University of Munich.

LogicBlocks are built in the style of the z3 bindings for C++. The library is designed to offer a simpler way to encode SAT/SMT problems in C++ code and hand it off to several different solvers or text exports. Note that at the moment the z3 integration is mostly working, as is export in DIMACs and the SMTLibv2 format.

If you have any questions, feel free to contact us via quantum.cda@xcit.tum.de or by creating an issue on GitHub.

Usage

LogicBlocks are designed to be used as a submodule in conjunction with git and CMake.

• In order to start using LogicBlocks, first the submodule needs to be added:

git submodule add https://github.com/cda-tum/LogicBlocks.git
git submodule update --init --recursive

Then, to include the necessary files in your project the following lines need to be added to your CMakeLists.txt:

add_subdirectory("${PROJECT_SOURCE_DIR}/LogicBlocks" "LogicBlocks")

As well as linking to the library:

target_link_libraries(${PROJECT_NAME} PUBLIC logicblocks::Logic)

Finally, in all files where LogicBlocks are needed, the required files need to be included:

#include "LogicBlocks/LogicBlock.hpp"

Examples

A minimal working example needs at least some kind of LogicBlock and some LogicTerms: The following example initializes a SMTLibv2 LogicBlock (supporting export to SMTLibv2 Format) and initializes two variables a and b with the respective LogicTerms, by creating variables from the LogicBlock.

#include "LogicBlocks/LogicBlock.hpp"
#include "LogicTerm/LogicTerm.hpp"

using namespace logicbase;
int main() {
   SMTLogicBlock logicBlock();

    LogicTerm a = logicBlock.makeVariable("a", CType::BOOL);
    LogicTerm b = logicBlock.makeVariable("b", CType::BOOL);

    logicBlock.assertFormula(a && b);
    logicBlock.produceInstance();
}

Then, assertFormula(LogicTerm) asserts a formula to the LogicBlock. Finally, produceInstance() produces an instance of all asserted formulas exported to SMTLibv2 format.

Structure

• LogicBlock - Contains the various interfaces for interacting with SAT/SMT Solvers.
  • LogicBlock.hpp - Contains the base classes, LogicBlock for encoding general SAT/SMT problems and LogicBlockOptimizer for encoding optimization problems.
  • Model.hpp - Contains the base class for models, optionally returned by SAT/SMT Solvers.
• LogicTerm/LogicTerm.hpp - Contains the main way of interacting and writing encodings of problems, the LogicTerm.
• Encodings/Encodings.hpp - Contain some different encodings for common problems, especially At most one and Exactly one encodings.

As of now there are several Theories besides pure SAT that are supported:

• Integer - Integer arithmetic and comparison, including +, -, /, *, <, >, <= and >=.
• Real - Real arithmetic and comparison, including +, -, /, *, <, >, <= and >=.
• Bitvector - Bitvector arithmetic and comparison, including +, -, /, *, <, >, <= and >=, and using BV_XOR, BV_AND and BV_OR bit wise operations on bitvectors.