-
Notifications
You must be signed in to change notification settings - Fork 0
/
input.c
106 lines (90 loc) · 2.21 KB
/
input.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
//main
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <sys/types.h>
#include <sys/wait.h>
#include <sys/stat.h>
#include <fcntl.h>
#define STDOUT 1
extern char **__environ;
void itoa (int n,char s[])
{
int i,j;
i=0;
do{
s[i++]=n%10+'0';//取下一个数字
}
while ((n/=10)>0);//删除该数字
s[i]='\0';
for(j=i-1;j>=i/2;j--)//生成的数字是逆序的,所以要逆序输出
{
int temp = s[j] ;
s[j] = s[i-1-j] ;
s[i-1-j] = temp ;
}
}
int main(int argc, char** argv)
{
int n = atoi(argv[1]) ;
int mode = 1 ;
int index = atoi(argv[2]) ;
printf("mode: %d\n", mode) ;
int i , j = 0 ;
FILE * fp = fopen("record.txt", "w");
char r[100] = "./random " ;
strcat(r, argv[1]) ;
strcat(r, " ") ;
strcat(r, "1") ;
system(r) ; // random, make input
int st = time(NULL) ;
for( i = 1 ; i <= n ; i ++ )
{
char s[100] = "cp -f test/" ;
char num[10] ;
itoa(i, num) ;
strcat(s, num) ;
char t[100] = ".cnf sample.cnf" ;
strcat(s, t) ;
system(s) ; // prepare for input
printf("%s\n", s) ;
if( mode == 0 ){ // run SAT solver
printf("l...") ;
system("./lingeling/lingeling sample.cnf > result.txt") ;
system("./readl < lingeling/result.txt") ;
j ++ ;
}
printf("g...") ;
system("cd glucose/core && ./glucose ../../sample.cnf >result.txt") ; // run
system("./readg < glucose/core/result.txt") ; // read result
j ++ ;
printf("m...") ;
system("cd minisat && minisat ../sample.cnf > result.txt") ;
system("./readm < minisat/result.txt") ;
j ++ ;
printf("c...") ;
system("cd cryptominisat && ./cryptominisat ../sample.cnf > result.txt") ;
//printf("c finished\n") ;
system("./readc < cryptominisat/result.txt") ;
j ++ ;
int et = time(NULL) ;
printf("phase time: %d\n", et-st ) ;
if( mode == 0 ){
printf("r...") ;
system("cd rsat && ./rsat ../sample.cnf > result.txt") ;
j ++ ;
}
printf("\n") ;
}
int et = time(NULL) ;
printf("phase time: %d\n", et-st ) ;
char s[100] = "./count ", num[10], space[3] = " " ;
itoa(j, num) ;
strcat(s, num) ;
strcat(s, space) ;
itoa(index, num) ;
strcat(s, num) ;
system(s) ; // add up time
return 0 ;
}