cclause.h

Go to the documentation of this file.

#ifndef CCLAUSE_H
#define CCLAUSE_H

#include <vector>
#include "core/SolverTypes.h"
class Clauses;

using namespace NSPACE;

class CClause {
 private:
  std::vector<Lit> lits;

 public:
  CClause(const std::vector<Lit> &);
  CClause(const Lit &);
  CClause(const Var &);
  CClause();
  std::vector<CClause> operator~();
  std::vector<CClause> operator&(const CClause &);
  Clauses operator&(const Clauses &);
  CClause operator|(const CClause &);
  Clauses operator|(const Clauses &);
  std::vector<CClause> operator>>(const CClause &);
  Clauses operator>>(const Clauses &);
  void createLitAndAdd(const Var &);
  void createLitAndAdd(const Var &, const Var &);
  void createLitAndAdd(const Var &, const Var &, const Var &);
  void addLits(const Lit &);
  void addLits(const Lit &, const Lit &);
  void addLits(const Lit &, const Lit &, const Lit &);
  void addLits(const std::vector<Lit> &);
  std::vector<Lit> getLits() const;
  void clear();
  void printClause();
};

#endif