text:
//=======================================================================
// Copyright 2001 Jeremy G. Siek, Andrew Lumsdaine, Lie-Quan Lee,
//
// Distributed under the Boost Software License, Version 1.0. (See
// accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//=======================================================================
#include <boost/config.hpp>
#include <iostream>
#include <boost/graph/adjacency_list.hpp>
#include <boost/graph/prim_minimum_spanning_tree.hpp>

int
main()
{
  using namespace boost;
  typedef adjacency_list < vecS, vecS, undirectedS,
    property<vertex_distance_t, int>, property < edge_weight_t, int > > Graph;
  typedef std::pair < int, int >E;
  const int num_nodes = 5;
  E edges[] = { E(0, 2), E(1, 3), E(1, 4), E(2, 1), E(2, 3),
    E(3, 4), E(4, 0)
  };
  int weights[] = { 1, 1, 2, 7, 3, 1, 1 };
#if defined(BOOST_MSVC) && BOOST_MSVC <= 1300
  Graph g(num_nodes);
  property_map<Graph, edge_weight_t>::type weightmap = get(edge_weight, g);
  for (std::size_t j = 0; j < sizeof(edges) / sizeof(E); ++j) {
    graph_traits<Graph>::edge_descriptor e; bool inserted;
    boost::tie(e, inserted) = add_edge(edges[j].first, edges[j].second, g);
    weightmap[e] = weights[j];
  }
#else
  Graph g(edges, edges + sizeof(edges) / sizeof(E), weights, num_nodes);
  property_map<Graph, edge_weight_t>::type weightmap = get(edge_weight, g);
#endif
  std::vector < graph_traits < Graph >::vertex_descriptor >
    p(num_vertices(g));

#if defined(BOOST_MSVC) && BOOST_MSVC <= 1300
  property_map<Graph, vertex_distance_t>::type distance = get(vertex_distance, g);
  property_map<Graph, vertex_index_t>::type indexmap = get(vertex_index, g);
  prim_minimum_spanning_tree
    (g, *vertices(g).first, &p[0], distance, weightmap, indexmap,
     default_dijkstra_visitor());
#else
  prim_minimum_spanning_tree(g, &p[0]);
#endif

  for (std::size_t i = 0; i != p.size(); ++i)
    if (p[i] != i)
      std::cout << "parent[" << i << "] = " << p[i] << std::endl;
    else
      std::cout << "parent[" << i << "] = no parent" << std::endl;

  return EXIT_SUCCESS;
}

max_stars_repo_name: randolphwong/mcsema

max_issues_repo_name: randolphwong/mcsema

max_forks_repo_name: randolphwong/mcsema


text:
#pragma once

// lua_strlen() and lua_equal() are used in Luabind, but these have been removed in Lua 5.4.
// Still we can enable the compatible macros by defining LUA_COMPAT_5_3 before including "luaconf.h".

#include "lua.hpp"

#if (LUA_VERSION_NUM >= 502)
// Lua 5.1 compatible functions.
inline void lua_setfenv(lua_State* L, int idx) { lua_setuservalue(L, idx); }
inline void lua_getfenv(lua_State* L, int idx) { lua_getuservalue(L, idx); }
inline lua_State* lua_open() { return luaL_newstate(); }

#if (LUA_VERSION_NUM >= 504)
inline int lua_resume(lua_State* L, int nargs)
{
	int nresults = 0;
	return lua_resume(L, nullptr, nargs, &nresults);
}
#else
inline int lua_resume(lua_State* L, int nargs) { return lua_resume(L, nullptr, nargs); }
#endif

struct DummyClassForLegacyLuaGlobalsIndex {};
const DummyClassForLegacyLuaGlobalsIndex LUA_GLOBALSINDEX;
inline void lua_pushvalue(lua_State* L, const DummyClassForLegacyLuaGlobalsIndex&) { lua_pushglobaltable(L); }
inline void lua_settable(lua_State* L, const DummyClassForLegacyLuaGlobalsIndex&) { lua_settable(L, LUA_REGISTRYINDEX); }
inline void lua_gettable(lua_State* L, const DummyClassForLegacyLuaGlobalsIndex&) { lua_gettable(L, LUA_REGISTRYINDEX); }
#else
// Lua 5.2 compatible functions.
inline void lua_pushglobaltable(lua_State* L) { lua_pushvalue(L, LUA_GLOBALSINDEX); }
#endif

// Suppress automatic inclusion of <boost/bind/placeholders.hpp> in <boost/bind/bind.hpp> in order to avoid conflict between Boost and C++11 placeholders.
#define BOOST_BIND_NO_PLACEHOLDERS

// Luabind 0.9.1 uses "boost::operator" but it has been moved to "boost::iterators::operator" in Boost 1.57.0 or later.
// As a result, many compilation errors will occur at the macro "LUABIND_OPERATOR_ADL_WKND" in "luabind/object.hpp".
// One of the best and wisest solutions is to modify the source code of Luabind directly.
// As an alternative way, the following workaround can avoid modifying it but is unbeautiful and pollutes the namespace "boost".

#include <boost/operators.hpp>
namespace luabind
{
	namespace detail
	{
		// Forward declaration
		template<typename T> class basic_iterator;
	}
}
namespace boost
{
	template<typename T> bool operator ==(
		const luabind::detail::basic_iterator<T>& x,
		const luabind::detail::basic_iterator<T>& y)
	{ return boost::iterators::operator ==(x, y); }

	template<typename T> bool operator !=(
		const luabind::detail::basic_iterator<T>& x,
		const luabind::detail::basic_iterator<T>& y)
	{ return boost::iterators::operator !=(x, y); }
}

ext: hpp

max_stars_repo_name: sygh-JP/CompactLua

max_issues_repo_name: sygh-JP/CompactLua

max_forks_repo_name: sygh-JP/CompactLua


text:
// Copyright 2021 National Technology & Engineering Solutions of Sandia, LLC (NTESS). Under the terms of Contract DE-NA0003525 with NTESS, the U.S. Government retains certain rights in this software. See LICENSE.txt for details.
//
// Author: Denis Bueno

// Represented by HornTransStateSpace: What is common to all the sliced
// transition relations? The state variables of the transition system; the rule
// activation vars.
//
// Represented by HornSetTrans: What is different between the sliced transition
// relations? The transition relation itself. The inputs derived from the
// quantified vars. The inputs for the commander vars. The cones.

#define BOOST_RESULT_OF_USE_DECLTYPE

#include <boost/algorithm/cxx11/all_of.hpp>
#include <boost/range/algorithm/transform.hpp>
#include <boost/range/algorithm/copy.hpp>
#include <boost/iterator/transform_iterator.hpp>
#include <boost/optional.hpp>
#include <boost/program_options.hpp>
#include <boost/range.hpp>
#include <boost/range/adaptor/indexed.hpp>
#include <boost/range/combine.hpp>
#include <fstream>
#include <gmpxx.h>
#include <map>
#include <set>
#include <sstream>
#include <vector>
#include <z3++.h>

#include "checker_types.h"
#include "supp/expr_flattener.h"
#include "supp/expr_iterators.h"
#include "supp/expr_rewriter.h"
#include "supp/expr_substitution.h"
#include "supp/expr_supp.h"
#include "supp/nnf_rewriter.h"
#include "xsys/state_vars.h"
#include "xsys/vmt_transition_system.h"
#include "one_hot.h"

using namespace std;
using namespace euforia;

using euforia::vmt::VmtTransitionSystem;

