text: #ifndef SMTSAMPLER_H_
  #define SMTSAMPLER_H_
  
  #include <unordered_map>
  
  #include "sampler.h"
  #include "sampler_config.h"
  
  class SMTSampler : public Sampler {
    std::vector<z3::func_decl> ind;
    int all_ind_count = 0;
    std::vector<std::pair<int, int>> cons_to_ind;
    std::vector<z3::expr> constraints;
    std::vector<std::vector<z3::expr>> soft_constraints;
    int strategy;
    int flips = 0;
    std::unordered_map<int, std::unordered_set<int>> unsat_ind;
    int unsat_ind_count = 0;
  
    //  std::unordered_set<Z3_ast> sub;
  
   public:
    SMTSampler(z3::context *_c, const std::string &input,
               const std::string &output_dir, const MeGA::SamplerConfig& config);
    /*
     * Finds additional valid models (samples) of the formula
     * (based on the given model, which is assumed valid).
     * Adds all valid samples to the samples set.
     * Returns the number of new samples found.
     */
    int sample(const z3::model &model);
    /*
     * Saves to the given file a list of all samples found during calls to sample.
     * File should already exist upon calling the function.
     */
    void save_valid_samples(std::string file);
    /*
     * Prints (to stdout) a list of all samples found during calls to sample.
     */
    void print_valid_samples();
  
    void do_epoch(const z3::model &model);
    void finish();
  
   protected:
    struct Triple {
      std::string a[3] = {"", "", ""};
    };
  
    std::string model_string(z3::model m, std::vector<z3::func_decl> ind);
    z3::expr value(char const *n, z3::sort s);
    z3::expr value(char const *n);
    long long ll_value(char const *n);
    bool b_value(char const *n);
    void add_constraints(z3::expr exp, z3::expr val, int count);
    void calculate_constraints(const std::string &m_string);
    void find_neighboring_solutions(std::unordered_set<std::string> &mutations);
    void find_combined_solutions(std::unordered_set<std::string> &mutations,
                                 const std::string &a_string);
    int combine_mutations(long long val_orig, long long val_b, long long val_c);
    bool combine_bool_mutations(bool val_orig, bool val_b, bool val_c);
    z3::model gen_model(const std::string &candidate,
                        std::vector<z3::func_decl> &ind);
    void assert_is_int_var(const z3::func_decl &v);
    
    std::string parse_function(std::string const &m_string, size_t &pos,
                               int arity,
                               std::unordered_map<std::string, Triple> &values,
                               int index);
    std::string combine_function(std::string const &str_a,
                                 std::string const &str_b,
                                 std::string const &str_c, size_t &pos_a,
                                 size_t &pos_b, size_t &pos_c, int arity,
                                 z3::sort s);
  };
  
  #endif /* SMTSAMPLER_H_ */
  