Вы можете перебрать строки: если строка начинается с c или пуста: отменить ее.Если оно начинается с p: проанализируйте определение проблемы.Если он начинается с числа: переключитесь в режим предложения и выполните синтаксический анализ предложений без учета конца строки.Стандартная библиотека C хорошо это облегчает.
Теперь это C, а C действительно не имеет хорошей поддержки для любых сложных структур данных.Реализация структур данных требует большой осторожности!Мы начнем с реализации «простого» типа Clause динамического размера: то, что в C ++ будет решаться с помощью std::vector<ClauseLiteral>.Нам нужно уделять много внимания обработке ошибок - иначе поведение программы будет неопределенным, и мы этого вообще не хотим.Мы заранее улавливаем любые арифметические переполнения!
#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
typedef int ClauseLiteral;
static const int ClauseLiteralMax = INT_MAX;
typedef struct Clause {
size_t size;
size_t capacity; // does not include the terminating zero
ClauseLiteral literals[1];
};
// Maximum capacity that doesn't overflow SIZE_MAX
static inline size_t Clause_max_capacity(void) {
return (SIZE_MAX-sizeof(Clause))/sizeof(ClauseLiteral);
}
static size_t Clause_size_for_(size_t const count_of_literals) {
assert(count_of_literals);
if (count_of_literals > Clause_max_capacity()) return 0;
return sizeof(Clause) + count_of_literals*sizeof(ClauseLiteral);
}
static size_t Clause_next_capacity_(size_t const capacity) {
assert(capacity);
const size_t growth_factor = 2;
if (capacity > Clause_max_capacity()/growth_factor) {
if (capacity < Clause_max_capacity()) return Clause_max_capacity();
return 0;
}
return capacity * growth_factor;
}
static Clause *new_Clause_impl_(size_t const capacity) {
size_t const alloc_size = Clause_size_for_(capacity);
assert(alloc_size);
Clause *const clause = calloc(alloc_size); // is zero-terminated
if (!clause) return NULL;
clause->size = 0;
clause->capacity = capacity;
return clause;
}
Clause *new_Clause(void) { return new_Clause_impl_(4); }
void free_Clause(Clause *clause) { free(clause); }
/** Assures that the clause exists and has room for at least by items */
bool Clause_grow(Clause **const clause_ptr, size_t by) {
assert(clause_ptr);
if (!*clause_ptr) return (*clause_ptr = new_Clause_impl_(by));
Clause *const clause = *clause_ptr;
assert(clause->size <= clause->capacity);
if (clause->size > (SIZE_MAX - by)) return false; // overflow
if (by > Clause_max_capacity()) return false; // won't fit
if (clause->size > (Clause_max_capacity() - by)) return false; // won't fit
size_t const new_size = clause->size + by;
assert(new_size <= Clause_max_capacity());
if (new_size > clause->capacity) {
size_t new_capacity = clause->capacity;
while (new_capacity && new_capacity < new_size)
new_capacity = Clause_next_capacity_(new_capacity);
if (!new_capacity) return false;
Clause *const new_clause = realloc(clause, Clause_size_for_(new_capacity));
if (!new_clause) return false;
*clause_ptr = new_clause;
}
*clause_ptr->literals[new_size] = 0; // zero-terminate
return true;
}
bool Clause_push_back(Clause **clause_ptr, ClauseLiteral literal) {
assert(clause_ptr);
assert(literal); // zero literals are not allowed within a clause
if (!Clause_grow(clause_ptr, 1)) return false;
(*clause_ptr)->literals[(*clause_ptr)->size++] = literal;
return true;
}
Теперь у нас есть возможность увеличивать предложения по мере их чтения.Итак, давайте прочитаем!
#include <stdio.h>
typedef struct CNF {
size_t variable_count;
size_t clause_count;
Clause *clauses[1];
};
static inline size_t CNF_max_clause_count() {
return (SIZE_MAX-sizeof(CNF))/sizeof(Clause*);
}
static size_t CNF_size_for_(size_t const clause_count) {
if (clause_count >= CNF_max_clause_count()) return 0;
return sizeof(CNF) + clause_count * sizeof(Clause*);
}
static CNF *new_CNF(size_t variable_count, size_t clause_count) {
assert(variable_count <= ClauseLiteralMax);
size_t const cnf_size = CNF_size_fir(clause_count);
CNF *cnf = calloc(cnf_size);
if (!cnf) return NULL;
cnf->variable_count = variable_count;
cnf->clause_count = clause_count;
return cnf;
}
static void free_CNF(CNF *const cnf) {
if (!cnf) return;
for (Clause **clause_ptr = &cnf->clauses[0]; *clause_ptr && clause+ptr < &cnf->clauses[clause_count]; clause_ptr++)
free_Clause(*clause_ptr);
free(cnf);
}
static CNF *read_p_line(FILE *file) {
assert(file);
size_t variable_count, clause_count;
int match_count = fscanf(file, "p cnf %zd %zd", &variable_count, &clause_count);
if (match_count != 2) return NULL;
if (variable_count > ClauseLiteralMax) return NULL;
return new_CNF(variable_count, clause_count);
}
static bool read_c_line(FILE *file) {
assert(file);
char c = fgetc(file);
if (c != 'c') return false;
while ((c = fgetc(file)) != EOF)
if (c == '\n') return true;
return false;
}
static bool read_clauses(FILE *file, CNF *cnf) {
assert(file);
if (!cnf) return false;
size_t const variable_count = cnf->variable_count;
for (Clause **clause_ptr = &cnf->clauses[0]; clause_ptr < &cnf->clauses[clause_count];) {
int literal;
int match_count = fscanf(file, "%d", &literal);
if (match_count != 1) return false;
if (literal == 0) {
if (!*clause_ptr) return false; // We disallow empty clauses.
clause_ptr++;
}
else if (literal >= -variable_count && literal <= variable_count) {
if (!Clause_push_back(clause_ptr, literal)) return false;
}
else return false;
}
return true;
}
CNF *read_CNF(FILE *file) {
assert(file);
CNF *cnf = NULL;
for (;;) {
char const c = fgetc(file);
if (c == EOF) goto error;
if (isspace(c)) continue; // skip leading whitespace
if (ungetc(c, file) == EOF) goto error;
if (c == 'p' && !(cnf = read_p_line(file))) goto error;
else if (c == 'c' && !read_c_line(file)) goto error;
else if (isdigit(c)) break;
goto error;
}
if (!read_clauses(file, cnf)) goto error;
return cnf;
error:
free_CNF(cnf);
return NULL;
}
Как видите, код далеко не тривиален, потому что это библиотечный код, который должен быть устойчивым и вообще не иметь неопределенного поведения.«Простые» вещи могут быть довольно сложными в C. Поэтому, надеюсь, вы предпочтете эту работу в C ++, если сможете.