clauses.cpp

#include "clauses.h"

#include <iostream>
#include <vector>
#include "cclause.h"
#include "core/SolverTypes.h"
#include "global_vars.h"
#include "utils.h"

using namespace NSPACE;

Clauses::Clauses(const std::vector<CClause> &clauses) {
  this->clauses = clauses;
}

Clauses::Clauses(const CClause &clause) {
  clauses.clear();
  clauses.push_back(clause);
}

Clauses::Clauses(const Lit &lit) {
  clauses.clear();
  CClause clause(lit);
  clauses.push_back(clause);
}

Clauses::Clauses(const Var &var) {
  clauses.clear();
  CClause clause(var);
  clauses.push_back(clause);
}

Clauses::Clauses() { clauses.clear(); }

Clauses Clauses::operator~() {
  if (clauses.size() == 0) {
    CClause clause;
    return Clauses(clause);
  }
  Clauses negationClause(~(clauses[0]));
  for (unsigned i = 1; i < clauses.size(); i++) {
    std::vector<CClause> negationClauseVector = ~(clauses[i]);
    Clauses negationThisClause(negationClauseVector);
    negationClause = (negationClause | negationThisClause);
  }
  return negationClause;
}

Clauses Clauses::operator&(const Clauses &other) {
  std::vector<CClause> thisClauses = clauses;
  std::vector<CClause> otherClauses = other.clauses;
  thisClauses.insert(std::end(thisClauses), std::begin(otherClauses),
                     std::end(otherClauses));
  Clauses result(thisClauses);
  return result;
}

Clauses Clauses::operator&(const CClause &other) {
  Clauses otherClauses(other);
  return operator&(otherClauses);
}

Clauses Clauses::operator|(const Clauses &other) {
  if (other.getClauses().size() == 0) {
    Clauses result = other;
    return result;
  }
  // x and y are auxiliary variables for the sets of the clauses that are being
  // disjunctioned
  Lit x = timetabler->newLiteral();
  Lit y = timetabler->newLiteral();
  Clauses result(CClause(x) | CClause(y));
  vec<Lit> xrep;
  xrep.push(x);
  vec<Lit> yrep;
  yrep.push(y);
  for (unsigned i = 0; i < clauses.size(); i++) {
    // c1 is the auxiliary variable for a ith clause
    Lit c1 = timetabler->newLiteral();
    xrep.push(~c1);
    vec<Lit> clause;
    clause.push(c1);
    clause.push(~x);
    timetabler->addToFormula(clause, -1);
    CClause c1rep(~c1);
    for (unsigned j = 0; j < clauses[i].getLits().size(); j++) {
      c1rep.addLits(clauses[i].getLits()[j]);
      vec<Lit> clause;
      clause.push(c1);
      clause.push(~clauses[i].getLits()[j]);
      timetabler->addToFormula(clause, -1);
    }
    timetabler->addClauses(c1rep, -1);
  }
  for (unsigned i = 0; i < other.clauses.size(); i++) {
    // c1 is the auxiliary variable for a ith clause
    Lit c1 = timetabler->newLiteral();
    yrep.push(~c1);
    vec<Lit> clause;
    clause.push(c1);
    clause.push(~y);
    timetabler->addToFormula(clause, -1);
    CClause c1rep(~c1);
    for (unsigned j = 0; j < other.clauses[i].getLits().size(); j++) {
      c1rep.addLits(other.clauses[i].getLits()[j]);
      vec<Lit> clause;
      clause.push(c1);
      clause.push(~other.clauses[i].getLits()[j]);
      timetabler->addToFormula(clause, -1);
    }
    timetabler->addClauses(c1rep, -1);
  }
  timetabler->addToFormula(xrep, -1);
  timetabler->addToFormula(yrep, -1);
  return result;
}

Clauses Clauses::operator|(const CClause &other) {
  Clauses otherClauses(other);
  return operator|(otherClauses);
}

Clauses Clauses::operator>>(const Clauses &other) {
  Clauses negateThis = operator~();
  return (negateThis | other);
}

void Clauses::addClauses(const CClause &other) { clauses.push_back(other); }

void Clauses::addClauses(const std::vector<CClause> &other) {
  clauses.insert(std::end(clauses), std::begin(other), std::end(other));
}

void Clauses::addClauses(const Clauses &other) {
  std::vector<CClause> otherClauses = other.getClauses();
  addClauses(otherClauses);
}

std::vector<CClause> Clauses::getClauses() const { return clauses; }

void Clauses::print() {
  for (CClause c : clauses) {
    c.printClause();
  }
  LOG_DEBUG(INFO) << "";
}

void Clauses::clear() { clauses.clear(); }