Program Listing for File structures.h

↰ Return to documentation for file (src/structures.h)

#ifndef STRUCTURES_H_
#define STRUCTURES_H_

#include <assert.h>
#include <vector>
#include <iostream>

#include "primitive_types.h"

#define INVALID_DL -1

typedef unsigned char TriValue;
#define   F_TRI  0
#define   T_TRI  1
#define   X_TRI  2

class LiteralID {
 public:
  LiteralID() {
    value_ = 0;
  }
  // This code does screwy casting.  Cannot use explicit
  LiteralID(int lit) {  // NOLINT (runtime/explicit)
    value_ = (abs(lit) << 1) + static_cast<unsigned>(lit > 0);
  }
  LiteralID(VariableIndex var, bool sign) {
    value_ = (var << 1) + static_cast<unsigned>(sign);
  }

  VariableIndex var() const {
    return (value_ >> 1);
  }
  int toInt() const {
    return (static_cast<int>(value_) >> 1) * ((sign()) ? 1 : -1);
  }
  void inc() {++value_;}
  void copyRaw(unsigned int v) {
    value_ = v;
  }
  const bool sign() const {
    return static_cast<bool>(value_ & 0x01);
  }
  const bool operator!=(const LiteralID &rL2) const {
    return value_ != rL2.value_;
  }
  const bool operator==(const LiteralID &rL2) const {
    return value_ == rL2.value_;
  }
  const bool operator<(const LiteralID &rL2) const {
    return value_ < rL2.value_;
  }
  const LiteralID neg() const {
    return LiteralID(var(), !sign());
  }

  void print() const {
    std::cout << (sign() ? " " : "-") << var() << " ";
  }
  inline unsigned raw() const { return value_;}

 private:
  unsigned value_;

  template <class _T> friend class LiteralIndexedVector;
};

static const LiteralID NOT_A_LIT(0, false);
#define SENTINEL_LIT NOT_A_LIT

class Literal {
 public:
  std::vector<LiteralID> binary_links_ = std::vector<LiteralID>(1, SENTINEL_LIT);
  std::vector<ClauseOfs> watch_list_ = std::vector<ClauseOfs>(1, SENTINEL_CL);  // Watch clauses
  float activity_score_ = 0.0f;

  void increaseActivity(unsigned u = 1) {
    activity_score_+= u;
  }
  void resetActivity() { activity_score_ = 0;}
  void removeWatchLinkTo(ClauseOfs clause_ofs) {
    for (auto it = watch_list_.begin(); it != watch_list_.end(); it++)
      if (*it == clause_ofs) {
        *it = watch_list_.back();  // Get last element in vector and replace item to be removed
        watch_list_.pop_back();  // Delete the last element
        return;
      }
  }

  void replaceWatchLinkTo(ClauseOfs clause_ofs, ClauseOfs replace_ofs) {
    for (auto it = watch_list_.begin(); it != watch_list_.end(); it++)
      if (*it == clause_ofs) {
        *it = replace_ofs;
        return;
      }
  }
  void addWatchLinkTo(ClauseIndex clause_ofs) {
    watch_list_.push_back(clause_ofs);
  }
  void addBinLinkTo(LiteralID lit) {
    binary_links_.back() = lit;
    binary_links_.push_back(SENTINEL_LIT);
  }
  void resetWatchList() {
    watch_list_.clear();
    watch_list_.push_back(SENTINEL_CL);
  }
  bool hasBinaryLinkTo(LiteralID lit) {
    for (auto l : binary_links_) {
      if (l == lit)
        return true;
    }
    return false;
  }
  bool hasBinaryLinks() {
    return !binary_links_.empty();
  }
};

class Antecedent {
  unsigned int val_;

 public:
  Antecedent() {
    val_ = 1;
  }
  explicit Antecedent(const ClauseOfs cl_ofs) {
    val_ = (cl_ofs << 1) | 1;
  }
  explicit Antecedent(const LiteralID idLit) {
    val_ = (idLit.raw() << 1);
  }
  bool isAClause() const {
    return val_ & 0x01;
  }
  ClauseOfs asCl() const {
    assert(isAClause());  // ZH - Verify the antecedent actually is a CLAUSE.
    return val_ >> 1;
  }
  LiteralID asLit() {
    assert(!isAClause());  // ZH - Verify the antecedent actually is a LITERAL.
    LiteralID idLit;
    idLit.copyRaw(val_ >> 1);
    return idLit;
  }
  bool isAnt() const {
    return val_ != 1;  // i.e. NOT a NOT_A_CLAUSE;
  }
};

struct Variable {
  Antecedent ante;
  long decision_level = INVALID_DL;
};


class ClauseHeader {
  unsigned creation_time_;  // number of conflicts seen at creation time
  unsigned score_;
  unsigned length_;

 public:
  void increaseScore() {
    score_++;
  }
  void decayScore() {
    score_ >>= 1;
  }
  unsigned score() const {
    return score_;
  }

  unsigned creation_time() {
    return creation_time_;
  }
  unsigned length() { return length_; }
  void set_length(unsigned length) { length_ = length; }

  void set_creation_time(unsigned time) {
    creation_time_ = time;
  }
  static unsigned overheadInLits() { return sizeof(ClauseHeader)/sizeof(LiteralID); }
};

#endif /* STRUCTURES_H_ */