chc_inv_in.h

// --- Hongce Zhang (hongcez@princeton.edu)

#ifndef CHC_INV_IN_H__
#define CHC_INV_IN_H__

#include <ilang/smt-inout/chc_inv_in_wrapper.h>
#include <ilang/smt-inout/yosys_smt_parser.h>

#include <functional>
#include <map>
#include <string>

extern "C" {
#include "smtparser/smtlib2abstractparser.h"
#include "smtparser/smtlib2abstractparser_private.h"
}

namespace ilang {
namespace smt {
// we will need a pointer to the SmtlibInvariantParser
class SmtlibInvariantParser;

struct smtlib2_abstract_parser_wrapper {
  smtlib2_abstract_parser parser;
  SmtlibInvariantParser* inv_parser;
}; // struct smtlib2_abstract_parser_wrapper

template <class T> struct SmtTermInfo {
  T _translate;
  var_type _type;
  SmtlibInvariantParser* _context;
  // --------------- CONSTRUCTOR -------------- //
  SmtTermInfo() {}
  SmtTermInfo(const T& trans, const var_type& p, SmtlibInvariantParser* c)
      : _translate(trans), _type(p), _context(c) {}
}; // struct SmtContext

typedef SmtTermInfo<std::string> SmtTermInfoVerilog;
typedef SmtTermInfoVerilog* SmtTermInfoVlgPtr;

class SmtlibInvariantParser : public SmtlibInvariantParserBase {
public:
  // -------------- TYPEs ------------------- //
  typedef std::function<std::string(const std::string&)>
      verilog_internal_name_lookup_fn_t;
  typedef std::map<std::string, SmtTermInfoVerilog> term_container_t;
  typedef std::map<std::string, SmtTermInfoVerilog> quantifier_temp_def_t;
  typedef std::vector<quantifier_temp_def_t> quantifier_def_stack_t;
  typedef std::map<std::string, var_type> sort_container_t;
  typedef std::map<std::string, SmtTermInfoVerilog> local_vars_t;
  typedef std::map<std::string, std::string> local_vars_lookup_t;
  typedef std::map<std::string, int> free_vars_t;

public:
  // -------------- CONSTRUCTOR ------------------- //
  SmtlibInvariantParser(YosysSmtParser* yosys_smt_info, bool _flatten_datatype,
                        bool _flatten_hierarchy,
                        const std::set<std::string>& _inv_pred_name,
                        const std::string& dut_instance_name,
                        bool discourageOutOfScopeVariable = true);
  SmtlibInvariantParser(const SmtlibInvariantParser&) = delete;
  SmtlibInvariantParser& operator=(const SmtlibInvariantParser&) = delete;

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

  // -------------- METHODS ------------------- //
  // parse from a file, we will add something there to make
  // if sat --> failed (return false)
  // if unsat --> add the (assert ...)
  bool virtual ParseInvResultFromFile(const std::string& fname) override;
  // parse from a string: assume we have the (assert ...) there
  void virtual ParseSmtResultFromString(const std::string& text) override;
  std::string GetFinalTranslateResult() const override;
  const local_vars_t& GetLocalVarDefs() const;
  const free_vars_t& GetFreeVarDefs() const;

protected:
  // ----------------- MEMBERS ------------------- //
  smtlib2_abstract_parser_wrapper* parser_wrapper;
  // we will allocate on this container
  // there will be pointers going into it
  term_container_t term_container;
  sort_container_t sort_container;
  quantifier_def_stack_t quantifier_def_stack;
  unsigned mask;
  const std::set<std::string> inv_pred_name;
  std::vector<unsigned> quantifier_var_def_idx_stack;
  local_vars_t local_vars;
  local_vars_lookup_t local_vars_lookup;
  free_vars_t free_vars;
  std::string final_translate_result;
  const std::string dut_verilog_instance_name;

  YosysSmtParser* design_smt_info_ptr;
  const bool datatype_flattened;
  const bool hierarchy_flattened;
  const bool no_outside_var_refer;

