1package solver23import (4 "bufio"5 "fmt"6 "io"7 "strconv"8 "strings"9)1011// ParseSlice parse a slice of slice of lits and returns the equivalent problem.12// The argument is supposed to be a well-formed CNF.13func ParseSlice(cnf [][]int) *Problem {14 var pb Problem15 pb.parseSlice(cnf)16 return &pb17}1819// ParseSliceNb parse a slice of slice of lits and returns the equivalent problem.20// The argument is supposed to be a well-formed CNF.21// The number of vars is provided because clauses might be added to it later.22func ParseSliceNb(cnf [][]int, nbVars int) *Problem {23 pb := Problem{NbVars: nbVars}24 pb.parseSlice(cnf)25 return &pb26}2728func (pb *Problem) parseSlice(cnf [][]int) {29 for _, line := range cnf {30 switch len(line) {31 case 0:32 pb.Status = Unsat33 return34 case 1:35 if line[0] == 0 {36 panic("null unit clause")37 }38 lit := IntToLit(int32(line[0]))39 v := lit.Var()40 if int(v) >= pb.NbVars {41 pb.NbVars = int(v) + 142 }43 pb.Units = append(pb.Units, lit)44 default:45 lits := make([]Lit, len(line))46 for j, val := range line {47 if val == 0 {48 panic(fmt.Sprintf("null literal in clause %v", lits))49 }50 lits[j] = IntToLit(int32(val))51 if v := int(lits[j].Var()); v >= pb.NbVars {52 pb.NbVars = v + 153 }54 }55 pb.Clauses = append(pb.Clauses, NewClause(lits))56 }57 }58 pb.Model = make([]decLevel, pb.NbVars)59 for _, unit := range pb.Units {60 v := unit.Var()61 if pb.Model[v] == 0 {62 if unit.IsPositive() {63 pb.Model[v] = 164 } else {65 pb.Model[v] = -166 }67 } else if pb.Model[v] > 0 != unit.IsPositive() {68 pb.Status = Unsat69 return70 }71 }72 pb.simplify2()73}7475func isSpace(b byte) bool {76 return b == ' ' || b == '\t' || b == '\n' || b == '\r'77}7879// readInt reads an int from r.80// 'b' is the last read byte. It can be a space, a '-' or a digit.81// The int can be negated.82// All spaces before the int value are ignored.83// Can return EOF.84func readInt(b *byte, r *bufio.Reader) (res int, err error) {85 for err == nil && isSpace(*b) {86 *b, err = r.ReadByte()87 }88 if err == io.EOF {89 return res, io.EOF90 }91 if err != nil {92 return res, fmt.Errorf("could not read digit: %v", err)93 }94 neg := 195 if *b == '-' {96 neg = -197 *b, err = r.ReadByte()98 if err != nil {99 return 0, fmt.Errorf("cannot read int: %v", err)100 }101 }102 for err == nil {103 if *b < '0' || *b > '9' {104 return 0, fmt.Errorf("cannot read int: %q is not a digit", *b)105 }106 res = 10*res + int(*b-'0')107 *b, err = r.ReadByte()108 if isSpace(*b) {109 break110 }111 }112 res *= neg113 return res, err114}115116func parseHeader(r *bufio.Reader) (nbVars, nbClauses int, err error) {117 line, err := r.ReadString('\n')118 if err != nil {119 return 0, 0, fmt.Errorf("cannot read header: %v", err)120 }121 fields := strings.Fields(line)122 if len(fields) < 3 {123 return 0, 0, fmt.Errorf("invalid syntax %q in header", line)124 }125 nbVars, err = strconv.Atoi(fields[1])126 if err != nil {127 return 0, 0, fmt.Errorf("nbvars not an int : %q", fields[1])128 }129 nbClauses, err = strconv.Atoi(fields[2])130 if err != nil {131 return 0, 0, fmt.Errorf("nbClauses not an int : '%s'", fields[2])132 }133 return nbVars, nbClauses, nil134}135136// ParseCNF parses a CNF file and returns the corresponding Problem.137func ParseCNF(f io.Reader) (*Problem, error) {138 r := bufio.NewReader(f)139 var (140 nbClauses int141 pb Problem142 )143 b, err := r.ReadByte()144 for err == nil {145 if b == 'c' { // Ignore comment146 b, err = r.ReadByte()147 for err == nil && b != '\n' {148 b, err = r.ReadByte()149 }150 } else if b == 'p' { // Parse header151 pb.NbVars, nbClauses, err = parseHeader(r)152 if err != nil {153 return nil, fmt.Errorf("cannot parse CNF header: %v", err)154 }155 pb.Model = make([]decLevel, pb.NbVars)156 pb.Clauses = make([]*Clause, 0, nbClauses)157 } else {158 lits := make([]Lit, 0, 3) // Make room for some lits to improve performance159 for {160 val, err := readInt(&b, r)161 if err == io.EOF {162 if len(lits) != 0 { // This is not a trailing space at the end...163 pb.Clauses = append(pb.Clauses, NewClause(lits))164 }165 break // When there are only several useless spaces at the end of the file, that is ok166 }167 if err != nil {168 return nil, fmt.Errorf("cannot parse clause: %v", err)169 }170 if val == 0 {171 pb.Clauses = append(pb.Clauses, NewClause(lits))172 break173 } else {174 if val > pb.NbVars || -val > pb.NbVars {175 return nil, fmt.Errorf("invalid literal %d for problem with %d vars only", val, pb.NbVars)176 }177 lits = append(lits, IntToLit(int32(val)))178 }179 }180 }181 b, err = r.ReadByte()182 }183 if err != io.EOF {184 return nil, err185 }186 pb.simplify2()187 return &pb, nil188}