cnf_reader.c File Reference

#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"

Include dependency graph for cnf_reader.c:

Go to the source code of this file.

Functions
int	satoko_parse_dimacs (char *fname, satoko_t **solver)

Function Documentation

satoko_parse_dimacs()

int satoko_parse_dimacs	(	char *	fname,
		satoko_t **	solver )

Start the solver and reads the DIMAC file.

Returns false upon immediate conflict.

Definition at line 108 of file cnf_reader.c.

{
    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;
}

Here is the call graph for this function: