From 50d8f27a7eb47d7398e14252895a656dbeed5c6a Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 27 Aug 2019 23:14:42 -0700 Subject: [PATCH 1/1] Add file to read in constraints from Dirk --- src/Test/dirkreader.cc | 340 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 340 insertions(+) create mode 100644 src/Test/dirkreader.cc diff --git a/src/Test/dirkreader.cc b/src/Test/dirkreader.cc new file mode 100644 index 0000000..60b4aee --- /dev/null +++ b/src/Test/dirkreader.cc @@ -0,0 +1,340 @@ +#include +#include +#include "csolver.h" +#include "hashset.h" +#include "cppvector.h" + +const char * assertstart = "ASSERTSTART"; +const char * assertend = "ASSERTEND"; +const char * satstart = "SATSTART"; +const char * satend = "SATEND"; + +int skipahead(const char * token1, const char * token2); +char * readuntilend(const char * token); +BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset); +void processEquality(char * constraint, int &offset); + +std::ifstream * file; +Order * order; +MutableSet * set; +class intwrapper { +public: + intwrapper(int _val) : value(_val) { + } + int32_t value; +}; + +unsigned int iw_hash_function(intwrapper *i) { + return i->value; +} + +bool iw_equals(intwrapper *key1, intwrapper *key2) { + return (key1->value == key2->value); +} + +typedef Hashset HashsetIW; + +class OrderRec { +public: + OrderRec() : set (NULL), value(-1), alloced(false) { + } + ~OrderRec() { + if (set != NULL) { + set->resetAndDelete(); + delete set; + } + } + HashsetIW * set; + int32_t value; + bool alloced; +}; + +typedef Hashtable HashtableIW; +typedef Hashtable HashtableBV; + +HashtableIW * ordertable = NULL; +HashtableBV * vartable = new HashtableBV(); + +int main(int numargs, char ** argv) { + file = new std::ifstream(argv[1]); + char * assert = NULL; + char * sat = NULL; + while(true) { + int retval = skipahead(assertstart, satstart); + printf("%d\n", retval); + if (retval == 0) + break; + if (retval == 1) { + if (assert != NULL) + free(assert); + assert = readuntilend(assertend); + printf("[%s]\n", assert); + } else if (retval == 2) { + if (sat != NULL) { + free(sat); + vartable->resetAndDeleteKeys(); + ordertable->resetAndDeleteVals(); + } else { + ordertable = new HashtableIW(); + } + sat = readuntilend(satend); + CSolver *solver = new CSolver(); + set = solver->createMutableSet(1); + order = solver->createOrder(SATC_TOTAL, (Set *) set); + int offset = 0; + processEquality(sat, offset); + offset = 0; + processEquality(assert, offset); + offset = 0; + solver->addConstraint(parseConstraint(solver, sat, offset)); + offset = 0; + solver->addConstraint(parseConstraint(solver, assert, offset)); + printf("[%s]\n", sat); + solver->finalizeMutableSet(set); + solver->serialize(); + solver->printConstraints(); + delete solver; + } + } + + file->close(); +} + +void skipwhitespace(char * constraint, int & offset) { + //skip whitespace + while (constraint[offset] == ' ' || constraint[offset] == '\n') + offset++; +} + +void doExit() { + printf("PARSE ERROR\n"); + exit(-1); +} + +int32_t getOrderVar(char *constraint, int & offset) { + if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) { + doExit(); + } + int32_t num = 0; + while(true) { + char next = constraint[offset]; + if (next >= '0' && next <= '9') { + num = (num * 10) + (next - '0'); + offset++; + } else + return num; + } +} + +int32_t getBooleanVar(char *constraint, int & offset) { + if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) { + doExit(); + } + int32_t num = 0; + while(true) { + char next = constraint[offset]; + if (next >= '0' && next <= '9') { + num = (num * 10) + (next - '0'); + offset++; + } else + return num; + } +} + +BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) { + intwrapper v(value); + if (vartable->contains(&v)) { + return BooleanEdge(vartable->get(&v)); + } else { + Boolean* ve = solver->getBooleanVar(2).getBoolean(); + vartable->put(new intwrapper(value), ve); + return BooleanEdge(ve); + } +} + +void mergeVars(int32_t value1, int32_t value2) { + intwrapper v1(value1); + intwrapper v2(value2); + OrderRec *r1 = ordertable->get(&v1); + OrderRec *r2 = ordertable->get(&v2); + if (r1 == r2) { + if (r1 == NULL) { + OrderRec * r = new OrderRec(); + r->value = value1; + r->set = new HashsetIW(); + intwrapper * k1 = new intwrapper(v1); + intwrapper * k2 = new intwrapper(v2); + r->set->add(k1); + r->set->add(k2); + ordertable->put(k1, r); + ordertable->put(k2, r); + } + } else if (r1 == NULL) { + intwrapper * k = new intwrapper(v1); + ordertable->put(k, r2); + r2->set->add(k); + } else if (r2 == NULL) { + intwrapper * k = new intwrapper(v2); + ordertable->put(k, r1); + r1->set->add(k); + } else { + SetIterator * it1 = r1->set->iterator(); + while (it1->hasNext()) { + intwrapper * k = it1->next(); + ordertable->put(k, r2); + r2->set->add(k); + } + delete r2->set; + r2->set = NULL; + delete r2; + delete it1; + } +} + +int32_t checkordervar(CSolver * solver, int32_t value) { + intwrapper v(value); + OrderRec * rec = ordertable->get(&v); + if (rec == NULL) { + intwrapper * k = new intwrapper(value); + rec = new OrderRec(); + rec->value = value; + ordertable->put(k, rec); + } + if (!rec->alloced) { + solver->addItem(set, rec->value); + rec->alloced = true; + } + return rec->value; +} + +void processEquality(char * constraint, int &offset) { + skipwhitespace(constraint, offset); + if (strncmp(&constraint[offset], "(and",4) == 0) { + offset +=4; + Vector vec; + while(true) { + skipwhitespace(constraint, offset); + if (constraint[offset] == ')') { + offset++; + return; + } + processEquality(constraint, offset); + } + } else if (strncmp(&constraint[offset], "(<", 2) == 0) { + offset+=2; + skipwhitespace(constraint, offset); + getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + if (constraint[offset++] != ')') + doExit(); + return; + } else if (strncmp(&constraint[offset], "(=", 2) == 0) { + offset+=2; + skipwhitespace(constraint, offset); + int v1=getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + int v2=getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + if (constraint[offset++] != ')') + doExit(); + mergeVars(v1, v2); + return; + } else { + getBooleanVar(constraint, offset); + skipwhitespace(constraint, offset); + return; + } +} + +BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) { + skipwhitespace(constraint, offset); + if (strncmp(&constraint[offset], "(and", 4) == 0) { + offset +=4; + Vector vec; + while(true) { + skipwhitespace(constraint, offset); + if (constraint[offset] == ')') { + offset++; + return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize()); + } + vec.push(parseConstraint(solver, constraint, offset)); + } + } else if (strncmp(&constraint[offset], "(<", 2) == 0) { + offset+=2; + skipwhitespace(constraint, offset); + int32_t v1 = getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + int32_t v2 = getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + if (constraint[offset++] != ')') + doExit(); + return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2)); + } else if (strncmp(&constraint[offset], "(=", 2) == 0) { + offset+=2; + skipwhitespace(constraint, offset); + getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + getOrderVar(constraint, offset); + skipwhitespace(constraint, offset); + if (constraint[offset++] != ')') + doExit(); + return solver->getBooleanTrue(); + } else { + int32_t v = getBooleanVar(constraint, offset); + skipwhitespace(constraint, offset); + return checkBooleanVar(solver, v); + } +} + +int skipahead(const char * token1, const char * token2) { + int index1 = 0, index2 = 0; + char buffer[256]; + while(true) { + if (token1[index1] == 0) + return 1; + if (token2[index2] == 0) + return 2; + if (file->eof()) + return 0; + file->read(buffer, 1); + if (buffer[0] == token1[index1]) + index1++; + else + index1 = 0; + if (buffer[0] == token2[index2]) + index2++; + else + index2 = 0; + } +} + +char * readuntilend(const char * token) { + int index = 0; + char buffer[256]; + int length = 256; + int offset = 0; + char * outbuffer = (char *) malloc(length); + while(true) { + if (token[index] == 0) { + outbuffer[offset - index] = 0; + return outbuffer; + } + if (file->eof()) { + free(outbuffer); + return NULL; + } + + file->read(buffer, 1); + outbuffer[offset++] = buffer[0]; + if (offset == length) { + length = length * 2; + outbuffer = (char *) realloc(outbuffer, length); + } + if (buffer[0] == token[index]) + index++; + else + index=0; + } +} -- 2.34.1