ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cadicalTest.c
Go to the documentation of this file.
1
20
21#include "cadicalSolver.h"
22
23ABC_NAMESPACE_IMPL_START
24
28
32void cadical_solver_test() {
33 int RetValue;
34 int Lits[3];
35 // test 1
36 {
37 cadical_solver *pSat = cadical_solver_new();
38 int a = cadical_solver_addvar(pSat);
39 int b = cadical_solver_addvar(pSat);
40 int c = cadical_solver_addvar(pSat);
41 assert(cadical_solver_nvars(pSat) == 3);
42 Lits[0] = Abc_Var2Lit(a, 0);
43 Lits[1] = Abc_Var2Lit(b, 0);
44 Lits[2] = Abc_Var2Lit(c, 0);
45 printf("adding (a, b, c)\n");
46 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 3);
47 assert(RetValue);
48 Lits[0] = Abc_Var2Lit(a, 0);
49 Lits[1] = Abc_Var2Lit(b, 1);
50 printf("adding (a, !b)\n");
51 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 2);
52 assert(RetValue);
53 Lits[0] = Abc_Var2Lit(a, 1);
54 printf("adding (!a)\n");
55 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
56 assert(RetValue);
57 RetValue = cadical_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
58 printf("solved: %d\n", RetValue);
59 assert(RetValue == 1);
60 int a_val = cadical_solver_get_var_value(pSat, a);
61 int b_val = cadical_solver_get_var_value(pSat, b);
62 int c_val = cadical_solver_get_var_value(pSat, c);
63 printf("a = %d, b = %d, c = %d\n", a_val, b_val, c_val);
64 assert(a_val == 0);
65 assert(b_val == 0);
66 assert(c_val == 1);
67 cadical_solver_delete(pSat);
68 printf("test 1 passed\n");
69 }
70 // test 2
71 {
72 cadical_solver *pSat = cadical_solver_new();
73 cadical_solver_setnvars(pSat, 2);
74 assert(cadical_solver_nvars(pSat) == 2);
75 Lits[0] = Abc_Var2Lit(0, 0);
76 Lits[1] = Abc_Var2Lit(1, 0);
77 printf("adding (x0, x1)\n");
78 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 2);
79 assert(RetValue);
80 Lits[0] = Abc_Var2Lit(0, 0);
81 Lits[1] = Abc_Var2Lit(1, 1);
82 printf("adding (x0, !x1)\n");
83 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 2);
84 assert(RetValue);
85 Lits[0] = Abc_Var2Lit(0, 1);
86 Lits[1] = Abc_Var2Lit(1, 1);
87 printf("adding (!x0, !x1)\n");
88 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 2);
89 assert(RetValue);
90 RetValue = cadical_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
91 printf("solved: %d\n", RetValue);
92 assert(RetValue == 1);
93 printf("x0 = %d, x1 = %d\n", cadical_solver_get_var_value(pSat, 0), cadical_solver_get_var_value(pSat, 1));
94 assert(cadical_solver_get_var_value(pSat, 0) == 1);
95 assert(cadical_solver_get_var_value(pSat, 1) == 0);
96 cadical_solver_delete(pSat);
97 printf("test 2 passed\n");
98 }
99 // test 3
100 {
101 cadical_solver *pSat = cadical_solver_new();
102 cadical_solver_setnvars(pSat, 3);
103 assert(cadical_solver_nvars(pSat) == 3);
104 Lits[0] = Abc_Var2Lit(0, 1);
105 Lits[1] = Abc_Var2Lit(1, 0);
106 Lits[2] = Abc_Var2Lit(2, 1);
107 printf("adding (!x0, x1, !x2)\n");
108 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 3);
109 assert(RetValue);
110 Lits[0] = Abc_Var2Lit(0, 0);
111 printf("adding (x0)\n");
112 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
113 assert(RetValue);
114 Lits[0] = Abc_Var2Lit(1, 1);
115 printf("adding (!x1)\n");
116 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
117 assert(RetValue);
118 Lits[0] = Abc_Var2Lit(2, 0);
119 printf("adding (x2)\n");
120 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
121 RetValue = cadical_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
122 printf("solved: %d\n", RetValue);
123 assert(RetValue == -1);
124 cadical_solver_delete(pSat);
125 printf("test 3 passed\n");
126 }
127 // test 4
128 {
129 cadical_solver *pSat = cadical_solver_new();
130 cadical_solver_setnvars(pSat, 3);
131 assert(cadical_solver_nvars(pSat) == 3);
132 Lits[0] = Abc_Var2Lit(0, 1);
133 Lits[1] = Abc_Var2Lit(1, 0);
134 Lits[2] = Abc_Var2Lit(2, 1);
135 printf("adding (!x0, x1, !x2)\n");
136 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 3);
137 assert(RetValue);
138 Lits[0] = Abc_Var2Lit(0, 0);
139 printf("adding (x0)\n");
140 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
141 assert(RetValue);
142 Lits[0] = Abc_Var2Lit(1, 1);
143 printf("assume (!x1)\n");
144 RetValue = cadical_solver_solve(pSat, Lits, Lits + 1, 0, 0, 0, 0);
145 printf("solved: %d\n", RetValue);
146 assert(RetValue == 1);
147 printf("x0 = %d, x1 = %d, x2 = %d\n", cadical_solver_get_var_value(pSat, 0), cadical_solver_get_var_value(pSat, 1), cadical_solver_get_var_value(pSat, 2));
148 assert(cadical_solver_get_var_value(pSat, 0) == 1);
149 assert(cadical_solver_get_var_value(pSat, 1) == 0);
150 assert(cadical_solver_get_var_value(pSat, 2) == 0);
151 cadical_solver_delete(pSat);
152 printf("test 4 passed\n");
153 }
154 // test 5
155 {
156 cadical_solver *pSat = cadical_solver_new();
157 cadical_solver_setnvars(pSat, 3);
158 assert(cadical_solver_nvars(pSat) == 3);
159 Lits[0] = Abc_Var2Lit(0, 1);
160 Lits[1] = Abc_Var2Lit(1, 0);
161 Lits[2] = Abc_Var2Lit(2, 1);
162 printf("adding (!x0, x1, !x2)\n");
163 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 3);
164 assert(RetValue);
165 Lits[0] = Abc_Var2Lit(0, 1);
166 Lits[1] = Abc_Var2Lit(1, 1);
167 Lits[2] = Abc_Var2Lit(2, 1);
168 printf("adding (!x0, !x1, !x2)\n");
169 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 3);
170 assert(RetValue);
171 Lits[0] = Abc_Var2Lit(0, 0);
172 printf("adding (x0)\n");
173 RetValue = cadical_solver_addclause(pSat, Lits, Lits + 1);
174 assert(RetValue);
175 Lits[0] = Abc_Var2Lit(1, 0);
176 Lits[1] = Abc_Var2Lit(2, 0);
177 printf("assume (x1, x2)\n");
178 RetValue = cadical_solver_solve(pSat, Lits, Lits + 2, 0, 0, 0, 0);
179 printf("solved: %d\n", RetValue);
180 assert(RetValue == -1);
181 int *pCore;
182 int nSize = cadical_solver_final(pSat, &pCore);
183 printf("core: ");
184 for(int i = 0; i < nSize; i++) {
185 if(i) {
186 printf(", ");
187 }
188 if(Abc_LitIsCompl(pCore[i])) {
189 printf("!");
190 }
191 printf("x%d", Abc_Lit2Var(pCore[i]));
192 }
193 printf("\n");
194 int neg_x2_in_core = 0;
195 for(int i = 0; i < nSize; i++) {
196 if(Abc_LitIsCompl(pCore[i]) && Abc_Lit2Var(pCore[i]) == 2) {
197 neg_x2_in_core = 1;
198 }
199 }
200 assert(neg_x2_in_core);
201 cadical_solver_delete(pSat);
202 printf("test 5 passed\n");
203 }
204}
205
209
210ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
cadical_solver_final
int cadical_solver_final(cadical_solver *s, int **ppArray)
Definition cadicalSolver.c:170
cadical_solver_addclause
int cadical_solver_addclause(cadical_solver *s, int *begin, int *end)
Definition cadicalSolver.c:90
cadical_solver_get_var_value
int cadical_solver_get_var_value(cadical_solver *s, int v)
Definition cadicalSolver.c:250
cadical_solver_nvars
int cadical_solver_nvars(cadical_solver *s)
Definition cadicalSolver.c:203
cadical_solver_setnvars
void cadical_solver_setnvars(cadical_solver *s, int n)
Definition cadicalSolver.c:233
cadical_solver_addvar
int cadical_solver_addvar(cadical_solver *s)
Definition cadicalSolver.c:218
cadical_solver_solve
int cadical_solver_solve(cadical_solver *s, int *begin, int *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition cadicalSolver.c:113
cadical_solver_new
ABC_NAMESPACE_IMPL_START cadical_solver * cadical_solver_new(void)
DECLARATIONS ///.
Definition cadicalSolver.c:45
cadical_solver_delete
void cadical_solver_delete(cadical_solver *s)
Definition cadicalSolver.c:65
cadical_solver
typedefABC_NAMESPACE_HEADER_START struct cadical_solver_ cadical_solver
INCLUDES ///.
Definition cadicalSolver.h:41
cadical_solver_test
ABC_NAMESPACE_IMPL_START void cadical_solver_test()
DECLARATIONS ///.
Definition cadicalTest.c:32
assert
#define assert(ex)
Definition util_old.h:213