COPYING file for distribution
[anf2cnf:anf2cnf.git] / SATsolve.c
1 /* Copyright (C) 2010, 2011 Luk Bettale
2
3    This program is free software: you can redistribute it and/or
4    modify it under the terms of the GNU General Public License as
5    published by the Free Software Foundation, either version 3 of the
6    License, or (at your option) any later version.
7
8    This program is distributed in the hope that it will be useful, but
9    WITHOUT ANY WARRANTY; without even the implied warranty of
10    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
11    General Public License for more details.
12
13    You should have received a copy of the GNU General Public License
14    along with this program. If not, see <http://www.gnu.org/licenses/>. */
15
16 #include <stdlib.h>
17 #include <stdio.h>
18 #include <string.h>
19 #include <stdbool.h>
20 #include <sys/wait.h>
21 #include "libanf2cnf.h"
22 #include "chrono.h"
23
24 int
25 main (int argc, char *argv[])
26 {
27   FILE *stream;
28   int err;
29   ANF_system *syst;
30   if (argc <= 1)
31     {
32       fprintf (stderr, "%s: Filename needed\n", argv[0]);
33       return 1;
34     }
35   stream = fopen (argv[argc - 1], "r");
36   if (!stream)
37     {
38       char str[1024] = "";
39       strcat (str, argv[0]);
40       strcat (str, ": ");
41       strcat (str, argv[argc - 1]);
42       perror (str);
43       return 2;
44     }
45   syst = malloc (sizeof *syst);
46   err = ANF_parse (syst, stream);
47   fclose (stream);
48   if (err)
49     {
50       ANF_free (syst);
51       if (err < 0)
52         fprintf (stderr, "%s: Variable should start from 1\n", argv[0]);
53       else
54         fprintf (stderr, "%s: Bad format (line %d)\n", argv[0], err);
55       return 4;
56     }
57   /* insert code here */
58   {
59     int sat;
60     ANF_system *clone;
61     FILE *cnf_file, *sol_file;
62     CNF_system *cnf_syst;
63     int *cnf_sol;
64     char cryptominisat[128] = "";
65
66     char cnf_file_name[] = "/tmp/cnf.XXXXXX";
67     char sol_file_name[] = "/tmp/sol.XXXXXX";
68
69     /* create temporary file names */
70     if (mkstemp (cnf_file_name) < 0)
71       {
72         char str[1024] = "";
73         strcat (str, argv[0]);
74         strcat (str, ": ");
75         strcat (str, cnf_file_name);
76         perror (str);
77         ANF_free (syst);
78         return 8;
79       }
80     if (mkstemp (sol_file_name) < 0)
81       {
82         char str[1024] = "";
83         strcat (str, argv[0]);
84         strcat (str, ": ");
85         strcat (str, sol_file_name);
86         perror (str);
87         remove (cnf_file_name);
88         ANF_free (syst);
89         return 8;
90       }
91
92     /* clone the original system for further checking */
93     clone = malloc (sizeof *clone);
94     ANF_clone (syst, clone);
95
96     /* propagation */
97     measure (ANF_propagate (syst), "propagate");
98
99     /* converts anf to cnf */
100     cnf_syst = malloc (sizeof *cnf_syst);
101     measure (anf2cnf (syst, cnf_syst), "anf2cnf");
102
103     /* print cnf into a file */
104     cnf_file = fopen (cnf_file_name, "r+");
105     CNF_fprint (cnf_file, cnf_syst);
106     fclose (cnf_file);
107
108     /* prepare the cryptominisat command */
109     strcat (cryptominisat, "cryptominisat ");
110     for (unsigned int i = 1; i < argc - 1; i++)
111       {
112         strcat (cryptominisat, argv[i]);
113         strcat (cryptominisat, " ");
114       }
115     strcat (cryptominisat, cnf_file_name);
116     strcat (cryptominisat, " ");
117     strcat (cryptominisat, sol_file_name);
118
119     /* run cryptominisat */
120 #ifdef DEBUG
121     fprintf (stderr, "%s\n", cryptominisat);
122 #endif
123     err = system (cryptominisat);
124     if (WEXITSTATUS (err) == 127 || WEXITSTATUS (err) == 1)
125       {
126         remove (cnf_file_name);
127         remove (sol_file_name);
128         ANF_free (syst);
129         CNF_free (cnf_syst);
130         return 127;
131       }
132
133     /* parse the output of cryptominisat */
134     cnf_sol = calloc (cnf_syst->rank + 1, sizeof *cnf_sol);
135     sol_file = fopen (sol_file_name, "r");
136     sat = solution_parse (sol_file, cnf_sol);
137     fclose (sol_file);
138
139     /* clean the temporary files */
140     remove (cnf_file_name);
141     remove (sol_file_name);
142
143     if (sat < 0)
144       {
145         ANF_free (syst);
146         CNF_free (cnf_syst);
147         printf ("[]\n");
148         return 0;
149       }
150
151     /* replace variables */
152     for (unsigned int i = 0; cnf_sol[i] >= 0; i++)
153       {
154         if (cnf_syst->map[i].degree == 1)
155           {
156             variable v = cnf_syst->map[i].variables[0];
157             if (syst->x[v - 1] == v)
158               syst->x[v - 1] = cnf_sol[i] - 1;
159           }
160       }
161     free (cnf_sol);
162     CNF_free (cnf_syst);
163
164     /* evaluate the anf system with newly found variables */
165     ANF_clean (syst);
166     ANF_evaluate (syst);
167
168     /* update the variables of clone to check the solution */
169     for (unsigned int i = 0; i < syst->rank; i++)
170       clone->x[i] = syst->x[i];
171     ANF_evaluate (clone);
172
173     /* check that the solution is a good one */
174     {
175       bool check = true;
176       for (unsigned int i = 0; i < clone->size; i++)
177         check = check && (clone->polynomials[i].length != 1);
178       ANF_free (clone);
179       if (!check)
180         {
181           fprintf (stderr, "Very bad: should not happen\n");
182           ANF_free (syst);
183           return 127;
184         }
185       printf ("[\n    ");
186       ANF_fprint_x (stdout, syst);
187       printf ("]\n");
188     }
189   }
190   /* end */
191   ANF_free (syst);
192   return 0;
193 }