Tags

v0.1.7

v0.1.7 — reset global stats on PbSolver construction and reset

rs::stats is process-global, but its counters gate restart and database-cleanup
scheduling against thresholds that restart with each rs::Solver. Because
reset() builds a fresh solver without clearing them, an identical query took a
different search path depending on what the process had solved earlier. The
counters are now reset alongside the Impl, and STARTTIME / RUNSTARTTIME are
stamped (the library never set them). Includes the v0.1.6 assumption fix.

PIC + hidden visibility + no boost_iostreams + dual toolchain
(gcc/libstdc++, clang/libc++) as before.

v0.1.6

v0.1.6 — fix SAT returned with assumptions violated

Solver::solve() resets its assumption bookkeeping as if the search were at
decision level 0, but PbSolver::solve() re-enters it on transient states
(notably INPROCESSED, which does not backjump). The reset could then land at
a nonzero decision level, letting assumption literals be skipped and the
search finish in a full assignment that falsifies them — solve() returning
SAT with assumptions violated. setAssumptions() is now called inside the
re-entry loop, which backjumps to level 0 and restores the precondition.

Affects every consumer that solves under assumptions; solving without
assumptions was never impacted. PIC + hidden visibility + no boost_iostreams
+ dual toolchain (gcc/libstdc++, clang/libc++) as in v0.1.5.

v0.1.5

v0.1.5 — silence stdout chatter

PbSolver now forces RoundingSat verbosity=0, so the library no longer
writes progress lines (c #Conflicts, c INPROCESSING, c Inconsistent
input constraint, ...) to the embedder's stdout. PIC + hidden visibility
+ no boost_iostreams + dual toolchain (gcc/libstdc++, clang/libc++) as
in v0.1.4.

v0.1.4

v0.1.4 — drop boost_iostreams from released library

Release artifacts now built with -Diostreams=OFF: the in-process API
never uses compressed-file I/O, so libroundingsat_lib.a no longer links
or references boost_iostreams. Consumers can drop -lboost_iostreams.
PIC + hidden visibility + dual toolchain (gcc/libstdc++, clang/libc++)
as before.

v0.1.3

v0.1.3 — hidden visibility, export only rs::api::PbSolver

Library built with -fvisibility=hidden; only the RS_API-annotated
rs::api::PbSolver surface is exported, RoundingSat internals are hidden.
PIC + dual-toolchain (gcc/libstdc++, clang/libc++) as in v0.1.2.

v0.1.2

v0.1.2 — PIC library build

Both toolchain variants of libroundingsat_lib.a are now built with
position-independent code, so the archive can be linked into a shared
library. Supersedes v0.1.1, whose artifacts were built without -fPIC.

v0.1.1

v0.1.1 — dual-toolchain library release

Adds a clang/libc++ build of libroundingsat_lib.a alongside the
gcc/libstdc++ one. The two C++ runtimes are not ABI compatible across
the std::string/std::vector public API, so consumers pick the archive
matching their own toolchain. Public PbSolver API surface is unchanged.

v0.1.0

v0.1.0 — first release of the in-process PbSolver API

Static library libroundingsat_lib.a plus the public PbSolver.hpp header
(Boost-free public surface) and the internal headers it transitively
requires, for embedding RoundingSat's PB solver in-process.

cp25-experiments

pb24-log

monthly.21.03

proofanalyze

stat_bound_development

objective_stats

jik-restarts

pure_lits_print

prefetch

roundingsat2-oldpropagation

roundingsat2-bnn

pure_lits