Program Listing for File stack.h

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

#ifndef STACK_H_
#define STACK_H_


#include <gmpxx.h>

#include <cassert>
#include <vector>
#include <string>

#include "model_sampler.h"
#include "cached_assignment.h"
#include "solver_config.h"


class StackLevel {
  const VariableIndex super_component_ = 0;
  bool active_branch_ = false;
  const VariableIndex literal_stack_ofs_ = 0;
  bool is_component_split_ = false;
  bool first_component_ = false;
  SampleAssignment cache_sample_[2];
  mpz_class branch_model_count_[2] = {0, 0};
  bool branch_found_unsat_[2] = {false, false};
  void includeSolutionVar(const mpz_class &solutions, mpz_class solution_var[],
                          const std::string &name_var);
  const VariableIndex remaining_components_ofs_ = 0;
  VariableIndex unprocessed_components_end_ = 0;
  static VariableIndex component_split_depth_;

  /*---------------------------------------*
   *       Begin Sampler Variables         *
   *---------------------------------------*/

  mpz_class stack_solution_count_multiplier_[2] = {1, 1};
  std::vector<std::vector<VariableIndex>> stack_emancipated_vars_;
  std::vector<CacheEntryID> cache_comp_ids_[2];
  static SolverConfiguration* config_;
  static DataAndStatistics* statistics_;
  CachedAssignment cached_assn_;

 public:
  bool hasUnprocessedComponents() const {
    assert(unprocessed_components_end_ >= remaining_components_ofs_);
    return unprocessed_components_end_ > remaining_components_ofs_;
  }
  void nextUnprocessedComponent() {
    assert(unprocessed_components_end_ > remaining_components_ofs_);
    unprocessed_components_end_--;
  }
  void resetRemainingComps() {
    unprocessed_components_end_ = remaining_components_ofs_;
  }
  const VariableIndex super_component() const {
    return super_component_;
  }
  const VariableIndex remaining_components_ofs() const {
    return remaining_components_ofs_;
  }
  const VariableIndex unprocessed_components_end() const {
    return unprocessed_components_end_;
  }
  void set_unprocessed_components_end(VariableIndex end) {
    unprocessed_components_end_ = end;
    assert(remaining_components_ofs_ <= unprocessed_components_end_);
  }

  StackLevel() {
    stack_emancipated_vars_.resize(2);
  }

  StackLevel(VariableIndex super_comp, VariableIndex lit_stack_ofs,
             ClauseOfs comp_stack_ofs) :
      super_component_(super_comp),
      literal_stack_ofs_(lit_stack_ofs),
      remaining_components_ofs_(comp_stack_ofs),
      unprocessed_components_end_(comp_stack_ofs) {
    assert(super_comp < comp_stack_ofs);
    stack_emancipated_vars_.resize(2);
  }
  VariableIndex currentRemainingComponent() {
    assert(remaining_components_ofs_ <= unprocessed_components_end_ - 1);
    return unprocessed_components_end_ - 1;
  }
  bool isSecondBranch() {
    return active_branch_;
  }
  void changeBranch() {
    active_branch_ = true;
  }
  bool anotherCompProcessible() {
    return (!branch_found_unsat()) && hasUnprocessedComponents();
  }

