133 lines
2.8 KiB
C++
133 lines
2.8 KiB
C++
|
|
#include <errno.h>
|
|
#include <string.h>
|
|
|
|
#include <parse.hpp>
|
|
#include <problem.hpp>
|
|
#include <list.hpp>
|
|
#include <refcounted.hpp>
|
|
#include <print.hpp>
|
|
|
|
refcounted<list<refcounted<problem>>> parse(const char* path)
|
|
{
|
|
refcounted<list<refcounted<problem>>> problems = new list<refcounted<problem>>();
|
|
|
|
FILE* stream = fopen(path, "r");
|
|
|
|
if (!stream)
|
|
{
|
|
printf("sat-solver: fopen(): %m\n");
|
|
exit(1);
|
|
}
|
|
|
|
char *line = NULL;
|
|
size_t len = 0;
|
|
ssize_t nread;
|
|
|
|
while ((nread = getline(&line, &len, stream)) > 0)
|
|
{
|
|
line[--nread] = 0;
|
|
|
|
// println("line = ", line);
|
|
|
|
if (line[0] == '\0') continue;
|
|
if (line[0] == 'c') continue;
|
|
|
|
// why do the satlib tests have the percent symbol at the end of the
|
|
// file?
|
|
if (line[0] == '%') break;
|
|
|
|
if (line[0] != 'p')
|
|
{
|
|
assert(!"TODO");
|
|
exit(1);
|
|
}
|
|
|
|
unsigned number_of_variables;
|
|
unsigned number_of_clauses;
|
|
|
|
int r = sscanf(line, " p cnf %u %u ", &number_of_variables, &number_of_clauses);
|
|
|
|
if (r < 2)
|
|
{
|
|
puts("syntax error");
|
|
exit(1);
|
|
}
|
|
|
|
refcounted<problem> p = new problem(number_of_variables);
|
|
|
|
for (unsigned i = 0; i < number_of_clauses; i++)
|
|
{
|
|
nread = getline(&line, &len, stream);
|
|
|
|
if (nread < 0)
|
|
{
|
|
puts("syntax error");
|
|
exit(1);
|
|
}
|
|
|
|
line[--nread] = 0;
|
|
|
|
// println("clause line = ", line);
|
|
|
|
refcounted<clause> c = new clause();
|
|
|
|
char *moving = line;
|
|
|
|
for (char* word; (word = strtok_r(NULL, " ", &moving)); )
|
|
{
|
|
errno = 0;
|
|
|
|
char* m;
|
|
|
|
signed variable = strtol(word, &m, 10);
|
|
|
|
if (errno || *m)
|
|
{
|
|
puts("syntax error");
|
|
exit(1);
|
|
}
|
|
|
|
if (variable == 0)
|
|
{
|
|
continue;
|
|
}
|
|
|
|
bool value = true;
|
|
|
|
if (variable < 0)
|
|
{
|
|
variable = -variable;
|
|
value = !value;
|
|
}
|
|
|
|
assert(variable > 0);
|
|
|
|
c->bundles.append(
|
|
(clause::bundle) {(unsigned) variable, value});
|
|
}
|
|
|
|
p->clauses.append(c);
|
|
}
|
|
|
|
problems->append(p);
|
|
}
|
|
|
|
free(line);
|
|
|
|
fclose(stream);
|
|
|
|
return problems;
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|