1 /*
2 * ezSAT -- A simple and easy to use CNF generator for SAT solvers
3 *
4 * Copyright (C) 2013 Claire Xenia Wolf <claire@yosyshq.com>
5 *
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
9 *
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17 *
18 */
19
20 #include "ezminisat.h"
21 #include <assert.h>
22
23 #define INIT_X 123456789
24 #define INIT_Y 362436069
25 #define INIT_Z 521288629
26 #define INIT_W 88675123
27
xorshift128()28 uint32_t xorshift128() {
29 static uint32_t x = INIT_X;
30 static uint32_t y = INIT_Y;
31 static uint32_t z = INIT_Z;
32 static uint32_t w = INIT_W;
33 uint32_t t = x ^ (x << 11);
34 x = y; y = z; z = w;
35 w ^= (w >> 19) ^ t ^ (t >> 8);
36 return w;
37 }
38
test_cmp(uint32_t a,uint32_t b)39 void test_cmp(uint32_t a, uint32_t b)
40 {
41 ezMiniSAT sat;
42
43 printf("A = %10u (%10d)\n", a, int32_t(a));
44 printf("B = %10u (%10d)\n", b, int32_t(b));
45 printf("\n");
46
47 std::vector<int> va = sat.vec_var("a", 32);
48 std::vector<int> vb = sat.vec_var("b", 32);
49
50 sat.vec_set_unsigned(va, a);
51 sat.vec_set_unsigned(vb, b);
52
53 #define MONITOR_VARS \
54 X(carry) X(overflow) X(sign) X(zero) \
55 X(lt_signed) X(le_signed) X(ge_signed) X(gt_signed) \
56 X(lt_unsigned) X(le_unsigned) X(ge_unsigned) X(gt_unsigned)
57
58 #define X(_n) int _n; bool _n ## _master;
59 MONITOR_VARS
60 #undef X
61
62 carry_master = ((uint64_t(a) - uint64_t(b)) >> 32) & 1;
63 overflow_master = (int32_t(a) - int32_t(b)) != (int64_t(int32_t(a)) - int64_t(int32_t(b)));
64 sign_master = ((a - b) >> 31) & 1;
65 zero_master = a == b;
66
67 sat.vec_cmp(va, vb, carry, overflow, sign, zero);
68
69 lt_signed_master = int32_t(a) < int32_t(b);
70 le_signed_master = int32_t(a) <= int32_t(b);
71 ge_signed_master = int32_t(a) >= int32_t(b);
72 gt_signed_master = int32_t(a) > int32_t(b);
73
74 lt_unsigned_master = a < b;
75 le_unsigned_master = a <= b;
76 ge_unsigned_master = a >= b;
77 gt_unsigned_master = a > b;
78
79 lt_signed = sat.vec_lt_signed(va, vb);
80 le_signed = sat.vec_le_signed(va, vb);
81 ge_signed = sat.vec_ge_signed(va, vb);
82 gt_signed = sat.vec_gt_signed(va, vb);
83
84 lt_unsigned = sat.vec_lt_unsigned(va, vb);
85 le_unsigned = sat.vec_le_unsigned(va, vb);
86 ge_unsigned = sat.vec_ge_unsigned(va, vb);
87 gt_unsigned = sat.vec_gt_unsigned(va, vb);
88
89 std::vector<int> modelExpressions;
90 std::vector<bool> modelValues, modelMaster;
91 std::vector<std::string> modelNames;
92
93 #define X(_n) modelExpressions.push_back(_n); modelNames.push_back(#_n); modelMaster.push_back(_n ## _master);
94 MONITOR_VARS
95 #undef X
96
97 std::vector<int> add_ab = sat.vec_add(va, vb);
98 std::vector<int> sub_ab = sat.vec_sub(va, vb);
99 std::vector<int> sub_ba = sat.vec_sub(vb, va);
100
101 sat.vec_append(modelExpressions, add_ab);
102 sat.vec_append(modelExpressions, sub_ab);
103 sat.vec_append(modelExpressions, sub_ba);
104
105 if (!sat.solve(modelExpressions, modelValues)) {
106 fprintf(stderr, "SAT solver failed to find a model!\n");
107 abort();
108 }
109
110 bool found_error = false;
111
112 for (size_t i = 0; i < modelMaster.size(); i++) {
113 if (modelMaster.at(i) != int(modelValues.at(i)))
114 found_error = true;
115 printf("%-20s %d%s\n", modelNames.at(i).c_str(), int(modelValues.at(i)),
116 modelMaster.at(i) != modelValues.at(i) ? " !!!" : "");
117 }
118 printf("\n");
119
120 uint32_t add_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, add_ab);
121 uint32_t sub_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ab);
122 uint32_t sub_ba_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ba);
123
124 printf("%-20s %10u %10u%s\n", "result(a+b)", add_ab_value, a+b, add_ab_value != a+b ? " !!!" : "");
125 printf("%-20s %10u %10u%s\n", "result(a-b)", sub_ab_value, a-b, sub_ab_value != a-b ? " !!!" : "");
126 printf("%-20s %10u %10u%s\n", "result(b-a)", sub_ba_value, b-a, sub_ba_value != b-a ? " !!!" : "");
127 printf("\n");
128
129 if (found_error || add_ab_value != a+b || sub_ab_value != a-b || sub_ba_value != b-a)
130 abort();
131 }
132
main()133 int main()
134 {
135 printf("\n");
136 for (int i = 0; i < 1024; i++) {
137 printf("************** %d **************\n\n", i);
138 uint32_t a = xorshift128();
139 uint32_t b = xorshift128();
140 if (xorshift128() % 16 == 0)
141 a = b;
142 test_cmp(a, b);
143 }
144 return 0;
145 }
146
147