  bool _bad_state;
  bool bad_state_return(void);

public:
  bool in_bad_state(void) const { return _bad_state; }

public:
  // ----------------- CALLBACK FUNS INTERFACE ------------------- //
  virtual SmtTermInfoVlgPtr push_quantifier_scope();
  virtual SmtTermInfoVlgPtr pop_quantifier_scope();
  virtual void declare_function(const std::string& name, var_type* sort);
  virtual var_type* make_sort(const std::string& name, const std::vector<int>&);
  virtual void declare_quantified_variable(const std::string& name,
                                           var_type* sort);
  virtual SmtTermInfoVlgPtr
  mk_function(const std::string& name, var_type* sort,
              const std::vector<int>& idx,
              const std::vector<SmtTermInfoVlgPtr>& args);
  virtual SmtTermInfoVlgPtr mk_number(const std::string& rep, int width,
                                      int base);
  virtual SmtTermInfoVlgPtr
  search_quantified_var_stack(const std::string& name);
  virtual void assert_formula(SmtTermInfoVlgPtr result);
  virtual void define_function(const std::string& func_name,
                               const std::vector<SmtTermInfoVlgPtr>& args,
                               var_type* ret_type, SmtTermInfoVlgPtr func_body);

#define DECLARE_OPERATOR(name)                                                 \
  SmtTermInfoVlgPtr mk_##name(const std::string& symbol, var_type* sort,       \
                              const std::vector<int>& idx,                     \
                              const std::vector<SmtTermInfoVlgPtr>& args)

  // I hope it will expand lexically
  DECLARE_OPERATOR(true);
  DECLARE_OPERATOR(false);

  DECLARE_OPERATOR(and);
  DECLARE_OPERATOR(or);
  DECLARE_OPERATOR(not);
  DECLARE_OPERATOR(implies);
  DECLARE_OPERATOR(eq);
  DECLARE_OPERATOR(ite);
  DECLARE_OPERATOR (xor);
  DECLARE_OPERATOR(nand);
  DECLARE_OPERATOR(concat);
  DECLARE_OPERATOR(bvnot);
  DECLARE_OPERATOR(bvand);
  DECLARE_OPERATOR(bvnand);
  DECLARE_OPERATOR(bvor);
  DECLARE_OPERATOR(bvnor);
  DECLARE_OPERATOR(bvxor);
  DECLARE_OPERATOR(bvxnor);
  DECLARE_OPERATOR(bvult);
  DECLARE_OPERATOR(bvslt);
  DECLARE_OPERATOR(bvule);
  DECLARE_OPERATOR(bvsle);
  DECLARE_OPERATOR(bvugt);
  DECLARE_OPERATOR(bvsgt);
  DECLARE_OPERATOR(bvuge);
  DECLARE_OPERATOR(bvsge);
  DECLARE_OPERATOR(bvcomp);
  DECLARE_OPERATOR(bvneg);
  DECLARE_OPERATOR(bvadd);
  DECLARE_OPERATOR(bvsub);
  DECLARE_OPERATOR(bvmul);
  DECLARE_OPERATOR(bvudiv);
  DECLARE_OPERATOR(bvsdiv);
  DECLARE_OPERATOR(bvsmod);
  DECLARE_OPERATOR(bvurem);
  DECLARE_OPERATOR(bvsrem);
  DECLARE_OPERATOR(bvshl);
  DECLARE_OPERATOR(bvlshr);
  DECLARE_OPERATOR(bvashr);
  DECLARE_OPERATOR(extract);
  DECLARE_OPERATOR(bit2bool);
  DECLARE_OPERATOR(repeat);
  DECLARE_OPERATOR(zero_extend);
  DECLARE_OPERATOR(sign_extend);
  DECLARE_OPERATOR(rotate_left);
  DECLARE_OPERATOR(rotate_right);

#undef DECLARE_OPERATOR

}; // SmtlibInvariantParser

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

#endif // CHC_INV_IN_H__