update vendor/

vendor/github.com/crillab/gophersat/solver/card.go

@@ -15,10 +15,11 @@ func AtLeast1(lits ...int) CardConstr {
 
 // AtMost1 returns a cardinality constraint stating that at most one of the given lits can be true.
 func AtMost1(lits ...int) CardConstr {
+	negated := make([]int, len(lits))
 	for i, lit := range lits {
-		lits[i] = -lit
+		negated[i] = -lit
 	}
-	return CardConstr{Lits: lits, AtLeast: len(lits) - 1}
+	return CardConstr{Lits: negated, AtLeast: len(lits) - 1}
 }
 
 // Exactly1 returns two cardinality constraints stating that exactly one of the given lits must be true.

vendor/github.com/crillab/gophersat/solver/parser.go

@@ -55,17 +55,21 @@ func ParseSlice(cnf [][]int) *Problem {
 			return &pb
 		}
 	}
-	pb.simplify()
+	pb.simplify2()
 	return &pb
 }
 
+func isSpace(b byte) bool {
+	return b == ' ' || b == '\t' || b == '\n' || b == '\r'
+}
+
 // readInt reads an int from r.
 // 'b' is the last read byte. It can be a space, a '-' or a digit.
 // The int can be negated.
 // All spaces before the int value are ignored.
 // Can return EOF.
 func readInt(b *byte, r *bufio.Reader) (res int, err error) {
-	for err == nil && (*b == ' ' || *b == '\t' || *b == '\n' || *b == '\r') {
+	for err == nil && isSpace(*b) {
 		*b, err = r.ReadByte()
 	}
 	if err == io.EOF {
@@ -88,7 +92,7 @@ func readInt(b *byte, r *bufio.Reader) (res int, err error) {
 		}
 		res = 10*res + int(*b-'0')
 		*b, err = r.ReadByte()
-		if *b == ' ' || *b == '\t' || *b == '\n' || *b == '\r' {
+		if isSpace(*b) {
 			break
 		}
 	}

vendor/github.com/crillab/gophersat/solver/parser_pb.go

@@ -65,6 +65,14 @@ func ParseCardConstrs(constrs []CardConstr) *Problem {
 	return &pb
 }
 
+func (pb *Problem) appendClause(constr PBConstr) {
+	lits := make([]Lit, len(constr.Lits))
+	for j, val := range constr.Lits {
+		lits[j] = IntToLit(int32(val))
+	}
+	pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, constr.AtLeast))
+}
+
 // ParsePBConstrs parses and returns a PB problem from PBConstr values.
 func ParsePBConstrs(constrs []PBConstr) *Problem {
 	var pb Problem
@@ -100,11 +108,7 @@ func ParsePBConstrs(constrs []PBConstr) *Problem {
 				}
 			}
 		} else {
-			lits := make([]Lit, len(constr.Lits))
-			for j, val := range constr.Lits {
-				lits[j] = IntToLit(int32(val))
-			}
-			pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, card))
+			pb.appendClause(constr)
 		}
 	}
 	pb.Model = make([]decLevel, pb.NbVars)

vendor/github.com/crillab/gophersat/solver/pb.go

@@ -57,12 +57,17 @@ func GtEq(lits []int, weights []int, n int) PBConstr {
 	if len(weights) != 0 && len(lits) != len(weights) {
 		panic("not as many lits as weights")
 	}
-	for i := range weights {
+	for i := 0; i < len(weights); i++ {
 		if weights[i] < 0 {
 			weights[i] = -weights[i]
 			n += weights[i]
 			lits[i] = -lits[i]
 		}
+		if weights[i] == 0 {
+			weights = append(weights[:i], weights[i+1:]...)
+			lits = append(lits[:i], lits[i+1:]...)
+			i--
+		}
 	}
 	return PBConstr{Lits: lits, Weights: weights, AtLeast: n}
 }

vendor/github.com/crillab/gophersat/solver/solver.go

@@ -87,10 +87,16 @@ func New(problem *Problem) *Solver {
 		return &Solver{status: Unsat}
 	}
 	nbVars := problem.NbVars
+
+	trailCap := nbVars
+	if len(problem.Units) > trailCap {
+		trailCap = len(problem.Units)
+	}
+
 	s := &Solver{
 		nbVars:     nbVars,
 		status:     problem.Status,
-		trail:      make([]Lit, len(problem.Units), nbVars),
+		trail:      make([]Lit, len(problem.Units), trailCap),
 		model:      problem.Model,
 		activity:   make([]float64, nbVars),
 		polarity:   make([]bool, nbVars),
@@ -343,7 +349,7 @@ func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status {
 				return Indet
 			}
 			if s.Stats.NbConflicts >= s.wl.idxReduce*s.wl.nbMax {
-				s.wl.idxReduce = (s.Stats.NbConflicts / s.wl.nbMax) + 1
+				s.wl.idxReduce = s.Stats.NbConflicts/s.wl.nbMax + 1
 				s.reduceLearned()
 				s.bumpNbMax()
 			}
@@ -738,7 +744,7 @@ func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) {
 		copy(s.lastModel, s.model) // Save this model: it might be the last one
 		cost = 0
 		for i, lit := range s.minLits {
-			if (s.model[lit.Var()] > 0) == lit.IsPositive() {
+			if s.model[lit.Var()] > 0 == lit.IsPositive() {
 				if s.minWeights == nil {
 					cost++
 				} else {
@@ -803,7 +809,7 @@ func (s *Solver) Minimize() int {
 		copy(s.lastModel, s.model) // Save this model: it might be the last one
 		cost = 0
 		for i, lit := range s.minLits {
-			if (s.model[lit.Var()] > 0) == lit.IsPositive() {
+			if s.model[lit.Var()] > 0 == lit.IsPositive() {
 				if s.minWeights == nil {
 					cost++
 				} else {