grain_inv_parse.h

// Hongce Zhang

/* Example :
(declare-fun S_m1.id_ex_reg_wen () (_ BitVec 1))
(declare-fun S_m1.id_ex_op () (_ BitVec 2))

(assert (=> (= S_m1.id_ex_op #b00) (= S_m1.id_ex_reg_wen #b0)))
(check-sat)
*/

#ifndef ILANG_VTARGET_OUT_GRAIN_INV_PARSE_H__
#define ILANG_VTARGET_OUT_GRAIN_INV_PARSE_H__

#include <ilang/config.h>
#ifdef INVSYN_INTERFACE

#include <ilang/smt-inout/chc_inv_in.h>

namespace ilang {
namespace smt {

class GrainInvariantParser : public SmtlibInvariantParser {

public:
  // -------------- CONSTRUCTOR ------------------- //
  GrainInvariantParser(YosysSmtParser* yosys_smt_info,
                       const std::string& dut_instance_name,
                       bool discourage_outside_var = true,
                       bool outside_var_to_freevar = true);
  GrainInvariantParser(const GrainInvariantParser&) = delete;
  GrainInvariantParser& operator=(const GrainInvariantParser&) = delete;

  // -------------- DESTRUCTOR ------------------- //
  virtual ~GrainInvariantParser();

protected:
  // -------------- MEMBER ------------------- //
  bool convert_out_var_to_free_var;

public:
  // -------------- INTERFACE ------------------- //
  bool virtual ParseInvResultFromFile(const std::string& fname) override;

  // -------------- CALLBACK FNs ------------------- //

  virtual var_type* make_sort(const std::string& name,
                              const std::vector<int>&) override;
  void declare_function(const std::string& name, var_type* sort) override;

  // virtual void assert_formula(SmtTermInfoVlgPtr result) override; -- use the
  // old one

  // -------------- Below are Disabled!--------------------- //
  virtual SmtTermInfoVlgPtr push_quantifier_scope() override;
  virtual SmtTermInfoVlgPtr pop_quantifier_scope() override;

  virtual void declare_quantified_variable(const std::string& name,
                                           var_type* sort) override;
  virtual SmtTermInfoVlgPtr
  mk_function(const std::string& name, var_type* sort,
              const std::vector<int>& idx,
              const std::vector<SmtTermInfoVlgPtr>& args) override;

  // virtual SmtTermInfoVlgPtr mk_number(const std::string & rep, int width, int
  // base) override;

  virtual SmtTermInfoVlgPtr
  search_quantified_var_stack(const std::string& name) override;

  virtual void define_function(const std::string& func_name,
                               const std::vector<SmtTermInfoVlgPtr>& args,
                               var_type* ret_type,
                               SmtTermInfoVlgPtr func_body) override;

}; // class GrainInvariantParser

}; // namespace smt
}; // namespace ilang

#endif // INVSYN_INTERFACE

#endif // ILANG_VTARGET_OUT_GRAIN_INV_PARSE_H__