Edits
authorbdemsky <bdemsky@uci.edu>
Sun, 14 Jan 2018 04:47:16 +0000 (20:47 -0800)
committerbdemsky <bdemsky@uci.edu>
Sun, 14 Jan 2018 04:47:16 +0000 (20:47 -0800)
12 files changed:
src/AST/astops.h
src/ASTAnalyses/Polarity/polarityassignment.cc
src/ASTAnalyses/Polarity/polarityassignment.h
src/ASTTransform/decomposeordertransform.cc
src/Backend/constraint.cc
src/Backend/satelemencoder.cc
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Backend/satfuncopencoder.cc
src/Backend/satfunctableencoder.cc
src/Encoders/elementencoding.cc
src/Encoders/elementencoding.h

index c385ba5..97d2c28 100644 (file)
@@ -25,5 +25,10 @@ enum ElementEncodingType {
 
 typedef enum ElementEncodingType ElementEncodingType;
 
+Polarity negatePolarity(Polarity This);
+bool impliesPolarity(Polarity curr, Polarity goal);
+
+
+
 
 #endif
index 6254832..ef988dd 100644 (file)
@@ -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);
+       }
+}
index 8873ef2..ce5096f 100644 (file)
 
 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);
 
index 7dad1d7..62b0828 100644 (file)
@@ -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();
index f716cce..febccd1 100644 (file)
@@ -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 <newvecedges; i++) {
+               Edge nedge = nnewvec->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);
index 27d5720..1fc1bb4 100644 (file)
@@ -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();
index b6e8da1..eebf4b0 100644 (file)
@@ -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;
        }
index 9750048..2217777 100644 (file)
@@ -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);
index 987f202..6210b99 100644 (file)
@@ -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 {
index 961d810..ea77e99 100644 (file)
@@ -19,11 +19,15 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
        Array<Element *> *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<Element *> *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<Element *> *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<Element *> *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);
 }
index cc96889..031b98f 100644 (file)
@@ -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) {
index 17314e9..346d735 100644 (file)
@@ -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) */