<commit_before>#pragma once
#include "../tags/QF_BV.hpp"
#include "../tags/QF_UF.hpp"
#include "../tags/Array.hpp"
#include "../result_wrapper.hpp"
#include "../Features.hpp"

#include <z3++.h>

#include <boost/any.hpp>
#include <boost/mpl/map/map40.hpp>
#include <boost/tuple/tuple.hpp>
#include <boost/tuple/tuple_io.hpp>
#include <boost/fusion/adapted/boost_tuple.hpp>
#include <boost/fusion/adapted/std_pair.hpp>

#include <gmp.h>

namespace metaSMT {

  // forward declare stack api
  struct stack_pop;
  struct stack_push;
  namespace features {
    struct stack_api;
  } // features

  namespace solver {
    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;
    namespace uftags = ::metaSMT::logic::QF_UF::tag;

    namespace detail {
      struct dummy {
        dummy() {}
      }; // dummy

      struct equals : boost::static_visitor<bool> {
        equals() {}

        template < typename T1, typename T2 >
        bool operator() (T1 const &, T2 const &) const {
          return false;
        }

        bool operator() (dummy const &, dummy const &) const {
          return true;
        }

        bool operator() (z3::func_decl const &lhs, z3::func_decl const &rhs) const {
          return eq(lhs, rhs);
        }

        bool operator() (z3::expr const &lhs, z3::expr const &rhs) const {
          return eq(lhs, rhs);
        }
      }; // equals

      struct domain_sort_visitor : boost::static_visitor<Z3_sort> {
        domain_sort_visitor(Z3_context &ctx)
          : ctx(ctx)
        {}

        Z3_sort operator() (type::Boolean const & ) const {
          return Z3_mk_bool_sort(ctx);
        }

        Z3_sort operator() (type::BitVector const &arg) const {
          return Z3_mk_bv_sort(ctx, arg.width);
        }

        Z3_sort operator() (type::Array const &arg) const {
          Z3_sort index_type = Z3_mk_bv_sort(ctx, arg.index_width);
          Z3_sort elem_type = Z3_mk_bv_sort(ctx, arg.elem_width);
          return Z3_mk_array_sort(ctx, index_type, elem_type);
        }

        Z3_context &ctx;
      }; // domain_sort_visitor
    } // detail

    class Z3_Backend {
    public:
      struct result_type {
        // first type in variant has to be default constructable
        boost::variant<
          detail::dummy
        , z3::func_decl
        , z3::expr
        > internal;

        result_type() {}

        result_type(z3::expr a)
          : internal(a)
        {}

        result_type(z3::func_decl a)
          : internal(a)
        {}

        inline operator z3::expr() const {
          return boost::get<z3::expr>(internal);
        }

        inline operator z3::func_decl() const {
          return boost::get<z3::func_decl>(internal);
        }

        inline bool operator ==(result_type const &r) const {
          return boost::apply_visitor(detail::equals(), internal, r.internal);
        }

        inline bool operator !=(result_type const &r) const {
          return !operator ==(r);
        }
#if 0
        inline bool operator <(result_type const &r) const {
          assert( false && "Yet not implemented" );
          return false;
        }
#endif
      }; // result_type

      // typedef z3::ast result_type;

      Z3_Backend()
        : solver_(ctx_)
        , assumption_( (*this)(predtags::true_tag(), boost::any()) )
      {}

      ~Z3_Backend()
      {}

      result_wrapper read_value(result_type const &var) {
        z3::model model = solver_.get_model();
        z3::expr r = model.eval(z3::expr(var), /* completion = */true);

        // predicate
        if (r.is_bool()) {
            auto b = Z3_get_bool_value(ctx_, r);
            if (b == Z3_L_FALSE) return result_wrapper(false);
            if (b == Z3_L_TRUE) return result_wrapper(true);
            return result_wrapper();
        }

        assert(r.is_bv());
        unsigned long long val = 0;
        if (Z3_get_numeral_uint64(ctx_, r, &val)) return result_wrapper(val, r.get_sort().bv_size());

        std::string str = Z3_ast_to_string(ctx_, r);
        assert(str.find("#b") == 0);
        return result_wrapper(str.substr(2));
      }

      void assertion( result_type const &e ) {
        solver_.add( static_cast<z3::expr const &>(e) );
      }

      void assumption( result_type const &e ) {<commit_msg>enable compilation of Z3_Backend with C++03<commit_after>#pragma once
#include "../tags/QF_BV.hpp"
#include "../tags/QF_UF.hpp"
#include "../tags/Array.hpp"
#include "../result_wrapper.hpp"
#include "../Features.hpp"

#include <z3++.h>

#include <boost/any.hpp>
#include <boost/mpl/map/map40.hpp>
#include <boost/tuple/tuple.hpp>
#include <boost/tuple/tuple_io.hpp>
#include <boost/fusion/adapted/boost_tuple.hpp>
#include <boost/fusion/adapted/std_pair.hpp>

#include <gmp.h>

namespace metaSMT {

  // forward declare stack api
  struct stack_pop;
  struct stack_push;
  namespace features {
    struct stack_api;
  } // features

  namespace solver {
    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;
    namespace uftags = ::metaSMT::logic::QF_UF::tag;

    namespace detail {
      struct dummy {
        dummy() {}
      }; // dummy

      struct equals : boost::static_visitor<bool> {
        equals() {}

        template < typename T1, typename T2 >
        bool operator() (T1 const &, T2 const &) const {
          return false;
        }

        bool operator() (dummy const &, dummy const &) const {
          return true;
        }

        bool operator() (z3::func_decl const &lhs, z3::func_decl const &rhs) const {
          return eq(lhs, rhs);
        }

        bool operator() (z3::expr const &lhs, z3::expr const &rhs) const {
          return eq(lhs, rhs);
        }
      }; // equals

      struct domain_sort_visitor : boost::static_visitor<Z3_sort> {
        domain_sort_visitor(Z3_context &ctx)
          : ctx(ctx)
        {}

        Z3_sort operator() (type::Boolean const & ) const {
          return Z3_mk_bool_sort(ctx);
        }

        Z3_sort operator() (type::BitVector const &arg) const {
          return Z3_mk_bv_sort(ctx, arg.width);
        }

        Z3_sort operator() (type::Array const &arg) const {
          Z3_sort index_type = Z3_mk_bv_sort(ctx, arg.index_width);
          Z3_sort elem_type = Z3_mk_bv_sort(ctx, arg.elem_width);
          return Z3_mk_array_sort(ctx, index_type, elem_type);
        }

        Z3_context &ctx;
      }; // domain_sort_visitor
    } // detail

    class Z3_Backend {
    public:
      struct result_type {
        // first type in variant has to be default constructable
        boost::variant<
          detail::dummy
        , z3::func_decl
        , z3::expr
        > internal;

        result_type() {}

        result_type(z3::expr a)
          : internal(a)
        {}

        result_type(z3::func_decl a)
          : internal(a)
        {}

        inline operator z3::expr() const {
          return boost::get<z3::expr>(internal);
        }

        inline operator z3::func_decl() const {
          return boost::get<z3::func_decl>(internal);
        }

        inline bool operator ==(result_type const &r) const {
          return boost::apply_visitor(detail::equals(), internal, r.internal);
        }

        inline bool operator !=(result_type const &r) const {
          return !operator ==(r);
        }
#if 0
        inline bool operator <(result_type const &r) const {
          assert( false && "Yet not implemented" );
          return false;
        }
#endif
      }; // result_type

      // typedef z3::ast result_type;

      Z3_Backend()
        : solver_(ctx_)
        , assumption_( (*this)(predtags::true_tag(), boost::any()) )
      {}

      ~Z3_Backend()
      {}

      result_wrapper read_value(result_type const &var) {
        z3::model model = solver_.get_model();
        z3::expr r = model.eval(z3::expr(var), /* completion = */true);

        // predicate
        if (r.is_bool()) {
            Z3_lbool b = Z3_get_bool_value(ctx_, r);
            if (b == Z3_L_FALSE) return result_wrapper(false);
            if (b == Z3_L_TRUE) return result_wrapper(true);
            return result_wrapper();
        }

        assert(r.is_bv());
        unsigned long long val = 0;
        if (Z3_get_numeral_uint64(ctx_, r, &val)) return result_wrapper(val, r.get_sort().bv_size());

        std::string str = Z3_ast_to_string(ctx_, r);
        assert(str.find("#b") == 0);
        return result_wrapper(str.substr(2));
      }

      void assertion( result_type const &e ) {
        solver_.add( static_cast<z3::expr const &>(e) );
      }

      void assumption( result_type const &e ) {
{'fraction_non_alphanumeric': 0.13204545454545455, 'fraction_numerical': 0.012045454545454545, 'mean_word_length': 2.2428150331613854, 'pattern_counts': {'":': 0, '<': 35, '<?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': '2957865', 'n_tokens_mistral': 2894, 'n_tokens_neox': 2783, 'n_words': 627}