namespace {
struct Config {
  string input_filename;
  bool allocate_vars_by_sort = false;
  bool allocate_inputs_by_sort = true;
  boost::optional<string> varmap_filename;
  bool slice_t = false;
  bool enable_one_hots = true;
};

Config config;

class Int2BvRewriter : public ExprRewriter<Int2BvRewriter>,
    public ExprVisitor<Int2BvRewriter, z3::expr> {
 public:
  Int2BvRewriter(z3::context& c, int bv_width) : bv_sort_(c.bv_sort(bv_width)) {}

  z3::expr operator()(const z3::expr& e) { return Rewrite(e); }

  z3::sort TranslateSort(const z3::sort& s) {
    switch (s.sort_kind()) {
      case Z3_INT_SORT:
        return bv_sort_;
      case Z3_ARRAY_SORT:
        return ctx().array_sort(TranslateSort(s.array_domain()),
                                TranslateSort(s.array_range()));
      default:
        return s;
    }
  }

  z3::expr visitExpr(const z3::expr& e) {
    return e.decl()(NewArgsExprVector(e));
  }

  z3::expr visitQUANTIFIER(const z3::expr& e) {
    z3::expr e_new(e.ctx());
    vector<Z3_sort> var_sorts;
    vector<Z3_symbol> var_names;
    for (unsigned i = 0; i < Z3_get_quantifier_num_bound(e.ctx(), e); i++) {
      z3::sort var_sort(e.ctx(), Z3_get_quantifier_bound_sort(e.ctx(), e, i));
      var_sorts.push_back(TranslateSort(var_sort));
      var_names.push_back(Z3_get_quantifier_bound_name(e.ctx(), e, i));
    }
    if (e.is_forall()) {
      Z3_pattern pats[0];
      e_new = z3::to_expr(
          e.ctx(),
          Z3_mk_forall(e.ctx(), 0, 0, pats, var_sorts.size(),
                       var_sorts.data(), var_names.data(), lookup(e.body())));
    } else if (e.is_exists()) {
      Z3_pattern pats[0];
      e_new = z3::to_expr(
          e.ctx(),
          Z3_mk_exists(e.ctx(), 0, 0, pats, var_sorts.size(),
                       var_sorts.data(), var_names.data(), lookup(e.body())));
    } else {
      EUFORIA_FATAL("unknown quantifier");
    }
    // logger.Log(0, "{}:{}", e, e.get_sort());
    // logger.Log(0, "{}:{}", e_new, e_new.get_sort());
    return e_new;
  }

  z3::expr visitVAR(const z3::expr& e) {
    auto ret = z3::to_expr(
        e.ctx(),
        Z3_mk_bound(e.ctx(), Z3_get_index_value(e.ctx(), e),
                    TranslateSort(e.get_sort())));
    return ret;
  }

  z3::expr visitANUM(const z3::expr& e) {
    string decimal_str;
    z3::expr bv(e.ctx());
    if (!e.is_numeral(decimal_str)) {
      EUFORIA_FATAL("not a numeral: {}", e);
    }
    logger.Log(4, "found numeral: {}", decimal_str);
    mpz_class num(decimal_str);
    string binstr = num.get_str(2);
    logger.Log(4, "    binary: {}", binstr);
    // create bits, which has num but padded with zeros
    string bits(bv_sort_.bv_size(), '0');
    int width = static_cast<int>(bv_sort_.bv_size());
    // binstr will be bits if num is positive, and -bits if num is negative
    if (binstr[0] != '-') {
      assert(binstr.size() > 0);
      assert(binstr.size() <= bv_sort_.bv_size());
      copy(binstr.begin(), binstr.end(),
           bits.begin() + (bits.size() - binstr.size()));
      bool bool_bits[width];
      // bits is in reverse order from what z3 expects; z3 wants LSB first
      for (int i = 0, j = width-1; i < width; i++, j--) {
        bool_bits[j] = bits[i] == '0' ? false : true;
      }
      bv = ctx().bv_val(width, bool_bits);
      logger.Log(4, "    binary padded: {}", bits);
    } else {
      assert(binstr.size() > 1);
      // create bits, which has num but padded with zeros
      copy(next(binstr.begin()), binstr.end(),
           next(bits.begin()) + (bits.size() - binstr.size()));
      logger.Log(4, "    binary uminus: {}", bits);
      bool bool_bits[width];
      // bits is in reverse order from what z3 expects; z3 wants LSB first
      for (int i = 0, j = width-1; i < width; i++, j--) {
        bool_bits[j] = bits[i] == '0' ? false : true;
      }
      bv = ctx().bv_val(width, bool_bits);
      // constant 1 bits
      for (int i = 0; i < width; i++) {
        bool_bits[i] = true;
      }
      auto all_ones = ctx().bv_val(width, bool_bits);
      // flip all the bits and add one: 2's complement representation
      bv = bv ^ all_ones;
      bv = bv + 1;
      bv = bv.simplify();
    }
    logger.Log(4, "    bv result: {}", bv);
    return bv;
  }

  z3::expr visitUNINTERPRETED(const z3::expr& e) {
    assert(!e.is_array());
    // Create an uninterpreted function that takes BVs instead of Ints
    auto e_decl = e.decl();
    vector<z3::sort> f_sorts;
    for (unsigned i = 0; i < e_decl.arity(); i++) {
      f_sorts.push_back(TranslateSort(e_decl.domain(i)));
    }
    auto f_decl = e.ctx().function(
        e_decl.name(), e_decl.arity(), f_sorts.data(),
        TranslateSort(e_decl.range()));
    return f_decl(NewArgsExprVector(e));
  }

  z3::expr visitSELECT(const z3::expr& e) {
    logger.Log(4, "select {}", e);
    for (auto&& arg : boost::make_iterator_range(args_begin(e), args_end(e))) {
      logger.Log(4, "    rewritten args {}:{}", arg, arg.get_sort());
    }
    return z3::select(arg(e,0), arg(e,1));
  }

  z3::expr visitSTORE(const z3::expr& e) {
    return z3::store(arg(e,0), arg(e,1), arg(e,2));
  }

  z3::expr visitEQ(const z3::expr& e) {
    return arg(e,0) == arg(e,1);
  }

  z3::expr visitADD(const z3::expr& e) {
    z3::expr ret(e.ctx());
    for (auto&& arg : boost::make_iterator_range(args_begin(e), args_end(e))) {
      ret = bool(ret) ? ret + arg : arg;
    }
    return ret;
  }

  z3::expr visitSUB(const z3::expr& e) {
    assert(e.num_args() == 2);
    return arg(e,0) - arg(e,1);
  }

  z3::expr visitUMINUS(const z3::expr& e) {
    return -arg(e,0);
  }

  z3::expr visitMUL(const z3::expr& e) {
    assert(e.num_args() == 2);
    return arg(e,0) * arg(e,1);
  }

  z3::expr visitDIV(const z3::expr& e) {
    return arg(e,0) / arg(e,1); // signed division
  }

  z3::expr visitIDIV(const z3::expr& e) {
    return arg(e,0) / arg(e,1);
  }

  z3::expr visitREM(const z3::expr& e) {
    return z3::srem(arg(e,0), arg(e,1));
  }

  z3::expr visitMOD(const z3::expr& e) {
    return z3::smod(arg(e,0), arg(e,1));
  }

  z3::expr visitLE(const z3::expr& e) {
    return arg(e,0) <= arg(e,1);
  }

  z3::expr visitLT(const z3::expr& e) {
    return arg(e,0) < arg(e,1);
  }

  z3::expr visitGE(const z3::expr& e) {
    return arg(e,0) >= arg(e,1);
  }

  z3::expr visitGT(const z3::expr& e) {
    return arg(e,0) > arg(e,1);
  }

  z3::context& ctx() const { return bv_sort_.ctx(); }

 private:
  z3::sort bv_sort_;
};

//^----------------------------------------------------------------------------^
//

class HornRule {
 public:
  HornRule(const z3::expr& rule, int index)
      : head_(rule.ctx()), body_(rule.ctx()), rule_(rule), index_(index) {
    auto b = rule;
    if (rule.is_quantifier()) {
      b = rule.body();
    } else if (is_not(rule) && rule.arg(0).is_quantifier()) {
      b = rule.arg(0).body();
    }
    body_ = ctx().bool_val(true);
    if (b.is_implies()) {
      head_ = b.arg(1);
      body_ = b.arg(0);
    } else {
      head_ = b;
    }
  }

  bool is_linear() const {
    IterExprSet visited;
    int relation_count =
        count_if(df_expr_ext_iterator::begin(body(), visited),
                 df_expr_ext_iterator::end(body(), visited),
                 [&](auto&& x) { return x.is_app() &&
                     x.decl().decl_kind() == Z3_OP_UNINTERPRETED; });
    // int relation_count =
    //     count_if(df_expr_iterator::begin(rule.body()),
    //              df_expr_iterator::end(rule.body()),
    //              [&](auto&& x) { return x.is_app() &&
    //                  relation_vars_.find(x.decl()) != relation_vars_.end(); });
    if (relation_count > 1) {
      return false;
      // throw std::runtime_error("nonlinear Horn clause detected, exiting");
    }
    return true;
  }

  bool is_query() const {
    if (is_literal_false(head())) {
      return true;
    }
   if (is_not(head()) &&
       head().arg(0).decl().decl_kind() == Z3_OP_UNINTERPRETED) {
     return true;
   }
   return false;
  }

  int index() const { return index_; }
  z3::context& ctx() const { return head_.ctx(); }
  z3::expr head() const { return head_; }
  z3::expr body() const { return body_; }
  operator z3::expr() const { return rule_; }
  std::string head_name() const {
    return head_.decl().name().str();
  }

 private:
  z3::expr head_;
  z3::expr body_;
  z3::expr rule_;
  int index_;
};

std::ostream& operator<<(std::ostream& os, const HornRule& r) {
  fmt::print(os, "HornRule: head {} body:\n{}", r.head(), r.body());
  return os;
}

//^----------------------------------------------------------------------------^
//

//! Groups a set of Horn clauses all of which have the same head symbol. The
//! head symbol is determined by the first rule added to the group.
class HornTransition {
 public:
  HornTransition() {}

  void AddRule(const HornRule& r, int i) {
    if (head_name_) {
      if (r.head_name() != head_name()) {
        throw std::runtime_error(
            fmt::format("adding bad rule to {} group: {}", *head_name_, r));
      }
    } else {
      head_name_ = r.head_name();
    }
    rules_.push_back({r,i});
  }

  const std::string& head_name() const { return *head_name_; }
  const std::vector<HornRule>& rules() const { return rules_; }

 private:
  boost::optional<std::string> head_name_;
  std::vector<HornRule> rules_;
};

//^----------------------------------------------------------------------------^
//

// Represents a complete set of Horn clauses -- a model checking instance -- as
// a collection of rules. Supports parsing both SMT2-style and
// declare-rel-style Horn clauses, thanks to z3.
class HornClauses {
 public:
  HornClauses(z3::context& c, const char *filename, bool int2bv = false)
      : ctx_(c) {

    // Reads file into buffer because we may need to parse twice
    std::ifstream fin(filename);
    std::stringstream sstr;
    sstr << fin.rdbuf();
    auto filebuf = sstr.str();

    // Parses as declare-rel at first
    z3::fixedpoint fp(ctx());
    auto vec = Z3_fixedpoint_from_string(c, fp, filebuf.c_str());
    if (!vec) {
      fmt::print(cerr, "Parse error: {}", filename);
      exit(1);
    }
    auto queries = z3::ast_vector_tpl<z3::expr>(c, vec);
    z3::expr_vector rules(c);
    rules = fp.rules();

    if (queries.size() > 0) {
      assert(queries[0].num_args() == 0);
      rules.push_back(z3::implies(queries[0], ctx().bool_val(false)));
    }

    if (rules.empty()) {
      logger.Log(2, "0 fp rules found, so parsing as smtlib2");
      // Parses again as SMTLIB-2 HORN file
      rules = ctx().parse_string(filebuf.c_str());
    }
    logger.Log(1, "parsed {} rules", rules.size());
    if (int2bv) {
      Int2BvRewriter rewrite_int2bv(ctx(), 32);
      for (unsigned i = 0; i < rules.size(); i++) {
        auto r = rewrite_int2bv(rules[i]);
        rules.set(i, r);
      }
    }
    rules_.reserve(rules.size());
    for (unsigned i = 0; i < rules.size(); i++) {
      rules_.push_back(HornRule(rules[i], i));
    }
  }

  z3::context& ctx() const { return ctx_; }

