Commit b259780d authored by Masahiko Sakai's avatar Masahiko Sakai
Browse files

removal of zero valued term from goal

parent d7e17b14

PbSolver.C

+34 −2
Original line number Diff line number Diff line
@@ -71,8 +71,11 @@ void PbSolver::addInterestVars(int num) 
    pb_i_vars = num; //reportf("pb_i_vars=%d\n",pb_i_vars); 

}



void PbSolver::addGoal(const vec<Lit>& ps, const vec<Int>& Cs)

void PbSolver::addGoal(vec<Lit>& ps, vec<Int>& Cs)

{



  PbSolver::simplifyGoal(ps, Cs);

  

  //**/debug_names = &index2name;

    //**/reportf("MIN: "); dump(ps, Cs); reportf("\n");

  assert(ps.size() == Cs.size());
@@ -442,6 +445,35 @@ bool PbSolver::normalizePb(vec<Lit>& ps, vec<Int>& Cs, Int& C, Lit llt) 
    return true;

}



// Delete terms with zero coefficient



void PbSolver::simplifyGoal(vec<Lit>& ps, vec<Int>& Cs)

{

  /*

  bool hasZero = false;

  for (int i = 0; i <ps.size(); i++){

    if (Cs[i] == 0){

      hasZero = true;

      break;

    }

  }

  */

  //  if(hasZero){

  int shrink = 0;

  for (int i = 0; i <ps.size(); i++){

    if (Cs[i] == 0) shrink++;

    else if (shrink > 0) {

      Cs[i-shrink] = Cs[i]; ps[i-shrink] = ps[i];

    }

  }

  assert(ps.size() >= shrink);

  //    if(ps.size() == shrink) shrink--;  // avoid null goal, leaving at least one 0*x.

  if(shrink > 0){

    ps.shrink(shrink); Cs.shrink(shrink);

  }

  //  }

}



bool PbSolver::rewritePureClause(const vec<Lit>& ps, const vec<Int>& Cs, Int lo, Int hi, Lit llt)

{

        if(lo == Int_MIN && hi == Int_MAX) {  // true constraint

PbSolver.h

+2 −1
Original line number Diff line number Diff line
@@ -93,6 +93,7 @@ public: 
    void    propagate();

    bool    addUnit  (Lit p) { return sat_solver.addUnit(p); }

    bool    normalizePb(vec<Lit>& ps, vec<Int>& Cs, Int& C, Lit llt=lit_Undef);

    void    simplifyGoal(vec<Lit>& ps, vec<Int>& Cs);

    void    storePb    (const vec<Lit>& ps, const vec<Int>& Cs, Int lo, Int hi, Lit llp=lit_Undef);

    void    setupOccurs();   // Called on demand from 'propagate()'.

    void    findIntervals();
@@ -161,7 +162,7 @@ public: 
    //

    int     getVar      (cchar* name);

    void    allocConstrs(int n_vars, int n_constrs);

    void    addGoal     (const vec<Lit>& ps, const vec<Int>& Cs);

    void    addGoal     (vec<Lit>& ps, vec<Int>& Cs);

    void    addInterestVars     (int num);



    /////////////////////