Skip to content

Commit

Permalink
Fix #28: Rename AddClauses to Add
Browse files Browse the repository at this point in the history
You generally will end up writing p.Add(Formula{...}) anyway, so Add's intention
is clear when you read it in code.
  • Loading branch information
wkschwartz committed Jan 5, 2017
1 parent 46969a7 commit aeeff7d
Show file tree
Hide file tree
Showing 4 changed files with 43 additions and 45 deletions.
10 changes: 5 additions & 5 deletions assume.go
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ var cZero C.int = 0

// Assume adds a temporary unit clause, i.e., a clause containing the one
// literal you pass as an argument. An assumption remains valid after the next
// call to Solve returns until a call to AddClauses, Assume, or a second Solve.
// You can add arbitrary many assumptions before the next call to Solve.
// Methods FailedAssumptions, FailedAssumptions, MaxSatisfiableAssumptions, and
// call to Solve returns until a call to Add, Assume, or a second Solve. You can
// add arbitrary many assumptions before the next call to Solve. Methods
// FailedAssumptions, FailedAssumptions, MaxSatisfiableAssumptions, and
// NextMaxSatisfiableAssumptions operate on the current, valid assumptions.
func (p *Pigosat) Assume(lit Literal) {
defer p.ready(false)()
Expand Down Expand Up @@ -92,8 +92,8 @@ func (p *Pigosat) MaxSatisfiableAssumptions() []Literal {
// BlockSolution, which modifies the underlying formula (thus changing the
// result of AddedOriginalClauses), and then reassuming the solutions that were
// valid when you called NextMaxSatisfiableAssumptions. Use it as follows.
// First, set your formula and assumptions using AddClauses and Assume. Then
// iterate over the different maximal satisfiable subsets of assumptions with:
// First, set your formula and assumptions using Add and Assume. Then iterate
// over the different maximal satisfiable subsets of assumptions with:
// for mss := p.NextMaxSatisfiableAssumptions(); len(mss) > 0; mss = p.NextMaxSatisfiableAssumptions() {
// // Do stuff with mss
// }
Expand Down
18 changes: 9 additions & 9 deletions assume_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ func TestAssumptionsSucceeding(t *testing.T) {
for i, at := range successTests {
t.Run(fmt.Sprintf("successTests[%d]", i), func(t *testing.T) {
p, _ := New(nil)
p.AddClauses(formulaTests[0].formula)
p.Add(formulaTests[0].formula)

count := 0
for ; ; count++ {
Expand Down Expand Up @@ -80,7 +80,7 @@ func TestAssumptionsSucceeding(t *testing.T) {

func TestAssumptionsFailing(t *testing.T) {
p, _ := New(nil)
p.AddClauses(formulaTests[0].formula)
p.Add(formulaTests[0].formula)
p.Assume(3)
p.Assume(4)
p.Assume(5)
Expand Down Expand Up @@ -122,7 +122,7 @@ func TestCrashOnUnsatResetFailedAssumptions(t *testing.T) {
run := func(name string, f func(*Pigosat)) {
t.Run(name, func(t *testing.T) {
p, _ := New(nil)
p.AddClauses(ft.formula)
p.Add(ft.formula)
p.Assume(3)
p.Assume(4)
p.Assume(5)
Expand Down Expand Up @@ -153,8 +153,8 @@ func TestCrashOnUnsatResetFailedAssumptions(t *testing.T) {
t.Fatalf(err.Error())
}
})
run("AddClauses-empty", func(p *Pigosat) { p.AddClauses(Formula{{3}}) })
run("AddClauses-nil", func(p *Pigosat) { p.AddClauses(Formula{nil}) })
run("Add-empty", func(p *Pigosat) { p.Add(Formula{{3}}) })
run("Add-nil", func(p *Pigosat) { p.Add(Formula{nil}) })
}

// TestNextMaxSatisfiableAssumptionsAsIterator tests that NextMaxSatisfiableAssumptions
Expand All @@ -163,7 +163,7 @@ func TestCrashOnUnsatResetFailedAssumptions(t *testing.T) {
func TestNextMaxSatisfiableAssumptionsAsIterator(t *testing.T) {
var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
p, _ := New(nil)
p.AddClauses(formula)
p.Add(formula)
p.Assume(1)
p.Assume(-2)
p.Solve()
Expand All @@ -183,7 +183,7 @@ func TestNextMaxSatisfiableAssumptionsAsIterator(t *testing.T) {
func ExamplePigosat_Assume() {
var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
p, _ := New(nil)
p.AddClauses(formula)
p.Add(formula)
fmt.Println("Formula:", formula)
solution, status := p.Solve()
fmt.Println("No assumptions:", status, "solution ==", solution)
Expand All @@ -198,7 +198,7 @@ func ExamplePigosat_Assume() {
solution, status = p.Solve()
fmt.Println(" ", status, "solution ==", solution)

// Calls to p.AddClauses or p.Assume cancel assumptions 1 and -2
// Calls to p.Add or p.Assume cancel assumptions 1 and -2
// immediately, or a second call to p.Solve also cancels the assumptions.
p.Assume(-3)
solution, status = p.Solve()
Expand Down Expand Up @@ -228,7 +228,7 @@ func ExamplePigosat_Assume() {
// Unknown status
// Assumptions are valid but p.Solve returns no Solution assignment. The
// solver knowns the status is Unknown until a call to p.Assume,
// p.AddClauses, or p.Solve resets the assumptions.
// p.Add, or p.Solve resets the assumptions.

// Output:
// Formula: [[1 2 3] [1 2] [2 3]]
Expand Down
16 changes: 8 additions & 8 deletions pigosat.go
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@
// The argument to New allows advanced users to pass in an Option instance. See
// its documentation for details. Next, supply the Pigosat instance with your
// formula:
// p.AddClauses(Formula{{1, 2, -3}, {3, 4}})
// p.Add(Formula{{1, 2, -3}, {3, 4}})
// (This is also a correct way to write the formula for PiGoSAT.)
//
// Calling p.Solve() returns two objects. The second is a Status object, one of
Expand Down Expand Up @@ -330,13 +330,13 @@ func (p *Pigosat) Seconds() time.Duration {
return time.Duration(float64(C.picosat_seconds(p.p)) * float64(time.Second))
}

// AddClauses appends a slice of Clauses to p's existing formula. See the
// documentation for Literal, Clause, and Formula to understand how p.Solve
// will interpret the formula.
// Add appends a slice of Clauses to p's existing formula. See the documentation
// for Literal, Clause, and Formula to understand how p.Solve will interpret the
// formula.
//
// A zero in a clause terminates the clause even if the zero is not at the end
// of the slice. An empty clause always causes the formula to be unsatisfiable.
func (p *Pigosat) AddClauses(clauses Formula) {
func (p *Pigosat) Add(clauses Formula) {
defer p.ready(false)()
var count int
for _, clause := range clauses {
Expand Down Expand Up @@ -386,9 +386,9 @@ func (p *Pigosat) blocksol(sol Solution) {
// Unsatisfiable, Satisfiable, or Unknown. If satisfiable, return a slice
// indexed by the variables in the formula (so the first element is always
// false). Assigning these boolean values to the variables will satisfy the
// formula and assumptions that p.AddClauses and p.Assume have added to the
// Pigosat object. See the documentation for Assume regarding when assumptions
// are valid.
// formula and assumptions that p.Add and p.Assume have added to the Pigosat
// object. See the documentation for Assume regarding when assumptions are
// valid.
//
// Solve can be used like an iterator, yielding a new solution until there are
// no more feasible solutions:
Expand Down
44 changes: 21 additions & 23 deletions pigosat_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ func TestFormulas(t *testing.T) {
for i, ft := range formulaTests {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
p, _ := New(nil)
p.AddClauses(ft.formula)
p.Add(ft.formula)
solution, status := p.Solve()
wasExpected(t, p, &ft, status, solution)
})
Expand All @@ -243,7 +243,7 @@ func TestIterSolveRes(t *testing.T) {
for i, ft := range formulaTests {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
p, _ := New(nil)
p.AddClauses(ft.formula)
p.Add(ft.formula)
count := 0
if res = p.Res(); res != Unknown {
t.Errorf("Res = %d before Solve called", res)
Expand Down Expand Up @@ -293,7 +293,7 @@ func TestBlockSolution(t *testing.T) {

// Solve should not return ft.expected if it's blocked
if ft.status == Satisfiable && !ft.onlyOne {
p.AddClauses(ft.formula)
p.Add(ft.formula)
if err := p.BlockSolution(ft.expected); err != nil {
t.Errorf("Unexpected error from BlockSolution: %v", err)
}
Expand Down Expand Up @@ -324,7 +324,7 @@ func TestPropLimit(t *testing.T) {
seenUn, seenSat := false, false
for limit := uint64(1); limit < 20; limit++ {
p, _ := New(&Options{PropagationLimit: limit})
p.AddClauses(ft.formula)
p.Add(ft.formula)
solution, status := p.Solve()
if status == Unknown {
seenUn = true
Expand Down Expand Up @@ -368,7 +368,7 @@ func TestOutput(t *testing.T) {
if err != nil {
t.Fatal(err)
}
p.AddClauses(ft.formula)
p.Add(ft.formula)
p.Solve()
// Ensure that closing p doesn't close the OutputFile.
p.Delete()
Expand All @@ -390,16 +390,16 @@ func TestMeasureAllCalls(t *testing.T) {
for i, ft := range formulaTests {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
p, _ := New(nil)
p.AddClauses(ft.formula)
p.Add(ft.formula)
if p.Seconds() != 0 {
t.Errorf("Seconds without MeasureAllCalls should not "+
"measure AddClauses, but p.Seconds() == %v", p.Seconds())
"measure Add, but p.Seconds() == %v", p.Seconds())
}
p, _ = New(&Options{MeasureAllCalls: true})
p.AddClauses(ft.formula)
p.Add(ft.formula)
if p.Seconds() == 0 {
t.Errorf("Seconds with MeasureAllCalls should measure "+
"AddClauses, but p.Seconds() == %v", p.Seconds())
"Add, but p.Seconds() == %v", p.Seconds())
}
})
}
Expand All @@ -424,9 +424,7 @@ func TestUninitializedOrDeleted(t *testing.T) {
b.Delete()
for name, p := range map[string]*Pigosat{"uninit": a, "deleted": b} {
t.Run(name, func(t *testing.T) {
assertPanics(t, "AddClauses", func() {
p.AddClauses(Formula{{1}, {2}})
})
assertPanics(t, "Add", func() { p.Add(Formula{{1}, {2}}) })
assertPanics(t, "Variables", func() { p.Variables() })
assertPanics(t, "AddedOriginalClauses", func() {
p.AddedOriginalClauses()
Expand Down Expand Up @@ -514,7 +512,7 @@ func TestPrint(t *testing.T) {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
buf.Reset()
p, _ := New(nil)
p.AddClauses(ft.formula)
p.Add(ft.formula)
err := p.Print(&buf)
if err != nil {
t.Errorf("Output file not written to: err=%v", err)
Expand All @@ -534,7 +532,7 @@ func TestWriteClausalCore(t *testing.T) {
for i, ft := range formulaTests {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
p, _ := New(&Options{EnableTrace: true})
p.AddClauses(ft.formula)
p.Add(ft.formula)
_, status := p.Solve()

buf.Reset()
Expand Down Expand Up @@ -564,7 +562,7 @@ func TestWriteTrace(t *testing.T) {
for i, ft := range formulaTests {
t.Run(fmt.Sprintf("formulaTests[%d]", i), func(t *testing.T) {
p, _ := New(&Options{EnableTrace: true})
p.AddClauses(ft.formula)
p.Add(ft.formula)
_, status := p.Solve()

buf.Reset()
Expand Down Expand Up @@ -639,7 +637,7 @@ func Example() {
// documentation.
defer p.Delete()

p.AddClauses(Formula{{1, 2, -3}, {3, 4}})
p.Add(Formula{{1, 2, -3}, {3, 4}})
fmt.Printf("Number of variables == %d\n", p.Variables())
fmt.Printf("Number of clauses == %d\n", p.AddedOriginalClauses())
solution, status := p.Solve()
Expand Down Expand Up @@ -680,7 +678,7 @@ func BenchmarkSolve(b *testing.B) {
b.ResetTimer()
for i := 0; i < b.N; i++ {
p, _ := New(nil)
p.AddClauses(formula)
p.Add(formula)
p.Solve()
}
}
Expand All @@ -694,19 +692,19 @@ func BenchmarkCreate(b *testing.B) {
}
// Shut the compiler up about not using p.
b.StopTimer()
p.AddClauses(formulaTests[benchTest].formula)
p.Add(formulaTests[benchTest].formula)
}

// BenchmarkAddClauses measures how long it takes to add a formula to a Pigosat
// object that already exists.
func BenchmarkAddClauses(b *testing.B) {
// BenchmarkAdd measures how long it takes to add a formula to a Pigosat object
// that already exists.
func BenchmarkAdd(b *testing.B) {
b.StopTimer()
formula := formulaTests[benchTest].formula
b.ResetTimer()
for i := 0; i < b.N; i++ {
p, _ := New(nil)
b.StartTimer()
p.AddClauses(formula)
p.Add(formula)
b.StopTimer()
}
}
Expand All @@ -719,7 +717,7 @@ func BenchmarkBlockSolution(b *testing.B) {
b.ResetTimer()
for i := 0; i < b.N; i++ {
p, _ := New(nil)
p.AddClauses(formulaTests[benchTest].formula)
p.Add(formulaTests[benchTest].formula)
b.StartTimer()
p.BlockSolution(solution)
b.StopTimer()
Expand Down

0 comments on commit aeeff7d

Please sign in to comment.