  VariableIndex literal_stack_ofs() const {
    return literal_stack_ofs_;
  }
  void includeSolution(const mpz_class &solutions) {
    includeSolutionVar(solutions, branch_model_count_, "branch_model_count");
  }
  void includeSolutionSampleMultiplier(const mpz_class &solutions) {
    includeSolutionVar(solutions, stack_solution_count_multiplier_,
                       "sampler_solution_multiplier");
  }
  void includeSolution(unsigned solutions);
  void configureNewLevel(const StackLevel &top, const DecisionLevel decision_level) {
    // Do not push down any counts at the top of the decision stack when doing reservoir sampling
    // This is required in some cases in top tree sampling since the solution count at each leaf
    // is required while traversing the tree.
    if (decision_level == 0 && !(config_->perform_top_tree_sampling && !top.isComponentSplit()))
      return;
    // Push down the solution multiplier and freed variable list
    // Make sure to only use the active branch.
    for (auto &multiplier : stack_solution_count_multiplier_)
      multiplier = top.getSamplerSolutionMultiplier();

    for (auto &freed_variables : stack_emancipated_vars_)
      freed_variables = top.emancipated_vars();

    for (auto &cache_comp_ids : cache_comp_ids_)
      cache_comp_ids = top.cached_comp_ids();
  }
  void addFreeVariables(const std::vector<VariableIndex> &freed_vars) {
    int idx = (active_branch_) ? 1 : 0;
    stack_emancipated_vars_[idx].insert(stack_emancipated_vars_[idx].end(),
                                       freed_vars.begin(), freed_vars.end());
  }
  void addCachedCompIds(const std::vector<CacheEntryID> &ids) {
    int idx = (active_branch_) ? 1 : 0;
//    assert(cached_comp_ids_.empty());
    if (ids.empty())
      return;
    cache_comp_ids_[idx].insert(cache_comp_ids_[idx].end(), ids.begin(), ids.end());
  }
  inline bool branch_found_unsat() const {
    return branch_found_unsat_[active_branch_];
  }
  inline void mark_branch_unsat() {
    branch_found_unsat_[active_branch_] = true;
  }
  const mpz_class getTotalModelCount() const {
    return branch_model_count_[0] + branch_model_count_[1];
  }
  const mpz_class& getActiveModelCount() const {
    if (!active_branch_)
      return branch_model_count_[0];
    else
      return branch_model_count_[1];
  }
  const mpz_class& getSamplerSolutionMultiplier() const {
    if (!active_branch_)
      return stack_solution_count_multiplier_[0];
    else
      return stack_solution_count_multiplier_[1];
  }
//  /**
//   * Calculates the total descendent model count for this stack level.  It is equal to:
//   *
//   * FalseModelCount * FalseCountMultiplier + TrueModelCount * TrueCountMultiplier
//   *
//   * @return Total descendent model count.
//   */
//  const mpz_class GetDescendentModelCount() const {
//    mpz_class total_model_count = 0;
//    for (int i = 0; i < 2; i++) {
//      if (stack_solution_count_multiplier_[i] == 1)
//        total_model_count += branch_model_count_[i];
//      else
//        total_model_count += branch_model_count_[i] * stack_solution_count_multiplier_[i];
//    }
//    return total_model_count;
//  }
  const bool HasNoDescendentModels() {
    return branch_found_unsat_[0] && branch_found_unsat_[1];
  }
  inline const std::vector<VariableIndex> &emancipated_vars() const {
    if (!active_branch_)
      return stack_emancipated_vars_[0];
    else
      return stack_emancipated_vars_[1];
  }
  inline const std::vector<CacheEntryID> &cached_comp_ids() const {
    if (!active_branch_)
      return cache_comp_ids_[0];
    else
      return cache_comp_ids_[1];
  }
  inline const bool isComponentSplit() const {
    return is_component_split_ && config_->perform_random_sampling_;
  }
  inline void setAsComponentSplit() {
    if (!config_->perform_random_sampling_)
      return;

    if (!is_component_split_) {
      component_split_depth_++;
      if (component_split_depth_ > statistics_->max_component_split_depth_)
        statistics_->max_component_split_depth_ = component_split_depth_;
    }
    is_component_split_ = true;
    first_component_ = true;
  }
  inline void unsetAsComponentSplit() {
    if (!config_->perform_random_sampling_)
      return;

    if (is_component_split_)
      component_split_depth_--;
    assert(component_split_depth_>= 0);
    is_component_split_ = false;
    first_component_ = false;
  }
  inline static VariableIndex componentSplitDepth() {
    return component_split_depth_;
  }
  inline const bool isFirstComponent() const {
    assert(is_component_split_);
    return first_component_ && config_->perform_random_sampling_;
  }
  inline void markFirstComponentComplete() {
    assert(is_component_split_);
    first_component_ = false;
  }
  inline static void set_solver_config_and_statistics(SolverConfiguration &config,
                                                      DataAndStatistics &statistics) {
    config_ = &config;
    statistics_ = &statistics;
  }
  inline void set_cached_assn(CachedAssignment &cached_assn) {
    assert(config_->perform_random_sampling_);
    cached_assn_ = cached_assn;
  }
  inline const CachedAssignment& cached_assn() const { return cached_assn_; }
  inline void ClearCachedAssn() { cached_assn_.clear(); }
  inline void set_cache_sample(const SampleAssignment & cache_sample) {
    if (!active_branch_)
      cache_sample_[0] = cache_sample;
    else
      cache_sample_[1] = cache_sample;
  }
  SampleAssignment random_cache_sample() const;
};

class DecisionStack: public std::vector<StackLevel> {
  VariableIndex failed_literal_test_active = 0;

 public:
  DecisionStack() : std::vector<StackLevel>() {}
  void startFailedLitTest() {
//    failed_literal_test_active = true;  // Thurley's old code. Relies on casting
    failed_literal_test_active = 1;
  }
  void stopFailedLitTest() {
//    failed_literal_test_active = false;  // Thurley's old code. Relies on casting
    failed_literal_test_active = 0;
  }
  // end for implicit BCP
  StackLevel &top() {
    return const_cast<StackLevel&>(top_const());  // Strip off the const
  }
  const StackLevel &top_const() const {
    assert(!empty());
    return back();
  }
  StackLevel &on_deck() {
    assert(size() >= 2);
    return (*this)[size() - 2];
  }
  DecisionLevel get_decision_level() const {
    assert(!empty());
    return size() - 1 + failed_literal_test_active;
  }  // 0 means pre-1st-decision
};

#endif  // STACK_H_