1 //===--- cnf_reader.h -------------------------------------------------------===
2 //
3 // satoko: Satisfiability solver
4 //
5 // This file is distributed under the BSD 2-Clause License.
6 // See LICENSE for details.
7 //
8 //===------------------------------------------------------------------------===
9 #include <assert.h>
10 #include <ctype.h>
11 #include <stdlib.h>
12 #include <stdio.h>
13 #include <string.h>
14
15 #include "satoko.h"
16 #include "solver.h"
17 #include "utils/mem.h"
18 #include "utils/vec/vec_uint.h"
19
20 #include "misc/util/abc_global.h"
21 ABC_NAMESPACE_IMPL_START
22
23 /** Read the file into an internal buffer.
24 *
25 * This function will receive a file name. The return data is a string ended
26 * with '\0'.
27 *
28 */
file_open(const char * fname)29 static char * file_open(const char *fname)
30 {
31 FILE *file = fopen(fname, "rb");
32 char *buffer;
33 int sz_file;
34 int ret;
35
36 if (file == NULL) {
37 printf("Couldn't open file: %s\n", fname);
38 return NULL;
39 }
40 fseek(file, 0, SEEK_END);
41 sz_file = ftell(file);
42 rewind(file);
43 buffer = satoko_alloc(char, sz_file + 3);
44 ret = fread(buffer, sz_file, 1, file);
45 buffer[sz_file + 0] = '\n';
46 buffer[sz_file + 1] = '\0';
47 return buffer;
48 }
49
skip_spaces(char ** pos)50 static void skip_spaces(char **pos)
51 {
52 assert(pos != NULL);
53 for (; isspace(**pos); (*pos)++);
54 }
55
skip_line(char ** pos)56 static void skip_line(char **pos)
57 {
58 assert(pos != NULL);
59 for(; **pos != '\n' && **pos != '\r' && **pos != EOF; (*pos)++);
60 if (**pos != EOF)
61 (*pos)++;
62 return;
63 }
64
read_int(char ** token)65 static int read_int(char **token)
66 {
67 int value = 0;
68 int neg = 0;
69
70 skip_spaces(token);
71 if (**token == '-') {
72 neg = 1;
73 (*token)++;
74 } else if (**token == '+')
75 (*token)++;
76
77 if (!isdigit(**token)) {
78 printf("Parsing error. Unexpected char: %c.\n", **token);
79 exit(EXIT_FAILURE);
80 }
81 while (isdigit(**token)) {
82 value = (value * 10) + (**token - '0');
83 (*token)++;
84 }
85 return neg ? -value : value;
86 }
87
read_clause(char ** token,vec_uint_t * lits)88 static void read_clause(char **token, vec_uint_t *lits)
89 {
90 int var;
91 unsigned sign;
92
93 vec_uint_clear(lits);
94 while (1) {
95 var = read_int(token);
96 if (var == 0)
97 break;
98 sign = (var > 0);
99 var = abs(var) - 1;
100 vec_uint_push_back(lits, var2lit((unsigned) var, (char)!sign));
101 }
102 }
103
104 /** Start the solver and reads the DIMAC file.
105 *
106 * Returns false upon immediate conflict.
107 */
satoko_parse_dimacs(char * fname,satoko_t ** solver)108 int satoko_parse_dimacs(char *fname, satoko_t **solver)
109 {
110 satoko_t *p = NULL;
111 vec_uint_t *lits = NULL;
112 int n_var;
113 int n_clause;
114 char *buffer = file_open(fname);
115 char *token;
116
117 if (buffer == NULL)
118 return -1;
119
120 token = buffer;
121 while (1) {
122 skip_spaces(&token);
123 if (*token == 0)
124 break;
125 else if (*token == 'c')
126 skip_line(&token);
127 else if (*token == 'p') {
128 token++;
129 skip_spaces(&token);
130 for(; !isspace(*token); token++); /* skip 'cnf' */
131
132 n_var = read_int(&token);
133 n_clause = read_int(&token);
134 skip_line(&token);
135 lits = vec_uint_alloc((unsigned) n_var);
136 p = satoko_create();
137 } else {
138 if (lits == NULL) {
139 printf("There is no parameter line.\n");
140 satoko_free(buffer);
141 return -1;
142 }
143 read_clause(&token, lits);
144 if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) {
145 printf("Unable to add clause: ");
146 vec_uint_print(lits);
147 return SATOKO_ERR;
148 }
149 }
150 }
151 vec_uint_free(lits);
152 satoko_free(buffer);
153 *solver = p;
154 return SATOKO_OK;
155 }
156
157 ABC_NAMESPACE_IMPL_END
158