gnu99 to c99 (not compiler dependent) produces a warning for mkstemp
[anf2cnf:anf2cnf.git] / libanf2cnf.h
1 /* Copyright (C) 2010, 2011 Luk Bettale
2    Time-stamp: <2011-05-27 08:37:09 Luk Bettale>
3
4    This program is free software: you can redistribute it and/or
5    modify it under the terms of the GNU General Public License as
6    published by the Free Software Foundation, either version 3 of the
7    License, or (at your option) any later version.
8
9    This program is distributed in the hope that it will be useful, but
10    WITHOUT ANY WARRANTY; without even the implied warranty of
11    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
12    General Public License for more details.
13
14    You should have received a copy of the GNU General Public License
15    along with this program. If not, see
16    <http://www.gnu.org/licenses/>. */
17
18 #ifndef LIBANF2CNF_H
19 #define LIBANF2CNF_H
20
21 #include <stdbool.h>
22
23 typedef int variable;
24 typedef int literal;
25
26 typedef struct
27 {
28   int degree;
29   variable *variables;
30 } monomial;
31
32 typedef struct
33 {
34   int k;
35   literal *literals;
36 } clause;
37
38 typedef struct
39 {
40   int length;
41   monomial *monomials;
42 } polynomial;
43
44 typedef struct
45 {
46   int rank;
47   int size;
48   variable *x;
49   polynomial *polynomials;
50 } ANF_system;
51
52 typedef struct
53 {
54   int rank;
55   int andsize;
56   int xorsize;
57   clause *clauses;
58   clause *xorclauses;
59   monomial *map;
60 } CNF_system;
61
62 extern void ANF_free (ANF_system *syst);
63 extern void CNF_free (CNF_system *syst);
64
65 extern void ANF_fprint (FILE *stream, const ANF_system *syst);
66 extern void ANF_fprint_syst (FILE *stream, const ANF_system *syst);
67 extern void ANF_fprint_x (FILE *stream, const ANF_system *syst);
68 extern void ANF_verbose_fprint (FILE *stream, const ANF_system *syst);
69 extern void CNF_fprint (FILE *stream, const CNF_system *syst);
70 extern void CNF_fprint_syst (FILE *stream, const CNF_system *syst);
71 extern void CNF_fprint_map (FILE *stream, const CNF_system *syst);
72
73 extern int ANF_parse (ANF_system *syst, FILE *stream);
74 extern void ANF_clone (const ANF_system *src, ANF_system *dest);
75 extern void ANF_clean (ANF_system *syst);
76 extern void ANF_evaluate (ANF_system *syst);
77 extern void ANF_propagate (ANF_system *syst);
78 extern void ANF_remap (ANF_system *syst);
79 extern void CNF_xorcut (CNF_system *syst, int k);
80
81 extern void anf2cnf (const ANF_system *anf_syst, CNF_system *cnf_syst);
82 extern int solution_parse (FILE *stream, int *tab);
83 extern int learnts_parse (FILE *stream, ANF_system *anf_syst, CNF_system *cnf_syst);
84
85 /* Helper functions */
86 extern int ANF_num_unknowns(const ANF_system* syst);
87 extern bool ANF_var_is_unknown(const ANF_system* syst, int v);
88 extern int ANF_get_rank(const ANF_system* syst);
89 extern void ANF_set_var(ANF_system* syst, int var, int val);
90 extern bool ANF_is_UNSAT(const ANF_system* syst);
91
92 #endif  /* LIBANF2CNF_H */