v1.0.0b
Pre-release
Pre-release
v1.0 beta
This is hopefully a feature-complete version 1.0. Ideally PiGoSAT's API will now be stable, and I promise it will be once it's out of beta. It will live in beta for awhile until I get some feedback or I get tired of it being in beta.
Special thanks to @justinfx for all his help.
Add support for
- Writing traces #13 (thanks to @justinfx)
- Making and analyzing assumptions #12 (thanks to @justinfx)
- Deleting
Pigosat
objects manually #18
Backward incompatible changes
- Renamed
AddClauses
toAdd
#28 - Switched order of
Solve
's return values #10 (this also resulted in switching the order of arguments and return values forMinimizer
) - Removed call to
BlockSolution
fromSolve
#22 - Renamed
NewPigosat
toNew
#7 - PiGoSAT-specific types for
Literal
,Clause
,Formula
#8 #9
Updating client code
Before
p := pigosat.New(nil)
p.AddClauses(pigosat.Formula{{1, 2}, {2, 3}, {1}})
for status, solution := p.Solve(); status == pigosat.Satisfiable; status, solution = p.Solve() {
// process solutions here
}
After
Most importantly, you need to
- use
Add
instead ofAddClauses
, - switch the order of solution and status, and
- explicitly call
p.BlockSolution(solution)
.
Callingp.Delete()
when you're done withp
is only important in library code or if you're generating a lot ofpigosat.Pigosat
objects. This is because the garbage collector can callp.Delete()
, but the GC may not get around to doing so before the program exits.
p := pigosat.New(nil)
defer p.Delete() // Not necessary in casual or one-off use
p.Add(pigosat.Formula{{1, 2}, {2, 3}, {1}})
for solution, status := p.Solve(); status == pigosat.Satisfiable; solution, status = p.Solve() {
// process solutions here
p.BlockSolution(solution)
}
Bug fixes
- Accept empty clauses #14 #15 (thanks to @sacado)
- Panic when trying to use uninitialized or deleted Pigosat objects #6