<commit_before>#include "dreal/smt2/driver.h"

#include <fstream>
#include <iostream>
#include <sstream>
#include <stdexcept>
#include <string>
#include <utility>

#include <fmt/format.h>
#include <fmt/ostream.h>

#include "dreal/smt2/scanner.h"
#include "dreal/solver/expression_evaluator.h"
#include "dreal/symbolic/prefix_printer.h"
#include "dreal/util/optional.h"

namespace dreal {

using std::cerr;
using std::cin;
using std::cout;
using std::endl;
using std::ifstream;
using std::istream;
using std::istringstream;
using std::ostream;
using std::ostringstream;
using std::runtime_error;
using std::string;
using std::stringstream;
using std::vector;

namespace {}  // namespace

FunctionDefinition::FunctionDefinition(vector<Variable> parameters,
                                       Sort return_type, Term body)
    : parameters_{std::move(parameters)},
      return_type_{return_type},
      body_{std::move(body)} {}

Term FunctionDefinition::operator()(const vector<Term>& arguments) const {
  if (parameters_.size() != arguments.size()) {
    throw runtime_error{
        fmt::format("This function definition expects {} arguments whereas the "
                    "provided arguments are of length {}.",
                    parameters_.size(), arguments.size())};
  }

  body_.Check(return_type_);
  Term t = body_;
  for (size_t i = 0; i < parameters_.size(); ++i) {
    const Variable& param_i{parameters_[i]};
    const Term& arg_i{arguments[i]};
    arg_i.Check(param_i.get_type());
    t = t.Substitute(param_i, arg_i);
  }

  return t;
}

Smt2Driver::Smt2Driver(Context context) : context_{std::move(context)} {}

bool Smt2Driver::parse_stream(istream& in, const string& sname) {
  streamname_ = sname;

  Smt2Scanner new_scanner(&in);
  new_scanner.set_debug(trace_scanning_);
  this->scanner = &new_scanner;

  Smt2Parser parser(*this);
  parser.set_debug_level(trace_parsing_);
  return (parser.parse() == 0);
}

bool Smt2Driver::parse_file(const string& filename) {
  if (filename.empty()) {
    // Option --in passed to dreal.
    return parse_stream(cin, "(stdin)");
  }
  ifstream in(filename.c_str());
  if (!in.good()) {
    return false;
  }
  return parse_stream(in, filename);
}

bool Smt2Driver::parse_string(const string& input, const string& sname) {
  istringstream iss(input);
  return parse_stream(iss, sname);
}

void Smt2Driver::error(const location& l, const string& m) {
  cerr << l << " : " << m << endl;
}

void Smt2Driver::error(const string& m) { cerr << m << endl; }

void Smt2Driver::CheckSat() {
  const optional<Box> model{context_.CheckSat()};
  if (model) {
    if (context_.config().smtlib2_compliant()) {
      cout << "delta-sat\n";
    } else {
      cout << "delta-sat with delta = " << context_.config().precision()
           << "\n";
      if (context_.config().produce_models()) {
        cout << *model << endl;
      }
    }
  } else {
    cout << "unsat" << endl;
  }
}

namespace {
ostream& PrintModel(ostream& os, const Box& box) {
  os << "(model\n";
  for (int i = 0; i < box.size(); ++i) {
    const Variable& var{box.variable(i)};
    os << "  (define-fun " << var << " () ";
    switch (var.get_type()) {
      case Variable::Type::CONTINUOUS:
        os << Sort::Real;
        break;
      case Variable::Type::BINARY:
        os << Sort::Binary;
        break;
      case Variable::Type::INTEGER:
        os << Sort::Int;
        break;
      case Variable::Type::BOOLEAN:
        os << Sort::Bool;
        break;
    }
    os << " ";
    const Box::Interval& iv{box[i]};
    if (var.get_type() == Variable::Type::BOOLEAN) {
      if (iv == iv.ONE) {
        os << "true";
      } else if (iv == iv.ZERO) {
        os << "false";
      }
    } else {
      if (iv.is_degenerated()) {
        os << iv.lb();
      } else {
        os << iv;
      }
    }
    os << ")\n";
  }
  return os << ")";
}
}  // namespace

void Smt2Driver::GetModel() const {
  const Box& box{context_.get_model()};
  if (box.empty()) {
    cout << "(error \"model is not available\")" << endl;
  } else {
    PrintModel(cout, box) << endl;
  }
}

void Smt2Driver::GetValue(const vector<Term>& term_list) const {
  const Box& box{context_.get_model()};
  fmt::print("(\n");
  for (const auto& term : term_list) {
    string term_str;
    string value_str;
    stringstream ss;
    PrefixPrinter pp{ss};

    switch (term.type()) {
      case Term::Type::EXPRESSION: {
        const Expression& e{term.expression()};
        const ExpressionEvaluator evaluator{e};
        pp.Print(e);
        term_str = ss.str();
        value_str =
            fmt::format("{}", ExpressionEvaluator(term.expression())(box));
        break;
      }
      case Term::Type::FORMULA: {
        const Formula& f{term.formula()};
        pp.Print(f);
        term_str = ss.str();
        if (is_variable(f)) {
          value_str =
              box[get_variable(f)] == Box::Interval::ONE ? "true" : "false";
        } else {
          throw std::runtime_error(fmt::format(
              "get-value does not handle a compound formula {}.", term_str));
        }
        break;
      }
    }

    fmt::print("\t({} {})\n", term_str, value_str);
  }
  fmt::print(")\n");
}

void Smt2Driver::GetOption(const string& key) const {
  const optional<string> value{context_.GetOption(key)};
  if (value) {
    fmt::print("{}\n", *value);
  } else {
    fmt::print("unsupported\n");
  }
}

Variable Smt2Driver::RegisterVariable(const string& name, const Sort sort) {
  const Variable v{ParseVariableSort(name, sort)};
  scope_.insert(v.get_name(), v);
  return v;
}

Variable Smt2Driver::DeclareVariable(const string& name, const Sort sort) {
  Variable v{RegisterVariable(name, sort)};
  context_.DeclareVariable(v);<commit_msg>fix(smt2): Flush cout after executing a command<commit_after>#include "dreal/smt2/driver.h"

#include <fstream>
#include <iostream>
#include <sstream>
#include <stdexcept>
#include <string>
#include <utility>

#include <fmt/format.h>
#include <fmt/ostream.h>

#include "dreal/smt2/scanner.h"
#include "dreal/solver/expression_evaluator.h"
#include "dreal/symbolic/prefix_printer.h"
#include "dreal/util/optional.h"

namespace dreal {

using std::cerr;
using std::cin;
using std::cout;
using std::ifstream;
using std::istream;
using std::istringstream;
using std::ostream;
using std::ostringstream;
using std::runtime_error;
using std::string;
using std::stringstream;
using std::vector;

namespace {}  // namespace

FunctionDefinition::FunctionDefinition(vector<Variable> parameters,
                                       Sort return_type, Term body)
    : parameters_{std::move(parameters)},
      return_type_{return_type},
      body_{std::move(body)} {}

Term FunctionDefinition::operator()(const vector<Term>& arguments) const {
  if (parameters_.size() != arguments.size()) {
    throw runtime_error{
        fmt::format("This function definition expects {} arguments whereas the "
                    "provided arguments are of length {}.",
                    parameters_.size(), arguments.size())};
  }

  body_.Check(return_type_);
  Term t = body_;
  for (size_t i = 0; i < parameters_.size(); ++i) {
    const Variable& param_i{parameters_[i]};
    const Term& arg_i{arguments[i]};
    arg_i.Check(param_i.get_type());
    t = t.Substitute(param_i, arg_i);
  }

  return t;
}

Smt2Driver::Smt2Driver(Context context) : context_{std::move(context)} {}

bool Smt2Driver::parse_stream(istream& in, const string& sname) {
  streamname_ = sname;

  Smt2Scanner new_scanner(&in);
  new_scanner.set_debug(trace_scanning_);
  this->scanner = &new_scanner;

  Smt2Parser parser(*this);
  parser.set_debug_level(trace_parsing_);
  return (parser.parse() == 0);
}

bool Smt2Driver::parse_file(const string& filename) {
  if (filename.empty()) {
    // Option --in passed to dreal.
    return parse_stream(cin, "(stdin)");
  }
  ifstream in(filename.c_str());
  if (!in.good()) {
    return false;
  }
  return parse_stream(in, filename);
}

bool Smt2Driver::parse_string(const string& input, const string& sname) {
  istringstream iss(input);
  return parse_stream(iss, sname);
}

void Smt2Driver::error(const location& l, const string& m) {
  cerr << l << " : " << m << "\n";
}

void Smt2Driver::error(const string& m) { cerr << m << "\n"; }

void Smt2Driver::CheckSat() {
  const optional<Box> model{context_.CheckSat()};
  if (model) {
    if (context_.config().smtlib2_compliant()) {
      cout << "delta-sat\n";
    } else {
      cout << "delta-sat with delta = " << context_.config().precision()
           << "\n";
      if (context_.config().produce_models()) {
        cout << *model << "\n";
      }
    }
  } else {
    cout << "unsat\n";
  }
  cout.flush();
}

namespace {
ostream& PrintModel(ostream& os, const Box& box) {
  os << "(model\n";
  for (int i = 0; i < box.size(); ++i) {
    const Variable& var{box.variable(i)};
    os << "  (define-fun " << var << " () ";
    switch (var.get_type()) {
      case Variable::Type::CONTINUOUS:
        os << Sort::Real;
        break;
      case Variable::Type::BINARY:
        os << Sort::Binary;
        break;
      case Variable::Type::INTEGER:
        os << Sort::Int;
        break;
      case Variable::Type::BOOLEAN:
        os << Sort::Bool;
        break;
    }
    os << " ";
    const Box::Interval& iv{box[i]};
    if (var.get_type() == Variable::Type::BOOLEAN) {
      if (iv == iv.ONE) {
        os << "true";
      } else if (iv == iv.ZERO) {
        os << "false";
      }
    } else {
      if (iv.is_degenerated()) {
        os << iv.lb();
      } else {
        os << iv;
      }
    }
    os << ")\n";
  }
  return os << ")";
}
}  // namespace

void Smt2Driver::GetModel() const {
  const Box& box{context_.get_model()};
  if (box.empty()) {
    cout << "(error \"model is not available\")\n";
  } else {
    PrintModel(cout, box) << "\n";
  }
  cout.flush();
}

void Smt2Driver::GetValue(const vector<Term>& term_list) const {
  const Box& box{context_.get_model()};
  fmt::print("(\n");
  for (const auto& term : term_list) {
    string term_str;
    string value_str;
    stringstream ss;
    PrefixPrinter pp{ss};

    switch (term.type()) {
      case Term::Type::EXPRESSION: {
        const Expression& e{term.expression()};
        const ExpressionEvaluator evaluator{e};
        pp.Print(e);
        term_str = ss.str();
        value_str =
            fmt::format("{}", ExpressionEvaluator(term.expression())(box));
        break;
      }
      case Term::Type::FORMULA: {
        const Formula& f{term.formula()};
        pp.Print(f);
        term_str = ss.str();
        if (is_variable(f)) {
          value_str =
              box[get_variable(f)] == Box::Interval::ONE ? "true" : "false";
        } else {
          throw std::runtime_error(fmt::format(
              "get-value does not handle a compound formula {}.", term_str));
        }
        break;
      }
    }
    fmt::print("\t({} {})\n", term_str, value_str);
  }
  fmt::print(")\n");
  cout.flush();
}

void Smt2Driver::GetOption(const string& key) const {
  const optional<string> value{context_.GetOption(key)};
  if (value) {
    fmt::print("{}\n", *value);
  } else {
    fmt::print("unsupported\n");
  }
  cout.flush();
}

Variable Smt2Driver::RegisterVariable(const string& name, const Sort sort) {
  const Variable v{ParseVariableSort(name, sort)};
  scope_.insert(v.get_name(), v);
  return v;
}

Variable Smt2Driver::DeclareVariable(const string& name, const Sort sort) {
  Variable v{RegisterVariable(name, sort)};
  context_.DeclareVariable(v);
{'fraction_non_alphanumeric': 0.16568661362850226, 'fraction_numerical': 0.003718436527153234, 'mean_word_length': 3.040880503144654, 'pattern_counts': {'":': 0, '<': 157, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7207671', 'n_tokens_mistral': 3933, 'n_tokens_neox': 3879, 'n_words': 843}