Program Listing for File cached_assignment.h

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

#ifndef SHARPSAT_CACHED_ASSIGNMENT_H
#define SHARPSAT_CACHED_ASSIGNMENT_H

#include <algorithm>
#include <vector>
#include "structures.h"

#define CACHED_VARIABLE_LEN 2 // In Bits

class CachedAssignment{
 public:
  CachedAssignment() {
    assigned_literals_.reserve(1);
    emancipated_vars_.reserve(1);
  }
  inline void Sort() {
    std::sort(assigned_literals_.begin(), assigned_literals_.end());
    std::sort(emancipated_vars_.begin(), emancipated_vars_.begin());
  }
  inline void IncreaseSize(VariableIndex size_adder) {
    VariableIndex new_size = assigned_literals_.capacity() + size_adder;
    assigned_literals_.reserve(new_size);
  }
//  /**
//   * Add the specified literal to the list of literals in the cache
//   * assignment.
//   *
//   * @param lit New literal value.
//   */
//  inline void AddLiteral(LiteralID lit) {assigned_literals_.push_back(lit);}
  const std::vector<VariableIndex> vars() {
    std::vector<VariableIndex> cached_vars;
    cached_vars.reserve(assigned_literals_.size());

    for (auto lit : assigned_literals_)
      cached_vars.push_back(lit.var());
    cached_vars.insert(cached_vars.end(), emancipated_vars_.begin(), emancipated_vars_.end());
    return cached_vars;
  }
  const VariableIndex num_components() const { return num_cached_components; }
  const bool empty() const {return num_cached_components == 0; }
  void ProcessComponent(const Component * comp, mpz_class model_count_and_assn) {
    // Nothing to store in the UNSAT case
    if (model_count_and_assn == 0)
      return;
    IncreaseSize(comp->num_variables());  // Increase the capacity

    // Extract the literal assignments from the MPZ object
    std::vector<ComponentVarAndCls> comp_data = comp->getData();
    for (VariableIndex i = 0; i < comp->num_variables(); i++) {
      VariableIndex bit_index = CACHED_VARIABLE_LEN * i;
      // Check if the variable is emancipated
      if (mpz_tstbit(model_count_and_assn.get_mpz_t(), bit_index + 1) == 1) {
        emancipated_vars_.emplace_back(comp_data[i]);
      } else {
        bool sign = (mpz_tstbit(model_count_and_assn.get_mpz_t(), bit_index) == 1);
        assigned_literals_.emplace_back(LiteralID(comp_data[i], sign));
      }
    }
    num_cached_components++;
  }
  const std::vector<LiteralID>& literals() const { return assigned_literals_; }
  const std::vector<VariableIndex>& emancipated_vars() const { return emancipated_vars_; }
  void clear() {
    assigned_literals_.clear();
    emancipated_vars_.clear();
    num_cached_components = 0;
  }
//  /**
//   * Component Split Accessor
//   *
//   * Accessor for whether this cached assignment corresponds with a component
//   * split.
//   *
//   * @return true if this cached assignment corresponds to a component split.
//   */
//  const bool is_component_split() const { return is_component_split_;}

 private:
  std::vector<VariableIndex> emancipated_vars_;
  std::vector<LiteralID> assigned_literals_;
  unsigned long num_cached_components = 0;
};

#endif // SHARPSAT_CACHED_ASSIGNMENT_H