6 #include "core/SolverTypes.h" 18 this->clauses = clauses;
28 clauses.push_back(clause);
40 clauses.push_back(clause);
54 clauses.push_back(clause);
72 if (clauses.size() == 0) {
76 Clauses negationClause(~(clauses[0]));
77 for (
unsigned i = 1; i < clauses.size(); i++) {
78 std::vector<CClause> negationClauseVector = ~(clauses[i]);
79 Clauses negationThisClause(negationClauseVector);
80 negationClause = (negationClause | negationThisClause);
82 return negationClause;
99 std::vector<CClause> thisClauses = clauses;
100 std::vector<CClause> otherClauses = other.clauses;
101 thisClauses.insert(std::end(thisClauses), std::begin(otherClauses),
102 std::end(otherClauses));
117 return operator&(otherClauses);
163 for (
unsigned i = 0; i < clauses.size(); i++) {
172 for (
unsigned j = 0; j < clauses[i].getLits().size(); j++) {
173 c1rep.
addLits(clauses[i].getLits()[j]);
176 clause.push(~clauses[i].getLits()[j]);
181 for (
unsigned i = 0; i < other.clauses.size(); i++) {
190 for (
unsigned j = 0; j < other.clauses[i].getLits().size(); j++) {
191 c1rep.
addLits(other.clauses[i].getLits()[j]);
194 clause.push(~other.clauses[i].getLits()[j]);
214 return operator|(otherClauses);
229 Clauses negateThis = operator~();
230 return (negateThis | other);
246 clauses.insert(std::end(clauses), std::begin(other), std::end(other));
255 std::vector<CClause> otherClauses = other.
getClauses();
256 addClauses(otherClauses);
273 LOG_DEBUG(INFO) <<
"";
Class for representing a clause.
Clauses()
Constructs the Clauses object, with no clauses in it.
std::vector< CClause > getClauses() const
Gets the clauses in this object.
Clauses operator>>(const Clauses &)
Defines the implication operation between two sets of Clauses.
Clauses operator|(const Clauses &)
Defines the disjunction operation between two sets of clauses.
void print()
Displays the clauses in this object.
void addClauses(const CClause &)
Adds a CClause to the set of clauses.
void addLits(const Lit &)
Adds a Lit, a literal, to the clause.
void clear()
Clears the Clauses object by removing all the clauses.
Class for representing a set of clauses.
Clauses operator~()
Defines the negation operation on a set of clauses.