Skip to content

Commit 3a1a4d9

Browse files
committed
Fix the strashCode; add benchmark
Thanks to Evan Cordell who spotted a problem with the strash code colliding. Interesting, as it has a strong impact on the logic/c performance (but none on solving). See #17
1 parent a1a5030 commit 3a1a4d9

File tree

2 files changed

+32
-1
lines changed

2 files changed

+32
-1
lines changed

logic/c.go

+1-1
Original file line numberDiff line numberDiff line change
@@ -376,5 +376,5 @@ func (p *C) grow() {
376376
}
377377

378378
func strashCode(a, b z.Lit) uint32 {
379-
return uint32((a << 13) * b)
379+
return uint32(^(a << 13) * b)
380380
}

logic/c_test.go

+31
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import (
1010
"testing"
1111

1212
"github.com/go-air/gini"
13+
"github.com/go-air/gini/gen"
1314
"github.com/go-air/gini/logic"
1415
"github.com/go-air/gini/z"
1516
)
@@ -149,3 +150,33 @@ func ExampleC_equiv() {
149150
}
150151
//Output: unsat
151152
}
153+
154+
type cAdder struct {
155+
c *logic.C
156+
f z.Lit
157+
buf []z.Lit
158+
}
159+
160+
func (a *cAdder) Add(m z.Lit) {
161+
if m != z.LitNull {
162+
a.buf = append(a.buf, m)
163+
return
164+
}
165+
clause := a.c.F
166+
for _, m := range a.buf {
167+
clause = a.c.Or(clause, m)
168+
}
169+
a.buf = a.buf[:0]
170+
a.f = a.c.And(a.f, clause)
171+
}
172+
173+
func BenchmarkStrash(b *testing.B) {
174+
175+
for i := 0; i < b.N; i++ {
176+
circuit := logic.NewC()
177+
ca := &cAdder{
178+
c: circuit,
179+
f: circuit.T}
180+
gen.Rand3Cnf(ca, 100, 300)
181+
}
182+
}

0 commit comments

Comments
 (0)