/* Copyright (C) 1993 by Fred Annexstein, John Franco, Humberto
   Ortiz-Zuazaga, Manian Swaminathan

   This program is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2 of the License, or (at
   your option) any later version.

   This program is distributed in the hope that it will be useful, but
   WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program; if not, write to the Free Software
   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. */
#ifndef CNF_H
#define CNF_H

enum {FAILURE, SUCCESS};
typedef enum {FALSE, TRUE, UNKNOWN} boolean;

typedef struct literalnode {
  boolean negated;
  struct variablenode *var_ptr;
  struct literalnode *next;
} LiteralNode;
typedef struct clausenode {
  int ID;
  int lit_cnt;
  int sat_count; /* count of ``redundant'' literals */
  boolean satisfied;
  struct literalnode *lit_head;
  struct literalnode *unlinked_literal_head;
} ClauseNode;
typedef struct clauselist {
    struct clausenode *clause_ptr;
    struct clauselist *next;
} ClauseList;
typedef struct variablenode {
  boolean value;
  struct clauselist *pos_head;
  struct clauselist *neg_head;
  struct clauselist *unit_head;
  struct clauselist *satisfied_clauselist;
  struct clauselist *unlinked_clauselist_nodes;
  struct weightnode *weight_ptr;
} VariableNode;

typedef struct variabletable {
  int size;
  struct variablenode *table;
} VariableTable;
typedef struct clausetable {
  int size;
  struct clausenode **table;   /* pointer to an array of clausenode pointers */
} ClauseTable;
typedef struct cnf {
  size_t clause_cnt;
  size_t var_cnt;
  size_t longest_clause;
  size_t number_literals;
  VariableTable *var_table;
  ClauseTable *clause_table;
} CNFInstance;

void DeleteClauseTable (ClauseTable *clause_table_p);

void DeleteCNFInstance (CNFInstance *instance);

CNFInstance *
BuildInstance (FILE *cnffile);

void WriteInstance (FILE *outfile, CNFInstance *instance);

void FreeCnf (void);

boolean TestInstance (CNFInstance *instance);

boolean TestClause (CNFInstance *instance, long *clause_offset);


#endif /* CNF_H */
