From: bdemsky Date: Sun, 14 Jan 2018 04:47:16 +0000 (-0800) Subject: Edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=f3afe6e2ef7e4c2bcd95000ea3e1e17f9e538789 Edits --- diff --git a/src/AST/astops.h b/src/AST/astops.h index c385ba5..97d2c28 100644 --- a/src/AST/astops.h +++ b/src/AST/astops.h @@ -25,5 +25,10 @@ enum ElementEncodingType { typedef enum ElementEncodingType ElementEncodingType; +Polarity negatePolarity(Polarity This); +bool impliesPolarity(Polarity curr, Polarity goal); + + + #endif diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc index 6254832..ef988dd 100644 --- a/src/ASTAnalyses/Polarity/polarityassignment.cc +++ b/src/ASTAnalyses/Polarity/polarityassignment.cc @@ -12,6 +12,22 @@ void computePolarities(CSolver *This) { delete iterator; } +void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) { + Boolean *bdst = dst.getBoolean(); + Boolean *bsrc = src.getBoolean(); + bool isNegated = dst.isNegated() ^ src.isNegated(); + Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity; + updatePolarity(bdst, p); +} + +void updateEdgePolarity(BooleanEdge dst, Polarity p) { + Boolean *bdst = dst.getBoolean(); + bool isNegated = dst.isNegated(); + if (isNegated) + p=negatePolarity(p); + updatePolarity(bdst, p); +} + bool updatePolarity(Boolean *This, Polarity polarity) { Polarity oldpolarity = This->polarity; Polarity newpolarity = (Polarity) (This->polarity | polarity); @@ -54,20 +70,6 @@ void computeLogicOpPolarity(BooleanLogic *This) { } } -Polarity negatePolarity(Polarity This) { - switch (This) { - case P_UNDEFINED: - case P_BOTHTRUEFALSE: - return This; - case P_TRUE: - return P_FALSE; - case P_FALSE: - return P_TRUE; - default: - ASSERT(0); - } -} - BooleanValue negateBooleanValue(BooleanValue This) { switch (This) { case BV_UNDEFINED: @@ -94,3 +96,17 @@ Polarity computeLogicOpPolarityChildren(BooleanLogic *This) { ASSERT(0); } } + +Polarity negatePolarity(Polarity This) { + switch (This) { + case P_UNDEFINED: + case P_BOTHTRUEFALSE: + return This; + case P_TRUE: + return P_FALSE; + case P_FALSE: + return P_TRUE; + default: + ASSERT(0); + } +} diff --git a/src/ASTAnalyses/Polarity/polarityassignment.h b/src/ASTAnalyses/Polarity/polarityassignment.h index 8873ef2..ce5096f 100644 --- a/src/ASTAnalyses/Polarity/polarityassignment.h +++ b/src/ASTAnalyses/Polarity/polarityassignment.h @@ -15,11 +15,12 @@ void computePolarities(CSolver *This); bool updatePolarity(Boolean *This, Polarity polarity); +void updateEdgePolarity(BooleanEdge dst, BooleanEdge src); +void updateEdgePolarity(BooleanEdge dst, Polarity polarity); void updateMustValue(Boolean *This, BooleanValue value); void computePolarity(Boolean *boolean, Polarity polarity); void computePredicatePolarity(BooleanPredicate *This); void computeLogicOpPolarity(BooleanLogic *boolean); -Polarity negatePolarity(Polarity This); BooleanValue negateBooleanValue(BooleanValue This); Polarity computeLogicOpPolarityChildren(BooleanLogic *boolean); diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 7dad1d7..62b0828 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -16,6 +16,7 @@ #include "decomposeorderresolver.h" #include "tunable.h" #include "orderanalysis.h" +#include "polarityassignment.h" DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver) @@ -153,6 +154,7 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG } BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second); solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint); + updateEdgePolarity(neworderconstraint, orderconstraint); dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum); } } @@ -212,6 +214,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode } //Add new order constraint BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID()); + updateEdgePolarity(orderconstraint, P_TRUE); solver->addConstraint(orderconstraint); //Add new edge @@ -324,6 +327,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID()); BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID()); + updateEdgePolarity(benew, be); solver->replaceBooleanWithBoolean(be, benew); } dstnode->inEdges.reset(); @@ -353,6 +357,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID()); BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID()); + updateEdgePolarity(benew, be); solver->replaceBooleanWithBoolean(be, benew); } dstnode->outEdges.reset(); diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index f716cce..febccd1 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -5,38 +5,7 @@ #include "common.h" #include "qsort.h" /* - V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios, - Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon. - - Permission is hereby granted, free of charge, to any person obtaining - a copy of this software and associated documentation files (the - "Software"), to deal in the Software without restriction, including - without limitation the rights to use, copy, modify, merge, publish, - distribute, sublicense, and/or sell copies of the Software, and to - permit persons to whom the Software is furnished to do so, subject to - the following conditions: - - The above copyright notice and this permission notice shall be - included in all copies or substantial portions of the Software. If - you download or use the software, send email to Pete Manolios - (pete@ccs.neu.edu) with your name, contact information, and a short - note describing what you want to use BAT for. For any reuse or - distribution, you must make clear to others the license terms of this - work. - - Contact Pete Manolios if you want any of these conditions waived. - - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, - EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF - MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND - NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE - LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION - OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION - WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. - */ - -/* - C port of CNF SAT Conversion Copyright Brian Demsky 2017. + CNF SAT Conversion Copyright Brian Demsky 2017. */ @@ -395,6 +364,190 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) { return result; } +Edge disjoinLit(Edge vec, Edge lit) { + Node *nvec = vec.node_ptr; + uint nvecedges = nvec->numEdges; + + for(uint i=0; i < nvecedges; i++) { + Edge ce = nvec->edges[i]; + if (!edgeIsVarConst(ce)) { + Node *cne = ce.node_ptr; + addEdgeToResizeNode(&cne, lit); + nvec->edges[i] = (Edge) {cne}; + } else { + Node *clause = allocResizeNode(2); + addEdgeToResizeNode(&clause, lit); + addEdgeToResizeNode(&clause, ce); + nvec->edges[i] = (Edge) {clause}; + } + } + return vec; +} + +Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) { + Node * result = allocResizeNode(1); + Node *nnewvec = newvec.node_ptr; + Node *ncnfform = cnfform.node_ptr; + uint newvecedges = nnewvec->numEdges; + uint cnfedges = ncnfform->numEdges; + if (newvecedges == 1 || cnfedges ==1) { + if (cnfedges != 1) { + Node *tmp = nnewvec; + nnewvec = ncnfform; + ncnfform = tmp; + newvecedges = cnfedges; + cnfedges = 1; + } + Edge e = ncnfform->edges[0]; + if (!edgeIsVarConst(e)) { + Node *n = e.node_ptr; + for(uint i=0; i < newvecedges; i++) { + Edge ce = nnewvec->edges[i]; + if (isNodeEdge(ce)) { + Node *cne = ce.node_ptr; + mergeNodeToResizeNode(&cne, n); + nnewvec->edges[i] = (Edge) {cne}; + } else { + Node *clause = allocResizeNode(n->numEdges + 1); + mergeNodeToResizeNode(&clause, n); + addEdgeToResizeNode(&clause, ce); + nnewvec->edges[i] = (Edge) {clause}; + } + } + } else { + for(uint i=0; i < newvecedges; i++) { + Edge ce = nnewvec->edges[i]; + if (!edgeIsVarConst(ce)) { + Node *cne = ce.node_ptr; + addEdgeToResizeNode(&cne, e); + nnewvec->edges[i] = (Edge) {cne}; + } else { + Node *clause = allocResizeNode(2); + addEdgeToResizeNode(&clause, e); + addEdgeToResizeNode(&clause, ce); + nnewvec->edges[i] = (Edge) {clause}; + } + } + } + freeEdgeCNF((Edge){ncnfform}); + return (Edge) {nnewvec}; + } + if ((newvecedges > 3 && cnfedges > 3) || + (newvecedges > 10 && cnfedges >=2) || + (newvecedges >= 2 && cnfedges > 10)) { + Edge proxyVar = constraintNewVar(cnf); + if (newvecedges > cnfedges) { + outputCNFOR(cnf, newvec, constraintNegate(proxyVar)); + freeEdgeCNF(newvec); + return disjoinLit(cnfform, proxyVar); + } else { + outputCNFOR(cnf, cnfform, constraintNegate(proxyVar)); + freeEdgeCNF(cnfform); + return disjoinLit(newvec, proxyVar); + } + } + for(uint i=0; i edges[i]; + uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1; + for(uint j=0; j < cnfedges; j++) { + Edge cedge = ncnfform->edges[j]; + uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1; + if (equalsEdge(cedge, nedge)) { + addEdgeToResizeNode(&result, cedge); + } else if (!sameNodeOppSign(nedge, cedge)) { + Node *clause = allocResizeNode(cSize + nSize); + if (isNodeEdge(nedge)) { + mergeNodeToResizeNode(&clause, nedge.node_ptr); + } else { + addEdgeToResizeNode(&clause, nedge); + } + if (isNodeEdge(cedge)) { + mergeNodeToResizeNode(&clause, cedge.node_ptr); + } else { + addEdgeToResizeNode(&clause, cedge); + } + addEdgeToResizeNode(&result, (Edge){clause}); + } + //otherwise skip + } + } + freeEdgeCNF(newvec); + freeEdgeCNF(cnfform); + return (Edge) {result}; +} + +Edge simplifyCNF(CNF *cnf, Edge input) { + if (edgeIsVarConst(input)) { + Node *newvec = allocResizeNode(1); + addEdgeToResizeNode(&newvec, input); + return (Edge) {newvec}; + } + bool negated = isNegEdge(input); + Node * node = getNodePtrFromEdge(input); + NodeType type = node->type; + if (!negated) { + if (type == NodeType_AND) { + //AND case + Node *newvec = allocResizeNode(node->numEdges); + uint numEdges = node->numEdges; + for(uint i = 0; i < numEdges; i++) { + Edge e = simplifyCNF(cnf, node->edges[i]); + mergeFreeNodeToResizeNode(&newvec, e.node_ptr); + } + return (Edge) {newvec}; + } else { + Edge cond = node->edges[0]; + Edge thenedge = node->edges[1]; + Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2]; + Edge thenedges[] = {cond, constraintNegate(thenedge)}; + Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges)); + Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)}; + Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges)); + Edge thencnf = simplifyCNF(cnf, thencons); + Edge elsecnf = simplifyCNF(cnf, elsecons); + //free temporary nodes + ourfree(getNodePtrFromEdge(thencons)); + ourfree(getNodePtrFromEdge(elsecons)); + Node * result = thencnf.node_ptr; + mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr); + return (Edge) {result}; + } + } else { + if (type == NodeType_AND) { + //OR Case + uint numEdges = node->numEdges; + + Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0])); + for(uint i = 1; i < numEdges; i++) { + Edge e = node->edges[i]; + Edge cnfform = simplifyCNF(cnf, constraintNegate(e)); + newvec = disjoinAndFree(cnf, newvec, cnfform); + } + return newvec; + } else { + Edge cond = node->edges[0]; + Edge thenedge = node->edges[1]; + Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2]; + + + Edge thenedges[] = {cond, constraintNegate(thenedge)}; + Edge thencons = createNode(NodeType_AND, 2, thenedges); + Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)}; + Edge elsecons = createNode(NodeType_AND, 2, elseedges); + + Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)}; + Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges)); + Edge result = simplifyCNF(cnf, combined); + //free temporary nodes + ourfree(getNodePtrFromEdge(thencons)); + ourfree(getNodePtrFromEdge(elsecons)); + ourfree(getNodePtrFromEdge(combined)); + return result; + } + } +} + +/* Edge simplifyCNF(CNF *cnf, Edge input) { if (edgeIsVarConst(input)) { Node *newvec = allocResizeNode(1); @@ -564,7 +717,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) { } } } - +*/ void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) { Node * andNode = cnfform.node_ptr; int orvar = getEdgeVar(eorvar); @@ -624,14 +777,16 @@ void outputCNF(CNF *cnf, Edge cnfform) { } void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) { - if (P_TRUE || P_BOTHTRUEFALSE) { + ASSERT(p != P_UNDEFINED); + if (p == P_TRUE || p == P_BOTHTRUEFALSE) { // proxy => expression Edge cnfexpr = simplifyCNF(cnf, expression); - freeEdgeRec(expression); + if (p == P_TRUE) + freeEdgeRec(expression); outputCNFOR(cnf, cnfexpr, constraintNegate(proxy)); freeEdgeCNF(cnfexpr); } - if (P_FALSE || P_BOTHTRUEFALSE) { + if (p == P_FALSE || p == P_BOTHTRUEFALSE) { // expression => proxy Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression)); freeEdgeRec(expression); diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 27d5720..1fc1bb4 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -4,17 +4,98 @@ #include "ops.h" #include "element.h" #include "set.h" +#include "predicate.h" -Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) { + +void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) { + uint numParents = elem->parents.getSize(); + uint posPolarity = 0; + uint negPolarity = 0; + memo = false; + if (elem->type == ELEMFUNCRETURN) { + memo = true; + } + for(uint i = 0; i < numParents; i++) { + ASTNode * node = elem->parents.get(i); + if (node->type == PREDICATEOP) { + BooleanPredicate * pred = (BooleanPredicate *) node; + Polarity polarity = pred->polarity; + FunctionEncodingType encType = pred->encoding.type; + bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; + if (pred->predicate->type == TABLEPRED) { + //Could be smarter, but just do default thing for now + + UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior; + + Polarity tpolarity=polarity; + if (generateNegation) + tpolarity = negatePolarity(tpolarity); + if (undefStatus ==SATC_FLAGFORCEUNDEFINED) + tpolarity = P_BOTHTRUEFALSE; + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE) + memo = true; + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE) + memo = true; + } else if (pred->predicate->type == OPERATORPRED) { + if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) { + Polarity tpolarity = polarity; + if (generateNegation) + tpolarity = negatePolarity(tpolarity); + PredicateOperator *predicate = (PredicateOperator *)pred->predicate; + uint numDomains = predicate->domains.getSize(); + bool isConstant = true; + for (uint i = 0; i < numDomains; i++) { + Element *e = pred->inputs.get(i); + if (elem != e && e->type != ELEMCONST) { + isConstant = false; + } + } + if (predicate->getOp() == SATC_EQUALS) { + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE) + posPolarity++; + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE) + negPolarity++; + } else { + if (isConstant) { + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE) + posPolarity++; + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE) + negPolarity++; + } else { + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE) + memo = true; + if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE) + memo = true; + } + } + } + } else { + ASSERT(0); + } + } else if (node->type == ELEMFUNCRETURN) { + //we are input to function, so memoize negative case + memo = true; + } else { + ASSERT(0); + } + } + if (posPolarity > 1) + memo = true; + if (negPolarity > 1) + memo = true; +} + + +Edge SATEncoder::getElementValueConstraint(Element *elem, Polarity p, uint64_t value) { switch (elem->getElementEncoding()->type) { case ONEHOT: - return getElementValueOneHotConstraint(elem, value); + return getElementValueOneHotConstraint(elem, p, value); case UNARY: - return getElementValueUnaryConstraint(elem, value); + return getElementValueUnaryConstraint(elem, p, value); case BINARYINDEX: - return getElementValueBinaryIndexConstraint(elem, value); + return getElementValueBinaryIndexConstraint(elem, p, value); case BINARYVAL: - return getElementValueBinaryValueConstraint(elem, value); + return getElementValueBinaryValueConstraint(elem, p, value); break; default: ASSERT(0); @@ -23,19 +104,60 @@ Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) { return E_BOGUS; } -Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) { +bool impliesPolarity(Polarity curr, Polarity goal) { + return (((int) curr) & ((int)goal)) == ((int) goal); +} + +Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p, uint64_t value) { ASTNodeType type = elem->type; ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST); ElementEncoding *elemEnc = elem->getElementEncoding(); + + //Check if we need to generate proxy variables + if (elemEnc->encoding == EENC_UNKNOWN && elemEnc->numVars > 1) { + bool memo = false; + shouldMemoize(elem, value, memo); + if (memo) { + elemEnc->encoding = EENC_BOTH; + elemEnc->polarityArray = (Polarity *) ourcalloc(1, sizeof(Polarity) * elemEnc->encArraySize); + elemEnc->edgeArray = (Edge *) ourcalloc(1, sizeof(Edge) * elemEnc->encArraySize); + } else { + elemEnc->encoding = EENC_NONE; + } + } + for (uint i = 0; i < elemEnc->encArraySize; i++) { if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) { - return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i); + if (elemEnc->numVars == 0) + return E_True; + + if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) { + if (impliesPolarity(elemEnc->polarityArray[i], p)) { + return elemEnc->edgeArray[i]; + } else { + if (edgeIsNull(elemEnc->edgeArray[i])) { + elemEnc->edgeArray[i] = constraintNewVar(cnf); + } + if (elemEnc->polarityArray[i] == P_UNDEFINED && p == P_BOTHTRUEFALSE) { + generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE); + elemEnc->polarityArray[i] = p; + } else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE) && impliesPolarity(p, P_TRUE)) { + generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE); + elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_TRUE)); + } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE) && impliesPolarity(p, P_FALSE)) { + generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE); + elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_FALSE)); + } + return elemEnc->edgeArray[i]; + } + } + return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i); } } return E_False; } -Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) { +Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value) { ASTNodeType type = elem->type; ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST); ElementEncoding *elemEnc = elem->getElementEncoding(); @@ -47,7 +169,7 @@ Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) return E_False; } -Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) { +Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value) { ASTNodeType type = elem->type; ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST); ElementEncoding *elemEnc = elem->getElementEncoding(); @@ -66,7 +188,7 @@ Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) { return E_False; } -Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) { +Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value) { ASTNodeType type = element->type; ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); ElementEncoding *elemEnc = element->getElementEncoding(); diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index b6e8da1..eebf4b0 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -68,9 +68,11 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) { model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type); exit(-1); } - if (constraint->parents.getSize() > 1) { + Polarity p = constraint->polarity; + uint pSize = constraint->parents.getSize(); + if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) { Edge e = getNewVarSATEncoder(); - generateProxy(cnf, result, e, constraint->polarity); + generateProxy(cnf, result, e, p); booledgeMap.put(constraint, e.node_ptr); result = e; } diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 9750048..2217777 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -22,6 +22,7 @@ public: CMEMALLOC; private: + void shouldMemoize(Element *elem, uint64_t val, bool & memo); Edge getNewVarSATEncoder(); void getArrayNewVarsSATEncoder(uint num, Edge *carray); Edge encodeVarSATEncoder(BooleanVar *constraint); @@ -31,11 +32,11 @@ private: void encodeElementSATEncoder(Element *element); void encodeElementFunctionSATEncoder(ElementFunction *function); void encodeTableElementFunctionSATEncoder(ElementFunction *This); - Edge getElementValueOneHotConstraint(Element *elem, uint64_t value); - Edge getElementValueUnaryConstraint(Element *elem, uint64_t value); - Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value); - Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value); - Edge getElementValueConstraint(Element *element, uint64_t value); + Edge getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value); + Edge getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value); + Edge getElementValueBinaryIndexConstraint(Element *element, Polarity p, uint64_t value); + Edge getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value); + Edge getElementValueConstraint(Element *element, Polarity p, uint64_t value); void generateOneHotEncodingVars(ElementEncoding *encoding); void generateUnaryEncodingVars(ElementEncoding *encoding); void generateBinaryIndexEncodingVars(ElementEncoding *encoding); diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 987f202..6210b99 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -25,9 +25,11 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) { PredicateOperator *predicate = (PredicateOperator *)constraint->predicate; uint numDomains = predicate->domains.getSize(); - + Polarity polarity = constraint->polarity; FunctionEncodingType encType = constraint->encoding.type; bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; + if (generateNegation) + polarity = negatePolarity(polarity); /* Call base encoders for children */ for (uint i = 0; i < numDomains; i++) { @@ -53,7 +55,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra //Include this in the set of terms for (uint i = 0; i < numDomains; i++) { Element *elem = constraint->inputs.get(i); - carray[i] = getElementValueConstraint(elem, vals[i]); + carray[i] = getElementValueConstraint(elem, polarity, vals[i]); } Edge term = constraintAND(cnf, numDomains, carray); pushVectorEdge(clauses, term); @@ -108,8 +110,6 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) vals[i] = set->getElement(indices[i]); } - Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus); - bool notfinished = true; while (notfinished) { Edge carray[numDomains + 1]; @@ -125,10 +125,10 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) //Include this in the set of terms for (uint i = 0; i < numDomains; i++) { Element *elem = func->inputs.get(i); - carray[i] = getElementValueConstraint(elem, vals[i]); + carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]); } if (isInRange) { - carray[numDomains] = getElementValueConstraint(func, result); + carray[numDomains] = getElementValueConstraint(func, P_TRUE, result); } Edge clause; @@ -140,6 +140,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) break; } case SATC_FLAGFORCESOVERFLOW: { + Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus); clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint))); break; } @@ -147,11 +148,13 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) if (isInRange) { clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]); } else { + Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus); clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint); } break; } case SATC_FLAGIFFOVERFLOW: { + Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus); if (isInRange) { clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint))); } else { diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 961d810..ea77e99 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -19,11 +19,15 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con Array *inputs = &constraint->inputs; uint inputNum = inputs->getSize(); uint size = table->getSize(); + Polarity polarity = constraint->polarity; bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; + if (generateNegation) + polarity = negatePolarity(polarity); + if (undefStatus ==SATC_FLAGFORCEUNDEFINED) + polarity = P_BOTHTRUEFALSE; + Edge constraints[size]; - Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus); - printCNF(undefConst); - model_print("**\n"); + SetIteratorTableEntry *iterator = table->getEntries(); uint i = 0; while (iterator->hasNext()) { @@ -35,9 +39,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con Edge carray[inputNum]; for (uint j = 0; j < inputNum; j++) { Element *el = inputs->get(j); - carray[j] = getElementValueConstraint(el, entry->inputs[j]); - printCNF(carray[j]); - model_print("\n"); + carray[j] = getElementValueConstraint(el, polarity, entry->inputs[j]); } Edge row; switch (undefStatus) { @@ -45,33 +47,35 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con row = constraintAND(cnf, inputNum, carray); break; case SATC_FLAGFORCEUNDEFINED: { - addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintNegate(undefConst))); + Edge proxy = constraintNewVar(cnf); + generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE); + Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus); + addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy, constraintNegate(undefConst))); if (generateNegation == (entry->output != 0)) { continue; } - row = constraintAND(cnf, inputNum, carray); + row = proxy; break; } default: ASSERT(0); } constraints[i++] = row; - printCNF(row); - - model_print("\n\n"); } delete iterator; ASSERT(i != 0); Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints)) : constraintOR(cnf, i, constraints); - printCNF(result); return result; } + Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) { #ifdef TRACE_DEBUG model_print("Enumeration Table Predicate ...\n"); #endif ASSERT(constraint->predicate->type == TABLEPRED); + Polarity polarity = constraint->polarity; + //First encode children Array *inputs = &constraint->inputs; uint inputNum = inputs->getSize(); @@ -90,6 +94,9 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE; uint numDomains = predicate->table->numDomains(); + if (generateNegation) + polarity = negatePolarity(polarity); + VectorEdge *clauses = allocDefVectorEdge(); uint indices[numDomains]; //setup indices @@ -101,8 +108,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint vals[i] = set->getElement(indices[i]); } bool hasOverflow = false; - Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus); - printCNF(undefConstraint); + bool notfinished = true; while (notfinished) { Edge carray[numDomains]; @@ -114,7 +120,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint Edge clause; for (uint i = 0; i < numDomains; i++) { Element *elem = constraint->inputs.get(i); - carray[i] = getElementValueConstraint(elem, vals[i]); + carray[i] = getElementValueConstraint(elem, polarity, vals[i]); } switch (predicate->undefinedbehavior) { @@ -122,10 +128,12 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint if (isInRange) { clause = constraintAND(cnf, numDomains, carray); } else { + Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus); addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) ); } break; - case SATC_FLAGIFFUNDEFINED: + case SATC_FLAGIFFUNDEFINED: { + Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus); if (isInRange) { clause = constraintAND(cnf, numDomains, carray); addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint))); @@ -133,7 +141,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) ); } break; - + } default: ASSERT(0); } @@ -166,6 +174,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint ASSERT(getSizeVectorEdge(clauses) != 0); result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); if (hasOverflow) { + Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus); result = constraintOR2(cnf, result, undefConstraint); } if (generateNegation) { @@ -180,6 +189,7 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior; ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED); Array *elements = &func->inputs; + Table *table = ((FunctionTable *) (func->getFunction()))->table; uint size = table->getSize(); Edge constraints[size]; @@ -192,28 +202,25 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) Edge carray[inputNum]; for (uint j = 0; j < inputNum; j++) { Element *el = elements->get(j); - carray[j] = getElementValueConstraint(el, entry->inputs[j]); + carray[j] = getElementValueConstraint(el, P_FALSE, entry->inputs[j]); } - Edge output = getElementValueConstraint(func, entry->output); - Edge row; + Edge output = getElementValueConstraint(func, P_TRUE, entry->output); switch (undefStatus ) { case SATC_IGNOREBEHAVIOR: { - row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output); + addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output)); break; } case SATC_FLAGFORCEUNDEFINED: { Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus); - row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))); + addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)))); break; } default: ASSERT(0); } - constraints[i++] = row; } delete iterator; - addConstraintCNF(cnf, constraintAND(cnf, size, constraints)); } void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) { @@ -221,6 +228,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc model_print("Enumeration Table functions ...\n"); #endif ASSERT(elemFunc->getFunction()->type == TABLEFUNC); + //First encode children Array *elements = &elemFunc->inputs; for (uint i = 0; i < elements->getSize(); i++) { @@ -239,8 +247,6 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc uint numDomains = function->table->numDomains(); - VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses - uint indices[numDomains]; //setup indices bzero(indices, sizeof(uint) * numDomains); @@ -250,7 +256,6 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc vals[i] = set->getElement(indices[i]); } - Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus); bool notfinished = true; while (notfinished) { Edge carray[numDomains + 1]; @@ -259,27 +264,29 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED); for (uint i = 0; i < numDomains; i++) { Element *elem = elemFunc->inputs.get(i); - carray[i] = getElementValueConstraint(elem, vals[i]); + carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]); } if (isInRange) { - carray[numDomains] = getElementValueConstraint(elemFunc, tableEntry->output); + carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, tableEntry->output); } - Edge clause; switch (function->undefBehavior) { case SATC_UNDEFINEDSETSFLAG: { if (isInRange) { - //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG - clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]); + addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains])); } else { + Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus); addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint)); } break; } case SATC_FLAGIFFUNDEFINED: { + Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus); if (isInRange) { - clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]); - addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) )); + Edge freshvar = constraintNewVar(cnf); + addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar )); + addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) )); + addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains])); } else { addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint)); } @@ -294,7 +301,6 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc printCNF(clause); model_print("\n"); #endif - pushVectorEdge(clauses, clause); } notfinished = false; @@ -312,11 +318,4 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc } } } - if (getSizeVectorEdge(clauses) == 0) { - deleteVectorEdge(clauses); - return; - } - Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - addConstraintCNF(cnf, cor); - deleteVectorEdge(clauses); } diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc index cc96889..031b98f 100644 --- a/src/Encoders/elementencoding.cc +++ b/src/Encoders/elementencoding.cc @@ -13,7 +13,10 @@ ElementEncoding::ElementEncoding(Element *_element) : variables(NULL), encodingArray(NULL), inUseArray(NULL), + edgeArray(NULL), + polarityArray(NULL), encArraySize(0), + encoding(EENC_UNKNOWN), numVars(0) { } @@ -24,6 +27,10 @@ ElementEncoding::~ElementEncoding() { ourfree(encodingArray); if (inUseArray != NULL) ourfree(inUseArray); + if (edgeArray != NULL) + ourfree(edgeArray); + if (polarityArray != NULL) + ourfree(polarityArray); } void ElementEncoding::allocEncodingArrayElement(uint size) { diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index 17314e9..346d735 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -4,6 +4,8 @@ #include "naiveencoder.h" #include "constraint.h" +typedef enum ElemEnc {EENC_UNKNOWN, EENC_NONE, EENC_BOTH} ElemEnc; + class ElementEncoding { public: ElementEncoding(Element *element); @@ -38,7 +40,10 @@ public: struct { uint64_t *encodingArray; /* List the Variables in the appropriate order */ uint64_t *inUseArray; /* Bitmap to track variables in use */ + Edge * edgeArray; + Polarity * polarityArray; uint encArraySize; + ElemEnc encoding; }; struct { uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */