<commit_before>#pragma once

#include "../tags/QF_BV.hpp"
#include "../tags/Array.hpp"
#include "../result_wrapper.hpp"

extern "C" {
#include <boolector.h>
}

#include <iostream>
#include <boost/mpl/map/map40.hpp>
#include <boost/any.hpp>
#include <boost/tuple/tuple.hpp>
#include <list>

namespace metaSMT {
  namespace solver {

    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;


    /**
     * @ingroup Backend
     * @class Boolector Boolector.hpp metaSMT/backend/Boolector.hpp
     * @brief The Boolector backend 
     */
    class Boolector {

      struct BoolectorAssertion : public std::runtime_error {
        BoolectorAssertion(const char* what)
          : std::runtime_error(what) {}
      };

      static void _boolector_error(int ec) {
        throw BoolectorAssertion("internal error in boolector");
      }

      public:
        typedef BtorExp* result_type;

        result_type ptr(BtorExp* expr) {
          _exprs.push_back(expr);
          return expr;
        }
      
        Boolector ()
        {
          _btor = boolector_new();
          boolector_enable_model_gen(_btor);
          boolector_enable_inc_usage(_btor);
          boolector_abort_function(&Boolector::_boolector_error);
        }

        ~Boolector() {
          for( std::list<BtorExp*>::iterator ite = _exprs.begin(); ite!=_exprs.end(); ++ite)
          {
            boolector_release(_btor, *ite);
          }
          boolector_delete(_btor);
        }

        void assertion( result_type e ) {
          boolector_assert(_btor, e);
        }

        void assumption( result_type e ) {
          boolector_assume(_btor, e);
        }

        bool solve() {
          return boolector_sat(_btor) == BOOLECTOR_SAT;
        }

        result_wrapper read_value(result_type var)
        {
          char* value = boolector_bv_assignment(_btor, var);
          std::string s(value);
          boolector_free_bv_assignment(_btor, value);
          return result_wrapper(s);
        }

        result_type operator() (predtags::var_tag const & var, boost::any args )
        {
          return ptr(boolector_var(_btor, 1, NULL));
        }

        result_type operator() (predtags::false_tag , boost::any arg ) {
          return ptr(boolector_false(_btor));
        }

        result_type operator() (predtags::true_tag , boost::any arg ) {
          return ptr(boolector_true(_btor));
        }

        result_type operator() (predtags::not_tag , result_type a) {
          return ptr(boolector_not(_btor, a) );
        }


        result_type operator() (bvtags::var_tag const & var, boost::any args )
        {
          assert ( var.width != 0 );
          return ptr(boolector_var(_btor, var.width, NULL));
        }

        result_type operator() (bvtags::bit0_tag , boost::any arg ) {
          return ptr(boolector_false(_btor));
        }

        result_type operator() (bvtags::bit1_tag , boost::any arg ) {
          return ptr(boolector_true(_btor));
        }

        result_type operator() (bvtags::bvuint_tag , boost::any arg ) {
          typedef boost::tuple<unsigned long, unsigned long> P;
          P p = boost::any_cast<P>(arg);
          //std::cout << "bvuint "<< p << std::endl;
          unsigned long value = boost::get<0>(p);
          unsigned long width = boost::get<1>(p);

          if ( value > std::numeric_limits<unsigned>::max() ) {
            std::string val (width, '0');

            std::string::reverse_iterator sit = val.rbegin();

            for (unsigned long i = 0; i < width; i++, ++sit) {
              *sit = (value & 1ul) ? '1':'0';
              value >>= 1;
            }
            return ptr( boolector_const(_btor, val.c_str()) );
          } else {
            return ptr(boolector_unsigned_int(_btor, value , width ));
          }
        }

        result_type operator() (bvtags::bvsint_tag , boost::any arg ) {
          typedef boost::tuple<long, unsigned long> P;
          P p = boost::any_cast<P>(arg);
          long value = boost::get<0>(p);
          unsigned long width = boost::get<1>(p);

          if (  value > std::numeric_limits<int>::max()
             || value < std::numeric_limits<int>::min()
          ) {
            std::string val (width, '0');

            std::string::reverse_iterator sit = val.rbegin();

            for (unsigned long i = 0; i < width; i++, ++sit) {
              *sit = (value & 1l) ? '1':'0';
              value >>= 1;
            }
            return ptr( boolector_const(_btor, val.c_str()) );
          } else {
            return ptr(boolector_int(_btor, boost::get<0>(p), boost::get<1>(p)));
          }
        }

        result_type operator() (bvtags::bvbin_tag , boost::any arg ) {
          std::string val = boost::any_cast<std::string>(arg);
          return ptr(boolector_const(_btor, val.c_str()));
        }

