z3_pipe.cpp

#include <fcntl.h>
#include <iostream>
#include <string>
#include <unistd.h>
#include <sys/wait.h>
#include <cstring>

#include "z3_pipe.h"

#define ensure(b) ensure_helper(b, __FILE__, __FUNCTION__, __LINE__)

static void ensure_helper(const bool b, const char *file, const char *func,
                          const int line) {
  if (b)
    return;

  std::cerr << "Error at " << file << ":" << line << " in function " << func
            << "\n";
  perror(nullptr);
  exit(-1);
}

ssize_t solver::safe_write(int fd, const void *buf, size_t count) {
  size_t n_write = 0;
  while (1) {
    size_t n = write(fd, (const char *)buf + n_write, count - n_write);
    n_write += n;
    if (n == -1)
      return -1;
    if (n == 0 || count == n_write)
      return n_write;
  }
}

void solver::exec_z3() {
  ensure(dup2(tosolver_fds[0], STDIN_FILENO) != -1);
  ensure(close(tosolver_fds[0]) == 0);
  ensure(close(tosolver_fds[1]) == 0);
  ensure(dup2(fromsolver_fds[1], STDOUT_FILENO) != -1);
  ensure(close(fromsolver_fds[0]) == 0);
  ensure(close(fromsolver_fds[1]) == 0);
  execlp("z3", "z3", "-smt2", "-in", "-t:1000", nullptr);
  ensure(false);
}

void solver::connect_z3() {
  ensure(pipe(tosolver_fds) == 0);
  ensure(pipe(fromsolver_fds) == 0);
  int pid = fork();
  ensure(pid != -1);
  if (pid == 0)
    exec_z3();

  ensure(close(tosolver_fds[0]) == 0);
  ensure(close(fromsolver_fds[1]) == 0);
  write_to_solver("(set-logic QF_BV)\n");

  query_count = 0;
}

void solver::shutdown_z3() {
  ensure(close(tosolver_fds[1]) == 0);
  ensure(close(fromsolver_fds[0]) == 0);
  ensure(wait(nullptr) != -1);  
}

solver_result solver::solve(const char *query) {
  ++query_count;
  if (query_count >= MAX_QUERIES) {
    shutdown_z3();
    connect_z3();
  } else {
    write_to_solver("(reset)\n");
  }
  write_to_solver(query);
  while (true) {
    // FIXME -- how large might models be?
    const int BUFLEN = 4096;
    char buf[BUFLEN];
    int res = read_from_solver(buf, BUFLEN);
    ensure(res >= 1);
    if (strncmp(buf, "sat\n", res) == 0)
      return solver_result::SAT;
    if (strncmp(buf, "unsat\n", res) == 0)
      return solver_result::UNSAT;
    return solver_result::ERROR;
  }
}

z3_pipe.h

enum class solver_result { SAT, UNSAT, TIMEOUT, ERROR };

class solver {
  int tosolver_fds[2], fromsolver_fds[2], query_count;
  const int MAX_QUERIES = 2000;
  ssize_t safe_write(int fd, const void *buf, size_t count);
  void exec_z3();
  void connect_z3();
  void shutdown_z3();
  ssize_t write_to_solver(const char *buf) {
    return safe_write(tosolver_fds[1], buf, strlen(buf));
  }
  ssize_t read_from_solver(char *buf, int count) {
    return read(fromsolver_fds[0], buf, count);
  }

public:
  solver() { connect_z3(); }
  ~solver() { shutdown_z3(); }
  solver_result solve(const char *query);
};