typedef enum ElementEncodingType ElementEncodingType;
+Polarity negatePolarity(Polarity This);
+bool impliesPolarity(Polarity curr, Polarity goal);
+
+
+
#endif
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);
}
}
-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:
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);
+ }
+}
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);
#include "decomposeorderresolver.h"
#include "tunable.h"
#include "orderanalysis.h"
+#include "polarityassignment.h"
DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
}
BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
+ updateEdgePolarity(neworderconstraint, orderconstraint);
dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
}
}
}
//Add new order constraint
BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+ updateEdgePolarity(orderconstraint, P_TRUE);
solver->addConstraint(orderconstraint);
//Add new edge
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();
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();
#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.
*/
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);
}
}
}
-
+*/
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
Node * andNode = cnfform.node_ptr;
int orvar = getEdgeVar(eorvar);
}
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);
#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);
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();
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();
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();
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;
}
CMEMALLOC;
private:
+ void shouldMemoize(Element *elem, uint64_t val, bool & memo);
Edge getNewVarSATEncoder();
void getArrayNewVarsSATEncoder(uint num, Edge *carray);
Edge encodeVarSATEncoder(BooleanVar *constraint);
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);
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++) {
//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);
vals[i] = set->getElement(indices[i]);
}
- Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
-
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains + 1];
//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;
break;
}
case SATC_FLAGFORCESOVERFLOW: {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
break;
}
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 {
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()) {
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) {
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();
bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
uint numDomains = predicate->table->numDomains();
+ if (generateNegation)
+ polarity = negatePolarity(polarity);
+
VectorEdge *clauses = allocDefVectorEdge();
uint indices[numDomains]; //setup indices
vals[i] = set->getElement(indices[i]);
}
bool hasOverflow = false;
- Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
- printCNF(undefConstraint);
+
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains];
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) {
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)));
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
-
+ }
default:
ASSERT(0);
}
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) {
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];
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) {
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++) {
uint numDomains = function->table->numDomains();
- VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
-
uint indices[numDomains]; //setup indices
bzero(indices, sizeof(uint) * numDomains);
vals[i] = set->getElement(indices[i]);
}
- Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains + 1];
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));
}
printCNF(clause);
model_print("\n");
#endif
- pushVectorEdge(clauses, clause);
}
notfinished = false;
}
}
}
- if (getSizeVectorEdge(clauses) == 0) {
- deleteVectorEdge(clauses);
- return;
- }
- Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(cnf, cor);
- deleteVectorEdge(clauses);
}
variables(NULL),
encodingArray(NULL),
inUseArray(NULL),
+ edgeArray(NULL),
+ polarityArray(NULL),
encArraySize(0),
+ encoding(EENC_UNKNOWN),
numVars(0) {
}
ourfree(encodingArray);
if (inUseArray != NULL)
ourfree(inUseArray);
+ if (edgeArray != NULL)
+ ourfree(edgeArray);
+ if (polarityArray != NULL)
+ ourfree(polarityArray);
}
void ElementEncoding::allocEncodingArrayElement(uint size) {
#include "naiveencoder.h"
#include "constraint.h"
+typedef enum ElemEnc {EENC_UNKNOWN, EENC_NONE, EENC_BOTH} ElemEnc;
+
class ElementEncoding {
public:
ElementEncoding(Element *element);
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) */
projects / satune.git / commitdiff