From 3a1a4d9135f5ef6217be78e3a3e7f498531f4ef1 Mon Sep 17 00:00:00 2001
From: Scott Cotton <scott@mindowl.com>
Date: Wed, 25 Aug 2021 09:44:43 +0200
Subject: [PATCH] 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
---
 logic/c.go      |  2 +-
 logic/c_test.go | 31 +++++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/logic/c.go b/logic/c.go
index d08091e..c42c9e5 100644
--- a/logic/c.go
+++ b/logic/c.go
@@ -376,5 +376,5 @@ func (p *C) grow() {
 }
 
 func strashCode(a, b z.Lit) uint32 {
-	return uint32((a << 13) * b)
+	return uint32(^(a << 13) * b)
 }
diff --git a/logic/c_test.go b/logic/c_test.go
index c9af878..54dfac3 100644
--- a/logic/c_test.go
+++ b/logic/c_test.go
@@ -10,6 +10,7 @@ import (
 	"testing"
 
 	"github.com/go-air/gini"
+	"github.com/go-air/gini/gen"
 	"github.com/go-air/gini/logic"
 	"github.com/go-air/gini/z"
 )
@@ -149,3 +150,33 @@ func ExampleC_equiv() {
 	}
 	//Output: unsat
 }
+
+type cAdder struct {
+	c   *logic.C
+	f   z.Lit
+	buf []z.Lit
+}
+
+func (a *cAdder) Add(m z.Lit) {
+	if m != z.LitNull {
+		a.buf = append(a.buf, m)
+		return
+	}
+	clause := a.c.F
+	for _, m := range a.buf {
+		clause = a.c.Or(clause, m)
+	}
+	a.buf = a.buf[:0]
+	a.f = a.c.And(a.f, clause)
+}
+
+func BenchmarkStrash(b *testing.B) {
+
+	for i := 0; i < b.N; i++ {
+		circuit := logic.NewC()
+		ca := &cAdder{
+			c: circuit,
+			f: circuit.T}
+		gen.Rand3Cnf(ca, 100, 300)
+	}
+}