#include <fstream>
#include <iostream>
#include <sys/stat.h>
#include <unistd.h>
#include <vector>
#include "z3++.h"

#include "Strategy.h"
#include "SymbolicInterpreter.h"

z3::context Ctx;
z3::solver Solver(Ctx);

void storeInput() {
  /// sat 结果写入到 "input.txt" 作为下一次输入
  std::ofstream OS(InputFile);
  z3::model Model = Solver.get_model();
  for (int I = 0; I < Model.size(); I++) {
    const z3::func_decl E = Model[I];
    z3::expr Input = Model.get_const_interp(E);
    if (Input.kind() == Z3_NUMERAL_AST) {
      int res = Input.get_numeral_int();
      OS << E.name() << "," << res << std::endl;
    }
  }
}

void printNewPathCondition(z3::expr_vector &Vec) {
  std::ofstream Log;
  /// 将路径条件写入到 “log.txt”
  Log.open(LogFile, std::ofstream::out | std::ofstream::app);
  Log << std::endl;
  Log << "=== New Path Condition ===" << std::endl;
  for (auto E : Vec) {
    Log << E << std::endl;
  }
}

/// 产生输入
void generateInput() {
  /// 获取 formula.smt2 中的内容
  z3::expr_vector Vec = Ctx.parse_file(FormulaFile);
    recordBranches(Vec);
    //std::cout<<"Vec: "<<Vec.size()<<std::endl;
  while (true) {
    /// 搜索策略（需要自己编写）
    searchStrategy(Vec);
    Solver.reset();
    /// Vec 格式:
    for (const auto &E : Vec) {
      Solver.add(E);
    }
    /// z3 求解器求解结果
    z3::check_result Result = Solver.check();
    /// 如果 sat
    if (Result == z3::sat) {
      /// 保存结果
      storeInput();
      /// 打印新的表达式，也就是这一次求解的表达式
      printNewPathCondition(Vec);
      break;
    }
  }
}

int main(int argc, char **argv) {
  if (argc < 2) {
    std::cerr << "Expected an argument - executable file name" << std::endl;
    return 1;
  }

  struct stat Buffer;
  if (stat(argv[1], &Buffer)) {
    std::cerr << argv[1] << " not found\n" << std::endl;
    return 1;
  }

  int MaxIter = INT_MAX;
  if (argc == 3) {
    /// 执行次数 argv[2]:
    /// ../build/dse ./simple0 1 -> MaxIter = 1
    MaxIter = atoi(argv[2]);
  }

  int Iter = 0;
  while (Iter < MaxIter) {
    /**
     * 执行命令  argv[1]
     * ../build/dse ./simple0 1 -> ./simple0
     * 如果程序中没有 DSE_Input，那么后续的 generateInput() 将不会产生 Vec
     * 也就是 z3::expr_vector Vec = Ctx.parse_file(FormulaFile) 为空
     * 如果有 DSE_Input，就会产生一些列反应
     */
    int Ret = std::system(argv[1]);
    /// 程序运行没有发生错误 -> Ret = 0
    /// 程序运行发生错误，如除 0 错： -> Ret = 35584 != 0
    if (Ret) {
      std::cout << "Crashing input found (" << Iter << " iters)" << std::endl;
      break;
    }
    /// stat: 获取文件信息，文件属性存放在结构体 stat 里
    if (stat(FormulaFile, &Buffer)) {
        /// 没有创建 formula.smt2
      std::cerr << FormulaFile << " not found" << std::endl;
      return 1;
    }
    /// 产生输入
    generateInput();
    /// 下次迭代
    Iter++;
  }
}
