incremental checkmodel compromise

in incremental usage with activations sat results only trigger checking
the result is sat if no clauses have been added (not activated) or a
check has not yet been performed.  This speeds up incremental usage
when using clause activation at increased risk.

gini.go

@@ -125,7 +125,10 @@ func (g *Gini) Solve() int {
 	return res
 }
 
-// Try solves with a timeout.
+// Try solves with a timeout.  Try returns
+//  1  if sat
+//  -1 if unsat
+//  0  if timeout
 func (g *Gini) Try(dur time.Duration) int {
 	return g.xo.Try(dur)
 }

internal/xo/cdb.go

@@ -24,7 +24,8 @@ type Cdb struct {
 	Added   []z.C
 	Learnts []z.C
 
-	Tracer Tracer
+	Tracer     Tracer
+	checkModel bool
 
 	// for multi-scheduling gc frequency
 	gc *Cgc
@@ -46,15 +47,16 @@ func NewCdb(v *Vars, capHint int) *Cdb {
 		capHint = 3
 	}
 	clss := &Cdb{
-		Vars:    v,
-		CDat:    *NewCDat(capHint * 5),
-		AddLits: make([]z.Lit, 0, 24),
-		AddVals: make([]int8, v.Top),
-		Bot:     CNull,
-		Added:   make([]z.C, 0, capHint/3),
-		Learnts: make([]z.C, 0, capHint-capHint/3),
-		Tracer:  nil,
-		gc:      NewCgc()}
+		Vars:       v,
+		CDat:       *NewCDat(capHint * 5),
+		AddLits:    make([]z.Lit, 0, 24),
+		AddVals:    make([]int8, v.Top),
+		Bot:        CNull,
+		Added:      make([]z.C, 0, capHint/3),
+		Learnts:    make([]z.C, 0, capHint-capHint/3),
+		Tracer:     nil,
+		gc:         NewCgc(),
+		checkModel: true}
 	return clss
 }
 
@@ -409,6 +411,9 @@ func (c *Cdb) CheckWatches() []error {
 
 // by default, called when sat as a sanity check.
 func (c *Cdb) CheckModel() []error {
+	if !c.checkModel {
+		return nil
+	}
 	if c.Active != nil {
 		// deactivations and simplificaations remove Added clauses, which are unlinked
 		// until sufficiently large to compact.  compaction
@@ -453,6 +458,7 @@ func (c *Cdb) CopyWith(ov *Vars) *Cdb {
 	copy(other.Learnts, c.Learnts)
 	c.CDat.CopyTo(&other.CDat)
 	other.gc = c.gc.Copy()
+	other.checkModel = c.checkModel
 	return other
 }
 

internal/xo/s.go

@@ -275,18 +275,18 @@ func (s *S) Solve() int {
 		// guess
 		m := guess.Guess(vars.Vals)
 		if m == z.LitNull {
-			if false {
-				errs := cdb.CheckModel()
-				if len(errs) != 0 {
-					for _, e := range errs {
-						log.Println(e)
-					}
-					log.Println(s.Vars)
-					log.Println(s.Trail)
-
-					log.Printf("%p %p internal error: sat model\n", s, s.control)
-
+			errs := cdb.CheckModel()
+			if s.Active != nil {
+				s.Cdb.checkModel = false
+			}
+			if len(errs) != 0 {
+				for _, e := range errs {
+					log.Println(e)
 				}
+				log.Println(s.Vars)
+				log.Println(s.Trail)
+
+				log.Printf("%p %p internal error: sat model\n", s, s.control)
 			}
 			s.stSat++
 			// don't do this, we store the model returned to the user
@@ -504,6 +504,7 @@ func (s *S) Add(m z.Lit) {
 	s.ensureLitCap(m)
 	if m == z.LitNull {
 		s.ensure0()
+		s.Cdb.checkModel = true
 	}
 	loc, u := s.Cdb.Add(m)
 	if u != z.LitNull {