text: #include "commander_encoding.h"
  
  #include <cmath>
  
  using namespace std;
  
  int64_t commander_encoding::encodingValue(const SimplePBConstraint& pbconstraint)
  {
    int k = config->commander_encoding_k;
    int n = pbconstraint.getN();
  
    int64_t auxvars = (double)n*((double)1/k)/(1-(double)1/k);
    int64_t clauses = ((k*(double)(k+1)/2)+1) * auxvars;
  
    return valueFunction(clauses, auxvars);
  }
  
  
  void commander_encoding::encode_non_recursive(vector< Lit >& literals, ClauseDatabase& formula, AuxVarManager& auxvars)
  {
  //    basic_amo_encoder.encode_intern(literals, formula, auxvars);
    naive_amo_encoder.encode_intern(literals, formula);
  }
  
  
  void commander_encoding::encode_intern(vector<Lit>&, ClauseDatabase& formula, AuxVarManager& auxvars, bool isExactlyOne)
  {
    int i;
  
    while (current_literals.size() > k)
    {
      _literals.clear();
      next_literals.clear();
      for (i = 0; i < current_literals.size(); ++i)
      {
        _literals.push_back(current_literals[i]);
  
        if (i % k == (k-1) || (i == current_literals.size() - 1) ) // is group full?
        {
  	// 1. at most one variable in a gtroup can be true
  	encode_non_recursive(_literals, formula, auxvars);
  
  	_literals.push_back(auxvars.getVariable());
  	next_literals.push_back(-1 * _literals.back());
  
  	if (isExactlyOne)
  	{
  	  //2. if the commander variable of a group is true, then at least one of the variables in the group must be true (only for the exactly one case)
  	  formula.addClause(_literals); // at least one
  	}
  
  	// 3. if the commander variable of a group is false, then none of the variables in the group can be true
  	for (int j = 0; j < _literals.size() - 1; ++j)
  	{
  	  formula.addClause(-1 * _literals.back(), -1 * _literals[j]);
  	}
  	_literals.clear();
        }
      }
  
      // exactly one of the commander variables is true
      current_literals = next_literals;
      isExactlyOne = true;
    }
  
    // at most one
    encode_non_recursive(current_literals, formula, auxvars);
  
  
    if (isExactlyOne)
    {
      // at least one
      formula.addClause(current_literals);
    }
  
  }
  
  
  void commander_encoding::encode(const SimplePBConstraint& pbconstraint, ClauseDatabase& formula, AuxVarManager& auxvars)
  {
      formula.addConditionals(pbconstraint.getConditionals());
  
      if (config->print_used_encodings)
        cout << "c encode with command encoder amo" << endl;
  
      assert(pbconstraint.getLeq() == 1);
  
      current_literals.clear();
      for (int i = 0; i < (int) pbconstraint.getN(); ++i)
        current_literals.push_back(pbconstraint.getWeightedLiterals()[i].lit);
  
      encode_intern(current_literals, formula, auxvars, (pbconstraint.getComparator() == PBLib::BOTH && (pbconstraint.getGeq() == 1)));
  
  
      for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
        formula.getConditionals().pop_back();
  }
  
  
  commander_encoding::commander_encoding(PBConfig& config) : Encoder(config), basic_amo_encoder(config), naive_amo_encoder(config)
  {
    k = config->commander_encoding_k;
  }
  