ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kissatTest.c
Go to the documentation of this file.
1
20
21#include "kissatSolver.h"
22
23ABC_NAMESPACE_IMPL_START
24
28
32void kissat_solver_test() {
33 int RetValue;
34 int Lits[3];
35 // test 1
36 {
37 kissat_solver *pSat = kissat_solver_new();
38 int a = kissat_solver_addvar(pSat);
39 int b = kissat_solver_addvar(pSat);
40 int c = kissat_solver_addvar(pSat);
41 assert(kissat_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 = kissat_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 = kissat_solver_addclause(pSat, Lits, Lits + 2);
52 assert(RetValue);
53 Lits[0] = Abc_Var2Lit(a, 1);
54 printf("adding (!a)\n");
55 RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
56 assert(RetValue);
57 RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
58 printf("solved: %d\n", RetValue);
59 assert(RetValue == 1);
60 int a_val = kissat_solver_get_var_value(pSat, a);
61 int b_val = kissat_solver_get_var_value(pSat, b);
62 int c_val = kissat_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 kissat_solver_delete(pSat);
68 printf("test 1 passed\n");
69 }
70 // test 2
71 {
72 kissat_solver *pSat = kissat_solver_new();
73 kissat_solver_setnvars(pSat, 2);
74 assert(kissat_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 = kissat_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 = kissat_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 = kissat_solver_addclause(pSat, Lits, Lits + 2);
89 assert(RetValue);
90 RetValue = kissat_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", kissat_solver_get_var_value(pSat, 0), kissat_solver_get_var_value(pSat, 1));
94 assert(kissat_solver_get_var_value(pSat, 0) == 1);
95 assert(kissat_solver_get_var_value(pSat, 1) == 0);
96 kissat_solver_delete(pSat);
97 printf("test 2 passed\n");
98 }
99 // test 3
100 {
101 kissat_solver *pSat = kissat_solver_new();
102 kissat_solver_setnvars(pSat, 3);
103 assert(kissat_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 = kissat_solver_addclause(pSat, Lits, Lits + 3);
109 assert(RetValue);
110 Lits[0] = Abc_Var2Lit(0, 0);
111 printf("adding (x0)\n");
112 RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
113 assert(RetValue);
114 Lits[0] = Abc_Var2Lit(1, 1);
115 printf("adding (!x1)\n");
116 RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
117 assert(RetValue);
118 Lits[0] = Abc_Var2Lit(2, 0);
119 printf("adding (x2)\n");
120 RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
121 RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
122 printf("solved: %d\n", RetValue);
123 assert(RetValue == -1);
124 kissat_solver_delete(pSat);
125 printf("test 3 passed\n");
126 }
127}
128
132
133ABC_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
kissat_solver_solve
int kissat_solver_solve(kissat_solver *s, int *begin, int *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition kissatSolver.c:105
kissat_solver_addclause
int kissat_solver_addclause(kissat_solver *s, int *begin, int *end)
Definition kissatSolver.c:82
kissat_solver_get_var_value
int kissat_solver_get_var_value(kissat_solver *s, int v)
Definition kissatSolver.c:190
kissat_solver_delete
void kissat_solver_delete(kissat_solver *s)
Definition kissatSolver.c:63
kissat_solver_new
ABC_NAMESPACE_IMPL_START kissat_solver * kissat_solver_new(void)
DECLARATIONS ///.
Definition kissatSolver.c:45
kissat_solver_nvars
int kissat_solver_nvars(kissat_solver *s)
Definition kissatSolver.c:143
kissat_solver_addvar
int kissat_solver_addvar(kissat_solver *s)
Definition kissatSolver.c:158
kissat_solver_setnvars
void kissat_solver_setnvars(kissat_solver *s, int n)
Definition kissatSolver.c:173
kissat_solver
typedefABC_NAMESPACE_HEADER_START struct kissat_solver_ kissat_solver
INCLUDES ///.
Definition kissatSolver.h:41
kissat_solver_test
ABC_NAMESPACE_IMPL_START void kissat_solver_test()
DECLARATIONS ///.
Definition kissatTest.c:32
assert
#define assert(ex)
Definition util_old.h:213