From 0fc529c88d7ea03156af7a2f1ad1fbb956c23c98 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 26 Aug 2019 12:01:00 -0700 Subject: [PATCH] fix tabbing --- src/AST/element.cc | 2 +- src/AST/element.h | 4 +-- src/ASTTransform/integerencoding.cc | 2 +- src/Backend/constraint.cc | 2 +- src/Backend/inc_solver.cc | 2 +- src/Backend/satelemencoder.cc | 4 +-- src/Backend/satencoder.cc | 4 +-- src/Collections/vector.h | 16 ++++++------ src/Test/incrementaltest.cc | 12 ++++----- src/Tuner/basictuner.cc | 4 +-- src/ccsolver.cc | 8 +++--- src/csolver.cc | 38 ++++++++++++++--------------- src/csolver.h | 16 ++++++------ src/satune_SatuneJavaAPI.cc | 8 +++--- src/satune_SatuneJavaAPI.h | 2 +- 15 files changed, 62 insertions(+), 62 deletions(-) mode change 100755 => 100644 src/Backend/satencoder.cc 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 621d2a8..25c5ec8 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -25,7 +25,7 @@ void IntegerEncodingTransform::doTransform() { while (orderit->hasNext()) { Order *order = orderit->next(); if (order->type == SATC_PARTIAL) - continue; + continue; if (GETVARTUNABLE(solver->getTuner(), order->set->type, ORDERINTEGERENCODING, &offon)) integerEncode(order); } 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 aa73924..b380c3a 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/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 fa2e342..aea2161 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 d1c6d33..17b3dc3 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -243,10 +243,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); } } @@ -408,24 +408,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) { @@ -640,8 +640,8 @@ int CSolver::solveIncremental() { if (isUnSAT()) { return IS_UNSAT; } - - + + long long startTime = getTimeNano(); bool deleteTuner = false; if (tuner == NULL) { @@ -650,7 +650,7 @@ int CSolver::solveIncremental() { } int result = IS_INDETER; ASSERT (!useInterpreter()); - + computePolarities(this); // long long time1 = getTimeNano(); // model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC); @@ -670,7 +670,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); @@ -696,7 +696,7 @@ int CSolver::solveIncremental() { time2 = getTimeNano(); elapsedTime = time2 - startTime; model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); - + if (deleteTuner) { delete tuner; tuner = NULL; @@ -770,7 +770,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"); @@ -837,9 +837,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 6996e42..b27e3c0 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,15 +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); - + /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ bool getBooleanValue(BooleanEdge boolean); @@ -165,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); @@ -194,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 21cd504..37bfba4 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 68703bc..93a386d 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 -- 2.34.1