From 83b19143aef2be4c543efc0d8f0d43baf25934dc Mon Sep 17 00:00:00 2001
From: Scott <wsc@iri-labs.com>
Date: Fri, 14 Dec 2018 18:28:55 +0100
Subject: [PATCH] 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                   | 6 ++++++
 internal/xo/s.go          | 6 ++----
 logic/aiger/aiger.go      | 4 ++--
 logic/aiger/aiger_test.go | 2 +-
 4 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/gini.go b/gini.go
index c9b70ab..30a254c 100644
--- a/gini.go
+++ b/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)
+}
diff --git a/internal/xo/s.go b/internal/xo/s.go
index ac45be4..1ecbc24 100644
--- a/internal/xo/s.go
+++ b/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
diff --git a/logic/aiger/aiger.go b/logic/aiger/aiger.go
index 1e0e1f7..c3a95fc 100644
--- a/logic/aiger/aiger.go
+++ b/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")
diff --git a/logic/aiger/aiger_test.go b/logic/aiger/aiger_test.go
index 6584ee2..8da79dd 100644
--- a/logic/aiger/aiger_test.go
+++ b/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