-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathsolver.c
More file actions
48 lines (41 loc) · 884 Bytes
/
solver.c
File metadata and controls
48 lines (41 loc) · 884 Bytes
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
#include <stdio.h>
#include <stdarg.h>
#include "solver.h"
/*
* Input: Variable list of integer arguments (0-terminated)
*/
void add_clause(solver *s, ...) {
va_list vargs;
int curr;
va_start(vargs, s);
while ((curr=va_arg(vargs, int))!=0)
s->add(curr);
va_end(vargs);
s->add(0);
}
/*
* Input: Literal
*
* Mock function: Uppon adding literals, simply print them. Output is space
* separated, end of clause (=0) starts a new line.
*/
void print_add(int lit) {
printf("%d%s", lit, lit==0 ? "\n" : " ");
}
/*
* Input: Literal
*
* Mock function, always return UNKNOWN
*/
sat_state print_sat(void) {
return ST_UNKNOWN;
}
/*
* Input: Array of assumed literals
*
* Mock function, always return UNKNOWN
*/
sat_state print_sat_assum(int *assumptions, int length) {
printf("#assumptions: %d (%p)\n", length, assumptions);
return ST_UNKNOWN;
}