  // Iterates over the database as HornRules
  auto rules() const {
    return boost::make_iterator_range(rules_.begin(), rules_.end());
  }

  FuncDeclMap<HornTransition> group_by_heads() const {
    using namespace boost::adaptors; // indexed
    // Groups horn rules by head symbol
    FuncDeclMap<HornTransition> head2trans;
    for (const auto& indexed_rule : rules() | indexed(0)) {
      const auto& index = indexed_rule.index();
      const auto& rule = indexed_rule.value();
      head2trans[rule.head().decl()].AddRule(rule, index);
    }
    return head2trans;
  }

  size_t size() const { return rules_.size(); }

 private:
  z3::context& ctx_;
  // Contains all the rules plus the query written as a rule (false => head)
  std::vector<HornRule> rules_;
};

//^----------------------------------------------------------------------------^
//

using RelationVarMap = FuncDeclMap<z3::expr>;
using PlaceVarsMap = FuncDeclMap<vector<z3::expr>>;

static string SortName(const z3::sort& sort) {
  if (sort.is_bv()) {
    return fmt::format("bv{}", sort.bv_size());
  } else if (sort.is_bool()) {
    return "bool";
  } else if (sort.is_array()) {
    auto domain_name = SortName(sort.array_domain());
    auto range_name = SortName(sort.array_range());
    return fmt::format("arr-{}-{}", domain_name, range_name);
  } else {
    fmt::print("{}\n", sort);
    EUFORIA_FATAL("unhandled sort");
  }
}

//! Represents the state space for translating a set of Horn clauses. Creates
//! relation variables, place variables, and rule activation inputs. All such
//! objects are created in the current output transition system, set in the
//! constructor and via set_output_xsys.
//!
//! This can be used to represent the state space for an entire set of clauses.
//! But it also has the flexibility of representing the state space for a
//! subset of clauses.
class HornTransStateSpace {
 public:
  HornTransStateSpace() : xsys_(nullptr) {}
  HornTransStateSpace(Config& cfg, const std::vector<HornRule>& rules,
                      VmtTransitionSystem *xsys)
      : xsys_(xsys) {
    SortMap<std::vector<z3::expr>> relation_places_by_sort;
    for (const auto& rule : rules) {
      logger.Log(3, "creating state space for rule: {} => {}", rule.body(),
                 rule.head());
      // Creates rule activation variables
      auto rule_activation_input =
          ctx().bool_const(("r-" + to_string(rule.index())).c_str());
      auto& rule_activation = xsys_->AddInput(MakeInput(rule_activation_input));
      activation_input_vars_.push_back(rule_activation);
      // Pick up relations from rule heads; then declare Boolean relation vars
      // and place vars for each place.
      if (auto decl = rule.head().decl();
          decl.decl_kind() == Z3_OP_UNINTERPRETED) {
        // Create r elation var
        auto relation_name = decl.name().str();
        auto var_name = "at-" + relation_name;
        if (xsys_->FindVar(var_name)) { // Skips present variables.
          continue;
        }
        auto& var = xsys_->AddVar(MakeStateVar(
                ctx().bool_const(var_name.c_str()),
                ctx().bool_const((var_name + "+").c_str())));
        relation_vars_.insert({decl, var.current()});
        // Ensures vector is initialized for all relations, even nullary ones
        (void)place_vars_[decl];
        // Open varmap file, if we need to
        ofstream varmap_out;
        if (cfg.varmap_filename) {
          varmap_out = ofstream(*cfg.varmap_filename);
          if (!varmap_out) {
            fmt::print(cerr, "warning: could not open varmap file: {}:\n{}\n",
                       *cfg.varmap_filename, strerror(errno));
            cfg.varmap_filename = boost::none;
          }
        }
        if (cfg.allocate_vars_by_sort) {
          SortMap<int> counts;
          for (unsigned i = 0; i < decl.arity(); i++) {
            if (counts.find(decl.domain(i)) == counts.end()) {
              counts[decl.domain(i)] = 0;
            }
            counts[decl.domain(i)] += 1;
          }
          for (auto&& [sort, num_occurrences] : counts) {
            int num_places =
                static_cast<int>(relation_places_by_sort[sort].size());
            for (int i = 0; i < (num_occurrences - num_places); i++) {
              auto name =
                  (SortName(sort) + "-place-" + to_string(num_places+i));
              auto& place_var = xsys_->AddVar(MakeStateVar(
                      ctx().constant(name.c_str(), sort),
                      ctx().constant((name + "+").c_str(), sort)));
              relation_places_by_sort[sort].push_back(place_var.current());
            }
          }
          counts.clear();
          for (unsigned i = 0; i < decl.arity(); i++) {
            auto place_var = relation_places_by_sort.at(
                decl.domain(i))[counts[decl.domain(i)]];
            if (varmap_out) {
              fmt::print(varmap_out, "Relation {} place {} mapped to var {}\n",
                         relation_name, i, place_var);
            }
            // EUFORIA_DEBUG_BREAK;
            place_vars_[decl].push_back(place_var);
            counts[decl.domain(i)]++;
          }
        } else {
          // allocate vars by relation
          for (unsigned i = 0; i < decl.arity(); i++) {
            auto place_name = relation_name + "-place-" + to_string(i);
            auto& place_var = xsys_->AddVar(MakeStateVar(
                    ctx().constant(place_name.c_str(), decl.domain(i)),
                    ctx().constant((place_name + "+").c_str(),
                                   decl.domain(i))));
            if (varmap_out) {
              fmt::print(varmap_out, "Relation {} place {} mapped to var {}\n",
                         relation_name, i, place_var.current());
            }
            place_vars_[decl].push_back(place_var.current());
          }
        }
      }
    }
    logger.Log(3, "created {} state variables", xsys_->num_vars());
    if (logger.ShouldLog(4)) {
      for (auto&& v : xsys_->vars()) {
        logger.Log(4, "  {}", v.current());
      }
    }
    logger.Log(3, "created {} inputs", xsys_->num_inputs());
  }

  const StateVar& get_head_relation_var(const HornRule& r) const {
    auto& v_expr = relation_vars_.at(r.head().decl());
    return *xsys_->FindVar(v_expr);
  }

  const PrimaryInput& get_activation_var(const HornRule& r) const {
    auto& i_expr = activation_input_vars_.at(r.index());
    return *xsys_->FindInput(i_expr);
  }

  auto iter_place_vars(const z3::expr& e) const {
    class GetVar {
     public:
      GetVar(const VmtTransitionSystem& xsys) : xsys_(xsys) {}
      const StateVar& operator()(const z3::expr& var) const {
        return *xsys_.FindVar(var);
      }
     private:
      const VmtTransitionSystem& xsys_;
    };
    const auto& place_var_vec = place_vars_.at(e.decl());
    return boost::make_iterator_range(
        boost::make_transform_iterator(begin(place_var_vec),
                                       GetVar(*xsys_)),
        boost::make_transform_iterator(end(place_var_vec),
                                       GetVar(*xsys_)));
  }

  //! Iterates over the place variables for the relation in r's head
  auto iter_head_place_vars(const HornRule& r) const {
    return iter_place_vars(r.head());
  }

  //! Iterates over the Boolean relation vars in the transition system
  auto relation_vars() const {
    class GetVar {
     public:
      GetVar(const VmtTransitionSystem& xsys) : xsys_(xsys) {}
      const StateVar& operator()(const RelationVarMap::value_type& p) const {
        return *xsys_.FindVar(p.second);
      }
      const VmtTransitionSystem& xsys_;
    };
    return boost::make_iterator_range(
        boost::make_transform_iterator(relation_vars_.begin(), GetVar(*xsys_)),
        boost::make_transform_iterator(relation_vars_.end(), GetVar(*xsys_)));
  }

  auto activation_input_vars_begin() const {
    return activation_input_vars_.cbegin();
  }

  auto activation_input_vars_end() const {
    return activation_input_vars_.cend();
  }

  //! Returns zipped iterator over [ <e-arg-0, place-var-0>, <e-arg-1,
  //! place-var-1>, ... ]. Precondition: e must be an unintpreted Horn relation
  //! symbol.
  auto iter_args_with_places(const z3::expr& e) const {
    assert(e.num_args() == place_vars_.at(e.decl()).size());
    return boost::combine(ExprArgs(e), iter_place_vars(e));
  }

  //! Finds Boolean relation var for uninterpreted application e
  boost::optional<z3::expr> find_relation_var(const z3::expr& e) const {
    if (auto search = relation_vars_.find(e.decl());
        search != relation_vars_.end()) {
      return search->second;
    }
    return boost::none;
  }

  z3::context& ctx() const { return xsys_->ctx(); }
  VmtTransitionSystem& xsys() const { return *xsys_; }
  size_t num_relations() const { return relation_vars_.size(); }

  void set_output_xsys(VmtTransitionSystem *xsys) { xsys_ = xsys; }

 private:
  // output to
  VmtTransitionSystem *xsys_;
  // Maps func_decl to Boolean state var
  RelationVarMap relation_vars_;
  // List of Boolean state vars
  std::vector<z3::expr> activation_input_vars_;
  // Maps func_decl to list of place state vars
  PlaceVarsMap place_vars_;
};

//^----------------------------------------------------------------------------^
//
//! Helper for rewriting the bodies of Horn clauses in terms of relation vars
//! and place vars
class Horn2VmtRewriter : public ExprRewriter<Horn2VmtRewriter> {
 public:
  Horn2VmtRewriter(const HornTransStateSpace& space) : space_(space) {}

  z3::expr operator()(const z3::expr& e) { return Rewrite(e); }

  // Precondition: e is a sub-formula of a Horn clause body.
  // If e is a relation occurrence, rewrites it in T-land using the relation
  // and place variables. Otherwise, simply rewrites e using previously
  // rewritten children.
  z3::expr visit(const z3::expr& e) {
    if (e.is_app()) {
      if (auto e_var = space_.find_relation_var(e)) {
        z3::expr_vector conj(e.ctx());
        ExprVectorInserter out(conj);
        *out++ = *e_var;
        for (auto&& zipped : space_.iter_args_with_places(e)) {
          z3::expr arg = boost::get<0>(zipped);
          const StateVar& place_var = boost::get<1>(zipped);
          *out++ = (arg == place_var.current());
        }
        return expr_mk_and(conj);
      }
      return e.decl()(NewArgsExprVector(e));
    }
    return e;
  }

 private:
  const HornTransStateSpace& space_;
};

//^----------------------------------------------------------------------------^
//
//! Represents the translation of a set of Horn clauses into a transition
//! relation. The transition relation is "functional" in that each state
//! variable has exactly one top-level equation for it; the activation vars are
//! also at the top level as implications.
//!
//! Anything head isn't simply H(...) for some uninterpreted H gets put into
//! queries()
class HornSetTrans {
 public:
  HornSetTrans(const HornTransStateSpace& space,
                     const std::vector<HornRule>& rules)
      : trans_(space.ctx()), to_vmt_(space) {
    ExprAndInserter trans_out(trans_);
    CreateQuantifiedVarInputs(space, rules);
    for (const auto& rule : rules) {
      if (rule.head().decl().decl_kind() != Z3_OP_UNINTERPRETED) {
        queries_.push_back(rule);
        continue;
      }
      const auto& activation_var = space.get_activation_var(rule);
      // Translates head and body.
      if (config.allocate_vars_by_sort) {
        // Don't worry about it if we're using the normal allocation strategy
        if (!rule.is_linear()) {
          throw std::runtime_error("nonlinear Horn clause detected, exiting");
        }
      }
      // Fills in var_subst_curr for rule: find var occurrences in relations:
      // 1. if it's a variable, maps [var -> place curr-state variable];
      // 2. otherwise, maps [var -> fresh input]
      ExprSubstitution var_subst_curr = make_var_subst(space, rule);
      // Removes relation occurrences from the rule's body and replaces them
      // with relation vars and place vars
      auto body_condition = to_vmt_(rule.body());
      logger.Log(3, "Rule {} condition from Horn:\n{}", rule.index(),
                 body_condition);
      // Removes bound vars from body_condition
      body_condition = var_subst_curr(body_condition);
      auto rule_condition = z3::implies(activation_var, body_condition);
      logger.Log(2, "Global rule {} condition to emit:\n{}",
                 rule.index(), rule_condition);
      // Done processing body, but it hasn't emitted the rule yet: it'll figure
      // out below which one to emit.

      *trans_out++ = rule_condition; // emit the rule condition

      // Adds this rule's next state to state-update cones
      CreateConesFromRule(space, rule, var_subst_curr);
    }

    // Sends next-state cones, which are complete, to the transition relation
    for (auto it = cones_.begin(), ie = cones_.end(); it != ie;
         // Erases them because they could free a lot of memory
         it = cones_.erase(it)) {
      auto&& [next_var, val] = *it;
      if (next_var.is_bool()) {
        val = val.simplify();
      }
      *trans_out++ = (next_var == val);
    }

    // Adds one-hot constraints for rules: exactly one rule should be chosen on
    // each transition.
    if (config.enable_one_hots) {
      OneHotConstraints ohc(space.ctx());
      ohc.insert(space.activation_input_vars_begin(),
                 space.activation_input_vars_end());
      if (space.activation_input_vars_begin() !=
          space.activation_input_vars_end()) {
        *trans_out++ = ohc.at_most(OneHotConstraints::Config::Commander(3));
        // *trans_out++ = ohc.at_most(OneHotConstraints::Config::Naive());
        for (auto&& v : ohc.commander_vars()) {
          space.xsys().AddInput(MakeInput(v));
        }
      }
    }
  }

  void CreateConesFromRule(const HornTransStateSpace& space,
                      const HornRule& rule,
                      const ExprSubstitution& var_subst_curr) {
      const auto& activation_var = space.get_activation_var(rule);
      const auto& relation_var = space.get_head_relation_var(rule);
      // The code below fills in cones_, the list of next-state equations for
      // the state variables updated by this rule.
      auto else_elt =
          cones_.insert({relation_var.next(),
                        relation_var.current()}).first;
      else_elt->second = z3::ite(activation_var, rule.ctx().bool_val(true),
                                 else_elt->second);
      for (auto&& zipped : space.iter_args_with_places(rule.head())) {
        z3::expr arg = boost::get<0>(zipped);
        const StateVar& place_var = boost::get<1>(zipped);
        else_elt =
            cones_.insert({place_var.next(),
                          place_var.current()}).first;
        else_elt->second = z3::ite(activation_var, var_subst_curr(arg),
                                   else_elt->second);
      }
      logger.Log(3, "cones fir this rule");
      for (auto&& [next_var, val] : cones_) {
        logger.Log(3, "    {}: {}", next_var, val);
      }
  }

  // outputs to rule_input_vars_
  void CreateQuantifiedVarInputs(const HornTransStateSpace& space,
                                 const vector<HornRule>& rules) {
    SortMap<std::vector<PrimaryInputRef>> rule_places_by_sort;
    for (auto& rule : rules) {
      // Makes any inputs required to express the quantified variables in the
      // rule, binning them by sort
      if (z3::expr rule_expr = rule; rule_expr.is_quantifier()) {
        const unsigned num_bound_vars =
            Z3_get_quantifier_num_bound(rule_expr.ctx(), rule_expr);
        if (config.allocate_inputs_by_sort) {
          SortMap<int> counts;
          for (unsigned i = 0; i < num_bound_vars; i++) {
            z3::sort sort(
                rule_expr.ctx(),
                Z3_get_quantifier_bound_sort(rule_expr.ctx(), rule_expr, i));
            if (counts.find(sort) == counts.end()) {
              counts[sort] = 0;
            }
            counts[sort]++;
          }
          for (auto&& [sort, num_occurrences] : counts) {
            int num_places =
                static_cast<int>(rule_places_by_sort[sort].size());
            for (int i = 0; i < (num_occurrences - num_places); i++) {
              auto name =
                  (SortName(sort) + "-input-" + to_string(num_places+i));
              auto& input_var = space.xsys().AddInput(MakeInput(
                      ctx().constant(name.c_str(), sort)));
              rule_places_by_sort[sort].push_back(input_var);
            }
          }
          counts.clear();
          for (unsigned i = 0; i < num_bound_vars; i++) {
            z3::sort sort(
                rule_expr.ctx(),
                Z3_get_quantifier_bound_sort(rule_expr.ctx(), rule_expr, i));
            auto var = rule_places_by_sort.at(sort)[counts[sort]];
            rule_input_vars_[rule.index()].push_back(var);
            counts[sort]++;
          }
          // Apparently the de-bruijn indices of variables are the revers from
          // the way they would be in a list...there's some verbiage to this
          // effect in the constructor for forall's in the Z3 documentation but
          // I didn't realize it would extend to this API. I guess it does.
          std::reverse(rule_input_vars_[rule.index()].begin(),
                       rule_input_vars_[rule.index()].end());
        } else {
          // Create inputs named input-<rule-number>-<deBruijn index>
          for (unsigned i = 0; i < num_bound_vars; i++) {
            z3::sort sort(
                rule_expr.ctx(),
                Z3_get_quantifier_bound_sort(rule_expr.ctx(), rule_expr, i));
            z3::symbol var_name(
                rule_expr.ctx(),
                Z3_get_quantifier_bound_name(rule_expr.ctx(), rule_expr, i));
            auto name = fmt::format("input-{}-{}", rule.index(), var_name.str());
            auto& input_var = space.xsys().AddInput(
                MakeInput(ctx().constant(name.c_str(), sort)));
            rule_input_vars_[rule.index()].push_back(input_var);
          }
          std::reverse(rule_input_vars_[rule.index()].begin(),
                       rule_input_vars_[rule.index()].end());
        }
      }

    }
  }

  z3::expr trans() const { return trans_; }
  z3::context& ctx() const { return trans_.ctx(); }

  auto queries() {
    return boost::make_iterator_range(queries_.begin(), queries_.end());
  }

  z3::expr translate(const z3::expr& e) {
    return to_vmt_(e);
  }

  const PrimaryInput& get_rule_input_var(const HornRule& r,
                                         const z3::expr& bound_var) const {
    // The inputs are indexed by rule and de-Bruijn index of the bound var
    return rule_input_vars_.at(r.index()).at(
        Z3_get_index_value(bound_var.ctx(), bound_var));
  }

 private:
  // Transition relation that has been translated from the Horn set
  z3::expr trans_;
  // Maps rule index to quantifier var place inputs
  unordered_map<int, vector<PrimaryInputRef>> rule_input_vars_;
  ExprMap<z3::expr> cones_;
  std::vector<HornRule> queries_;
  Horn2VmtRewriter to_vmt_;
  ExprSubstitution make_var_subst(
      const HornTransStateSpace&, const HornRule& rule);
};

ExprSubstitution HornSetTrans::make_var_subst(
    const HornTransStateSpace& space, const HornRule& rule) {
  ExprSubstitution var_subst_curr(rule.ctx());
  // Set of vars mapped to places by visit_map_var()
  IterExprSet vars_with_places;
  // Set of all visited nodes for df traversal
  IterExprSet visited;
  // Precondition: e is a sub-expression of rule.body().
  // visit_map_var(), for a relation occurrence R(a,b,c,...), looks in a,b,c
  // for variable occurrences (as opposed to expressions) and maps them
  // directly to place vars, because this helps EUForia's pre-image
  // computation.
  auto visit_map_var = [&](const z3::expr& e) {
    if (e.is_app()) {
      if (auto e_var = space.find_relation_var(e)) {
        logger.Log(3, "--- visiting relation {}", e.decl());
        for (auto&& zipped : space.iter_args_with_places(e)) {
          z3::expr arg = boost::get<0>(zipped);
          const StateVar& place_var = boost::get<1>(zipped);
          if (arg.is_var()) {
            vars_with_places.insert(arg);
            logger.Log(3, "adding place_var [{} / {}] to var_subst_curr",
                       arg, place_var);
            var_subst_curr.AddSubstitution(arg, place_var.current());
          }
        }
      }
    }
  };
  // Precondition: e is a sub-expression of anything in rule that hasn't been
  // visited by visit_map_var().
  auto visit_create_input = [&](const z3::expr& e) {
    if (e.is_var()) {
      // for (unsigned i = 0; i < rule_input_vars.size(); i++) {
      //   auto input = rule_input_vars[i];
      //   logger.Log(3, "    rule_place {}: {}:{}", i, input, input.get_sort());
      // }
      // const z3::expr& i_expr = rule_input_vars[Z3_get_index_value(e.ctx(), e)];
      const z3::expr& i_expr = get_rule_input_var(rule, e);
      // auto fresh_input =
      //     ctx().constant(("y-" + to_string(counter_++)).c_str(), e.get_sort());
      // auto& input = xsys_.AddInput(MakeInput(fresh_input));
      var_subst_curr.AddSubstitution(e, i_expr);
      logger.Log(3, "adding input [{} / {}] to var_subst_curr", e, i_expr);
    }
  };

  // put var -> place in subst for anything in body
  for_each(df_expr_ext_iterator::begin(rule.body(), visited),
           df_expr_ext_iterator::end(rule.body(), visited), visit_map_var);
  // fill in rest woth var -> input, over body and head, but skip visiting any
  // vars already mapped to places
  visited = vars_with_places;
  for_each(df_expr_ext_iterator::begin(rule.body(), visited),
           df_expr_ext_iterator::end(rule.body(), visited), visit_create_input);
  for_each(df_expr_ext_iterator::begin(rule.head(), visited),
           df_expr_ext_iterator::end(rule.head(), visited), visit_create_input);
  return var_subst_curr;
}

} // end anonymous namespace

//^----------------------------------------------------------------------------^
//

class Horn2Vmt {
 public:
  Horn2Vmt(const HornTransStateSpace& space, const vector<HornRule>& all_rules)
      : state_space_(space), rules_(all_rules) {
    // Sets transition relation
    HornSetTrans all_trans(state_space_, all_rules);
    xsys().set_trans(all_trans.trans());

    // Sets property
    for (const auto& rule : all_trans.queries()) {
      if (is_not(rule.head()) &&
          rule.head().arg(0).decl().decl_kind() == Z3_OP_UNINTERPRETED) {
        // property is denoted by (assert !R)
        xsys().set_property(all_trans.translate(rule.head()));
      } else if (z3::eq(rule.head(), ctx().bool_val(false))) {
        // property is denoted by (R => false)
        xsys().set_property(!all_trans.translate(rule.body()));
      } else {
        EUFORIA_FATAL("unrecognized rule: {} => {}", rule.body(), rule.head());
      }
    }

    // Sets initial state. In the initial state, all relations are false.
    z3::expr init(ctx());
    boost::transform(
        state_space_.relation_vars(), ExprAndInserter(init),
        [&](auto&& var) { return !var.current(); });
    xsys().set_init_state(init);

    // Performs normalizations that make Z3 a happy boi
    NnfRewriter nnf;
    ExprFlattener flatten;
    auto normalize = [&](auto&& e) {
      nnf.Reset(); flatten.Reset(); return flatten(nnf(e)); };
    xsys().RewriteSystem(normalize);
  }

  void Print(std::ostream& os) const {
    int64_t index = 0;
    fmt::print(os, "; {} rules\n", rules_.size());
    fmt::print(os, "; {} relations\n", state_space_.num_relations());
    fmt::print(os, "; {} state vars\n", xsys().num_vars());
    for (auto&& var : xsys().vars()) {
      fmt::print(os, "{}\n", var.current().decl());
      fmt::print(os, "{}\n", var.next().decl());
      fmt::print(os, "(define-fun .def{} () {} (! {} :next {}))\n", index,
                 var.current().get_sort(), var.current(),
                 var.next());
      ++index;
    }
    fmt::print(os, "; {} inputs\n", xsys().num_inputs());
    for (const z3::expr& input : xsys().inputs()) {
      fmt::print(os, "{}\n", input.decl());
    }
    fmt::print(os, "(define-fun .def{} () Bool (! {} :init true))\n",
               index++, xsys().init_state());
    fmt::print(os, "(define-fun .def{} () Bool (! {} :trans true))\n",
               index++, xsys().trans());
    fmt::print(os, "(define-fun .def{} () Bool (! {} :invar-property 0))\n",
               index, xsys().property());
  }

  // XXX instead of vmt print this in SMT2??????
  void PrintTrans(std::ostream& os) {
    int64_t index = 0;
    fmt::print(os, "; {} rules\n", rules_.size());
    fmt::print(os, "; {} relations\n", state_space_.num_relations());
    fmt::print(os, "; {} state vars\n", xsys().num_vars());
    fmt::print(os, "; begin state vars\n");
    // XXX print all declares in a block then print the defines after in a block so they're easier to delet
    for (auto&& var : xsys().vars()) {
      fmt::print(os, "{}\n", var.current().decl());
      fmt::print(os, "{}\n", var.next().decl());
      // fmt::print(os, "(define-fun .def{} () {} (! {} :next {}))\n", index,
      //            var.current().get_sort(), var.current(),
      //            var.next());
      ++index;
    }
    fmt::print(os, "; end state vars\n");
    fmt::print(os, "; {} inputs\n", xsys().num_inputs());
    fmt::print(os, "; begin inputs\n");
    for (const z3::expr& input : xsys().inputs()) {
      fmt::print(os, "{}\n", input.decl());
    }
    fmt::print(os, "; end inputs\n");
    fmt::print(os, "(declare-fun .trans () Bool)\n");
    fmt::print(os, "(assert (= .trans {}))\n", xsys().trans());
    // fmt::print(os, "(define-fun .def{} () Bool (! {} :trans true))\n",
    //            index++, xsys().trans());
  }

  z3::context& ctx() const { return state_space_.ctx(); }

 private:
  const HornTransStateSpace& state_space_;
  const vector<HornRule>& rules_;

  const VmtTransitionSystem& xsys() const { return state_space_.xsys(); }
  VmtTransitionSystem& xsys() { return state_space_.xsys(); }
};

//^----------------------------------------------------------------------------^
//
namespace po = boost::program_options;

po::options_description desc("options");

int main(int argc, char **argv) {
  // option parsing
  desc.add_options()
      ("help,h", "help")
      ("v", po::value<int>()->default_value(0), "set log level")
      ("int2bv", "convert ints to bvs as well")
      ("slice", po::value<string>()->default_value(""),
       "output sliced transition using given prefix (suppresses normal output)")
      ("onehots", po::value<bool>()->default_value(true),
       "enable explicit one-hot transition constraints")
      ("varmap", po::value<string>(),
       "output mapping between relation places and state variables to this file")
      ("strategy", po::value<string>()->default_value("relation"),
       "sort - allocates one state variable per distinct place of a given sort\nrelation - allocates one state variable per relation place")
      ("input-file", po::value<string>(), "SMT2 file to convert");
  po::positional_options_description pd;
  pd.add("input-file", -1);
  po::variables_map opts;
  po::store(po::command_line_parser(argc, argv).
            options(desc).positional(pd).run(), opts);
  po::notify(opts);

  if (!opts.count("input-file")) {
    fmt::print(cerr, "error: missing input-file\n");
  }
  if (opts.count("help") || !opts.count("input-file")) {
    fmt::print(cout, "{} input-file\n", argv[0]);
    fmt::print(cout, "{}\n", desc);
    return EXIT_FAILURE;
  }

  logger.set_level(opts["v"].as<int>());

  config.enable_one_hots = opts["onehots"].as<bool>();

  config.allocate_vars_by_sort = true;
  if (opts["strategy"].as<string>() == "relation") {
    config.allocate_vars_by_sort = false;
  }
  if (auto strat = opts["strategy"].as<string>();
      !(strat == "sort" || strat == "relation")) {
    fmt::print(cerr, "error: unknown variable allocation strategy: {}\n",
               strat);
    return EXIT_FAILURE;
  }

  if (opts.count("varmap")) {
    config.varmap_filename = string(opts["varmap"].as<string>());
  }

  auto slice_prefix = opts["slice"].as<string>();
  config.slice_t = slice_prefix != "";

  z3::context ctx;
  config.input_filename = opts["input-file"].as<string>();
  HornClauses clause_db(ctx, config.input_filename.c_str(),
                        bool(opts.count("int2bv")));
  if (config.slice_t) {
    logger.Log(1, "config: slicing T into multiple files");
    int i = 0;
    auto head2trans = clause_db.group_by_heads();
    vector<HornTransition> queries;
    VmtTransitionSystem xsys(ctx);
    vector<HornRule> all_rules;
    boost::copy(clause_db.rules(), back_inserter(all_rules));
    HornTransStateSpace space(config, all_rules, &xsys);
    for (auto&& [head, horn_trans] : head2trans) {
      if (boost::algorithm::all_of(
              horn_trans.rules(),
              [](const HornRule& r) { return r.is_query(); })) {
        logger.Log(0, "skipping {} queries due to T slicing",
                   horn_trans.rules().size());
        continue;
      }

      // Inputs for quantified vars will be created during translation to Vmt;
      // make sure those go into xsys_copy since they shouldn't interact with
      // other slices of T.
      VmtTransitionSystem xsys_copy(xsys);
      space.set_output_xsys(&xsys_copy);
      logger.Log(1, "translating {} clauses for slice of {}",
                 horn_trans.rules().size(), head.name());
      std::vector<HornRule> rules;
      boost::copy(horn_trans.rules(), back_inserter(rules));
      Horn2Vmt h2v(space, rules);
      ofstream trans_out(fmt::format("{}{}.vmt", slice_prefix, i));
      fmt::print(trans_out, "; common head: {}\n", head.name());
      h2v.PrintTrans(trans_out);
      logger.Log(1, "slice of {} written to {}{}.vmt", head.name(),
                 slice_prefix, i);
      i++;
    }
  } else {
    VmtTransitionSystem xsys(ctx);
    std::vector<HornRule> all_rules;
    boost::copy(clause_db.rules(), back_inserter(all_rules));
    HornTransStateSpace space(config, all_rules, &xsys);
    Horn2Vmt h2v(space, all_rules);
    h2v.Print(std::cout);
  }

  if (config.varmap_filename) {
    logger.Log(1, "wrote varmap to {}", *config.varmap_filename);
  }

  return EXIT_SUCCESS;
}

ext: cc

max_stars_repo_name: dbueno/euforia

max_issues_repo_name: dbueno/euforia

max_forks_repo_name: dbueno/euforia


text:
#include <memory>

#include <thread>

#include <viz3d/ui.h>
#include <viz3d/vtk_window.h>
#include <misc/cpp/imgui_stdlib.h>

#include <vtkConeSource.h>
#include <vtkNamedColors.h>
#include <vtkNew.h>
#include <vtkPolyDataMapper.h>
#include <vtkProperty.h>
#include <vtkStructuredPoints.h>
#include <vtkPointData.h>
#include <vtkFloatArray.h>
#include <vtkCellData.h>

#include <Eigen/Dense>

// Define a Custom viz3d::ImGuiWindow to add custom ImGUI Components
struct TestWindow : viz3d::ImGuiWindow {

    TestWindow(std::string &&winname) : viz3d::ImGuiWindow(std::move(winname)) {}

    void DrawImGUIContent() override {
        ImGui::Text("This is a Custom Defined ImGui Window !");
        ImGui::InputText("Write a string", &test_string);
        ImGui::Text(test_string.c_str());
    }

    std::string test_string;
};

// A Point Cloud Actor (fills the content of a PolyData), with a scalar field
auto GetPointCloudActor() {
    auto poly_data = vtkSmartPointer<vtkPolyData>::New();
    int num_points_per_primitive = 10000;
    int num_primitives = 3;
    int num_points = num_primitives * num_points_per_primitive;

    // Setup an array of Points
    vtkNew<vtkPoints> points;
    points->SetDataTypeToFloat();
    points->Allocate(num_points);
    points->SetNumberOfPoints(num_points);
    points->GetData()->SetName("Points_XYZ");
    poly_data->SetPoints(points.GetPointer());

    // Assign for each cell vertex indices
    vtkNew<vtkIdTypeArray> cells;
    cells->SetNumberOfValues(num_points * 2);
    vtkIdType *ids = cells->GetPointer(0);
    for (vtkIdType i = 0; i < num_points; ++i) {
        ids[i * 2] = 1; // num points in the cell = 1
        ids[i * 2 + 1] = i; // pid
    }
    vtkSmartPointer<vtkCellArray> cellArray = vtkSmartPointer<vtkCellArray>::New();
    cellArray->SetCells(num_points, cells.GetPointer());
    poly_data->SetVerts(cellArray);

    // Construct a Scalar field (to see colors)
    vtkNew<vtkFloatArray> scalar_values;
    scalar_values->Allocate(num_points);
    scalar_values->SetNumberOfTuples(num_points);
    scalar_values->SetName("Z");
    poly_data->GetPointData()->AddArray(scalar_values);

    // Generate the points randomly from 3 different planes
    for (auto k(0); k < num_primitives; ++k) {
        auto generate_point = [k]() {
            Eigen::Vector3f random = Eigen::Vector3f::Random();
            random[k] = 0;
            return random;
        };
        for (auto i(0); i < num_points_per_primitive; ++i) {
            Eigen::Vector3f random = generate_point();
            auto idx = k * num_points_per_primitive + i;
            points->SetPoint(idx, random.data());
            scalar_values->SetValue(idx, random.z());
        }
    }
    poly_data->GetPointData()->SetActiveScalars("Z");
    vtkNew<vtkPolyDataMapper> polydata_mapper;
    polydata_mapper->SetInputData(poly_data.Get());

    vtkNew<vtkActor> coneActor;
    coneActor->SetMapper(polydata_mapper);

    return coneActor;
}

// Generate a Cone Actor
auto GetConeActor() {
    vtkNew<vtkNamedColors> colors;
    vtkNew<vtkConeSource> cone;
    cone->SetHeight(3.0);
    cone->SetRadius(1.0);
    cone->SetResolution(20);
    vtkNew<vtkPolyDataMapper> coneMapper;
    coneMapper->SetInputConnection(cone->GetOutputPort());
    vtkNew<vtkActor> coneActor;
    coneActor->SetMapper(coneMapper);
    return coneActor;
}

// Get Lines Actor
auto GetLineActor() {
    const auto num_lines = 10;
    const auto num_points = num_lines + 1;

    auto poly_data = vtkSmartPointer<vtkPolyData>::New();

    // Setup the array of points
    auto vtk_points = vtkSmartPointer<vtkPoints>::New();
    vtk_points->SetDataTypeToFloat();
    vtk_points->Allocate(num_points);
    vtk_points->SetNumberOfPoints(num_points);
    vtk_points->GetData()->SetName("Points_XYZ");
    poly_data->SetPoints(vtk_points.GetPointer());

    // Assign for each cell vertex indices
    auto cell_ids = vtkSmartPointer<vtkIdTypeArray>::New();
    cell_ids->SetNumberOfValues(num_lines * 3);
    vtkIdType *ids = cell_ids->GetPointer(0);
    for (vtkIdType line_id = 0; line_id < num_lines; ++line_id) {
        auto cell_id = line_id * 3;
        ids[cell_id] = 2; // num points in the cell = 2
        ids[cell_id + 1] = line_id; // origin pid
        ids[cell_id + 2] = line_id + 1; // pid of the endpoint of the line
    }

    double scale = 5.;

    vtkSmartPointer<vtkCellArray> cellArray = vtkSmartPointer<vtkCellArray>::New();
    cellArray->SetCells(num_lines, cell_ids.GetPointer());
    poly_data->SetLines(cellArray);

    auto color_field = vtkSmartPointer<vtkFloatArray>::New();
    color_field->Allocate(num_lines);
    color_field->SetName("Scalar");
    color_field->SetNumberOfTuples(num_points);
    poly_data->GetCellData()->AddArray(color_field);

    Eigen::Vector3f previous_point = Eigen::Vector3f::Random() * scale;
    for (auto line_idx(0); line_idx < num_lines; line_idx++) {

        if (line_idx == 0)
            vtk_points->SetPoint(0, previous_point.data());

        Eigen::Vector3f new_point = Eigen::Vector3f::Random() * scale;
        vtk_points->SetPoint(line_idx + 1, new_point.data());
        previous_point = new_point;

        color_field->SetValue(line_idx, float(line_idx) / (num_lines - 1));
    }
    poly_data->GetCellData()->SetActiveScalars("Scalar");

    vtkNew<vtkPolyDataMapper> polydata_mapper;
    polydata_mapper->SetInputData(poly_data.Get());

    vtkNew<vtkActor> poly_data_actor;
    poly_data_actor->SetMapper(polydata_mapper);

    return poly_data_actor;
}

int main(int argc, char **argv) {
    auto &gui = viz3d::GUI::Instance();
    gui.AddWindow(std::make_shared<TestWindow>("Test Window"));

    {
        auto vtk_window = std::make_shared<viz3d::VTKWindow>("VTK Window");
        vtk_window->AddActor(GetConeActor());
        gui.AddWindow(vtk_window);
    }

    size_t window_id;
    {
        auto vtk_window2 = std::make_shared<viz3d::VTKWindow>("VTK Window 2");
        vtk_window2->AddActor(GetPointCloudActor());
        vtk_window2->AddActor(GetLineActor());
        window_id = gui.AddWindow(vtk_window2);
    }

    std::thread gui_thread{viz3d::GUI::LaunchMainLoop, "GUI"};
    gui_thread.join();
    gui.RemoveWindow(window_id);
    gui.ClearWindows();

    return 0;
}

ext: cxx


text:
//////////////////////////////////////////////////////////////////
// example93.cpp
//
// Copyright (c) 2015 Robert Ramey
//
// Distributed under the Boost Software License, Version 1.0. (See
// accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)

#include <iostream>

// include headers to support safe integers
#include <boost/safe_numerics/cpp.hpp>
#include <boost/safe_numerics/exception.hpp>
#include <boost/safe_numerics/safe_integer.hpp>
#include <boost/safe_numerics/safe_integer_range.hpp>
#include <boost/safe_numerics/safe_integer_literal.hpp>

// use same type promotion as used by the pic compiler
// target compiler XC8 supports:
using pic16_promotion = boost::safe_numerics::cpp<
    8,  // char      8 bits
    16, // short     16 bits
    16, // int       16 bits
    16, // long      16 bits
    32  // long long 32 bits
>;

// ***************************
// 1. Specify exception policies so we will generate a
// compile time error whenever an operation MIGHT fail.

// ***************************
// generate runtime errors if operation could fail
using exception_policy = boost::safe_numerics::default_exception_policy;

// generate compile time errors if operation could fail
using trap_policy = boost::safe_numerics::loose_trap_policy;

// ***************************
// 2. Create a macro named literal an integral value
// that can be evaluated at compile time.
#define literal(n) make_safe_literal(n, pic16_promotion, void)

// For min speed of 2 mm / sec (24.8 format)
// sec / step = sec / 2 mm * 2 mm / rotation * rotation / 200 steps
#define C0      literal(5000 << 8)

// For max speed of 400 mm / sec
// sec / step = sec / 400 mm * 2 mm / rotation * rotation / 200 steps
#define C_MIN   literal(25 << 8)

static_assert(
    C0 < make_safe_literal(0xffffff, pic16_promotion,trap_policy),
    "Largest step too long"
);
static_assert(
    C_MIN > make_safe_literal(0, pic16_promotion,trap_policy),
    "Smallest step must be greater than zero"
);

// ***************************
// 3. Create special ranged types for the motor program
// These wiil guarantee that values are in the expected
// ranges and permit compile time determination of when
// exceptional conditions might occur.

using pic_register_t = boost::safe_numerics::safe<
    uint8_t,
    pic16_promotion,
    trap_policy // use for compiling and running tests
>;

// note: the maximum value of step_t would be:
// 50000 = 500 mm / 2 mm/rotation * 200 steps/rotation.
// But in one expression the value of number of steps * 4 is
// used.  To prevent introduction of error, permit this
// type to hold the larger value.
using step_t = boost::safe_numerics::safe_unsigned_range<
    0,
    200000,
    pic16_promotion,
    exception_policy
>;

// position
using position_t = boost::safe_numerics::safe_unsigned_range<
    0,
    50000, // 500 mm / 2 mm/rotation * 200 steps/rotation
    pic16_promotion,
    exception_policy
>;

// next end of step timer value in format 24.8
// where the .8 is the number of bits in the fractional part.
using ccpr_t = boost::safe_numerics::safe<
    uint32_t,
    pic16_promotion,
    exception_policy
>;

// pulse length in format 24.8
// note: this value is constrainted to be a positive value. But
// we still need to make it a signed type. We get an arithmetic
// error when moving to a negative step number.
using c_t = boost::safe_numerics::safe_unsigned_range<
    C_MIN,
    C0,
    pic16_promotion,
    exception_policy
>;

// 32 bit unsigned integer used for temporary purposes
using temp_t = boost::safe_numerics::safe_unsigned_range<
    0, 0xffffffff,
    pic16_promotion,
    exception_policy
>;

// index into phase table
// note: The legal values are 0-3.  So why must this be a signed
// type?  Turns out that expressions like phase_ix + d
// will convert both operands to unsigned.  This in turn will
// create an exception.  So leave it signed even though the
// value is greater than zero.
using phase_ix_t = boost::safe_numerics::safe_signed_range<
    0,
    3,
    pic16_promotion,
    trap_policy
>;

// settings for control value output
using phase_t = boost::safe_numerics::safe<
    uint16_t,
    pic16_promotion,
    trap_policy
>;

// direction of rotation
using direction_t = boost::safe_numerics::safe_signed_range<
    -1,
    +1,
    pic16_promotion,
    trap_policy
>;

// some number of microseconds
using microseconds = boost::safe_numerics::safe<
    uint32_t,
    pic16_promotion,
    trap_policy
>;

// ***************************
// emulate PIC features on the desktop

// filter out special keyword used only by XC8 compiler
#define __interrupt
// filter out XC8 enable/disable global interrupts
#define ei()
#define di()

// emulate PIC special registers
pic_register_t RCON;
pic_register_t INTCON;
pic_register_t CCP1IE;
pic_register_t CCP2IE;
pic_register_t PORTC;
pic_register_t TRISC;
pic_register_t T3CON;
pic_register_t T1CON;

pic_register_t CCPR2H;
pic_register_t CCPR2L;
pic_register_t CCPR1H;
pic_register_t CCPR1L;
pic_register_t CCP1CON;
pic_register_t CCP2CON;
pic_register_t TMR1H;
pic_register_t TMR1L;

// ***************************
// special checked type for bits - values restricted to 0 or 1
using safe_bit_t = boost::safe_numerics::safe_unsigned_range<
    0,
    1,
    pic16_promotion,
    trap_policy
>;

// create type used to map PIC bit names to
// correct bit in PIC register
template<typename T, std::int8_t N>
struct bit {
    T & m_word;
    constexpr explicit bit(T & rhs) :
        m_word(rhs)
    {}
    // special functions for assignment of literal
    constexpr bit & operator=(decltype(literal(1))){
        m_word |= literal(1 << N);
        return *this;
    }
    constexpr bit & operator=(decltype(literal(0))){
        m_word &= ~literal(1 << N);
        return *this;
    }
    // operator to convert to 0 or 1
    constexpr operator safe_bit_t () const {
        return m_word >> literal(N) & literal(1);
    }
};

// define bits for T1CON register
struct  {
    bit<pic_register_t, 7> RD16{T1CON};
    bit<pic_register_t, 5> T1CKPS1{T1CON};
    bit<pic_register_t, 4> T1CKPS0{T1CON};
    bit<pic_register_t, 3> T1OSCEN{T1CON};
    bit<pic_register_t, 2> T1SYNC{T1CON};
    bit<pic_register_t, 1> TMR1CS{T1CON};
    bit<pic_register_t, 0> TMR1ON{T1CON};
} T1CONbits;

// define bits for T1CON register
struct  {
    bit<pic_register_t, 7> GEI{INTCON};
    bit<pic_register_t, 5> PEIE{INTCON};
    bit<pic_register_t, 4> TMR0IE{INTCON};
    bit<pic_register_t, 3> RBIE{INTCON};
    bit<pic_register_t, 2> TMR0IF{INTCON};
    bit<pic_register_t, 1> INT0IF{INTCON};
    bit<pic_register_t, 0> RBIF{INTCON};
} INTCONbits;

#include "motor3.c"

#include <chrono>
#include <thread>

// round 24.8 format to microseconds
microseconds to_microseconds(ccpr_t t){
    return (t + literal(128)) / literal(256);
}

using result_t = uint8_t;
const result_t success = 1;
const result_t fail = 0;

// move motor to the indicated target position in steps
result_t test(position_t new_position){
    try {
        std::cout << "move motor to " << new_position << '\n';
        motor_run(new_position);
        std::cout
        << "step #" << ' '
        << "delay(us)(24.8)" << ' '
        << "delay(us)" << ' '
        << "CCPR" << ' '
        << "motor position" << '\n';
        while(busy()){
            std::this_thread::sleep_for(std::chrono::microseconds(to_microseconds(c)));
            c_t last_c = c;
            ccpr_t last_ccpr = ccpr;
            isr_motor_step();
            std::cout << i << ' '
            << last_c << ' '
            << to_microseconds(last_c) << ' '
            << std::hex << last_ccpr << std::dec << ' '
            << motor_position << '\n';
        };
    }
    catch(const std::exception & e){
        std::cout << e.what() << '\n';
        return fail;
    }
    return success;
}

int main(){
    std::cout << "start test\n";
    result_t result = success;
    try {
        initialize();
        // move motor to position 1000
        result &= test(literal(9000));
        // move to the left before zero position
        // fails to compile !
        // result &= ! test(-10);
        // move motor to position 200
        result &= test(literal(200));
        // move motor to position 200 again! Should result in no movement.
        result &= test(literal(200));
        // move motor to position 50000.
        result &= test(literal(50000));
        // move motor back to position 0.
        result &= test(literal(0));
    }
    catch(...){
        std::cout << "test interrupted\n";
        return EXIT_FAILURE;
    }
    std::cout << "end test\n";
    return result == success ? EXIT_SUCCESS : EXIT_FAILURE;
}

ext: cpp


text:
#include "liver/macrocell_tree.hpp"
#include "utility/options.hpp"
#include <boost/filesystem.hpp>
#include <boost/program_options.hpp>

namespace po = boost::program_options;
using namespace jhmi;

int main(int argc, char* argv[]) {
  GOOGLE_PROTOBUF_VERIFY_VERSION;

  try {
    auto opts = options<treefile_option>{};
    if (!opts.parse(argc, argv))
      return 1;
    auto tree = macrocell_tree{load_tree, opts.treefile().string()};
    tree.validate();

    google::protobuf::ShutdownProtobufLibrary();
  }
  catch (std::exception const& e) {
    fmt::print("Failed with exception: {}\n", e.what());
  }
  return 0;
}


text:
/**
 *	amqp11.hpp:
 * 				amqp11 is a small and simple AMQP client library for C++11
 *
 */
#pragma once

#define AMQPPORT 5672
#define AMQPHOST "localhost"
#define AMQPVHOST "/"
#define AMQPLOGIN "guest"
#define AMQPPSWD  "guest"

#define AMQPDEBUG ":5673"

#define AMQP_AUTODELETE		1
#define AMQP_DURABLE		2
#define AMQP_PASSIVE		4
#define AMQP_MANDATORY		8
#define AMQP_IMMIDIATE		16
#define AMQP_IFUNUSED		32
#define AMQP_EXCLUSIVE		64
#define AMQP_NOWAIT			128
#define AMQP_NOACK			256
#define AMQP_NOLOCAL		512
#define AMQP_MULTIPLE		1024

#define HEADER_FOOTER_SIZE 8 //  7 bytes up front, then payload, then 1 byte footer
#define FRAME_MAX 131072    // max lenght (size) of frame

#define RAND_STR_LENGTH 8

#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <strings.h>

#include <unistd.h>
#include <stdint.h>

#include <amqp.h>
#include <amqp_tcp_socket.h>
#include <amqp_framing.h>

#include <sstream>
#include <vector>
#include <map>
#include <memory>
#include <functional>
#include <algorithm>
#include <boost/shared_ptr.hpp>
#include <boost/lexical_cast.hpp>

#include <iostream>

class AMQPQueue;

enum class AMQPEventType {
	AMQP_MESSAGE, AMQP_SIGUSR, AMQP_CANCEL, AMQP_CLOSE_CHANNEL
};

class AMQPException {
	std::string message;
	int code;
public:
	AMQPException(std::string message);
	AMQPException(amqp_rpc_reply_t * res);

	std::string getMessage();
	uint16_t getReplyCode();
};

class AMQPMessage {
	char * data;
	uint32_t len;
	std::string exchange;
	std::string routing_key;
	uint32_t delivery_tag;
	int message_count;
	std::string consumer_tag;
	AMQPQueue * queue;
	std::map<std::string, std::string> headers;

public:
	AMQPMessage(AMQPQueue * queue);
	~AMQPMessage();

	void setMessage(const char * data, uint32_t length);
	std::string getMessage(uint32_t * length);

	void addHeader(std::string name, amqp_bytes_t * value);
	void addHeader(std::string name, uint64_t * value);
	void addHeader(std::string name, uint8_t * value);
	void addHeader(amqp_bytes_t * name, amqp_bytes_t * value);
	std::string getHeader(std::string name);

