7 const char * assertstart = "ASSERTSTART";
8 const char * assertend = "ASSERTEND";
9 const char * satstart = "SATSTART";
10 const char * satend = "SATEND";
12 int skipahead(const char * token1, const char * token2);
13 char * readuntilend(const char * token);
14 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
15 void processEquality(char * constraint, int &offset);
22 intwrapper(int _val) : value(_val) {
27 unsigned int iw_hash_function(intwrapper *i) {
31 bool iw_equals(intwrapper *key1, intwrapper *key2) {
32 return (key1->value == key2->value);
35 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
39 OrderRec() : set (NULL), value(-1), alloced(false) {
43 set->resetAndDelete();
52 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
53 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
55 HashtableIW * ordertable = NULL;
56 HashtableBV * vartable = new HashtableBV();
58 int main(int numargs, char ** argv) {
59 file = new std::ifstream(argv[1]);
63 int retval = skipahead(assertstart, satstart);
64 printf("%d\n", retval);
70 assert = readuntilend(assertend);
71 printf("[%s]\n", assert);
72 } else if (retval == 2) {
75 vartable->resetAndDeleteKeys();
76 ordertable->resetAndDeleteVals();
78 ordertable = new HashtableIW();
80 sat = readuntilend(satend);
81 CSolver *solver = new CSolver();
82 set = solver->createMutableSet(1);
83 order = solver->createOrder(SATC_TOTAL, (Set *) set);
85 processEquality(sat, offset);
87 processEquality(assert, offset);
89 solver->addConstraint(parseConstraint(solver, sat, offset));
91 solver->addConstraint(parseConstraint(solver, assert, offset));
92 printf("[%s]\n", sat);
93 solver->finalizeMutableSet(set);
95 solver->printConstraints();
103 void skipwhitespace(char * constraint, int & offset) {
105 while (constraint[offset] == ' ' || constraint[offset] == '\n')
110 printf("PARSE ERROR\n");
114 int32_t getOrderVar(char *constraint, int & offset) {
115 if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
120 char next = constraint[offset];
121 if (next >= '0' && next <= '9') {
122 num = (num * 10) + (next - '0');
129 int32_t getBooleanVar(char *constraint, int & offset) {
130 if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
135 char next = constraint[offset];
136 if (next >= '0' && next <= '9') {
137 num = (num * 10) + (next - '0');
144 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
146 if (vartable->contains(&v)) {
147 return BooleanEdge(vartable->get(&v));
149 Boolean* ve = solver->getBooleanVar(2).getBoolean();
150 vartable->put(new intwrapper(value), ve);
151 return BooleanEdge(ve);
155 void mergeVars(int32_t value1, int32_t value2) {
156 intwrapper v1(value1);
157 intwrapper v2(value2);
158 OrderRec *r1 = ordertable->get(&v1);
159 OrderRec *r2 = ordertable->get(&v2);
162 OrderRec * r = new OrderRec();
164 r->set = new HashsetIW();
165 intwrapper * k1 = new intwrapper(v1);
166 intwrapper * k2 = new intwrapper(v2);
169 ordertable->put(k1, r);
170 ordertable->put(k2, r);
172 } else if (r1 == NULL) {
173 intwrapper * k = new intwrapper(v1);
174 ordertable->put(k, r2);
176 } else if (r2 == NULL) {
177 intwrapper * k = new intwrapper(v2);
178 ordertable->put(k, r1);
181 SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
182 while (it1->hasNext()) {
183 intwrapper * k = it1->next();
184 ordertable->put(k, r2);
194 int32_t checkordervar(CSolver * solver, int32_t value) {
196 OrderRec * rec = ordertable->get(&v);
198 intwrapper * k = new intwrapper(value);
199 rec = new OrderRec();
201 ordertable->put(k, rec);
204 solver->addItem(set, rec->value);
210 void processEquality(char * constraint, int &offset) {
211 skipwhitespace(constraint, offset);
212 if (strncmp(&constraint[offset], "(and",4) == 0) {
214 Vector<BooleanEdge> vec;
216 skipwhitespace(constraint, offset);
217 if (constraint[offset] == ')') {
221 processEquality(constraint, offset);
223 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
225 skipwhitespace(constraint, offset);
226 getOrderVar(constraint, offset);
227 skipwhitespace(constraint, offset);
228 getOrderVar(constraint, offset);
229 skipwhitespace(constraint, offset);
230 if (constraint[offset++] != ')')
233 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
235 skipwhitespace(constraint, offset);
236 int v1=getOrderVar(constraint, offset);
237 skipwhitespace(constraint, offset);
238 int v2=getOrderVar(constraint, offset);
239 skipwhitespace(constraint, offset);
240 if (constraint[offset++] != ')')
245 getBooleanVar(constraint, offset);
246 skipwhitespace(constraint, offset);
251 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
252 skipwhitespace(constraint, offset);
253 if (strncmp(&constraint[offset], "(and", 4) == 0) {
255 Vector<BooleanEdge> vec;
257 skipwhitespace(constraint, offset);
258 if (constraint[offset] == ')') {
260 return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
262 vec.push(parseConstraint(solver, constraint, offset));
264 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
266 skipwhitespace(constraint, offset);
267 int32_t v1 = getOrderVar(constraint, offset);
268 skipwhitespace(constraint, offset);
269 int32_t v2 = getOrderVar(constraint, offset);
270 skipwhitespace(constraint, offset);
271 if (constraint[offset++] != ')')
273 return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
274 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
276 skipwhitespace(constraint, offset);
277 getOrderVar(constraint, offset);
278 skipwhitespace(constraint, offset);
279 getOrderVar(constraint, offset);
280 skipwhitespace(constraint, offset);
281 if (constraint[offset++] != ')')
283 return solver->getBooleanTrue();
285 int32_t v = getBooleanVar(constraint, offset);
286 skipwhitespace(constraint, offset);
287 return checkBooleanVar(solver, v);
291 int skipahead(const char * token1, const char * token2) {
292 int index1 = 0, index2 = 0;
295 if (token1[index1] == 0)
297 if (token2[index2] == 0)
301 file->read(buffer, 1);
302 if (buffer[0] == token1[index1])
306 if (buffer[0] == token2[index2])
313 char * readuntilend(const char * token) {
318 char * outbuffer = (char *) malloc(length);
320 if (token[index] == 0) {
321 outbuffer[offset - index] = 0;
329 file->read(buffer, 1);
330 outbuffer[offset++] = buffer[0];
331 if (offset == length) {
333 outbuffer = (char *) realloc(outbuffer, length);
335 if (buffer[0] == token[index])