Camada ("layer" in Portuguese) is a permissively licensed C++17 wrapper for multiple SMT solvers. It exposes a unified API across:

• Bitwuzla
• CVC5
• MathSAT
• STP
• Yices
• Z3

The library is designed to make solver switching cheap while still filling feature gaps in backends that are missing parts of the SMT-LIB surface.

Current encoded/common-layer features:

• floating-point fallback via bit-vector encoding
• array support, with some remaining tuple-related gaps
• tuple encoding layer: planned

Camada is intentionally a thin common layer:

• solver-specific wrappers live in the backend classes
• common behavior and missing-feature encodings live in the shared layer
• expressions and sorts are solver-owned handles

This makes it practical to:

• switch solvers without rewriting the calling code
• route unsupported features through common-layer encodings
• keep backend-specific quirks contained in one place

Camada uses CMake as its build system. Follow these steps to build and install the library:

• CMake (Version 3.15 or higher)
• C++ Compiler (Supporting C++17)
• Any of the supported solvers

# Clone the Camada repository
git clone https://github.com/mikhailramalho/camada.git
cd camada

# Run CMake to configure the project
cmake -S . -B build

# Build the library
cmake --build build

# Install Camada
cmake --install build

Useful configure options:

• -DCMAKE_BUILD_TYPE=Release
• -DCAMADA_DOWNLOAD_DEPENDENCIES=ALL
• -DCAMADA_SOLVER_<NAME>_ENABLE=ON/OFF to control enabled backends

Camada can now download and build missing solver dependencies during CMake configure, following the same general approach used in ESBMC:

cmake -S . -B build -DCAMADA_DOWNLOAD_DEPENDENCIES=ALL
cmake --build build

CAMADA_DOWNLOAD_DEPENDENCIES accepts three modes:

• OFF: do not download dependencies.
• ALL: download all supported solver dependencies.
• PERMISSIVE: download only solvers with permissive licenses (Bitwuzla, CVC5, STP, and Z3).

Downloaded sources and locally installed solver artifacts are stored under <build-dir>/deps/src and <build-dir>/deps/install.

When CMake downloads dependencies itself:

• Bitwuzla uses the prebuilt static release archive from 0.9.0.
• Z3 uses the prebuilt release archive from z3-4.16.0.
• CVC5 uses the prebuilt static release archive from cvc5-1.3.3.
• Yices uses a source build.
• GMP uses a source build when it is needed by downloaded dependencies and no suitable staged copy is already available.
• MathSAT uses the vendor-provided prebuilt archive from 5.6.15.
• STP still falls back to a source build. The 2.3.4_cadical GitHub release only ships a standalone stp executable, not the headers and libraries that Camada needs to link against the STP C++ API.
• CryptoMiniSat and Minisat still build from source as part of the STP dependency chain.

The <build-dir>/deps/install directory will contain the staged solver headers, libraries, and auxiliary artifacts, and Camada will use them from this location during the build.

¹ fp.fma and fp.rem are bit-blasted when using MathSAT because it does not support these operations natively. ROUND_TO_AWAY is also not supported by the native MathSAT floating-point API and aborts with an error if requested.

Camada currently provides public APIs for:

• booleans
• bit-vectors
• integers and reals on supporting backends
• floating-point
• rounding modes
• arrays
• uninterpreted functions on supporting backends
• incremental solving (push/pop)
• model queries for supported value kinds

Still not implemented:

• tuples

Partially backend-dependent:

• quantifiers
  • supported on Bitwuzla, CVC5, and Z3
  • implemented but still unreliable on MathSAT in the current setup
  • unsupported on STP and Yices
• integers/reals
  • supported on CVC5, MathSAT, Yices, and Z3
  • unsupported on Bitwuzla and STP
• uninterpreted functions
  • supported on Bitwuzla, CVC5, MathSAT, Yices, and Z3
  • unsupported on STP

Array support is currently partial in the larger structured-data sense:

• plain SMT arrays are supported
• backend-specific array gaps such as Array<Idx, Bool> are handled
• arrays of tuples remain part of the unfinished tuple work

Expression and sort handles are solver-owned. Any SMTExprRef or SMTSortRef obtained from a solver becomes invalid after:

• solver->reset()
• solver destruction

Handles must not be reused across those boundaries.

If a backend lacks native floating-point support, Camada can encode FP operations through bit-vectors in the common layer.

This behavior can also be forced on supported solvers through:

solver->useCamadaFP = true;

This is useful for:

• backend parity testing
• benchmarking the common FP encoding layer
• working around backend-specific native-FP gaps

Camada also smooths over backend quirks where practical. For example:

• MathSAT and STP now lower Array<Idx, Bool> through backend Array<Idx, BV1> representations internally
• Yices constant arrays use a backend-native lambda encoding instead of a full store chain
• MathSAT native FP still falls back for unsupported operations such as fp.rem

Camada does some solver-local caching, but it is intentionally narrow.

The goal is to keep the wrapper lightweight, not to implement a full-blown global expression cache for every sort and node shape. The built-in caching is focused on cases where reuse is very frequent and the cache overhead is low, such as:

• canonical sorts per solver generation
• common symbols
• boolean constants
• a small set of high-hit-rate bit-vector and floating-point helper constants

This means Camada does not try to intern every generated expression or sort. If a client needs broader structural caching, it is expected to build that at a higher layer on top of Camada, with the application owning the larger expression cache while Camada stays focused on backend adaptation and common-layer encodings.

Camada is designed as a wrapper library to simplify the usage of multiple SMT solvers. It provides a common interface for interacting with these solvers, allowing developers to switch between them seamlessly without changing their codebase.

Camada is based on the backend written for ESBMC so some of the implementation decisions were geared towards the verification of C programs, in particular, camada diverges from the SMT standard in:

• fp.neg supports negative NaNs. See Z3Prover/z3#4466 for a more detailed discussion.

#include <camada/camada.h>

int main() {
  // Create a solver instance (example using Z3)
  auto solver = camada::createZ3Solver();

  // This flag controls if you want to bit-blast floating-point, using Camada's internal bit-vector encoding
  // Floating-point bitblast is always enabled for solvers that don't support floating-point natively.
  /* solver->useCamadaFP = true; */

  // Add assertions, check satisfiability, etc.
  camada::SMTSortRef fp64sort = solver->mkFPSort(11, 52);
  camada::SMTExprRef roundingMode =
      solver->mkRM(camada::RM::ROUND_TO_MINUS_INF);

  camada::SMTExprRef x = solver->mkSymbol("x", fp64sort);
  camada::SMTExprRef y = solver->mkSymbol("y", fp64sort);
  camada::SMTExprRef r = solver->mkSymbol("r", fp64sort);

  camada::SMTExprRef xV = solver->mkFPFromBin(
      "0111011101100100111000010001001010111000010010111000100101001010", 11);
  camada::SMTExprRef yV = solver->mkFPFromBin(
      "0100100101001110001001011011001100110001111010011101010010000001", 11);
  camada::SMTExprRef rV = solver->mkFPFromBin(
      "0111111111101111111111111111111111111111111111111111111111111111", 11);

  camada::SMTExprRef xE = solver->mkEqual(x, xV);
  camada::SMTExprRef yE = solver->mkEqual(y, yV);
  camada::SMTExprRef rE = solver->mkEqual(r, rV);

  solver->addConstraint(xE);
  solver->addConstraint(yE);
  solver->addConstraint(rE);

  camada::SMTExprRef mul = solver->mkFPMul(x, y, roundingMode);
  camada::SMTExprRef eq = solver->mkEqual(mul, r);
  camada::SMTExprRef notEq = solver->mkNot(eq);

  solver->addConstraint(notEq);
  camada::checkResult result = solver->check();

  if (result == camada::checkResult::SAT) {
    /* Query the model for the value of the exprs */

    /* Dump the model */
    solver->dumpModel();

  } else if (result == camada::checkResult::UNSAT) {
    /* The formula is unsatisfiable */
  } else if (result == camada::checkResult::UNKNOWN) {
    /* Something went wrong when checking the formula, timeouts, etc. */
  }
}

The regression tests are also a good source of small usage examples:

• regression/simple.test.h
• regression/array.test.h
• regression/fp.test.h

Backend-specific feature coverage is also demonstrated in:

• regression/cvc5.test.cpp
• regression/mathsat.test.cpp
• regression/yices.test.cpp
• regression/z3.test.cpp

Camada includes a standalone benchmark driver:

• regression/bench/main.cpp
• scripts/compare-bench.py

Typical local workflow:

python3 scripts/compare-bench.py ./build/bin/camada-bench 200

This runs repeated pinned benchmark samples, computes medians, and compares the result against scripts/baseline.txt.