1 // *********************************************************************
2 // Copyright 2000-2004, Princeton University. All rights reserved.
3 // By using this software the USER indicates that he or she has read,
4 // understood and will comply with the following:
6 // --- Princeton University hereby grants USER nonexclusive permission
7 // to use, copy and/or modify this software for internal, noncommercial,
8 // research purposes only. Any distribution, including commercial sale
9 // or license, of this software, copies of the software, its associated
10 // documentation and/or modifications of either is strictly prohibited
11 // without the prior consent of Princeton University. Title to copyright
12 // to this software and its associated documentation shall at all times
13 // remain with Princeton University. Appropriate copyright notice shall
14 // be placed on all software copies, and a complete copy of this notice
15 // shall be included in all copies of the associated documentation.
16 // No right is granted to use in advertising, publicity or otherwise
17 // any trademark, service mark, or the name of Princeton University.
20 // --- This software and any associated documentation is provided "as is"
22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24 // PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
28 // Princeton University shall not be liable under any circumstances for
29 // any direct, indirect, special, incidental, or consequential damages
30 // with respect to any claim by USER or any third party on account of
31 // or arising from the use, or inability to use, this software or its
32 // associated documentation, even if Princeton University has been advised
33 // of the possibility of those damages.
34 // *********************************************************************
36 #ifndef __CLAUSE_GENERATOR__
37 #define __CLAUSE_GENERATOR__
38 #include "zchaff_solver.h"
42 inline static int * ptr(vector<int>::iterator itr) {
45 inline static int pos(int i) {
48 inline static int neg(int i) {
53 static void and2(CSolver & solver, int a, int b, int o, int gid = 0) {
54 // a*b=c <==> (a + o')( b + o')(a'+b'+o)
57 lits.push_back(pos(a));
58 lits.push_back(neg(o));
59 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
61 lits.push_back(pos(b));
62 lits.push_back(neg(o));
63 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
65 lits.push_back(neg(a));
66 lits.push_back(neg(b));
67 lits.push_back(pos(o));
68 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
71 static void and_n(CSolver & solver, int * inputs, int num_input, int o,
75 for (i = 0; i < num_input; ++i) {
77 lits.push_back(pos(inputs[i]));
78 lits.push_back(neg(o));
79 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
82 for (i = 0; i < num_input; ++i)
83 lits.push_back(neg(inputs[i]));
84 lits.push_back(pos(o));
85 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
88 static void or2(CSolver & solver, int a, int b, int o, int gid = 0) {
89 // a+b=c <==> (a' + c)( b' + c)(a + b + c')
92 lits.push_back(neg(a));
93 lits.push_back(pos(o));
94 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
96 lits.push_back(neg(b));
97 lits.push_back(pos(o));
98 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
100 lits.push_back(pos(a));
101 lits.push_back(pos(b));
102 lits.push_back(neg(o));
103 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
106 static void or_n(CSolver & solver, int * inputs, int num_input, int o,
110 for (i = 0; i < num_input; ++i) {
112 lits.push_back(neg(inputs[i]));
113 lits.push_back(pos(o));
114 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
117 for (i = 0; i < num_input; ++i)
118 lits.push_back(pos(inputs[i]));
119 lits.push_back(neg(o));
120 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
123 static void nand2(CSolver & solver, int a, int b, int o, int gid = 0) {
124 // a Nand b = o <==> (a + o)( b + o)(a' + b' + o')
127 lits.push_back(pos(a));
128 lits.push_back(pos(o));
129 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
131 lits.push_back(pos(b));
132 lits.push_back(pos(o));
133 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
135 lits.push_back(neg(a));
136 lits.push_back(neg(b));
137 lits.push_back(neg(o));
138 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
141 static void nand_n(CSolver & solver, int * inputs, int num_input, int o,
145 for (i = 0; i < num_input; ++i) {
147 lits.push_back(pos(inputs[i]));
148 lits.push_back(pos(o));
149 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
152 for (i = 0; i < num_input; ++i)
153 lits.push_back(neg(inputs[i]));
154 lits.push_back(neg(o));
155 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
158 static void nor2(CSolver & solver, int a, int b, int o, int gid = 0) {
159 // a Nor b = o <==> (a' + o')( b' + o')(a + b + o)
162 lits.push_back(neg(a));
163 lits.push_back(neg(o));
164 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
166 lits.push_back(neg(b));
167 lits.push_back(neg(o));
168 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
170 lits.push_back(pos(a));
171 lits.push_back(pos(b));
172 lits.push_back(pos(o));
173 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
176 static void nor_n(CSolver & solver, int * inputs, int num_input, int o,
180 for (i = 0; i < num_input; ++i) {
182 lits.push_back(neg(inputs[i]));
183 lits.push_back(neg(o));
184 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
187 for (i = 0; i < num_input; ++i)
188 lits.push_back(pos(inputs[i]));
189 lits.push_back(pos(o));
190 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
193 static void xor2(CSolver & solver, int a, int b, int o, int gid = 0) {
194 // a xor b = o <==> (a' + b' + o')
200 lits.push_back(neg(a));
201 lits.push_back(neg(b));
202 lits.push_back(neg(o));
203 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
205 lits.push_back(pos(a));
206 lits.push_back(pos(b));
207 lits.push_back(neg(o));
208 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
210 lits.push_back(neg(a));
211 lits.push_back(pos(b));
212 lits.push_back(pos(o));
213 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
215 lits.push_back(pos(a));
216 lits.push_back(neg(b));
217 lits.push_back(pos(o));
218 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
221 static void not1(CSolver & solver, int a, int o, int gid = 0) {
222 // a' = o <==> (a' + o')( a + o)
225 lits.push_back(neg(a));
226 lits.push_back(neg(o));
227 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
229 lits.push_back(pos(a));
230 lits.push_back(pos(o));
231 solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);