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