<commit_before>#pragma once

#include "../tags/QF_BV.hpp"
#include "../tags/Array.hpp"
#include "../support/SMT_Tag_Mapping.hpp"
#include "../support/find_executable.hpp"

#include "../result_wrapper.hpp"

#include <iostream>
#include <fstream>
#include <boost/mpl/map/map40.hpp>
#include <boost/any.hpp>
#include <boost/function.hpp>
#include <boost/format.hpp>
#include <boost/tuple/tuple.hpp>
#include <boost/iostreams/device/file_descriptor.hpp>
#include <boost/iostreams/stream.hpp>
#include <boost/iostreams/tee.hpp>

#include <boost/spirit/include/qi.hpp>
#include <boost/tuple/tuple_io.hpp>
#include <boost/fusion/adapted/boost_tuple.hpp>
#include <boost/fusion/adapted/std_pair.hpp>

namespace metaSMT {

  struct set_symbol_table_cmd;

  std::string default_symbol_table(unsigned id) {
    char buf[64];
    sprintf(buf, "var_%u", id);
    return buf;
  }

  struct write_comment;
  namespace features {
    struct comment_api;
  } /* features */
  namespace solver {

    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;
  
    struct lazy_string {
      
      lazy_string ()
        : dirty(false), _str(), _concats()
      {}

      lazy_string (std::string const & s)
        : dirty(false), _str(s), _concats()
      {}
      
      //operator std::string {
      //  _eval();
      //  return _str;
      //}

      size_t size() const {
        size_t ret = _str.size();
        BOOST_FOREACH( lazy_string const & ls, _concats ) {
          ret += ls.size();
        }
        return ret;
      }

      void _eval( std::string & str) {
        if( dirty ) {
          str.reserve(size());
          BOOST_FOREACH( lazy_string const & ls, _concats ) {
            //str += (std::string) ls;
          }
        }
        dirty = false;
      }

      bool dirty;
      std::string _str;
      std::list<lazy_string> _concats;
    };

    struct smt2_solver_pipe {
      smt2_solver_pipe(std::ofstream &os, std::ofstream &solution_os) 
        : os_(os)
        , solution_os_(solution_os)
        , _solver(NULL)
        , _result(NULL)
      {
        int toSolver[2];
        int fromSolver[2];
        if ( pipe(toSolver) == -1 || pipe(fromSolver) == -1 ) {
          throw std::runtime_error("opening pipe failed");
        }
        int cpid = fork();
        if( cpid == -1) {
          close(toSolver[0]);
          close(toSolver[1]);
          close(fromSolver[0]);
          close(fromSolver[1]);
          throw std::runtime_error("fork failed");
        }

        if(cpid == 0 ) {
          // solver process
          close(toSolver[1]);   // unused
          close(fromSolver[0]); // unused

          dup2(toSolver[0],0);
          dup2(fromSolver[1],1);
          //execlp("cat", "cat", NULL);
          std::string z3 = support::find_executable("z3", "Z3_EXECUTABLE");
          //std::cerr << "using Z3: " << z3 << std::endl;
          execlp(z3.c_str(), z3.c_str(), "-smt2", "-in", NULL);
          perror("exec");
          exit(1);
        } else {
          // parent writes solution
          close(toSolver[0]);   // unused
          close(fromSolver[1]); // unused

          _solver = new solver_stream(toSolver[1], boost::iostreams::close_handle);
          _result = new result_stream(fromSolver[0], boost::iostreams::close_handle);
        }
      }

      void command ( write_comment const &, std::string const & message) {
        os_ << ";; " << message << '\n';
      }

      ~smt2_solver_pipe() {<commit_msg>removed write_comment from SMT2 pipe<commit_after>#pragma once

#include "../tags/QF_BV.hpp"
#include "../tags/Array.hpp"
#include "../support/SMT_Tag_Mapping.hpp"
#include "../support/find_executable.hpp"

#include "../result_wrapper.hpp"

#include <iostream>
#include <fstream>
#include <boost/mpl/map/map40.hpp>
#include <boost/any.hpp>
#include <boost/function.hpp>
#include <boost/format.hpp>
#include <boost/tuple/tuple.hpp>
#include <boost/iostreams/device/file_descriptor.hpp>
#include <boost/iostreams/stream.hpp>
#include <boost/iostreams/tee.hpp>

#include <boost/spirit/include/qi.hpp>
#include <boost/tuple/tuple_io.hpp>
#include <boost/fusion/adapted/boost_tuple.hpp>
#include <boost/fusion/adapted/std_pair.hpp>

namespace metaSMT {

  struct set_symbol_table_cmd;

  std::string default_symbol_table(unsigned id) {
    char buf[64];
    sprintf(buf, "var_%u", id);
    return buf;
  }

  struct write_comment;
  namespace features {
    struct comment_api;
  } /* features */
  namespace solver {

    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;
  
    struct lazy_string {
      
      lazy_string ()
        : dirty(false), _str(), _concats()
      {}

      lazy_string (std::string const & s)
        : dirty(false), _str(s), _concats()
      {}
      
      //operator std::string {
      //  _eval();
      //  return _str;
      //}

      size_t size() const {
        size_t ret = _str.size();
        BOOST_FOREACH( lazy_string const & ls, _concats ) {
          ret += ls.size();
        }
        return ret;
      }

      void _eval( std::string & str) {
        if( dirty ) {
          str.reserve(size());
          BOOST_FOREACH( lazy_string const & ls, _concats ) {
            //str += (std::string) ls;
          }
        }
        dirty = false;
      }

      bool dirty;
      std::string _str;
      std::list<lazy_string> _concats;
    };

    struct smt2_solver_pipe {
      smt2_solver_pipe(std::ofstream &os, std::ofstream &solution_os) 
        : os_(os)
        , solution_os_(solution_os)
        , _solver(NULL)
        , _result(NULL)
      {
        int toSolver[2];
        int fromSolver[2];
        if ( pipe(toSolver) == -1 || pipe(fromSolver) == -1 ) {
          throw std::runtime_error("opening pipe failed");
        }
        int cpid = fork();
        if( cpid == -1) {
          close(toSolver[0]);
          close(toSolver[1]);
          close(fromSolver[0]);
          close(fromSolver[1]);
          throw std::runtime_error("fork failed");
        }

        if(cpid == 0 ) {
          // solver process
          close(toSolver[1]);   // unused
          close(fromSolver[0]); // unused

          dup2(toSolver[0],0);
          dup2(fromSolver[1],1);
          //execlp("cat", "cat", NULL);
          std::string z3 = support::find_executable("z3", "Z3_EXECUTABLE");
          //std::cerr << "using Z3: " << z3 << std::endl;
          execlp(z3.c_str(), z3.c_str(), "-smt2", "-in", NULL);
          perror("exec");
          exit(1);
        } else {
          // parent writes solution
          close(toSolver[0]);   // unused
          close(fromSolver[1]); // unused

          _solver = new solver_stream(toSolver[1], boost::iostreams::close_handle);
          _result = new result_stream(fromSolver[0], boost::iostreams::close_handle);
        }
      }

      ~smt2_solver_pipe() {
{'fraction_non_alphanumeric': 0.15372582480091013, 'fraction_numerical': 0.010949943117178612, 'mean_word_length': 2.257526632700324, 'pattern_counts': {'":': 0, '<': 51, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6860393', 'n_tokens_mistral': 2434, 'n_tokens_neox': 2349, 'n_words': 434}