inv_cnf.h

// Hongce Zhang

#ifndef INV_CNF_H__
#define INV_CNF_H__

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

#include <set>
#include <string>
#include <tuple>
#include <unordered_map>
#include <vector>

namespace ilang {

class InvariantInCnf {
public:
  // Type definitions
  typedef std::tuple<bool, std::string, unsigned> literal;
  typedef std::vector<literal> clause;
  typedef std::unordered_map<std::string, clause> cnf_t;

  // helper functions
  static std::string Lit2Str(const literal& l);
  static void CanonicalizeClause(clause& c);
  static std::string Clause2Str(const clause& c);
  static void VarsToClause(const std::set<std::string>& vars, clause& out);

public:
  void ExportInCnfFormat(std::ostream& os) const;
  void ExportInCociFormat(std::ostream& os) const;
  void ImportFromFile(std::istream& os);

public:
  // members function : insert clause
  void InsertClause(clause& c);

  // insert clause (from another clause, so no need to reorder)
  void InsertClauseNoReorder(const clause& c);

  // members function : insert clause if it does not exist before
  void InsertClauseNewerFromReference(clause& c, const InvariantInCnf& ref);

  // members function : insert the incremental clauses
  void InsertClauseIncremental(const InvariantInCnf& ref);

  const cnf_t& GetCnfs() const { return _cnf_; }
  void Clear();

protected:
  // members
  cnf_t _cnf_;

}; // class InvariantInCnf

}; // namespace ilang

#endif // INVSYN_INTERFACE

#endif // INV_CNF_H__