From 5ad6cd72ea65e150c10336108f8b4687f6c39c8d Mon Sep 17 00:00:00 2001 From: William Schwartz Date: Sun, 15 Feb 2015 12:25:31 -0500 Subject: [PATCH] Fix #8 Create Pigosat-specific types for literals, clauses, etc. This makes it easier for users of the API to remember the relationships among the different argument and return-value types from the different Pigosat methods. Further, it makes maintenance easier: e.g., we can change the literal type from int32 to int64 just by changing the `type Literal int32` line. --- optimize.go | 4 ++-- optimize_test.go | 9 +++---- pigosat.go | 50 +++++++++++++++++++++++++------------- pigosat_test.go | 62 ++++++++++++++++++++++++------------------------ 4 files changed, 72 insertions(+), 53 deletions(-) diff --git a/optimize.go b/optimize.go index 198645d..96dd7c5 100644 --- a/optimize.go +++ b/optimize.go @@ -21,12 +21,12 @@ type Minimizer interface { // any set of constraints it likes as long as there is a unique integer K // such that k < K implies IsFeasible(k) returns status Unsatisfiable and // k >= K implies IsFeasible(k) returns status Satisfiable. - IsFeasible(k int) (status int, solution []bool) + IsFeasible(k int) (status Status, solution Solution) // RecordSolution allows types implementing this interface to store // solutions for after minimization has finished. Must be safe for parallel // use. - RecordSolution(k, status int, solution []bool) + RecordSolution(k int, status Status, solution Solution) } // Minimize finds the value min that minimizes Minimizer m. If the value can be diff --git a/optimize_test.go b/optimize_test.go index f784df7..4c51e82 100644 --- a/optimize_test.go +++ b/optimize_test.go @@ -19,8 +19,9 @@ type parameters struct { } type arguments struct { - k, status int - solution []bool + k int + status Status + solution Solution } type minimizer struct { @@ -40,7 +41,7 @@ func (m *minimizer) LowerBound() int { return m.params.lower } func (m *minimizer) UpperBound() int { return m.params.upper } -func (m *minimizer) IsFeasible(k int) (status int, solution []bool) { +func (m *minimizer) IsFeasible(k int) (status Status, solution Solution) { if k < from { m.t.Errorf("k too low: %d", k) } @@ -55,7 +56,7 @@ func (m *minimizer) IsFeasible(k int) (status int, solution []bool) { return } -func (m *minimizer) RecordSolution(k, status int, solution []bool) { +func (m *minimizer) RecordSolution(k int, status Status, solution Solution) { m.args <- arguments{k, status, solution} } diff --git a/pigosat.go b/pigosat.go index 0e3f940..4b35f32 100644 --- a/pigosat.go +++ b/pigosat.go @@ -28,14 +28,33 @@ var Version = SemanticVersion{0, 4, 0, "", 0} // PicosatVersion is the version string from the underlying Picosat library. const PicosatVersion = "960" +// Argument/result types for Pigosat methods. + +// Literals describe the variables in the formula. A positive value indicates +// the variable must be true; negative indicates it must be false. Variables +// should be indexed from one. The zero literal indicates the end of a clause. +type Literal int32 +// Clauses are slices of literals ORed together. An optional zero ends a clause, +// even in the middle of a slice; [1, 0, 2] is the same as [1, 0] is the same as +// [1]. +type Clause []Literal +// Formulas are slices of Clauses ANDed together. +type Formula []Clause +// Solutions are indexed by variable and return the truth value of the given +// variable. The zeroth element has no meaning and is always false. +type Solution []bool +// Statuses are returned by Pigosat.Solve to indicate success or failure. +type Status int + + // Return values for Pigosat.Solve's status. const ( // PicoSAT cannot determine the satisfiability of the formula. - Unknown int = C.PICOSAT_UNKNOWN + Unknown Status = C.PICOSAT_UNKNOWN // The formula is satisfiable. - Satisfiable int = C.PICOSAT_SATISFIABLE + Satisfiable Status = C.PICOSAT_SATISFIABLE // The formula cannot be satisfied. - Unsatisfiable int = C.PICOSAT_UNSATISFIABLE + Unsatisfiable Status = C.PICOSAT_UNSATISFIABLE ) // Struct Pigosat must be created with New and stores the state of the @@ -188,15 +207,14 @@ func (p *Pigosat) Seconds() time.Duration { return time.Duration(float64(C.picosat_seconds(p.p)) * float64(time.Second)) } -// AddClauses adds a list (as a slice) of clauses (the sub-slices). Each clause -// is a list of integers called literals. The absolute value of the literal i is +// AddClauses adds a slice of clauses, each of which are a slice of literals. +// Each clause is a list of integers called literals. The absolute value of the literal i is // the subscript for some variable x_i. If the literal is positive, x_i must end // up being true when the formula is solved. If the literal is negative, it must // end up false. Each clause ORs the literals together. All the clauses are -// ANDed together. Literals cannot be zero: a zero in the middle of a slice ends -// the clause, and causes AddClauses to skip reading the rest of the slice. Nil -// slices are ignored and skipped. -func (p *Pigosat) AddClauses(clauses [][]int32) { +// ANDed together. An optional zero ends a clause, even in the middle of a +// slice; [1, 0, 2] is the same as [1, 0] is the same as [1]. +func (p *Pigosat) AddClauses(clauses Formula) { defer p.ready(false)() var count int for _, clause := range clauses { @@ -226,7 +244,7 @@ func (p *Pigosat) Print(file *os.File) error { // blocksol adds the inverse of the solution to the clauses. // This private method does not acquire the lock or check if p is nil. -func (p *Pigosat) blocksol(sol []bool) { +func (p *Pigosat) blocksol(sol Solution) { n := C.picosat_variables(p.p) clause := make([]C.int, n+1) for i := C.int(1); i <= n; i++ { @@ -248,17 +266,17 @@ func (p *Pigosat) blocksol(sol []bool) { // for status, solution := p.Solve(); status == Satisfiable; status, solution = p.Solve() { // // Do stuff with status, solution // } -func (p *Pigosat) Solve() (status int, solution []bool) { +func (p *Pigosat) Solve() (status Status, solution Solution) { defer p.ready(false)() // int picosat_sat (PicoSAT *, int decision_limit); - status = int(C.picosat_sat(p.p, -1)) + status = Status(C.picosat_sat(p.p, -1)) if status == Unsatisfiable || status == Unknown { return } else if status != Satisfiable { panic(fmt.Errorf("Unknown sat status: %d", status)) } n := int(C.picosat_variables(p.p)) // Calling Pigosat.Variables deadlocks - solution = make([]bool, n+1) + solution = make(Solution, n+1) for i := 1; i <= n; i++ { // int picosat_deref (PicoSAT *, int lit); if val := C.picosat_deref(p.p, C.int(i)); val > 0 { @@ -272,17 +290,17 @@ func (p *Pigosat) Solve() (status int, solution []bool) { } // Res returns Solve's last status, or Unknown if Solve hasn't yet been called. -func (p *Pigosat) Res() (status int) { +func (p *Pigosat) Res() (status Status) { defer p.ready(true)() // int picosat_res (PicoSAT *); - return int(C.picosat_res(p.p)) + return Status(C.picosat_res(p.p)) } // BlockSolution adds a clause to the formula ruling out a given solution. It is // a no-op if p is nil and returns an error if the solution is the wrong // length. There is no need to call BlockSolution after calling Pigosat.Solve, // which calls it automatically for every Satisfiable solution. -func (p *Pigosat) BlockSolution(solution []bool) error { +func (p *Pigosat) BlockSolution(solution Solution) error { defer p.ready(false)() if n := int(C.picosat_variables(p.p)); len(solution) != n+1 { return fmt.Errorf("solution length %d, but have %d variables", diff --git a/pigosat_test.go b/pigosat_test.go index 01880e8..ad04fe6 100644 --- a/pigosat_test.go +++ b/pigosat_test.go @@ -10,8 +10,8 @@ import ( "time" ) -// abs takes the absolute value of an int32 and casts it to int. -func abs(x int32) int { +// abs takes the absolute value of an Literal and casts it to int. +func abs(x Literal) int { if x < 0 { return int(-x) } @@ -19,7 +19,7 @@ func abs(x int32) int { } // equal returns true if the two slices have the same contents. -func equal(x, y []bool) bool { +func equal(x, y Solution) bool { if len(x) != len(y) { return false } @@ -33,7 +33,7 @@ func equal(x, y []bool) bool { // Evaluate a formula when the variables take on the values given by the // solution. -func evaluate(formula [][]int32, solution []bool) bool { +func evaluate(formula Formula, solution Solution) bool { var c bool // The value for the clause var index int for _, clause := range formula { @@ -61,11 +61,11 @@ func evaluate(formula [][]int32, solution []bool) bool { } type formulaTest struct { - formula [][]int32 + formula Formula variables int // count clauses int // count - status int - expected []bool // solution + status Status + expected Solution onlyOne bool // No solution other than `expected` could satisfy dimacs string // DIMACS-format CNF } @@ -74,15 +74,15 @@ var formulaTests = []formulaTest{ // The first three tests are cribbed from Ilan Schnell's Pycosat. See // https://github.com/ContinuumIO/pycosat. In particular, these are from // commit d81df1e in test_pycosat.py. - 0: {[][]int32{{1, -5, 4}, {-1, 5, 3, 4}, {-3, -4}}, + 0: {Formula{{1, -5, 4}, {-1, 5, 3, 4}, {-3, -4}}, 5, 3, Satisfiable, - []bool{false, true, false, false, false, true}, false, + Solution{false, true, false, false, false, true}, false, `p cnf 5 3 1 4 -5 0 -1 3 4 5 0 -3 -4 0 `}, - 1: {[][]int32{{-1}, {1}}, + 1: {Formula{{-1}, {1}}, 1, 2, Unsatisfiable, nil, false, `p cnf 1 3 @@ -90,18 +90,18 @@ var formulaTests = []formulaTest{ 1 0 0 `}, - 2: {[][]int32{{-1, 2}, {-1, -2}, {1, -2}}, + 2: {Formula{{-1, 2}, {-1, -2}, {1, -2}}, 2, 3, Satisfiable, - []bool{false, false, false}, true, + Solution{false, false, false}, true, `p cnf 2 3 1 -2 0 -1 2 0 -1 -2 0 `}, // For testing that empty clauses are skipped and 0s end clauses - 3: {[][]int32{{1, -5, 4, 0, 9}, {-1, 5, 3, 4, 0, 100}, {}, {-3, -4, 0}, nil}, + 3: {Formula{{1, -5, 4, 0, 9}, {-1, 5, 3, 4, 0, 100}, {}, {-3, -4, 0}, nil}, 5, 3, Satisfiable, - []bool{false, true, false, false, false, true}, false, + Solution{false, true, false, false, false, true}, false, `p cnf 5 3 1 4 -5 0 -1 3 4 5 0 @@ -111,7 +111,7 @@ var formulaTests = []formulaTest{ // given 2011-01-24, pp. 23-48, // http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf // From "DIMACS example 1" - 4: {[][]int32{{-2}, {-1, -3}, {1, 2}, {2, 3}}, + 4: {Formula{{-2}, {-1, -3}, {1, 2}, {2, 3}}, 3, 4, Unsatisfiable, nil, false, `p cnf 3 6 -2 0 @@ -122,15 +122,15 @@ var formulaTests = []formulaTest{ 2 3 0 `}, // From "Satisfying Assignments Example 2" - 5: {[][]int32{{1, 2}, {-1, 2}, {-2, 1}}, + 5: {Formula{{1, 2}, {-1, 2}, {-2, 1}}, 2, 3, Satisfiable, - []bool{false, true, true}, true, + Solution{false, true, true}, true, `p cnf 2 3 1 2 0 1 -2 0 -1 2 0 `}, - 6: {[][]int32{{1, 2}, {-1, 2}, {-2, 1}, {-1}}, + 6: {Formula{{1, 2}, {-1, 2}, {-2, 1}, {-1}}, 2, 4, Unsatisfiable, nil, false, `p cnf 2 4 -1 0 @@ -138,7 +138,7 @@ var formulaTests = []formulaTest{ 1 -2 0 -1 2 0 `}, - 7: {[][]int32{{1, 2}, {-1, 2}, {-2, 1}, {-2}}, + 7: {Formula{{1, 2}, {-1, 2}, {-2, 1}, {-2}}, 2, 4, Unsatisfiable, nil, false, `p cnf 2 4 -2 0 @@ -147,7 +147,7 @@ var formulaTests = []formulaTest{ -1 2 0 `}, // From "ex3.cnf" - 8: {[][]int32{{1, 2, 3}, {1, 2, -3}, {1, -2, 3}, {1, -2, -3}, {4, 5, 6}, + 8: {Formula{{1, 2, 3}, {1, 2, -3}, {1, -2, 3}, {1, -2, -3}, {4, 5, 6}, {4, 5, -6}, {4, -5, 6}, {4, -5, -6}, {-1, -4}, {1, 4}}, 6, 10, Unsatisfiable, nil, false, `p cnf 6 10 @@ -163,10 +163,10 @@ var formulaTests = []formulaTest{ -1 -4 0 `}, // From "ex4.cnf" - 9: {[][]int32{{1, 2, 3}, {1, 2 - 3}, {1, -2, 3}, {1, -2, -3}, {4, 5, 6}, + 9: {Formula{{1, 2, 3}, {1, 2 - 3}, {1, -2, 3}, {1, -2, -3}, {4, 5, 6}, {4, 5, -6}, {4, -5, 6}, {4, -5, -6}, {-1, -4}, {-1, 4}, {-1, -4}}, 6, 11, Satisfiable, - []bool{false, false, false, true, true, false, false}, false, + Solution{false, false, false, true, true, false, false}, false, `p cnf 6 10 1 2 3 0 1 -2 3 0 @@ -190,8 +190,8 @@ func init() { } } -func wasExpected(t *testing.T, i int, p *Pigosat, ft *formulaTest, status int, - solution []bool) { +func wasExpected(t *testing.T, i int, p *Pigosat, ft *formulaTest, + status Status, solution Solution) { if status != ft.status { t.Errorf("Test %d: Expected status %d but got %d", i, ft.status, status) } @@ -229,8 +229,8 @@ func TestFormulas(t *testing.T) { // TestIterSolveRes tests that Pigosat.Solve works as an iterator and that // Pigosat.Res returns Solve's last status. func TestIterSolveRes(t *testing.T) { - var status, res int - var this, last []bool // solutions + var status, res Status + var this, last Solution for i, ft := range formulaTests { p, _ := New(nil) p.AddClauses(ft.formula) @@ -262,12 +262,12 @@ func TestIterSolveRes(t *testing.T) { } func TestBlockSolution(t *testing.T) { - var status int + var status Status for i, ft := range formulaTests { p, _ := New(nil) // Test bad inputs: one too short (remember sol[0] is always blank) - solution := make([]bool, p.Variables()) + solution := make(Solution, p.Variables()) if err := p.BlockSolution(solution); err == nil { t.Errorf("Test %d: Expected error when solution too short", i) } @@ -403,7 +403,7 @@ func TestUninitializedOrDeleted(t *testing.T) { b.delete() for name, p := range map[string]*Pigosat{"uninit": a, "deleted": b} { assertPanics(t, name, "AddClauses", func() { - p.AddClauses([][]int32{{1}, {2}}) + p.AddClauses(Formula{{1}, {2}}) }) assertPanics(t, name, "Variables", func() { p.Variables() }) assertPanics(t, name, "AddedOriginalClauses", func() { @@ -412,7 +412,7 @@ func TestUninitializedOrDeleted(t *testing.T) { assertPanics(t, name, "Seconds", func() { p.Seconds() }) assertPanics(t, name, "Solve", func() { p.Solve() }) assertPanics(t, name, "BlockSolution", func() { - p.BlockSolution([]bool{}) + p.BlockSolution(Solution{}) }) assertPanics(t, name, "Print", func() { p.Print(nil) }) } @@ -448,7 +448,7 @@ func TestPrint(t *testing.T) { // This is the example from the README. func Example_readme() { p, _ := New(nil) - p.AddClauses([][]int32{{1, 2}, {1}, {-2}}) + p.AddClauses(Formula{{1, 2}, {1}, {-2}}) fmt.Printf("# variables == %d\n", p.Variables()) fmt.Printf("# clauses == %d\n", p.AddedOriginalClauses()) status, solution := p.Solve()