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
During private release preparation, cloning requires repository access. An authenticated SSH clone works too.
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.
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 Contributing to Primo: draft.
Read the book locally#
make docs-serve
Open http://localhost:8000. This first runs the strict documentation build,
then serves 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. Website deployment remains part of the publication plan.