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;
54 Vector<OrderRec*> * orderRecVector = NULL;
55 HashtableIW * ordertable = NULL;
56 HashtableBV * vartable = new HashtableBV();
58 void cleanAndFreeOrderRecVector(){
59 for(uint i=0; i< orderRecVector->getSize(); i++){
60 delete orderRecVector->get(i);
62 orderRecVector->clear();
65 int main(int numargs, char ** argv) {
66 file = new std::ifstream(argv[1]);
69 Vector<OrderRec*> orderRecs;
70 orderRecVector = &orderRecs;
72 int retval = skipahead(assertstart, satstart);
73 printf("%d\n", retval);
82 assert = readuntilend(assertend);
83 printf("[%s]\n", assert);
84 } else if (retval == 2) {
88 vartable->resetAndDeleteKeys();
90 cleanAndFreeOrderRecVector();
92 ordertable = new HashtableIW();
94 sat = readuntilend(satend);
95 CSolver *solver = new CSolver();
96 solver->turnoffOptimizations();
97 set = solver->createMutableSet(1);
98 order = solver->createOrder(SATC_TOTAL, (Set *) set);
100 processEquality(sat, offset);
102 processEquality(assert, offset);
104 solver->addConstraint(parseConstraint(solver, sat, offset));
106 solver->addConstraint(parseConstraint(solver, assert, offset));
107 printf("[%s]\n", sat);
108 solver->finalizeMutableSet(set);
110 solver->printConstraints();
115 cleanAndFreeOrderRecVector();
116 if(ordertable != NULL){
125 vartable->resetAndDeleteKeys();
131 void skipwhitespace(char * constraint, int & offset) {
133 while (constraint[offset] == ' ' || constraint[offset] == '\n')
138 printf("PARSE ERROR\n");
142 int32_t getOrderVar(char *constraint, int & offset) {
143 if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
148 char next = constraint[offset];
149 if (next >= '0' && next <= '9') {
150 num = (num * 10) + (next - '0');
157 int32_t getBooleanVar(char *constraint, int & offset) {
158 if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
163 char next = constraint[offset];
164 if (next >= '0' && next <= '9') {
165 num = (num * 10) + (next - '0');
172 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
174 if (vartable->contains(&v)) {
175 return BooleanEdge(vartable->get(&v));
177 Boolean* ve = solver->getBooleanVar(2).getBoolean();
178 vartable->put(new intwrapper(value), ve);
179 return BooleanEdge(ve);
183 void mergeVars(int32_t value1, int32_t value2) {
184 intwrapper v1(value1);
185 intwrapper v2(value2);
186 OrderRec *r1 = ordertable->get(&v1);
187 OrderRec *r2 = ordertable->get(&v2);
190 OrderRec * r = new OrderRec();
191 orderRecVector->push(r);
193 r->set = new HashsetIW();
194 intwrapper * k1 = new intwrapper(v1);
195 intwrapper * k2 = new intwrapper(v2);
198 ordertable->put(k1, r);
199 ordertable->put(k2, r);
201 } else if (r1 == NULL) {
202 intwrapper * k = new intwrapper(v1);
203 ordertable->put(k, r2);
205 } else if (r2 == NULL) {
206 intwrapper * k = new intwrapper(v2);
207 ordertable->put(k, r1);
210 SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
211 while (it1->hasNext()) {
212 intwrapper * k = it1->next();
213 ordertable->put(k, r2);
223 int32_t checkordervar(CSolver * solver, int32_t value) {
225 OrderRec * rec = ordertable->get(&v);
227 intwrapper * k = new intwrapper(value);
228 rec = new OrderRec();
229 orderRecVector->push(rec);
231 rec->set = new HashsetIW();
233 ordertable->put(k, rec);
236 solver->addItem(set, rec->value);
242 void processEquality(char * constraint, int &offset) {
243 skipwhitespace(constraint, offset);
244 if (strncmp(&constraint[offset], "(and",4) == 0) {
246 Vector<BooleanEdge> vec;
248 skipwhitespace(constraint, offset);
249 if (constraint[offset] == ')') {
253 processEquality(constraint, offset);
255 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
257 skipwhitespace(constraint, offset);
258 getOrderVar(constraint, offset);
259 skipwhitespace(constraint, offset);
260 getOrderVar(constraint, offset);
261 skipwhitespace(constraint, offset);
262 if (constraint[offset++] != ')')
265 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
267 skipwhitespace(constraint, offset);
268 int v1=getOrderVar(constraint, offset);
269 skipwhitespace(constraint, offset);
270 int v2=getOrderVar(constraint, offset);
271 skipwhitespace(constraint, offset);
272 if (constraint[offset++] != ')')
277 getBooleanVar(constraint, offset);
278 skipwhitespace(constraint, offset);
283 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
284 skipwhitespace(constraint, offset);
285 if (strncmp(&constraint[offset], "(and", 4) == 0) {
287 Vector<BooleanEdge> vec;
289 skipwhitespace(constraint, offset);
290 if (constraint[offset] == ')') {
292 return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
294 vec.push(parseConstraint(solver, constraint, offset));
296 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
298 skipwhitespace(constraint, offset);
299 int32_t v1 = getOrderVar(constraint, offset);
300 skipwhitespace(constraint, offset);
301 int32_t v2 = getOrderVar(constraint, offset);
302 skipwhitespace(constraint, offset);
303 if (constraint[offset++] != ')')
305 return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
306 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
308 skipwhitespace(constraint, offset);
309 getOrderVar(constraint, offset);
310 skipwhitespace(constraint, offset);
311 getOrderVar(constraint, offset);
312 skipwhitespace(constraint, offset);
313 if (constraint[offset++] != ')')
315 return solver->getBooleanTrue();
317 int32_t v = getBooleanVar(constraint, offset);
318 skipwhitespace(constraint, offset);
319 return checkBooleanVar(solver, v);
323 int skipahead(const char * token1, const char * token2) {
324 int index1 = 0, index2 = 0;
327 if (token1[index1] == 0)
329 if (token2[index2] == 0)
333 file->read(buffer, 1);
334 if (buffer[0] == token1[index1])
338 if (buffer[0] == token2[index2])
345 char * readuntilend(const char * token) {
350 char * outbuffer = (char *) malloc(length);
352 if (token[index] == 0) {
353 outbuffer[offset - index] = 0;
361 file->read(buffer, 1);
362 outbuffer[offset++] = buffer[0];
363 if (offset == length) {
365 outbuffer = (char *) realloc(outbuffer, length);
367 if (buffer[0] == token[index])