	void setConsumerTag(amqp_bytes_t consumer_tag);
	void setConsumerTag(std::string consumer_tag);
	std::string getConsumerTag();

	void setMessageCount(int count);
	int getMessageCount();

	void setExchange(amqp_bytes_t exchange);
	void setExchange(std::string exchange);
	std::string getExchange();

	void setRoutingKey(amqp_bytes_t routing_key);
	void setRoutingKey(std::string routing_key);
	std::string getRoutingKey();

	uint32_t getDeliveryTag();
	void setDeliveryTag(uint32_t delivery_tag);

	AMQPQueue * getQueue();
};

class AMQPBase
{
protected:
	std::string name;
	short params;
	amqp_connection_state_t * cnn;
	int channelNum;
	AMQPMessage * pmessage;

	short opened;

	void checkReply(amqp_rpc_reply_t * res);
	void checkClosed(amqp_rpc_reply_t * res);
	void openChannel();

	std::string randomStr(size_t length);

public:
	virtual ~AMQPBase();
	int getChannelNum();
	void setParam(short param);
	std::string getName();
	void closeChannel();
	void reopen();
	void setName(const char * name);
	void setName(std::string name);
};

class AMQPQueue: public AMQPBase
{
protected:
	std::map<AMQPEventType, std::function<int(AMQPMessage*)>> events;
	amqp_bytes_t consumer_tag;
	uint32_t delivery_tag;
	uint32_t count;

public:
	AMQPQueue(amqp_connection_state_t * cnn, int channelNum);

	void Declare();
	void Declare(std::string name);
	void Declare(std::string name, short params);
	void Declare(short params);

	void Delete();
	void Delete(std::string name);

	void Purge();
	void Purge(std::string name);

	void Bind(std::string exchangeName, std::string key);

	void unBind(std::string exchangeName, std::string key);

	void Get();
	void Get(short param);

	void Consume();
	void Consume(short param);

	void Cancel(amqp_bytes_t consumer_tag);
	void Cancel(std::string consumer_tag);

	void Ack();
	void Ack(uint32_t delivery_tag);

	AMQPMessage * getMessage()
	{
		return pmessage;
	}

	uint32_t getCount()
	{
		return count;
	}

	void setConsumerTag(std::string consumer_tag);
	amqp_bytes_t getConsumerTag();

	void addEvent(AMQPEventType eventType, std::function<int(AMQPMessage*)> callable);

	virtual ~AMQPQueue();

	void Qos(uint32_t prefetch_size, uint16_t prefetch_count,
			amqp_boolean_t global);

private:
	void sendDeclareCommand();
	void sendDeleteCommand();
	void sendPurgeCommand();
	void sendBindCommand(const char * exchange, const char * key);
	void sendUnBindCommand(const char * exchange, const char * key);
	void sendGetCommand();
	void sendConsumeCommand();
	void sendCancelCommand();
	void sendAckCommand();
	void setHeaders(amqp_basic_properties_t * p);
};

enum class ExchangeType
{
	DIRECT, FANOUT, TOPIC
};

class AMQPExchange: public AMQPBase
{
	ExchangeType type;
	std::map<std::string, std::string> sHeaders;
	std::map<std::string, std::string> sHeadersSpecial;
	std::map<std::string, int> iHeaders;

public:
	AMQPExchange(amqp_connection_state_t * cnn, int channelNum);
	virtual ~AMQPExchange();

	void Declare(std::string name);
	void Declare(std::string name, ExchangeType type);
	void Declare(std::string name, ExchangeType type, short params);

	void Delete();
	void Delete(std::string name);

	void Bind(std::string queueName);
	void Bind(std::string queueName, std::string key);

	void Publish(std::string message, std::string key);
	void Publish(const char * data, uint32_t length, std::string key);

	void setHeader(std::string name, int value);
	void setHeader(std::string name, std::string value);
	void setHeader(std::string name, std::string value, bool special);

private:
	AMQPExchange();
	void checkType();
	const char * exchangetype_ctr(ExchangeType type);

	void sendDeclareCommand();
	void sendDeleteCommand();
	void sendPublishCommand();

	void sendBindCommand(const char * queueName, const char * key);
	void sendPublishCommand(amqp_bytes_t messageByte, const char * key);
	void sendCommand();
	void checkReply(amqp_rpc_reply_t * res);
	void checkClosed(amqp_rpc_reply_t * res);
};

class AMQP
{
	int port;
	std::string host;
	std::string vhost;
	std::string user;
	std::string password;

	int channelNumber;

	boost::shared_ptr<AMQPExchange> exchange;
	std::vector<boost::shared_ptr<AMQPBase>> channels;

	amqp_socket_t * socket;
	amqp_connection_state_t conn;

	struct timeval * tv;

public:
	AMQP();
	AMQP(std::string connStr);
	~AMQP();

	boost::shared_ptr<AMQPExchange>	createExchange();
	boost::shared_ptr<AMQPQueue>		createQueue();

	void printConnect();

	void closeChannel();

private:
	AMQP(AMQP &obj);
	void init();
	void initDefault();
	void connect();
	void parseCnnString(std::string cnnString);
	void parseHostPort(std::string hostPortString);
	void parseUserStr(std::string userString);
	void sockConnect();
	void login();
};

// utility functions
class fn {
	static inline std::string & ltrim(std::string & s) {
		s.erase(
			s.begin(),
			std::find_if(s.begin(), s.end(),
									std::not1(std::ptr_fun<int,int>(std::isspace))));
		return s;
	}
	static inline std::string & rtrim(std::string & s) {
		s.erase(
			std::find_if(s.rbegin(), s.rend(),
							std::not1(std::ptr_fun<int,int>(std::isspace))).base(),
			s.end()
		);
		return s;
	}
public:
	static inline std::string & trim(std::string & s) {
		return ltrim(rtrim(s));
	}
};


text: #include <boost/geometry/strategies/geographic/azimuth.hpp>

max_stars_repo_name: miathedev/BoostForArduino

max_issues_repo_name: miathedev/BoostForArduino

max_forks_repo_name: miathedev/BoostForArduino


text:
/*
 * Copyright 2010 Vicente J. Botet Escriba
 * Copyright 2015 Andrey Semashev
 *
 * Distributed under the Boost Software License, Version 1.0.
 * See http://www.boost.org/LICENSE_1_0.txt
 */

#ifndef BOOST_WINAPI_HANDLES_HPP_INCLUDED_
#define BOOST_WINAPI_HANDLES_HPP_INCLUDED_

#include <boost/winapi/basic_types.hpp>
#include <boost/winapi/detail/header.hpp>

#ifdef BOOST_HAS_PRAGMA_ONCE
#pragma once
#endif

#if !defined( BOOST_USE_WINDOWS_H )
extern "C" {
BOOST_WINAPI_IMPORT_EXCEPT_WM boost::winapi::BOOL_ BOOST_WINAPI_WINAPI_CC
CloseHandle(boost::winapi::HANDLE_ handle);

BOOST_WINAPI_IMPORT_EXCEPT_WM boost::winapi::BOOL_ BOOST_WINAPI_WINAPI_CC
DuplicateHandle(
    boost::winapi::HANDLE_ hSourceProcessHandle,
    boost::winapi::HANDLE_ hSourceHandle,
    boost::winapi::HANDLE_ hTargetProcessHandle,
    boost::winapi::HANDLE_* lpTargetHandle,
    boost::winapi::DWORD_ dwDesiredAccess,
    boost::winapi::BOOL_ bInheritHandle,
    boost::winapi::DWORD_ dwOptions);

#if BOOST_USE_WINAPI_VERSION >= BOOST_WINAPI_VERSION_WIN10
BOOST_WINAPI_IMPORT boost::winapi::BOOL_ BOOST_WINAPI_WINAPI_CC
CompareObjectHandles(
    boost::winapi::HANDLE_ hFirstObjectHandle,
    boost::winapi::HANDLE_ hSecondObjectHandle);
#endif
} // extern "C"
#endif

namespace boost {
namespace winapi {

using ::CloseHandle;
using ::DuplicateHandle;

#if BOOST_USE_WINAPI_VERSION >= BOOST_WINAPI_VERSION_WIN10
using ::CompareObjectHandles;
#endif

// Note: MSVC-14.1 does not interpret INVALID_HANDLE_VALUE_ initializer as a constant expression
#if defined( BOOST_USE_WINDOWS_H )
BOOST_CONSTEXPR_OR_CONST DWORD_ DUPLICATE_CLOSE_SOURCE_ = DUPLICATE_CLOSE_SOURCE;
BOOST_CONSTEXPR_OR_CONST DWORD_ DUPLICATE_SAME_ACCESS_ = DUPLICATE_SAME_ACCESS;
const HANDLE_ INVALID_HANDLE_VALUE_ = INVALID_HANDLE_VALUE;
#else
BOOST_CONSTEXPR_OR_CONST DWORD_ DUPLICATE_CLOSE_SOURCE_ = 1;
BOOST_CONSTEXPR_OR_CONST DWORD_ DUPLICATE_SAME_ACCESS_ = 2;
const HANDLE_ INVALID_HANDLE_VALUE_ = (HANDLE_)(-1);
#endif

BOOST_CONSTEXPR_OR_CONST DWORD_ duplicate_close_source = DUPLICATE_CLOSE_SOURCE_;
BOOST_CONSTEXPR_OR_CONST DWORD_ duplicate_same_access = DUPLICATE_SAME_ACCESS_;
// Note: The "unused" attribute here should not be necessary because the variable is a constant.
//       However, MinGW gcc 5.3 spams warnings about this particular constant.
const HANDLE_ invalid_handle_value BOOST_ATTRIBUTE_UNUSED = INVALID_HANDLE_VALUE_;

}
}

#include <boost/winapi/detail/footer.hpp>

#endif // BOOST_WINAPI_HANDLES_HPP_INCLUDED_

max_stars_repo_name: kindlychung/mediasoup-sfu-cpp

max_issues_repo_name: kindlychung/mediasoup-sfu-cpp

max_forks_repo_name: kindlychung/mediasoup-sfu-cpp