Commit 9a6a789c authored by Masahiko Sakai's avatar Masahiko Sakai
Browse files

Bug fixed for Zero coefficient in goal

parent 7d9365c7
Loading
Loading
Loading
Loading
+16 −9
Original line number Diff line number Diff line
@@ -76,18 +76,25 @@ void PbSolver::addGoal(const vec<Lit>& ps, const vec<Int>& Cs)
    //**/debug_names = &index2name;
    //**/reportf("MIN: "); dump(ps, Cs); reportf("\n");
  assert(ps.size() == Cs.size());
  assert(ps.size() > 0);
  //if (ps.size() == 0) return;
  assert(ps.size() >= 0);

  // GCD;
  vec<Int> norm_Cs;
  if(opt_goal_gcd) {
    assert(Cs[0] != 0);
    if(Cs[0] < 0) goal_coeff = -Cs[0]; else goal_coeff = Cs[0];
    for (int i = 1; i < Cs.size(); i++) {
      assert(Cs[i] != 0);
    int i = 0; bool emptyGoal = true;
    for (; i < Cs.size(); i++) {
      if(Cs[i] != 0) {
        if(Cs[i] < 0) goal_coeff = -Cs[i]; else goal_coeff = Cs[i];
	emptyGoal = false;
	break;
      }
    } reportf("i=%d\n",i);
    if(!emptyGoal)
      for (; i < Cs.size(); i++) {
        if(Cs[i] < 0) goal_coeff = gcdg(goal_coeff, -Cs[i]);
      else goal_coeff = gcdg(goal_coeff, Cs[i]);
        else if(Cs[i] > 0) goal_coeff = gcdg(goal_coeff, Cs[i]);
      }
    else goal_coeff = 1;
  } else goal_coeff = 1;

  if(opt_verbosity >=1 )