From 74263c61d7ad3019320724b441c5e6a2a66b2f71 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 17:05:48 -0700 Subject: [PATCH] More fixes --- src/AST/element.cc | 3 ++- src/Backend/constraint.cc | 14 +++++++++----- src/Backend/inc_solver.h | 2 +- src/Backend/satfunctableencoder.cc | 4 ++-- src/Backend/satorderencoder.cc | 6 ++++-- src/Encoders/orderencoder.cc | 4 ++-- src/Test/logicopstest.cc | 17 +++++++++++------ src/Test/ordergraphtest.cc | 5 +++-- src/Test/tablefuncencodetest.cc | 3 ++- src/Test/tablepredicencodetest.cc | 6 ++++-- src/csolver.cc | 2 +- 11 files changed, 41 insertions(+), 25 deletions(-) diff --git a/src/AST/element.cc b/src/AST/element.cc index 5d126c7..91551e5 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -33,7 +33,8 @@ Element *allocElementConst(uint64_t value, VarType type) { ElementConst *This = (ElementConst *)ourmalloc(sizeof(ElementConst)); GETELEMENTTYPE(This) = ELEMCONST; This->value = value; - This->set = allocSet(type, (uint64_t[]) {value}, 1); + uint64_t array[]={value}; + This->set = allocSet(type, array, 1); initDefVectorASTNode(GETELEMENTPARENTS(This)); initElementEncoding(&This->encoding, (Element *) This); return &This->base; diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index a339988..df812df 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -183,7 +183,7 @@ int comparefunction(const Edge *e1, const Edge *e2) { Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) { ASSERT(numEdges != 0); qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction); - int initindex = 0; + uint initindex = 0; while (initindex < numEdges && equalsEdge(edges[initindex], E_True)) initindex++; @@ -288,18 +288,22 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) { if (equalsEdge(cond, E_True)) { result = thenedge; } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) { - result = constraintOR(cnf, 2, (Edge[]) {cond, elseedge}); + Edge array[] = {cond, elseedge}; + result = constraintOR(cnf, 2, array); } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) { result = constraintIMPLIES(cnf, cond, thenedge); } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) { - result = constraintAND(cnf, 2, (Edge[]) {cond, thenedge}); + Edge array[] = {cond, thenedge}; + result = constraintAND(cnf, 2, array); } else if (equalsEdge(thenedge, elseedge)) { result = thenedge; } else if (sameNodeOppSign(thenedge, elseedge)) { if (ltEdge(cond, thenedge)) { - result = createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge}); + Edge array[] = {cond, thenedge}; + result = createNode(cnf, NodeType_IFF, 2, array); } else { - result = createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond}); + Edge array[] = {thenedge, cond}; + result = createNode(cnf, NodeType_IFF, 2, array); } } else { Edge edges[] = {cond, thenedge, elseedge}; diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h index 9e9424e..78506b4 100644 --- a/src/Backend/inc_solver.h +++ b/src/Backend/inc_solver.h @@ -22,7 +22,7 @@ struct IncrementalSolver { int *buffer; int *solution; int solutionsize; - int offset; + uint offset; pid_t solver_pid; int to_solver_fd; int from_solver_fd; diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index d37e6dc..44bbc32 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -28,7 +28,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat uint i = 0; while (hasNextTableEntry(iterator)) { TableEntry *entry = nextTableEntry(iterator); - if (generateNegation == entry->output && undefStatus == IGNOREBEHAVIOR) { + if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) { //Skip the irrelevant entries continue; } @@ -46,7 +46,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat break; case FLAGFORCEUNDEFINED: { addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintNegate(undefConst))); - if (generateNegation == entry->output) { + if (generateNegation == (entry->output != 0)) { continue; } row = constraintAND(This->cnf, inputNum, carray); diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 64f414c..cfa97fd 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -58,8 +58,10 @@ Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ setElementEncodingType(encoding, BINARYINDEX); encodingArrayInitialization(encoding); } - Predicate *predicate =allocPredicateOperator(LT, (Set*[]){order->set, order->set}, 2); - Boolean * boolean=allocBooleanPredicate(predicate, (Element *[]){elem1,elem2}, 2, NULL); + Set * sarray[]={order->set, order->set}; + Predicate *predicate =allocPredicateOperator(LT, sarray, 2); + Element * parray[]={elem1, elem2}; + Boolean * boolean=allocBooleanPredicate(predicate, parray, 2, NULL); setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT); {//Adding new elements and boolean/predicate to solver regarding memory management pushVectorBoolean(This->solver->allBooleans, boolean); diff --git a/src/Encoders/orderencoder.cc b/src/Encoders/orderencoder.cc index 99f826b..80558f3 100644 --- a/src/Encoders/orderencoder.cc +++ b/src/Encoders/orderencoder.cc @@ -119,7 +119,7 @@ void completePartialOrderGraph(OrderGraph *graph) { //Compute in set for entire SCC uint rSize = getSizeVectorOrderNode(&sccNodes); - for (int j = 0; j < rSize; j++) { + for (uint j = 0; j < rSize; j++) { OrderNode *rnode = getVectorOrderNode(&sccNodes, j); //Compute source sets HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges); @@ -134,7 +134,7 @@ void completePartialOrderGraph(OrderGraph *graph) { } deleteIterOrderEdge(iterator); } - for (int j=0; j < rSize; j++) { + for (uint j=0; j < rSize; j++) { //Copy in set of entire SCC OrderNode *rnode = getVectorOrderNode(&sccNodes, j); HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources); diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc index 9d12a05..d0b2976 100644 --- a/src/Test/logicopstest.cc +++ b/src/Test/logicopstest.cc @@ -13,12 +13,17 @@ int main(int numargs, char **argv) { Boolean *b3 = getBooleanVar(solver, 0); Boolean *b4 = getBooleanVar(solver, 0); //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES - Boolean *andb1b2 = applyLogicalOperation(solver, L_AND,(Boolean *[]) {b1, b2}, 2); - Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, (Boolean *[]) {andb1b2, b3}, 2); + Boolean * barray1[]={b1,b2}; + Boolean *andb1b2 = applyLogicalOperation(solver, L_AND, barray1, 2); + Boolean * barray2[]={andb1b2, b3}; + Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, barray2, 2); addConstraint(solver, imply); - Boolean *notb3 = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {b3}, 1); - addConstraint(solver, applyLogicalOperation(solver, L_OR, (Boolean *[]) {notb3, b4}, 2)); - addConstraint(solver, applyLogicalOperation(solver, L_XOR, (Boolean * []) {b1, b4}, 2)); + Boolean * barray3[] ={b3}; + Boolean *notb3 = applyLogicalOperation(solver, L_NOT, barray3, 1); + Boolean * barray4[] ={notb3, b4}; + addConstraint(solver, applyLogicalOperation(solver, L_OR, barray4, 2)); + Boolean * barray5[] ={b1, b4}; + addConstraint(solver, applyLogicalOperation(solver, L_XOR, barray5, 2)); if (startEncoding(solver) == 1) printf("b1=%d b2=%d b3=%d b4=%d\n", getBooleanValue(solver,b1), getBooleanValue(solver, b2), @@ -26,4 +31,4 @@ int main(int numargs, char **argv) { else printf("UNSAT\n"); deleteSolver(solver); -} \ No newline at end of file +} diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index 646b195..f32d447 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -16,6 +16,7 @@ int main(int numargs, char **argv) { Boolean *o58 = orderConstraint(solver, order, 5, 8); Boolean *o81 = orderConstraint(solver, order, 8, 1); + /* addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) ); Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2); Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1); @@ -32,6 +33,6 @@ int main(int numargs, char **argv) { if (startEncoding(solver) == 1) printf("SAT\n"); else - printf("UNSAT\n"); + printf("UNSAT\n");*/ deleteSolver(solver); -} \ No newline at end of file +} diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc index a7b9412..98b4a27 100644 --- a/src/Test/tablefuncencodetest.cc +++ b/src/Test/tablefuncencodetest.cc @@ -41,7 +41,8 @@ int main(int numargs, char **argv) { addTableEntry(solver, t1, row5, 2, 3); addTableEntry(solver, t1, row6, 2, 5); Function *f1 = completeTable(solver, t1, FLAGIFFUNDEFINED); - Element *e3 = applyFunction(solver, f1, (Element * []) {e1,e2}, 2, overflow); + Element * tmparray[]={e1, e2}; + Element *e3 = applyFunction(solver, f1, tmparray, 2, overflow); Set *deq[] = {s3,s2}; Predicate *lte = createPredicateOperator(solver, LTE, deq, 2); diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc index ee9094b..4f19f67 100644 --- a/src/Test/tablepredicencodetest.cc +++ b/src/Test/tablepredicencodetest.cc @@ -42,7 +42,8 @@ int main(int numargs, char **argv) { addTableEntry(solver, t1, row6, 3, true); Predicate *p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED); Boolean *undef = getBooleanVar(solver, 2); - Boolean *b1 = applyPredicateTable(solver, p1, (Element * []) {e1, e2, e3}, 3, undef); + Element * tmparray[] = {e1, e2, e3}; + Boolean *b1 = applyPredicateTable(solver, p1, tmparray, 3, undef); addConstraint(solver, b1); Set *deq[] = {s3,s2}; @@ -53,7 +54,8 @@ int main(int numargs, char **argv) { Set *d1[] = {s1, s2}; Predicate *eq = createPredicateOperator(solver, EQUALS, d1, 2); - Boolean *pred2 = applyPredicate(solver, eq,(Element *[]) {e1, e2}, 2); + Element * tmparray2[] = {e1, e2}; + Boolean *pred2 = applyPredicate(solver, eq, tmparray2, 2); addConstraint(solver, pred2); if (startEncoding(solver) == 1) diff --git a/src/csolver.cc b/src/csolver.cc index e9c9526..b4c8208 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -207,7 +207,7 @@ int startEncoding(CSolver *This) { encodeAllSATEncoder(This, satEncoder); int result = solveCNF(satEncoder->cnf); model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize); - for (uint i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) { + for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) { model_print("%d, ", satEncoder->cnf->solver->solution[i]); } model_print("\n"); -- 2.34.1