Build and run Primo

Build and run Primo#

Start here to build Primo and solve a small SMT-LIB problem. Commands below run from the repository root. The capability map describes what this version accepts and where solving can return unknown.

Prerequisites#

Use a Unix-like environment with a C++20 compiler, CMake 3.20 or newer, GNU Make, Git, Python 3, and a shell. Dependency bootstrap needs network access. The documentation build also needs Python’s venv and pip modules. Linux is the environment used for this manual’s verification; this is not a claim of validation on every platform.

Build#

git clone https://github.com/primo-solver/primo.git
cd primo
make build
./build/primo --version

make build installs CLI11, CaDiCaL and GMP under contrib/local, configures CMake in build/, and builds build/primo. It selects a Release build unless you have configured another build type. No parser generator is required. Reference solvers and fuzzers are optional tools, not prerequisites for this first solve. See Makefile, CMakeLists.txt, and the GMP installer for the actual build paths.

Record --version when sharing results: it identifies the revision and build configuration. Re-run make build after changing the source.

If GMP bootstrap reports Network is unreachable, the failure is downloading the archive, before compilation. The installer tries GNU’s download server, then the kernel.org GNU mirror if the first download fails or has a bad checksum. Downloads of the pinned GMP 6.3.0 release are checked against its SHA-256 digest before extraction; other versions do not yet have pinned digests. Each connection/read has a 30-second socket timeout, which is not a total download deadline. If both sources fail, the error lists both failures. To select an accessible release archive explicitly, run python3 contrib/install_gmp.py --url https://your-mirror.example/gmp-6.3.0.tar.xz. An explicit URL disables fallback and still checks the pinned release digest. An existing extracted source directory is reused without another download; download verification does not revalidate that directory.

CMake also supports a backend-disabled scaffold (set IPASIR_UP_INCLUDE_DIR=OFF and CADICAL_LIBRARY=OFF). It compiles the non-backend infrastructure but supplies no SAT solver. Both integer solving and retained solving require an IPASIR backend; this build is not a solving fallback.

First solve#

This problem is contradictory: equal arguments must give equal results for f, while the last assertion requires different results.

(set-logic QF_UF)
(declare-sort U 0)
(declare-const a U)
(declare-const b U)
(declare-fun f (U) U)
(assert (= a b))
(assert (distinct (f a) (f b)))
(check-sat)
(exit)

Run the included file:

./build/primo --quiet docs/examples/first-solve.smt2

Expected standard output:

unsat

--quiet suppresses the startup banner. Answers go to standard output; diagnostics and requested statistics go to standard error. A file can contain several check-sat commands. With no filename, Primo reads commands from stdin and flushes each response as it becomes available:

./build/primo --quiet < docs/examples/first-solve.smt2

The session guide shows how to add and retract assertions during one process. The model guide shows how to inspect a satisfying assignment. Use the command-line reference for options, output and exit-code conventions.

Check the build and examples#

make test
python3 scripts/check_doc_examples.py --solver ./build/primo

The example check verifies the small programs used in this manual. It is not a replacement for solver fuzzing or independent model validation. Contributor requirements are in Correctness before performance.

Read the book locally#

make docs-serve

Open http://localhost:8000. This first runs the strict documentation build, then serves the current manual from docs/_build/html. Stop the server with Ctrl-C. For just the HTML, run make docs and open docs/_build/html/index.html.

The generated book does not require a running solver or database service. Use make docs-site to build both current and historical books and assemble the publication artifact in docs/_build/site. Local preview and build commands do not deploy it.