source: vis_dev/zchaff/zchaff_clsgen.h @ 25

Last change on this file since 25 was 10, checked in by cecile, 13 years ago

Zchaff
File size: 8.4 KB
Line 
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:
5//
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.
18//
19//
20// --- This software and any associated documentation is provided "as is"
21//
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.
27//
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// *********************************************************************
35
36#ifndef __CLAUSE_GENERATOR__
37#define __CLAUSE_GENERATOR__
38#include "zchaff_solver.h"
39
40class CClause_Gen {
41  private:
42    inline static int * ptr(vector<int>::iterator itr) {
43      return &(*itr);
44    }
45    inline static int pos(int i) {
46      return i;
47    }
48    inline static int neg(int i) {
49      return i^0x1;
50    }
51
52  public:
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)
55      vector <int> lits;
56      lits.clear();
57      lits.push_back(pos(a));
58      lits.push_back(neg(o));
59      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
60      lits.clear();
61      lits.push_back(pos(b));
62      lits.push_back(neg(o));
63      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
64      lits.clear();
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);
69    }
70
71    static void and_n(CSolver & solver, int * inputs, int num_input, int o,
72                      int gid = 0) {
73      vector <int> lits;
74      int i;
75      for (i = 0; i < num_input; ++i) {
76        lits.clear();
77        lits.push_back(pos(inputs[i]));
78        lits.push_back(neg(o));
79        solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
80      }
81      lits.clear();
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);
86    }
87
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')
90      vector <int> lits;
91      lits.clear();
92      lits.push_back(neg(a));
93      lits.push_back(pos(o));
94      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
95      lits.clear();
96      lits.push_back(neg(b));
97      lits.push_back(pos(o));
98      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
99      lits.clear();
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);
104    }
105
106    static void or_n(CSolver & solver, int * inputs, int num_input, int o,
107                     int gid = 0) {
108      vector <int> lits;
109      int i;
110      for (i = 0; i < num_input; ++i) {
111        lits.clear();
112        lits.push_back(neg(inputs[i]));
113        lits.push_back(pos(o));
114        solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
115      }
116      lits.clear();
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);
121    }
122
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')
125      vector <int> lits;
126      lits.clear();
127      lits.push_back(pos(a));
128      lits.push_back(pos(o));
129      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
130      lits.clear();
131      lits.push_back(pos(b));
132      lits.push_back(pos(o));
133      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
134      lits.clear();
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);
139    }
140
141    static void nand_n(CSolver & solver, int * inputs, int num_input, int o,
142                       int gid = 0) {
143      vector <int> lits;
144      int i;
145      for (i = 0; i < num_input; ++i) {
146        lits.clear();
147        lits.push_back(pos(inputs[i]));
148        lits.push_back(pos(o));
149        solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
150      }
151      lits.clear();
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);
156    }
157
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)
160      vector <int> lits;
161      lits.clear();
162      lits.push_back(neg(a));
163      lits.push_back(neg(o));
164      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
165      lits.clear();
166      lits.push_back(neg(b));
167      lits.push_back(neg(o));
168      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
169      lits.clear();
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);
174    }
175
176    static void nor_n(CSolver & solver, int * inputs, int num_input, int o,
177               int gid = 0) {
178      vector <int> lits;
179      int i;
180      for (i = 0; i < num_input; ++i) {
181        lits.clear();
182        lits.push_back(neg(inputs[i]));
183        lits.push_back(neg(o));
184        solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
185      }
186      lits.clear();
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);
191    }
192
193    static void xor2(CSolver & solver, int a, int b, int o, int gid = 0) {
194      // a xor b = o <==> (a' + b' + o')
195      //                  (a + b + o' )
196      //                  (a' + b + o)
197      //                         (a + b' + o)
198      vector <int> lits;
199      lits.clear();
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);
204      lits.clear();
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);
209      lits.clear();
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);
214      lits.clear();
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);
219    }
220
221    static void not1(CSolver & solver, int a, int o, int gid = 0) {
222      // a' = o <==> (a' + o')( a + o)
223      vector <int> lits;
224      lits.clear();
225      lits.push_back(neg(a));
226      lits.push_back(neg(o));
227      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
228      lits.clear();
229      lits.push_back(pos(a));
230      lits.push_back(pos(o));
231      solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
232    }
233};
234#endif
Note: See TracBrowser for help on using the repository browser.