        result_type operator() (bvtags::bvhex_tag , boost::any arg ) {
          std::string hex = boost::any_cast<std::string>(arg);
          std::string bin (hex.size()*4,'\0');

          for (unsigned i = 0; i < hex.size(); ++i) {
            switch ( tolower(hex[i]) ) {<commit_msg>minor cleanup in backend Boolector bvsint_tag<commit_after>#pragma once

#include "../tags/QF_BV.hpp"
#include "../tags/Array.hpp"
#include "../result_wrapper.hpp"

extern "C" {
#include <boolector.h>
}

#include <iostream>
#include <boost/mpl/map/map40.hpp>
#include <boost/any.hpp>
#include <boost/tuple/tuple.hpp>
#include <list>

namespace metaSMT {
  namespace solver {

    namespace predtags = ::metaSMT::logic::tag;
    namespace bvtags = ::metaSMT::logic::QF_BV::tag;
    namespace arraytags = ::metaSMT::logic::Array::tag;


    /**
     * @ingroup Backend
     * @class Boolector Boolector.hpp metaSMT/backend/Boolector.hpp
     * @brief The Boolector backend 
     */
    class Boolector {

      struct BoolectorAssertion : public std::runtime_error {
        BoolectorAssertion(const char* what)
          : std::runtime_error(what) {}
      };

      static void _boolector_error(int ec) {
        throw BoolectorAssertion("internal error in boolector");
      }

      public:
        typedef BtorExp* result_type;

        result_type ptr(BtorExp* expr) {
          _exprs.push_back(expr);
          return expr;
        }
      
        Boolector ()
        {
          _btor = boolector_new();
          boolector_enable_model_gen(_btor);
          boolector_enable_inc_usage(_btor);
          boolector_abort_function(&Boolector::_boolector_error);
        }

        ~Boolector() {
          for( std::list<BtorExp*>::iterator ite = _exprs.begin(); ite!=_exprs.end(); ++ite)
          {
            boolector_release(_btor, *ite);
          }
          boolector_delete(_btor);
        }

        void assertion( result_type e ) {
          boolector_assert(_btor, e);
        }

        void assumption( result_type e ) {
          boolector_assume(_btor, e);
        }

        bool solve() {
          return boolector_sat(_btor) == BOOLECTOR_SAT;
        }

        result_wrapper read_value(result_type var)
        {
          char* value = boolector_bv_assignment(_btor, var);
          std::string s(value);
          boolector_free_bv_assignment(_btor, value);
          return result_wrapper(s);
        }

        result_type operator() (predtags::var_tag const & var, boost::any args )
        {
          return ptr(boolector_var(_btor, 1, NULL));
        }

        result_type operator() (predtags::false_tag , boost::any arg ) {
          return ptr(boolector_false(_btor));
        }

        result_type operator() (predtags::true_tag , boost::any arg ) {
          return ptr(boolector_true(_btor));
        }

        result_type operator() (predtags::not_tag , result_type a) {
          return ptr(boolector_not(_btor, a) );
        }


        result_type operator() (bvtags::var_tag const & var, boost::any args )
        {
          assert ( var.width != 0 );
          return ptr(boolector_var(_btor, var.width, NULL));
        }

        result_type operator() (bvtags::bit0_tag , boost::any arg ) {
          return ptr(boolector_false(_btor));
        }

        result_type operator() (bvtags::bit1_tag , boost::any arg ) {
          return ptr(boolector_true(_btor));
        }

        result_type operator() (bvtags::bvuint_tag , boost::any arg ) {
          typedef boost::tuple<unsigned long, unsigned long> P;
          P p = boost::any_cast<P>(arg);
          //std::cout << "bvuint "<< p << std::endl;
          unsigned long value = boost::get<0>(p);
          unsigned long width = boost::get<1>(p);

          if ( value > std::numeric_limits<unsigned>::max() ) {
            std::string val (width, '0');

            std::string::reverse_iterator sit = val.rbegin();

            for (unsigned long i = 0; i < width; i++, ++sit) {
              *sit = (value & 1ul) ? '1':'0';
              value >>= 1;
            }
            return ptr( boolector_const(_btor, val.c_str()) );
          } else {
            return ptr(boolector_unsigned_int(_btor, value , width ));
          }
        }

        result_type operator() (bvtags::bvsint_tag , boost::any arg ) {
          typedef boost::tuple<long, unsigned long> P;
          P const p = boost::any_cast<P>(arg);
          long value = boost::get<0>(p);
          unsigned long const width = boost::get<1>(p);

          if (  value > std::numeric_limits<int>::max()
             || value < std::numeric_limits<int>::min()
          ) {
            std::string val (width, '0');

            std::string::reverse_iterator sit = val.rbegin();

            for (unsigned long i = 0; i < width; i++, ++sit) {
              *sit = (value & 1l) ? '1':'0';
              value >>= 1;
            }
            return ptr( boolector_const(_btor, val.c_str()) );
          } else {
            return ptr( boolector_int(_btor, value, width) );
          }
        }

        result_type operator() (bvtags::bvbin_tag , boost::any arg ) {
          std::string val = boost::any_cast<std::string>(arg);
          return ptr(boolector_const(_btor, val.c_str()));
        }

        result_type operator() (bvtags::bvhex_tag , boost::any arg ) {
          std::string hex = boost::any_cast<std::string>(arg);
          std::string bin (hex.size()*4,'\0');

          for (unsigned i = 0; i < hex.size(); ++i) {
            switch ( tolower(hex[i]) ) {
{'fraction_non_alphanumeric': 0.1382005337399924, 'fraction_numerical': 0.004956157072054899, 'mean_word_length': 2.122916666666667, 'pattern_counts': {'":': 0, '<': 65, '<?xml version=': 0, '>': 57, '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': '6324462', 'n_tokens_mistral': 3404, 'n_tokens_neox': 3338, 'n_words': 664}