cclause.cpp

#include "cclause.h"

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

using namespace NSPACE;

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

CClause::CClause(const Lit &lit) {
  lits.clear();
  lits.push_back(lit);
}

CClause::CClause(const Var &var) {
  lits.clear();
  lits.push_back(mkLit(var, false));
}

CClause::CClause() { lits.clear(); }

std::vector<CClause> CClause::operator~() {
  std::vector<CClause> result;
  result.clear();
  for (unsigned i = 0; i < lits.size(); i++) {
    CClause unitClause(~(lits[i]));
    result.push_back(unitClause);
  }
  return result;
}

std::vector<CClause> CClause::operator&(const CClause &other) {
  std::vector<CClause> result;
  result.clear();
  result.push_back(*this);
  result.push_back(other);
  return result;
}

Clauses CClause::operator&(const Clauses &other) {
  Clauses result(other.getClauses());
  result.addClauses(*this);
  return result;
}

CClause CClause::operator|(const CClause &other) {
  std::vector<Lit> thisLits = this->lits;
  std::vector<Lit> otherLits = other.getLits();
  // appending the literals
  thisLits.insert(std::end(thisLits), std::begin(otherLits),
                  std::end(otherLits));
  std::sort(thisLits.begin(), thisLits.end());
  // removing duplicates
  thisLits.erase(std::unique(thisLits.begin(), thisLits.end()), thisLits.end());
  bool existBothPolarities = false;
  int indexLitBothPolarities = -1;
  for (unsigned i = 0; i < thisLits.size(); i++) {
    for (unsigned j = i + 1; j < thisLits.size(); j++) {
      // if any two literals are such that they are x and ~x
      if (var(thisLits[i]) == var(thisLits[j])) {
        existBothPolarities = true;
        indexLitBothPolarities = i;
        break;
      }
    }
    if (existBothPolarities) {
      break;
    }
  }
  // replace the entire clause with x AND ~x, as it is true anyway
  if (existBothPolarities) {
    CClause result;
    result.addLits(thisLits[indexLitBothPolarities]);
    result.addLits(~thisLits[indexLitBothPolarities]);
    return result;
  }
  CClause result(thisLits);
  return result;
}

Clauses CClause::operator|(const Clauses &other) {
  Clauses thisLHS(*this);
  return (thisLHS | other);
}

std::vector<CClause> CClause::operator>>(const CClause &other) {
  std::vector<CClause> lhs = ~(*this);
  std::vector<CClause> result;
  result.clear();
  for (unsigned i = 0; i < lhs.size(); i++) {
    CClause thisClause = lhs[i] | other;
    result.push_back(thisClause);
  }
  return result;
}

Clauses CClause::operator>>(const Clauses &other) {
  Clauses thisLHS(~(*this));
  return (thisLHS | other);
}

void CClause::createLitAndAdd(const Var &var1) {
  lits.push_back(mkLit(var1, false));
}

void CClause::createLitAndAdd(const Var &var1, const Var &var2) {
  lits.push_back(mkLit(var1, false));
  lits.push_back(mkLit(var2, false));
}

void CClause::createLitAndAdd(const Var &var1, const Var &var2,
                              const Var &var3) {
  lits.push_back(mkLit(var1, false));
  lits.push_back(mkLit(var2, false));
  lits.push_back(mkLit(var3, false));
}

void CClause::addLits(const Lit &lit1) { lits.push_back(lit1); }

void CClause::addLits(const Lit &lit1, const Lit &lit2) {
  lits.push_back(lit1);
  lits.push_back(lit2);
}

void CClause::addLits(const Lit &lit1, const Lit &lit2, const Lit &lit3) {
  lits.push_back(lit1);
  lits.push_back(lit2);
  lits.push_back(lit3);
}

void CClause::addLits(const std::vector<Lit> &otherLits) {
  lits.insert(std::end(lits), std::begin(otherLits), std::end(otherLits));
}

std::vector<Lit> CClause::getLits() const { return lits; }

void CClause::printClause() {
  for (Lit lit : lits) {
    LOG_DEBUG(INFO) << (sign(lit) ? "-" : " ") << var(lit) << " ";
  }
  LOG_DEBUG(INFO) << "";
}

void CClause::clear() { lits.clear(); }