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

@@ -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

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}
 }
 

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",

pigosat_test.go

@@ -10,16 +10,16 @@ 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)
 	}
 	return int(x)
 }
 
 // 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,34 +74,34 @@ 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
 -1 0
 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,23 +122,23 @@ 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
 1 2 0
 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()