aiger bugfix and usability improvements

This commit fixes a bug in the aiger ascii output for latch values and
adds some usability/performance improvements

For usability, we have added a Write method to gini to have it dump
a dimacs CNF to a writer.

For performance, we have made it so that more learned clauses could be
derived in incremental mode with test scopes when the last solve gave
unsat.

gini.go

@@ -271,3 +271,9 @@ func (g *Gini) ActivationLit() z.Lit {
 func (g *Gini) Deactivate(m z.Lit) {
 	g.xo.Deactivate(m)
 }
+
+// Write writes the underlying CNF in dimacs format to dst,
+// returning any i/o error which occured in the process.
+func (g *Gini) Write(dst io.Writer) error {
+	return g.xo.Cdb.Write(dst)
+}

internal/xo/s.go

@@ -292,10 +292,7 @@ func (s *S) Solve() int {
 				log.Fatalf("%p %p internal error in solve: sat model\n", s, s.control)
 			}
 			s.stSat++
-			// don't do this, we store the model returned to the user
-			// with regular assignments, and backtrack on next call to
-			// solve instead.
-			//trail.Back(0)
+			//fmt.Printf("vars %s\n", s.Vars)
 			return 1
 		}
 		if u, c, ms := cdb.MaybeCompact(); u != 0 {
@@ -659,6 +656,7 @@ func (s *S) cleanupSolve() z.C {
 		trail.Back(drvd.TargetLevel)
 		trail.Assign(drvd.Unit, drvd.P)
 		s.x = trail.Prop()
+		continue
 	}
 	trail.Back(s.endTestLevel)
 	s.xLit = z.LitNull

logic/aiger/aiger.go

@@ -303,9 +303,9 @@ func (a *T) WriteAscii(w io.Writer) error {
 		ini := a.Init(m)
 		switch ini {
 		case a.S.F:
-			bw.WriteString("1\n")
-		case a.S.T:
 			bw.WriteString("0\n")
+		case a.S.T:
+			bw.WriteString("1\n")
 		case z.LitNull:
 			writeLit(bw, m, a.S.T)
 			bw.WriteString("\n")

logic/aiger/aiger_test.go

@@ -16,7 +16,7 @@ import (
 // note this is 1.9 version: we have MILOABCJF
 var expectedOutput1 = `aag 4 1 1 2 1 0 0 0 0
 2
-4 6 1
+4 6 0
 4
 5
 6 2 4