From bd37625e499f9f859a38eb8e6251036b358e02db Mon Sep 17 00:00:00 2001
From: Alexandre GBAGUIDI AISSE <gbagui_a@epita.fr>
Date: Wed, 21 Dec 2016 16:39:05 +0100
Subject: [PATCH] misc: Add 'SPOT_XCNF' environment variable

* spot/misc/satsolver.cc: Handle xcnf writing.
* spot/misc/satsolver.hh: Handle xcnf writing.
---
 spot/misc/satsolver.cc | 79 ++++++++++++++++++++++++++++++++++++++++--
 spot/misc/satsolver.hh | 10 ++++++
 2 files changed, 87 insertions(+), 2 deletions(-)

diff --git a/spot/misc/satsolver.cc b/spot/misc/satsolver.cc
index dfff47dc6..3350597b0 100644
--- a/spot/misc/satsolver.cc
+++ b/spot/misc/satsolver.cc
@@ -74,12 +74,30 @@ namespace spot
   // easy to check if psat_ was initialized or not.
   satsolver::satsolver()
     : cnf_tmp_(nullptr), cnf_stream_(nullptr), nclauses_(0), nvars_(0),
-    nassumptions_vars_(0), nsols_(0), psat_(nullptr)
+    nassumptions_vars_(0), nsols_(0), psat_(nullptr), xcnf_tmp_(nullptr),
+    xcnf_stream_(nullptr), path_("")
   {
-    if (cmd_.command_given())
+    // Check SPOT_XCNF env var.
+    static std::string path = []()
+    {
+      auto s = getenv("SPOT_XCNF");
+      return s ? s : "";
+    }();
+    if (!path.empty())
+      path_ = path;
+
+    bool satsolver_set = cmd_.command_given();
+    bool xcnf_set = xcnf_mode();
+
+    if (satsolver_set)
     {
       start();
     }
+    else if (xcnf_set) // If !satsolver_set and xcnf_set.
+    {
+      throw std::runtime_error("XNCF generation requires an external SAT solver"
+                               " to be defined with SPOT_SATSOLVER");
+    }
     else
     {
       psat_ = picosat_init();
@@ -99,6 +117,21 @@ namespace spot
       delete cnf_tmp_;
       delete cnf_stream_;
     }
+
+    if (xcnf_mode())
+    {
+      xcnf_tmp_->close();
+      xcnf_stream_->close();
+      delete xcnf_tmp_;
+      delete xcnf_stream_;
+    }
+  }
+
+  bool
+  satsolver::xcnf_mode()
+  {
+    static bool res = !path_.empty();
+    return res;
   }
 
   void satsolver::start()
@@ -109,6 +142,15 @@ namespace spot
 
     // Add empty line for the header
     *cnf_stream_ << "                                                 \n";
+
+    if (xcnf_mode()) // If xcnf mode.
+    {
+      xcnf_tmp_ = new std::ofstream(path_ + "/incr.tmp", std::ios_base::trunc);
+      xcnf_tmp_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
+      *xcnf_tmp_ << "                                                 \n+\n";
+      xcnf_stream_ = new std::ofstream(path_ + "/incr.xcnf", std::ios::trunc);
+      xcnf_stream_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
+    }
   }
 
   // Must be called only when SPOT_SATSOLVER is given
@@ -118,6 +160,9 @@ namespace spot
     nclauses_ += 1;
     if (nclauses_ < 0)
       throw std::runtime_error(": too many SAT clauses (more than INT_MAX).");
+
+    if (xcnf_mode())
+      *xcnf_tmp_ << '\n';
   }
 
   void satsolver::adjust_nvars(int nvars)
@@ -156,6 +201,9 @@ namespace spot
       }
       else
       {
+        if (xcnf_mode())
+          *xcnf_tmp_ << v << ' ';
+
         *cnf_stream_ << v << ' ';
         if (!v) // ..., 0)
           end_clause();
@@ -174,6 +222,9 @@ namespace spot
     }
     else
     {
+      if (xcnf_mode())
+        *xcnf_tmp_ << v << ' ';
+
       *cnf_stream_ << v << ' ';
       if (!v) // 0
         end_clause();
@@ -293,6 +344,30 @@ namespace spot
       p.second = satsolver_get_sol(output->name());
       delete output;
     }
+
+    if (xcnf_mode() && !p.second.empty())
+    {
+      // Update xcnf_tmp_ header
+      xcnf_tmp_->seekp(0);
+      *xcnf_tmp_ << "p cnf " << (get_nb_vars() + 1);
+      xcnf_tmp_->seekp(0, std::ios_base::end);
+      if (!*xcnf_tmp_)
+        throw std::runtime_error("Failed to update xcnf_tmp_ header");
+
+      // Copy xcnf_tmp_ into xcnf_stream_
+      xcnf_tmp_->close();
+      std::ifstream ifile(path_ + "/incr.tmp", std::ios::in);
+      *xcnf_stream_ << ifile.rdbuf();
+      *xcnf_stream_ << "X\n";
+
+      // Erase xcnf_tmp_ content
+      delete xcnf_tmp_;
+      xcnf_tmp_ = new std::ofstream(path_ + "/incr.tmp", std::ios_base::trunc);
+      xcnf_tmp_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
+      *xcnf_tmp_ << "                                                 \n";
+      *xcnf_tmp_ << "+\n";
+    }
+
     return p;
   }
 
diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh
index 889164643..ece0a2dc1 100644
--- a/spot/misc/satsolver.hh
+++ b/spot/misc/satsolver.hh
@@ -143,6 +143,10 @@ namespace spot
     satsolver::solution
     satsolver_get_sol(const char* filename);
 
+    /// \brief Check if <code>SPOT_XCNF</code> env var is set.
+    bool
+    xcnf_mode();
+
   private:  // variables
     /// \brief A satsolver_command. Check if SPOT_SATSOLVER is given.
     satsolver_command cmd_;
@@ -161,6 +165,12 @@ namespace spot
 
     /// \brief Picosat satsolver instance.
     PicoSAT* psat_;
+
+    // The next 2 pointers will be initialized if SPOT_XCNF env var
+    // is set. This recquires SPOT_SATSOLVER to be set as well.
+    std::ofstream* xcnf_tmp_;
+    std::ofstream* xcnf_stream_;
+    std::string path_;
   };
 
   /// \brief Extract the solution of a SAT solver output.