From b4d0b9ee4289305b16ff0012c5750cc707edcd06 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 17 Dec 2013 15:55:23 +0100
Subject: [PATCH] sat: more debug.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: More debuging
code.
---
 src/tgbaalgos/dtbasat.cc  | 18 ++++++++++++++++++
 src/tgbaalgos/dtgbasat.cc |  1 +
 2 files changed, 19 insertions(+)

diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index fad083ee2..3b3522bec 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <iostream>
+#include <fstream>
 #include <sstream>
 #include "dtbasat.hh"
 #include "reachiter.hh"
@@ -901,6 +902,8 @@ namespace spot
 	     satdict.prodid.begin(); pit != satdict.prodid.end(); ++pit)
 	if (positive.find(pit->second) != positive.end())
 	  dout << pit->second << "\t" << pit->first << "\n";
+	else
+	  dout << -pit->second << "\t¬" << pit->first << "C\n";
 
       dout << "--- pathid_cand variables ---\n";
       for (std::map<path, int>::const_iterator pit =
@@ -908,6 +911,9 @@ namespace spot
 	   pit != satdict.pathid_cand.end(); ++pit)
 	if (positive.find(pit->second) != positive.end())
 	  dout << pit->second << "\t" << pit->first << "C\n";
+	else
+	  dout << -pit->second << "\t¬" << pit->first << "C\n";
+
 
       dout << "--- pathid_ref variables ---\n";
       for (std::map<path, int>::const_iterator pit =
@@ -915,6 +921,18 @@ namespace spot
 	   pit != satdict.pathid_ref.end(); ++pit)
 	if (positive.find(pit->second) != positive.end())
 	  dout << pit->second << "\t" << pit->first << "R\n";
+	else
+	  dout << -pit->second << "\t¬" << pit->first << "C\n";
+
+      dout << "--- pathcand variables ---\n";
+      for (std::map<state_pair, int>::const_iterator pit =
+	     satdict.pathcand.begin();
+	   pit != satdict.pathcand.end(); ++pit)
+	if (positive.find(pit->second) != positive.end())
+	  dout << pit->second << "\t" << pit->first << "C\n";
+	else
+	  dout << -pit->second << "\t¬" << pit->first << "C\n";
+
 #endif
 
       a->merge_transitions();
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 2be755505..8ecc9ab68 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <iostream>
+#include <fstream>
 #include <sstream>
 #include "dtgbasat.hh"
 #include "reachiter.hh"