neurosym_conv.h

Go to the documentation of this file.

#ifndef _ESBMC_SOLVERS_NEUROSYM_NEUROSYM_CONV_H
#define _ESBMC_SOLVERS_NEUROSYM_NEUROSYM_CONV_H
 
#include <solvers/smtlib/smtlib_conv.h>
 
#include <map>
#include <optional>

class neurosym_convt : public smtlib_convt
{
public:
  neurosym_convt(const namespacet &ns, const optionst &options);
  ~neurosym_convt() override;
 
  smt_resultt dec_solve() override;
  const std::string solver_text() override;
  std::string dump_smt() override;
 
  bool has_model() const override
  {
    return !local_model.empty() || smtlib_convt::has_model();
  }
 
  tvt get_bool(smt_astt a) override;
  tvt l_get(smt_astt a) override;
  BigInt get_bv(smt_astt a, bool is_signed) override;
 
private:
  neurosym_convt(
    const namespacet &ns,
    const optionst &options,
    const std::string &formula_path);

  void parse_model_block(const std::string &output);

  std::map<std::string, std::string> local_model;

  std::optional<BigInt> local_lookup(const std::string &symname) const;

  std::optional<BigInt> local_eval_bv(smt_astt a) const;

  std::optional<bool> local_eval_bool(smt_astt a) const;

  std::optional<bool> local_lookup_bool(const std::string &symname) const;
  std::optional<bool>
  eval_bool_fold(smt_func_kind kind, const smtlib_smt_ast *ast) const;
  std::optional<bool> eval_bool_eq(const smtlib_smt_ast *ast) const;

  std::optional<BigInt>
  local_eval_array_at(smt_astt array_term, const BigInt &index) const;

  bool ensure_model_prog_ready();
  bool model_prog_response_read = false;
 
  std::string formula_path;
  bool solved = false;
};
 
#endif /* _ESBMC_SOLVERS_NEUROSYM_NEUROSYM_CONV_H */