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 Minisat;

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