From: Hamed Gorjiara Date: Thu, 5 Sep 2019 23:01:44 +0000 (-0700) Subject: Merging + fixing memory bugs X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=85d422935f1a6ebdb689f4108185521b022a51d9;hp=974a00584da88dce9c638bd5fd981f2164176e2c Merging + fixing memory bugs --- diff --git a/src/AST/element.cc b/src/AST/element.cc index 8044966..4fc9f4b 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -10,7 +10,7 @@ Element::Element(ASTNodeType _type) : ASTNode(_type), encoding(this), anyValue(false), - frozen(false){ + frozen(false) { } ElementSet::ElementSet(Set *s) : diff --git a/src/AST/element.h b/src/AST/element.h index 166078a..53f6008 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -15,8 +15,8 @@ public: Vector parents; ElementEncoding encoding; inline ElementEncoding *getElementEncoding() { return &encoding; } - inline void freezeElement(){frozen = true;} - inline bool isFrozen(){return frozen;} + inline void freezeElement() {frozen = true;} + inline bool isFrozen() {return frozen;} virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}; virtual void serialize(Serializer *serializer) = 0; virtual void print() = 0; diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index 34bcd74..25c5ec8 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -24,7 +24,9 @@ void IntegerEncodingTransform::doTransform() { SetIteratorOrder *orderit = orders->iterator(); while (orderit->hasNext()) { Order *order = orderit->next(); - if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &offon)) + if (order->type == SATC_PARTIAL) + continue; + if (GETVARTUNABLE(solver->getTuner(), order->set->type, ORDERINTEGERENCODING, &offon)) integerEncode(order); } delete orders; diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 5246101..27de064 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -589,7 +589,7 @@ void addClause(CNF *cnf, uint numliterals, int *literals) { addArrayClauseLiteral(cnf->solver, numliterals, literals); } -void freezeVariable(CNF *cnf, Edge e){ +void freezeVariable(CNF *cnf, Edge e) { int literal = getEdgeVar(e); freeze(cnf->solver, literal); } diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc index 72d3408..a89ed8b 100644 --- a/src/Backend/inc_solver.cc +++ b/src/Backend/inc_solver.cc @@ -102,7 +102,7 @@ int getSolution(IncrementalSolver *This) { } readSolver(This, &This->solution[1], numVars * sizeof(int)); This->solutionsize = numVars; - } else { //Reading unsat explanation + } else {//Reading unsat explanation int numVars = readIntSolver(This); if (numVars > This->solutionsize) { if (This->solution != NULL) diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index d924e6a..7687f35 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -220,9 +220,9 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) { generateAnyValueBinaryValueEncoding(encoding); } -void SATEncoder::freezeElementVariables(ElementEncoding *encoding){ +void SATEncoder::freezeElementVariables(ElementEncoding *encoding) { ASSERT(encoding->element->frozen); - for(uint i=0; i< encoding->numVars; i++){ + for (uint i = 0; i < encoding->numVars; i++) { Edge e = encoding->variables[i]; ASSERT(edgeIsVarConst(e)); freezeVariable(cnf, e); diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc old mode 100755 new mode 100644 index 5312b4f..2e09491 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -34,7 +34,7 @@ int SATEncoder::solve(long timeout) { long long startTime = getTimeNano(); finishedClauses(cnf->solver); cnf->encodeTime = getTimeNano() - startTime; - if(solver->isIncrementalMode()){ + if (solver->isIncrementalMode()) { solver->freezeElementsVariables(); } return solveCNF(cnf); @@ -47,7 +47,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); - if(!csolver->isConstraintEncoded(constraint)){ + if (!csolver->isConstraintEncoded(constraint)) { Edge c = encodeConstraintSATEncoder(constraint); addConstraintCNF(cnf, c); csolver->addEncodedConstraint(constraint); diff --git a/src/Collections/vector.h b/src/Collections/vector.h index 2dd5e69..6c53253 100644 --- a/src/Collections/vector.h +++ b/src/Collections/vector.h @@ -9,9 +9,9 @@ type *array; \ }; \ typedef struct Vector ## name Vector ## name; \ - Vector ## name *allocVector ## name(uint capacity); \ - Vector ## name *allocDefVector ## name(); \ - Vector ## name *allocVectorArray ## name(uint capacity, type * array); \ + Vector ## name * allocVector ## name(uint capacity); \ + Vector ## name * allocDefVector ## name(); \ + Vector ## name * allocVectorArray ## name(uint capacity, type * array); \ void pushVector ## name(Vector ## name * vector, type item); \ type lastVector ## name(Vector ## name * vector); \ void popVector ## name(Vector ## name * vector); \ @@ -29,18 +29,18 @@ void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array); #define VectorImpl(name, type, defcap) \ - Vector ## name *allocDefVector ## name() { \ + Vector ## name * allocDefVector ## name() { \ return allocVector ## name(defcap); \ } \ - Vector ## name *allocVector ## name(uint capacity) { \ - Vector ## name *tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \ + Vector ## name * allocVector ## name(uint capacity) { \ + Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \ tmp->size = 0; \ tmp->capacity = capacity; \ tmp->array = (type *) ourmalloc(sizeof(type) * capacity); \ return tmp; \ } \ - Vector ## name *allocVectorArray ## name(uint capacity, type * array) { \ - Vector ## name *tmp = allocVector ## name(capacity); \ + Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \ + Vector ## name * tmp = allocVector ## name(capacity); \ tmp->size = capacity; \ memcpy(tmp->array, array, capacity * sizeof(type)); \ return tmp; \ diff --git a/src/Test/dirkreader.cc b/src/Test/dirkreader.cc new file mode 100644 index 0000000..56393fb --- /dev/null +++ b/src/Test/dirkreader.cc @@ -0,0 +1,372 @@ +#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; +Vector * orderRecVector = NULL; +HashtableIW * ordertable = NULL; +HashtableBV * vartable = new HashtableBV(); + +void cleanAndFreeOrderRecVector(){ + for(uint i=0; i< orderRecVector->getSize(); i++){ + delete orderRecVector->get(i); + } + orderRecVector->clear(); +} + +int main(int numargs, char ** argv) { + file = new std::ifstream(argv[1]); + char * assert = NULL; + char * sat = NULL; + Vector orderRecs; + orderRecVector = &orderRecs; + while(true) { + int retval = skipahead(assertstart, satstart); + printf("%d\n", retval); + if (retval == 0){ + break; + } + if (retval == 1) { + if (assert != NULL){ + free(assert); + assert = NULL; + } + assert = readuntilend(assertend); + printf("[%s]\n", assert); + } else if (retval == 2) { + if (sat != NULL) { + free(sat); + sat = NULL; + vartable->resetAndDeleteKeys(); + ordertable->reset(); + cleanAndFreeOrderRecVector(); + } else { + ordertable = new HashtableIW(); + } + sat = readuntilend(satend); + CSolver *solver = new CSolver(); + solver->turnoffOptimizations(); + 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; + } + } + + cleanAndFreeOrderRecVector(); + if(ordertable != NULL){ + delete ordertable; + } + if(assert != NULL){ + free(assert); + } + if(sat != NULL){ + free(sat); + } + vartable->resetAndDeleteKeys(); + delete vartable; + file->close(); + delete file; +} + +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(); + orderRecVector->push(r); + 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(); + orderRecVector->push(rec); + rec->value = value; + rec->set = new HashsetIW(); + rec->set->add(k); + 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; + } +} diff --git a/src/Test/incrementaltest.cc b/src/Test/incrementaltest.cc index c71645d..e559630 100644 --- a/src/Test/incrementaltest.cc +++ b/src/Test/incrementaltest.cc @@ -17,21 +17,21 @@ int main(int numargs, char **argv) { solver->addConstraint(b); solver->freezeElement(e1); solver->freezeElement(e2); - if (solver->solve() == 1){ + if (solver->solve() == 1) { int run = 1; - do{ + do { printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2)); - for(int i=0; i< INPUTSIZE; i++){ + for (int i = 0; i < INPUTSIZE; i++) { uint64_t val = solver->getElementValue(inputs[i]); Element *econst = solver->getElementConst(0, val); - Element * tmpInputs[] = {inputs[i], econst}; + Element *tmpInputs[] = {inputs[i], econst}; BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE); solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b)); } run++; - }while(solver->solveIncremental() == 1); + } while (solver->solveIncremental() == 1); printf("After %d runs, there are no more models to find ...\n", run); - }else{ + } else { printf("UNSAT\n"); } delete solver; diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc index 7d08098..44cd2bc 100644 --- a/src/Tuner/basictuner.cc +++ b/src/Tuner/basictuner.cc @@ -182,10 +182,10 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) { updateTimeout(problem, metric); snprintf(buffer, sizeof(buffer), "tuner%uused", execnum); tuner->getTuner()->addUsed(buffer); - } else if (status == 124 << 8){ // timeout happens ... + } else if (status == 124 << 8) {// timeout happens ... tuner->getTuner()->copySettingstoUsedSettings(); } - + //Increment execution count execnum++; diff --git a/src/ccsolver.cc b/src/ccsolver.cc index 7707b74..aca46a5 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -104,16 +104,16 @@ void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int n void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize) { BooleanEdge constr [asize]; - for(uint i=0; i< asize; i++){ - constr[i] = BooleanEdge((Boolean*)array[i]); + for (uint i = 0; i < asize; i++) { + constr[i] = BooleanEdge((Boolean *)array[i]); } return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, constr, (uint) asize).getRaw(); } void *applyExactlyOneConstraint(void *solver, void **array, unsigned int asize) { BooleanEdge constr [asize]; - for(uint i=0; i< asize; i++){ - constr[i] = BooleanEdge((Boolean*)array[i]); + for (uint i = 0; i < asize; i++) { + constr[i] = BooleanEdge((Boolean *)array[i]); } return CCSOLVER(solver)->applyExactlyOneConstraint( constr, (uint) asize).getRaw(); } diff --git a/src/csolver.cc b/src/csolver.cc index 3798586..17e2378 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -244,10 +244,10 @@ void CSolver::mustHaveValue(Element *element) { } void CSolver::freezeElementsVariables() { - - for(uint i=0; i< allElements.getSize(); i++){ + + for (uint i = 0; i < allElements.getSize(); i++) { Element *e = allElements.get(i); - if(e->frozen){ + if (e->frozen) { satEncoder->freezeElementVariables(&e->encoding); } } @@ -409,24 +409,24 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin return applyLogicalOperation(op, newarray, asize); } -BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize){ +BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) { BooleanEdge newarray[asize + 1]; newarray[asize] = applyLogicalOperation(SATC_OR, array, asize); - for (uint i=0; i< asize; i++){ + for (uint i = 0; i < asize; i++) { BooleanEdge oprand1 = array[i]; - BooleanEdge carray [asize -1]; + BooleanEdge carray [asize - 1]; uint index = 0; - for( uint j =0; j< asize; j++){ - if(i != j){ + for ( uint j = 0; j < asize; j++) { + if (i != j) { BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]); carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2); } } - ASSERT(index == asize -1); - newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1); + ASSERT(index == asize - 1); + newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1); } - return applyLogicalOperation(SATC_AND, newarray, asize+1); + return applyLogicalOperation(SATC_AND, newarray, asize + 1); } BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { @@ -641,8 +641,8 @@ int CSolver::solveIncremental() { if (isUnSAT()) { return IS_UNSAT; } - - + + long long startTime = getTimeNano(); bool deleteTuner = false; if (tuner == NULL) { @@ -672,7 +672,7 @@ int CSolver::solveIncremental() { //Doing element optimization on new constraints // ElementOpt eop(this); // eop.doTransform(); - + //Since no new element is added, we assuming adding new constraint //has no impact on previous encoding decisions // EncodingGraph eg(this); @@ -698,7 +698,7 @@ int CSolver::solveIncremental() { time2 = getTimeNano(); elapsedTime = time2 - startTime; model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); - + if (deleteTuner) { delete tuner; tuner = NULL; @@ -775,7 +775,7 @@ int CSolver::solve() { model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC); model_print("Is problem UNSAT after encoding: %d\n", unsat); - + result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout); model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT"); @@ -842,9 +842,9 @@ uint64_t CSolver::getElementValue(Element *element) { exit(-1); } -void CSolver::freezeElement(Element *e){ +void CSolver::freezeElement(Element *e) { e->freezeElement(); - if(!incrementalMode){ + if (!incrementalMode) { incrementalMode = true; } } diff --git a/src/csolver.h b/src/csolver.h index 49438b6..eba7b3c 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -58,7 +58,7 @@ public: Set *getElementRange (Element *element); void mustHaveValue(Element *element); - + BooleanEdge getBooleanTrue(); BooleanEdge getBooleanFalse(); @@ -103,9 +103,9 @@ public: /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/ BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize); - + /** This function applies a logical operation to the Booleans in its input. */ - + BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize); /** This function applies a logical operation to the Booleans in its input. */ @@ -133,17 +133,15 @@ public: * Incremental Solving for SATUNE. * It only supports incremental solving for elements! * No support for BooleanVar, BooleanOrder or using interpreters - * @return + * @return */ int solveIncremental(); - + /** After getting the solution from the SAT solver, client can get the value of an element via this function*/ uint64_t getElementValue(Element *element); void freezeElement(Element *e); - void turnoffOptimizations(){optimizationsOff = true;} - /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ bool getBooleanValue(BooleanEdge boolean); @@ -167,7 +165,7 @@ public: SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); } bool isConstraintEncoded(BooleanEdge be) { return encodedConstraints.contains(be);} void addEncodedConstraint(BooleanEdge be) {encodedConstraints.add(be);} - + SATEncoder *getSATEncoder() {return satEncoder;} void replaceBooleanWithTrue(BooleanEdge bexpr); @@ -196,7 +194,7 @@ private: void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child); void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child); void handleFunction(ElementFunction *ef, BooleanEdge child); - + //These two functions are helpers if the client has a pointer to a //Boolean object that we have since replaced BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize); diff --git a/src/satune_SatuneJavaAPI.cc b/src/satune_SatuneJavaAPI.cc index e337590..0a7d672 100644 --- a/src/satune_SatuneJavaAPI.cc +++ b/src/satune_SatuneJavaAPI.cc @@ -1,7 +1,7 @@ /* DO NOT EDIT THIS FILE - it is machine generated */ #include "satune_SatuneJavaAPI.h" #include "ccsolver.h" -#define CCSOLVER(solver) (void*)solver +#define CCSOLVER(solver) (void *)solver /* Header for class SatuneJavaAPI */ /* @@ -14,7 +14,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver (JNIEnv *env, jobject obj) { return (jlong)createCCSolver(); - + } /* @@ -158,7 +158,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar * Signature: (JI)J */ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue - (JNIEnv * env, jobject obj, jlong solver) + (JNIEnv *env, jobject obj, jlong solver) { return (jlong)getBooleanTrue((void *)solver); } @@ -169,7 +169,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue * Signature: (JI)J */ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse - (JNIEnv * env, jobject obj, jlong solver) + (JNIEnv *env, jobject obj, jlong solver) { return (jlong)getBooleanFalse((void *)solver); } diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h index e606b44..0a0b6e5 100644 --- a/src/satune_SatuneJavaAPI.h +++ b/src/satune_SatuneJavaAPI.h @@ -38,7 +38,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver * Signature: (JIJI)J */ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet - (JNIEnv *, jobject , jlong , jint , jlongArray arr); + (JNIEnv *, jobject, jlong, jint, jlongArray arr); /* * Class: satune_SatuneJavaAPI