All notable changes to this project will be documented in this file.
- Check variable addition overflow in debug
Var
andLit
constructors inconst
context- Implement
kani::Arbitrary
forTernaryVal
BinaryAdder
PB encoding- Initialize encodings when calling
reserve
- Include rustsat version in header
- Include C sources for newest version
- Unnecessary
mut
warning inclause![]
- Spelling
- Switch to nextest for running tests
- Bump a bunch of dependencies
- Cleanup file endings and trailing whitespace
- Set up pre-commit hooks
- Group dependabot PRs
- Clippy
- Do not run nextest if no tests
- Fix docsrs build
- External solver interface
- Batsat solver interface
- Generalize batsat interface
lit
method forVar
- Implement
Default
forTernaryVal
iter
method forAssignment
is_sat
forCnf
andAssignment
ergonomicsPropagate
traitCl
as light-weight DST for clauses- [breaking] Add
evaluate
, replacingis_sat
- Add generalized totalizer to capi
Cnf::clear
- Ladder at-most-one encoding
- Bitwise at-most-one encoding
- Commander at-most-one encoding
- Bimander at-most-one encoding
- Fix ambiguous links
- Mark
internals
properly - Fix typos
- Move main crate to project root
- Pedantic clippy
- [breaking] Breaking clippy suggestions
- [breaking] Rename constraint types
- Update dependencies
- Run clippy nightly on prs
- Update dependencies
- Clippy with most-recent nightly
- Set up nix dev shell and tools package
- [breaking] Make reading functions take reader by reference
- Use bindgen to generate solver bindings
- Paths relative to manifest
- Basic kani harnesses for
Var
andLit
- [breaking] Mark unchecked functions as unsafe
- Incremental precision in DPW
- Format vars and lits nicely with debug
- Make
Node
type (ofdbtotalizer
) opaque. This is technically a breaking change, but since theNode
type was never intended to be transparent, we are not treating it as one. If you are relying on having access to theNode
type, use the featureinternal
instead, but note that the internal API is unstable.
- Fix warnings
This release contains breaking changes. For detailed instructions on how to handle migration, please refer to the migration guide.
- Incorrect coarse_ub in dpw when unweighted
- Dynamic polynomial watchdog edge cases with < 2 inputs
- Clarify lit rep and relation to IPASIR/DIMACS
- Add missing documentation
- Fix broken links
- Migrate error handling to
anyhow
create - Move IPASIR bindings to separate crate
- Instance ergonomics for member variables
- Ergonomics for opb writing
- Ergonomics for dimacs writing
- Add
add_clause_ref
method toSolve
trait - Add
add_nary
function - Have file parsers take
BufRead
types Extend<&Clause>
for solvers- Catch memory out in solvers
- Catch memory outs in clause collector
- Parse external solver output
ipasir-display
feature
- Update to
pyo3
0.21 - Specify minimum rust version
- Add
BufWriter
when writing to file - Avoid unnecessary cloning
- Clean up control flow in solver methods
- Clean up control flow in dimacs parsing
- Factor out C-API
- Factor out Python API
- Internal
from_raw
methods for db totalizers - Thorough merge strategy for
NodeById
- Make opb defaults more like pbo competition specs
- Output opbs with
#variable
line
- Remove
weight_sum
field fromDbGte
- Disable cbindgen on docs.rs
- Mark required features in documentation on docs.rs
- Improve doc examples
- Add shields to READMEs
- Helpful shortcuts in instances and solver
- Index assignments by var and negate ternary vals
- Set var manager in SatInstance::from_iter
- Set vm correctly in SatInstance::from(Cnf)
- Coarse convergence bounds
- Link capi tests to archive libs
- Typo in capi
- Parse empty instances correctly
- Limited connections in node db
- Next value in db-referencing gtes
- (limited) python api documentation
- Python api expose lit, clause, cnf
- Python len and indexing support for clause and cnf
- Feature switch for python api
- Python iterators
- Totalizer and comparison operators in pyapi
- Expose all encodings in python api
- Extend internal node api
- Limited connections in node db
- Constant method for objective
- Allow cloning totalizer db
- Allow encodings to output straight to solvers
- Alternative totalizer implementation based on a totalizer database
- Dynamic polynomial watchdog encoing
- Changes to public API: changed some vectores to slices
- Changed internal variable/literal representation from
usize
tou32
Solver interfaces factored out into seperate crates. See detailed changes in GitHub Releases.
Updated initial version with working dependencies.
Yanked because of dependencies that don't exist anymore