From: bdemsky Date: Tue, 11 Jul 2017 04:19:24 +0000 (-0700) Subject: It compiles X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e665793f5f5cf1cc673b4d21d7983fce30f89134;p=satune.git It compiles --- diff --git a/src/AST/boolean.c b/src/AST/boolean.c index 3166c5d..4fd2c86 100644 --- a/src/AST/boolean.c +++ b/src/AST/boolean.c @@ -8,7 +8,7 @@ Boolean* allocBoolean(VarType t) { BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar)); GETBOOLEANTYPE(tmp)=BOOLEANVAR; tmp->vtype=t; - tmp->var=NULL; + tmp->var=E_NULL; allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp)); return & tmp->base; } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index a59aff1..7382908 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -6,6 +6,7 @@ #include "structs.h" #include "astnode.h" #include "functionencoding.h" +#include "constraint.h" /** This is a little sketchy, but apparently legit. @@ -29,7 +30,7 @@ struct BooleanOrder { struct BooleanVar { Boolean base; VarType vtype; - Constraint * var; + Edge var; }; struct BooleanLogic { diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c index 46c8c5e..6065e5f 100644 --- a/src/Backend/constraint.c +++ b/src/Backend/constraint.c @@ -1,422 +1,860 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - #include "constraint.h" -#include "mymemory.h" +#include +#include #include "inc_solver.h" +#include "cnfexpr.h" -Constraint ctrue={TRUE, 0xffffffff, NULL, NULL}; -Constraint cfalse={FALSE, 0xffffffff, NULL, NULL}; - -Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) { - Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint)); - This->type=t; - This->numoperandsorvar=2; - This->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *)); - This->neg=NULL; - ASSERT(l!=NULL); - //if (type==IMPLIES) { - //type=OR; - // operands[0]=l->negate(); - // } else { - This->operands[0]=l; - // } - This->operands[1]=r; - return This; -} - -Constraint * allocUnaryConstraint(CType t, Constraint *l) { - Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint)); - This->type=t; - This->numoperandsorvar=1; - This->operands=(Constraint **) ourmalloc(sizeof(Constraint *)); - This->neg=NULL; - This->operands[0]=l; - return This; -} - -Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) { - Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint)); - This->type=t; - This->numoperandsorvar=num; - This->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *)); - This->neg=NULL; - memcpy(This->operands, array, num*sizeof(Constraint *)); - return This; -} - -Constraint * allocVarConstraint(CType t, uint v) { - Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint)); - This->type=t; - This->numoperandsorvar=v; - This->operands=NULL; - This->neg=NULL; - return This; -} - -void deleteConstraint(Constraint *This) { - if (This->operands!=NULL) - ourfree(This->operands); - ourfree(This); -} - -void dumpConstraint(Constraint * This, IncrementalSolver *solver) { - if (This->type==VAR) { - addClauseLiteral(solver, This->numoperandsorvar); - addClauseLiteral(solver, 0); - } else if (This->type==NOTVAR) { - addClauseLiteral(solver, -This->numoperandsorvar); - addClauseLiteral(solver, 0); - } else { - ASSERT(This->type==OR); - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=This->operands[i]; - if (c->type==VAR) { - addClauseLiteral(solver, c->numoperandsorvar); - } else if (c->type==NOTVAR) { - addClauseLiteral(solver, -c->numoperandsorvar); - } else ASSERT(0); - } - addClauseLiteral(solver, 0); +/* +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. +*/ + + +VectorImpl(Edge, Edge, 16) +Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT}; +Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)}; +Edge E_BOGUS={(Node *)0x12345673}; +Edge E_NULL={(Node *)NULL}; + + +CNF * createCNF() { + CNF * cnf=ourmalloc(sizeof(CNF)); + cnf->varcount=1; + cnf->capacity=DEFAULT_CNF_ARRAY_SIZE; + cnf->mask=cnf->capacity-1; + cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity); + cnf->size=0; + cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR); + cnf->enableMatching=true; + allocInlineDefVectorEdge(& cnf->constraints); + allocInlineDefVectorEdge(& cnf->args); + cnf->solver=allocIncrementalSolver(); + return cnf; +} + +void deleteCNF(CNF * cnf) { + for(uint i=0;icapacity;i++) { + Node *n=cnf->node_array[i]; + if (n!=NULL) + ourfree(n); } + deleteVectorArrayEdge(& cnf->constraints); + deleteVectorArrayEdge(& cnf->args); + deleteIncrementalSolver(cnf->solver); + ourfree(cnf->node_array); + ourfree(cnf); } -void internalfreeConstraint(Constraint * This) { - switch(This->type) { - case TRUE: - case FALSE: - case NOTVAR: - case VAR: - return; - case BOGUS: - ASSERT(0); - default: - This->type=BOGUS; - deleteConstraint(This); +void resizeCNF(CNF *cnf, uint newCapacity) { + Node **old_array=cnf->node_array; + Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity); + uint oldCapacity=cnf->capacity; + uint newMask=newCapacity-1; + for(uint i=0;ihashCode; + uint newindex=hashCode & newMask; + for(;;newindex=(newindex+1) & newMask) { + if (new_array[newindex] == NULL) { + new_array[newindex]=n; + break; + } + } } + ourfree(old_array); + cnf->node_array=new_array; + cnf->capacity=newCapacity; + cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR); + cnf->mask=newMask; } -void freerecConstraint(Constraint *This) { - switch(This->type) { - case TRUE: - case FALSE: - case NOTVAR: - case VAR: - return; - case BOGUS: - ASSERT(0); - default: - if (This->operands!=NULL) { - for(uint i=0;inumoperandsorvar;i++) - freerecConstraint(This->operands[i]); +Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) { + Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges); + memcpy(n->edges, edges, sizeof(Edge)*numEdges); + n->flags.type=type; + n->flags.wasExpanded=0; + n->flags.cnfVisitedDown=0; + n->flags.cnfVisitedUp=0; + n->flags.varForced=0; + n->numEdges=numEdges; + n->hashCode=hashcode; + n->intAnnot[0]=0;n->intAnnot[1]=0; + n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL; + return n; +} + +Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) { + if (cnf->size > cnf->maxsize) { + resizeCNF(cnf, cnf->capacity << 1); + } + uint hashvalue=hashNode(type, numEdges, edges); + uint mask=cnf->mask; + uint index=hashvalue & mask; + Node **n_ptr; + for(;;index=(index+1)&mask) { + n_ptr=&cnf->node_array[index]; + if (*n_ptr!=NULL) { + if ((*n_ptr)->hashCode==hashvalue) { + if (compareNodes(*n_ptr, type, numEdges, edges)) { + Edge e={*n_ptr}; + return e; + } + } + } else { + break; } - This->type=BOGUS; - deleteConstraint(This); } + *n_ptr=allocNode(type, numEdges, edges, hashvalue); + Edge e={*n_ptr}; + return e; } +uint hashNode(NodeType type, uint numEdges, Edge * edges) { + uint hashvalue=type ^ numEdges; + for(uint i=0;i> 29); //rotate left by 3 bits + } + return (uint) hashvalue; +} -void printConstraint(Constraint * This) { - switch(This->type) { - case TRUE: - model_print("true"); - break; - case FALSE: - model_print("false"); - break; - case IMPLIES: - model_print("("); - printConstraint(This->operands[0]); - model_print(")"); - model_print("=>"); - model_print("("); - printConstraint(This->operands[1]); - model_print(")"); - break; - case AND: - case OR: - model_print("("); - for(uint i=0;inumoperandsorvar;i++) { - if (i!=0) { - if (This->type==AND) - model_print(" ^ "); - else - model_print(" v "); +bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) { + if (node->flags.type!=type || node->numEdges != numEdges) + return false; + Edge *nodeedges=node->edges; + for(uint i=0;inode_ptr)-((uintptr_t)e2->node_ptr); +} + +Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) { + qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction); + int initindex=0; + while(initindexoperands[i]); + } else + edges[++lowindex]=edges[initindex]; + } + lowindex++; //Make lowindex look like size + + if (lowindex==1) + return edges[0]; + + if (cnf->enableMatching && lowindex==2 && + isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) && + getNodeType(edges[0]) == NodeType_AND && + getNodeType(edges[1]) == NodeType_AND && + getNodeSize(edges[0]) == 2 && + getNodeSize(edges[1]) == 2) { + Edge * e0edges=getEdgeArray(edges[0]); + Edge * e1edges=getEdgeArray(edges[1]); + if (sameNodeOppSign(e0edges[0], e1edges[0])) { + return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1])); + } else if (sameNodeOppSign(e0edges[0], e1edges[1])) { + return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0])); + } else if (sameNodeOppSign(e0edges[1], e1edges[0])) { + return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1])); + } else if (sameNodeOppSign(e0edges[1], e1edges[1])) { + return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0])); } - model_print(")"); - break; - case VAR: - model_print("t%u",This->numoperandsorvar); - break; - case NOTVAR: - model_print("!t%u",This->numoperandsorvar); - break; - default: - model_print("In printingConstraint: %d", This->type); - ASSERT(0); - } -} - -Constraint * cloneConstraint(Constraint * This) { - switch(This->type) { - case TRUE: - case FALSE: - case VAR: - case NOTVAR: - return This; - case IMPLIES: - return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1])); - case AND: - case OR: { - Constraint *array[This->numoperandsorvar]; - for(uint i=0;inumoperandsorvar;i++) { - array[i]=cloneConstraint(This->operands[i]); + } + + return createNode(cnf, NodeType_AND, lowindex, edges); +} + +Edge constraintAND2(CNF * cnf, Edge left, Edge right) { + Edge edges[2]={left, right}; + return constraintAND(cnf, 2, edges); +} + +Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) { + Edge array[2]; + array[0]=left; + array[1]=constraintNegate(right); + Edge eand=constraintAND(cnf, 2, array); + return constraintNegate(eand); +} + +Edge constraintIFF(CNF * cnf, Edge left, Edge right) { + bool negate=!sameSignEdge(left, right); + Edge lpos=getNonNeg(left); + Edge rpos=getNonNeg(right); + + Edge e; + if (equalsEdge(lpos, rpos)) { + e=E_True; + } else if (ltEdge(lpos, rpos)) { + Edge edges[]={lpos, rpos}; + e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges); + } else { + Edge edges[]={rpos, lpos}; + e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges); + } + if (negate) + e=constraintNegate(e); + return e; +} + +Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) { + if (isNegEdge(cond)) { + cond=constraintNegate(cond); + Edge tmp=thenedge; + thenedge=elseedge; + elseedge=tmp; + } + + bool negate = isNegEdge(thenedge); + if (negate) { + thenedge=constraintNegate(thenedge); + elseedge=constraintNegate(elseedge); + } + + Edge result; + if (equalsEdge(cond, E_True)) { + result=thenedge; + } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) { + result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge}); + } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) { + result=constraintIMPLIES(cnf, cond, thenedge); + } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) { + result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge}); + } else if (equalsEdge(thenedge, elseedge)) { + result=thenedge; + } else if (sameNodeOppSign(thenedge, elseedge)) { + if (ltEdge(cond, thenedge)) { + result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge}); + } else { + result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond}); } - return allocArrayConstraint(This->type, This->numoperandsorvar, array); + } else { + Edge edges[]={cond, thenedge, elseedge}; + result=createNode(cnf, NodeType_ITE, 3, edges); } - default: - ASSERT(0); - return NULL; + if (negate) + result=constraintNegate(result); + return result; +} + +void addConstraint(CNF *cnf, Edge constraint) { + pushVectorEdge(&cnf->constraints, constraint); +} + +Edge constraintNewVar(CNF *cnf) { + uint varnum=cnf->varcount++; + Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) }; + return e; +} + +int solveCNF(CNF *cnf) { + countPass(cnf); + convertPass(cnf, false); + finishedClauses(cnf->solver); + return solve(cnf->solver); +} + +bool getValueCNF(CNF *cnf, Edge var) { + Literal l=getEdgeVar(var); + bool isneg=(l<0); + l=abs(l); + return isneg ^ getValueSolver(cnf->solver, l); +} + +void countPass(CNF *cnf) { + uint numConstraints=getSizeVectorEdge(&cnf->constraints); + VectorEdge *ve=allocDefVectorEdge(); + for(uint i=0; iconstraints, i)); } + deleteVectorEdge(ve); } -Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) { - Constraint *carray[numvars]; - for(uint j=0;j>1; +void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) { + //Skip constants and variables... + if (edgeIsVarConst(eroot)) + return; + + clearVectorEdge(stack);pushVectorEdge(stack, eroot); + + bool isMatching=cnf->enableMatching; + + while(getSizeVectorEdge(stack) != 0) { + Edge e=lastVectorEdge(stack); popVectorEdge(stack); + bool polarity=isNegEdge(e); + Node *n=getNodePtrFromEdge(e); + if (getExpanded(n, polarity)) { + if (n->flags.type == NodeType_IFF || + n->flags.type == NodeType_ITE) { + Edge pExp={n->ptrAnnot[polarity]}; + getNodePtrFromEdge(pExp)->intAnnot[0]++; + } else { + n->intAnnot[polarity]++; + } + } else { + setExpanded(n, polarity); + + if (n->flags.type == NodeType_ITE|| + n->flags.type == NodeType_IFF) { + n->intAnnot[polarity]=0; + Edge cond=n->edges[0]; + Edge thenedge=n->edges[1]; + Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2]; + thenedge=constraintNegateIf(thenedge, !polarity); + elseedge=constraintNegateIf(elseedge, !polarity); + thenedge=constraintAND2(cnf, cond, thenedge); + cond=constraintNegate(cond); + elseedge=constraintAND2(cnf, cond, elseedge); + thenedge=constraintNegate(thenedge); + elseedge=constraintNegate(elseedge); + cnf->enableMatching=false; + Edge succ1=constraintAND2(cnf, thenedge, elseedge); + n->ptrAnnot[polarity]=succ1.node_ptr; + cnf->enableMatching=isMatching; + pushVectorEdge(stack, succ1); + if (getExpanded(n, !polarity)) { + Edge succ2={(Node *)n->ptrAnnot[!polarity]}; + Node *n1=getNodePtrFromEdge(succ1); + Node *n2=getNodePtrFromEdge(succ2); + n1->ptrAnnot[0]=succ2.node_ptr; + n2->ptrAnnot[0]=succ1.node_ptr; + n1->ptrAnnot[1]=succ2.node_ptr; + n2->ptrAnnot[1]=succ1.node_ptr; + } + } else { + n->intAnnot[polarity]=1; + for (uint i=0;inumEdges;i++) { + Edge succ=n->edges[i]; + succ=constraintNegateIf(succ, polarity); + if(!edgeIsVarConst(succ)) { + pushVectorEdge(stack, succ); + } + } + } + } } +} - return allocArrayConstraint(AND, numvars, carray); +void convertPass(CNF *cnf, bool backtrackLit) { + uint numConstraints=getSizeVectorEdge(&cnf->constraints); + VectorEdge *ve=allocDefVectorEdge(); + for(uint i=0; iconstraints, i), backtrackLit); + } + deleteVectorEdge(ve); } -/** Generates a constraint to ensure that all encodings are less than value */ -Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) { - Constraint *orarray[numvars]; - Constraint *andarray[numvars]; - uint andi=0; +void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) { + Node *nroot=getNodePtrFromEdge(root); + + if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) { + root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]}; + } + + if (edgeIsConst(root)) { + if (isNegEdge(root)) { + //trivally unsat + Edge newvar=constraintNewVar(cnf); + Literal var=getEdgeVar(newvar); + Literal clause[] = {var}; + addArrayClauseLiteral(cnf->solver, 1, clause); + clause[0]=-var; + addArrayClauseLiteral(cnf->solver, 1, clause); + return; + } else { + //trivially true + return; + } + } else if (edgeIsVarConst(root)) { + Literal clause[] = { getEdgeVar(root)}; + addArrayClauseLiteral(cnf->solver, 1, clause); + return; + } + + clearVectorEdge(stack);pushVectorEdge(stack, root); + while(getSizeVectorEdge(stack)!=0) { + Edge e=lastVectorEdge(stack); + Node *n=getNodePtrFromEdge(e); - while(true) { - uint val=value; - uint ori=0; - for(uint j=0;j>1; + if (edgeIsVarConst(e)) { + popVectorEdge(stack); + continue; + } else if (n->flags.type==NodeType_ITE || + n->flags.type==NodeType_IFF) { + popVectorEdge(stack); + if (n->ptrAnnot[0]!=NULL) + pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]}); + if (n->ptrAnnot[1]!=NULL) + pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]}); + continue; } - //no ones to flip, so bail now... - if (ori==0) { - return allocArrayConstraint(AND, andi, andarray); + + bool needPos = (n->intAnnot[0] > 0); + bool needNeg = (n->intAnnot[1] > 0); + if ((!needPos || n->flags.cnfVisitedUp & 1) && + (!needNeg || n->flags.cnfVisitedUp & 2)) { + popVectorEdge(stack); + } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) || + (needNeg && !(n->flags.cnfVisitedDown & 2))) { + if (needPos) + n->flags.cnfVisitedDown|=1; + if (needNeg) + n->flags.cnfVisitedDown|=2; + for(uint i=0; inumEdges; i++) { + Edge arg=n->edges[i]; + arg=constraintNegateIf(arg, isNegEdge(e)); + pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE + } + } else { + popVectorEdge(stack); + produceCNF(cnf, e); } - andarray[andi++]=allocArrayConstraint(OR, ori, orarray); + } + CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)]; + if (isProxy(cnfExp)) { + Literal l=getProxy(cnfExp); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } else if (backtrackLit) { + Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root)); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } else { + outputCNF(cnf, cnfExp); + } - value=value+(1<<(__builtin_ctz(value))); - //flip the last one + if (!((intptr_t) cnfExp & 1)) { + deleteCNFExpr(cnfExp); + nroot->ptrAnnot[isNegEdge(root)] = NULL; } } -Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) { - if (numvars==0) - return &ctrue; - Constraint *array[numvars*2]; - for(uint i=0;iflags.cnfVisitedUp & (1<ptrAnnot[!isNeg]; + if (isProxy(otherExp)) + l = -getProxy(otherExp); + } else { + Edge semNeg={(Node *) n->ptrAnnot[isNeg]}; + Node * nsemNeg=getNodePtrFromEdge(semNeg); + if (nsemNeg != NULL) { + if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) { + CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg]; + if (isProxy(otherExp)) + l = -getProxy(otherExp); + } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) { + CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg]; + if (isProxy(otherExp)) + l = getProxy(otherExp); + } + } } - return allocArrayConstraint(AND, numvars*2, array); + + if (l == 0) { + Edge newvar = constraintNewVar(cnf); + l = getEdgeVar(newvar); + } + // Output the constraints on the auxiliary variable + constrainCNF(cnf, l, exp); + deleteCNFExpr(exp); + + n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1); + + return l; } -Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) { - Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2); - Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2))); +void produceCNF(CNF * cnf, Edge e) { + CNFExpr* expPos = NULL; + CNFExpr* expNeg = NULL; + Node *n = getNodePtrFromEdge(e); + + if (n->intAnnot[0] > 0) { + expPos = produceConjunction(cnf, e); + } + + if (n->intAnnot[1] > 0) { + expNeg = produceDisjunction(cnf, e); + } - return allocConstraint(AND, imp1, imp2); + /// @todo Propagate constants across semantic negations (this can + /// be done similarly to the calls to propagate shown below). The + /// trick here is that we need to figure out how to get the + /// semantic negation pointers, and ensure that they can have CNF + /// produced for them at the right point + /// + /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false) + + // propagate from positive to negative, negative to positive + if (!propagate(cnf, & expPos, expNeg, true)) + propagate(cnf, & expNeg, expPos, true); + + // The polarity heuristic entails visiting the discovery polarity first + if (isPosEdge(e)) { + saveCNF(cnf, expPos, e, false); + saveCNF(cnf, expNeg, e, true); + } else { + saveCNF(cnf, expNeg, e, true); + saveCNF(cnf, expPos, e, false); + } } -bool mergeandfree(VectorConstraint * to, VectorConstraint * from) { - for(uint i=0;itype==TRUE) - continue; - if (c->type==FALSE) { - for(uint j=i+1;jsolver, 1, clause); + } else { + Literal clause[] = {-getProxy(*dest)}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } + + *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); + } else { + clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); } - pushVectorConstraint(to, c); + return true; } - deleteVectorConstraint(from); return false; } -VectorConstraint * simplifyConstraint(Constraint * This) { - switch(This->type) { - case TRUE: - case VAR: - case NOTVAR: - case FALSE: { - VectorConstraint * vec=allocDefVectorConstraint(); - pushVectorConstraint(vec, This); - return vec; - } - case AND: { - VectorConstraint *vec=allocDefVectorConstraint(); - for(uint i=0;inumoperandsorvar;i++) { - VectorConstraint * subvec=simplifyConstraint(This->operands[i]); - if (mergeandfree(vec, subvec)) { - for(uint j=i+1;jnumoperandsorvar;j++) { - freerecConstraint(This->operands[j]); - } - internalfreeConstraint(This); - return vec; - } +void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) { + Node *n=getNodePtrFromEdge(e); + n->flags.cnfVisitedUp |= (1 << sign); + if (exp == NULL || isProxy(exp)) return; + + if (exp->litSize == 1) { + Literal l = getLiteralLitVector(&exp->singletons, 0); + deleteCNFExpr(exp); + n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1); + } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) { + introProxy(cnf, e, exp, sign); + } else { + n->ptrAnnot[sign] = exp; + } +} + +void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) { + if (alwaysTrueCNF(expr)) { + return; + } else if (alwaysFalseCNF(expr)) { + Literal clause[] = {-lcond}; + addArrayClauseLiteral(cnf->solver, 1, clause); + return; + } + + for(uint i=0;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + Literal clause[] = {-lcond, l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } + for(uint i=0;iclauses);i++) { + LitVector *lv=getVectorLitVector(&expr->clauses,i); + addClauseLiteral(cnf->solver, -lcond); //Add first literal + addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest + } +} + +void outputCNF(CNF *cnf, CNFExpr *expr) { + for(uint i=0;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } + for(uint i=0;iclauses);i++) { + LitVector *lv=getVectorLitVector(&expr->clauses,i); + addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); + } +} + +CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) { + clearVectorEdge(&cnf->args); + + *largestEdge = (Edge) {(Node*) NULL}; + CNFExpr* largest = NULL; + Node *n=getNodePtrFromEdge(e); + int i = n->numEdges; + while (i != 0) { + Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg); + Node * narg = getNodePtrFromEdge(arg); + + if (edgeIsVarConst(arg)) { + pushVectorEdge(&cnf->args, arg); + continue; } - internalfreeConstraint(This); - return vec; - } - case OR: { - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=This->operands[i]; - switch(c->type) { - case TRUE: { - VectorConstraint * vec=allocDefVectorConstraint(); - pushVectorConstraint(vec, c); - freerecConstraint(This); - return vec; - } - case FALSE: { - Constraint *array[This->numoperandsorvar-1]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) { - if (j!=i) - array[index++]=This->operands[j]; + + if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) { + arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]}; + } + + if (narg->intAnnot[isNegEdge(arg)] == 1) { + CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; + if (!isProxy(argExp)) { + if (largest == NULL) { + largest = argExp; + * largestEdge = arg; + continue; + } else if (argExp->litSize > largest->litSize) { + pushVectorEdge(&cnf->args, *largestEdge); + largest = argExp; + * largestEdge = arg; + continue; } - Constraint *cn=allocArrayConstraint(OR, index, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(This); - return vec; } - case VAR: - case NOTVAR: - break; - case OR: { - uint nsize=This->numoperandsorvar+c->numoperandsorvar-1; - Constraint *array[nsize]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) - if (j!=i) - array[index++]=This->operands[j]; - for(uint j=0;jnumoperandsorvar;j++) - array[index++]=c->operands[j]; - Constraint *cn=allocArrayConstraint(OR, nsize, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(This); - internalfreeConstraint(c); - return vec; - } - case IMPLIES: { - uint nsize=This->numoperandsorvar+1; - Constraint *array[nsize]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) - if (j!=i) - array[index++]=This->operands[j]; - array[index++]=negateConstraint(c->operands[0]); - array[index++]=c->operands[1]; - Constraint *cn=allocArrayConstraint(OR, nsize, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(This); - internalfreeConstraint(c); - return vec; + } + pushVectorEdge(&cnf->args, arg); + } + + if (largest != NULL) { + Node *nlargestEdge=getNodePtrFromEdge(*largestEdge); + nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL; + } + + return largest; +} + +void printCNF(Edge e) { + if (edgeIsVarConst(e)) { + Literal l=getEdgeVar(e); + printf ("%d", l); + return; + } + bool isNeg=isNegEdge(e); + if (edgeIsConst(e)) { + if (isNeg) + printf("T"); + else + printf("F"); + return; + } + Node *n=getNodePtrFromEdge(e); + if (isNeg) + printf("!"); + switch(getNodeType(e)) { + case NodeType_AND: + printf("and"); + break; + case NodeType_ITE: + printf("ite"); + break; + case NodeType_IFF: + printf("iff"); + break; + } + printf("("); + for(uint i=0;inumEdges;i++) { + Edge e=n->edges[i]; + if (i!=0) + printf(" "); + printCNF(e); + } + printf(")"); +} + +CNFExpr * produceConjunction(CNF * cnf, Edge e) { + Edge largestEdge; + + CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge); + if (accum == NULL) accum = allocCNFExprBool(true); + + int i = getSizeVectorEdge(&cnf->args); + while (i != 0) { + Edge arg = getVectorEdge(&cnf->args, --i); + if (edgeIsVarConst(arg)) { + conjoinCNFLit(accum, getEdgeVar(arg)); + } else { + Node *narg=getNodePtrFromEdge(arg); + CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; + + bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0); + if (isProxy(argExp)) { // variable has been introduced + conjoinCNFLit(accum, getProxy(argExp)); + } else { + conjoinCNFExpr(accum, argExp, destroy); + if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL; } - case AND: { - Constraint *array[This->numoperandsorvar]; - - VectorConstraint *vec=allocDefVectorConstraint(); - for(uint j=0;jnumoperandsorvar;j++) { - //copy other elements - for(uint k=0;knumoperandsorvar;k++) { - if (k!=i) { - array[k]=cloneConstraint(This->operands[k]); - } - } + } + } + + return accum; +} - array[i]=cloneConstraint(c->operands[j]); - Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array); - VectorConstraint * newvec=simplifyConstraint(cn); - if (mergeandfree(vec, newvec)) { - freerecConstraint(This); - return vec; - } +#define CLAUSE_MAX 3 + +CNFExpr* produceDisjunction(CNF *cnf, Edge e) { + Edge largestEdge; + CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge); + if (accum == NULL) + accum = allocCNFExprBool(false); + + // This is necessary to check to make sure that we don't start out + // with an accumulator that is "too large". + + /// @todo Strictly speaking, introProxy doesn't *need* to free + /// memory, then this wouldn't have to reallocate CNFExpr + + /// @todo When this call to introProxy is made, the semantic + /// negation pointer will have been destroyed. Thus, it will not + /// be possible to use the correct proxy. That should be fixed. + + // at this point, we will either have NULL, or a destructible expression + if (getClauseSizeCNF(accum) > CLAUSE_MAX) + accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge))); + + int i = getSizeVectorEdge(&cnf->args); + while (i != 0) { + Edge arg=getVectorEdge(&cnf->args, --i); + Node *narg=getNodePtrFromEdge(arg); + if (edgeIsVarConst(arg)) { + disjoinCNFLit(accum, getEdgeVar(arg)); + } else { + CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; + + bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0); + if (isProxy(argExp)) { // variable has been introduced + disjoinCNFLit(accum, getProxy(argExp)); + } else if (argExp->litSize == 0) { + disjoinCNFExpr(accum, argExp, destroy); + } else { + // check to see if we should introduce a proxy + int aL = accum->litSize; // lits in accum + int eL = argExp->litSize; // lits in argument + int aC = getClauseSizeCNF(accum); // clauses in accum + int eC = getClauseSizeCNF(argExp); // clauses in argument + + if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) { + disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg))); + } else { + disjoinCNFExpr(accum, argExp, destroy); + if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL; } - freerecConstraint(This); - return vec; - } - default: - ASSERT(0); } - //continue on to next item } - VectorConstraint * vec=allocDefVectorConstraint(); - if (This->numoperandsorvar==1) { - Constraint *c=This->operands[0]; - freerecConstraint(This); - pushVectorConstraint(vec, c); - } else - pushVectorConstraint(vec, This); - return vec; - } - case IMPLIES: { - Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]); - VectorConstraint * vec=simplifyConstraint(cn); - internalfreeConstraint(This); - return vec; - } - default: - ASSERT(0); - return NULL; - } -} - -Constraint * negateConstraint(Constraint * This) { - switch(This->type) { - case TRUE: - return &cfalse; - case FALSE: - return &ctrue; - case NOTVAR: - case VAR: - return This->neg; - case IMPLIES: { - Constraint *l=This->operands[0]; - Constraint *r=This->operands[1]; - This->operands[0]=r; - This->operands[1]=l; - return This; - } - case AND: - case OR: { - for(uint i=0;inumoperandsorvar;i++) { - This->operands[i]=negateConstraint(This->operands[i]); + } + + return accum; +} + +Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) { + Edge carray[numvars]; + for(uint j=0;j>1; + } + + return constraintAND(cnf, numvars, carray); +} + +/** Generates a constraint to ensure that all encodings are less than value */ +Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) { + Edge orarray[numvars]; + Edge andarray[numvars]; + uint andi=0; + + while(true) { + uint val=value; + uint ori=0; + for(uint j=0;j>1; + } + //no ones to flip, so bail now... + if (ori==0) { + return constraintAND(cnf, andi, andarray); } - This->type=(This->type==AND) ? OR : AND; - return This; + andarray[andi++]=constraintOR(cnf, ori, orarray); + + value=value+(1<<(__builtin_ctz(value))); + //flip the last one } - default: - ASSERT(0); - return NULL; +} + +Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) { + if (numvars==0) + return E_True; + Edge array[numvars]; + for(uint i=0;i - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - #ifndef CONSTRAINT_H #define CONSTRAINT_H #include "classlist.h" -#include "structs.h" +#include "vector.h" + +#define NEGATE_EDGE 1 +#define EDGE_IS_VAR_CONSTANT 2 +#define VAR_SHIFT 2 +#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT) + +typedef int Literal; + +struct Edge; +typedef struct Edge Edge; + +struct Node; +typedef struct Node Node; -enum ConstraintType { - TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS +struct Edge { + Node * node_ptr; }; -typedef enum ConstraintType CType; +VectorDef(Edge, Edge) -struct Constraint { - CType type; - uint numoperandsorvar; - Constraint ** operands; - Constraint *neg; +enum NodeType { + NodeType_AND, + NodeType_ITE, + NodeType_IFF }; -Constraint * allocConstraint(CType t, Constraint *l, Constraint *r); -Constraint * allocUnaryConstraint(CType t, Constraint *l); -Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array); -Constraint * allocVarConstraint(CType t, uint var); +typedef enum NodeType NodeType; + +struct NodeFlags { + NodeType type:2; + int varForced:1; + int wasExpanded:2; + int cnfVisitedDown:2; + int cnfVisitedUp:2; +}; + +typedef struct NodeFlags NodeFlags; + +struct Node { + NodeFlags flags; + uint numEdges; + uint hashCode; + uint intAnnot[2]; + void * ptrAnnot[2]; + Edge edges[]; +}; + +#define DEFAULT_CNF_ARRAY_SIZE 256 +#define LOAD_FACTOR 0.25 + +struct CNF { + uint varcount; + uint capacity; + uint size; + uint mask; + uint maxsize; + bool enableMatching; + Node ** node_array; + IncrementalSolver * solver; + VectorEdge constraints; + VectorEdge args; +}; + +typedef struct CNF CNF; + +struct CNFExpr; +typedef struct CNFExpr CNFExpr; + +static inline bool getExpanded(Node *n, int isNegated) { + return n->flags.wasExpanded & (1<flags.wasExpanded |= (1<flags.type; +} + +static inline bool equalsEdge(Edge e1, Edge e2) { + return e1.node_ptr == e2.node_ptr; +} + +static inline bool ltEdge(Edge e1, Edge e2) { + return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr; +} + +static inline uint getNodeSize(Edge e) { + Node * n=getNodePtrFromEdge(e); + return n->numEdges; +} + +static inline Edge * getEdgeArray(Edge e) { + Node * n=getNodePtrFromEdge(e); + return n->edges; +} + +static inline Edge getNonNeg(Edge e) { + Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))}; + return enew; +} + +static inline bool edgeIsConst(Edge e) { + return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT; +} + +static inline bool edgeIsNull(Edge e) { + return e.node_ptr == NULL; +} + +static inline bool edgeIsVarConst(Edge e) { + return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT; +} + +static inline Edge constraintNegateIf(Edge e, bool negate) { + Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ negate)}; + return eret; +} + +static inline Literal getEdgeVar(Edge e) { + int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT); + return isNegEdge(e) ? -val : val; +} + +static inline bool isProxy(CNFExpr *expr) { + return (bool) (((intptr_t) expr) & 1); +} -void deleteConstraint(Constraint *); -void printConstraint(Constraint * c); -void dumpConstraint(Constraint * c, IncrementalSolver *solver); -static inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;} -VectorConstraint * simplifyConstraint(Constraint * This); -static inline CType getType(Constraint * c) {return c->type;} -static inline bool isFalse(Constraint * c) {return c->type==FALSE;} -static inline bool isTrue(Constraint * c) {return c->type==TRUE;} -void internalfreeConstraint(Constraint * c); -void freerecConstraint(Constraint * c); -Constraint * cloneConstraint(Constraint * c); -static inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;} -Constraint *negateConstraint(Constraint * c); +static inline Literal getProxy(CNFExpr *expr) { + return (Literal) (((intptr_t) expr) >> 1); +} +CNF * createCNF(); +void deleteCNF(CNF * cnf); -extern Constraint ctrue; -extern Constraint cfalse; +uint hashNode(NodeType type, uint numEdges, Edge * edges); +Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode); +bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges); +Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges); +Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges); +Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges); +Edge constraintOR2(CNF * cnf, Edge left, Edge right); +Edge constraintAND2(CNF * cnf, Edge left, Edge right); +Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right); +Edge constraintIFF(CNF * cnf, Edge left, Edge right); +static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));} +Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge); +Edge constraintNewVar(CNF *cnf); +void countPass(CNF *cnf); +void countConstraint(CNF *cnf, VectorEdge * stack, Edge e); +void addConstraint(CNF *cnf, Edge constraint); +int solveCNF(CNF *cnf); +bool getValueCNF(CNF *cnf, Edge var); +void printCNF(Edge e); -Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value); -Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); -Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); -Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); +void convertPass(CNF *cnf, bool backtrackLit); +void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit); +void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp); +void produceCNF(CNF * cnf, Edge e); +CNFExpr * produceConjunction(CNF * cnf, Edge e); +CNFExpr* produceDisjunction(CNF *cnf, Edge e); +bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate); +void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign); +CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge); +Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg); +void outputCNF(CNF *cnf, CNFExpr *expr); +Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value); +Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value); +Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2); +extern Edge E_True; +extern Edge E_False; +extern Edge E_BOGUS; +extern Edge E_NULL; #endif diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c deleted file mode 100644 index 9d6e855..0000000 --- a/src/Backend/nodeedge.c +++ /dev/null @@ -1,810 +0,0 @@ -#include "nodeedge.h" -#include -#include -#include "inc_solver.h" -#include "cnfexpr.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. -*/ - - -VectorImpl(Edge, Edge, 16) - -CNF * createCNF() { - CNF * cnf=ourmalloc(sizeof(CNF)); - cnf->varcount=1; - cnf->capacity=DEFAULT_CNF_ARRAY_SIZE; - cnf->mask=cnf->capacity-1; - cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity); - cnf->size=0; - cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR); - cnf->enableMatching=true; - allocInlineDefVectorEdge(& cnf->constraints); - allocInlineDefVectorEdge(& cnf->args); - cnf->solver=allocIncrementalSolver(); - return cnf; -} - -void deleteCNF(CNF * cnf) { - for(uint i=0;icapacity;i++) { - Node *n=cnf->node_array[i]; - if (n!=NULL) - ourfree(n); - } - deleteVectorArrayEdge(& cnf->constraints); - deleteVectorArrayEdge(& cnf->args); - deleteIncrementalSolver(cnf->solver); - ourfree(cnf->node_array); - ourfree(cnf); -} - -void resizeCNF(CNF *cnf, uint newCapacity) { - Node **old_array=cnf->node_array; - Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity); - uint oldCapacity=cnf->capacity; - uint newMask=newCapacity-1; - for(uint i=0;ihashCode; - uint newindex=hashCode & newMask; - for(;;newindex=(newindex+1) & newMask) { - if (new_array[newindex] == NULL) { - new_array[newindex]=n; - break; - } - } - } - ourfree(old_array); - cnf->node_array=new_array; - cnf->capacity=newCapacity; - cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR); - cnf->mask=newMask; -} - -Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) { - Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges); - memcpy(n->edges, edges, sizeof(Edge)*numEdges); - n->flags.type=type; - n->flags.wasExpanded=0; - n->flags.cnfVisitedDown=0; - n->flags.cnfVisitedUp=0; - n->flags.varForced=0; - n->numEdges=numEdges; - n->hashCode=hashcode; - n->intAnnot[0]=0;n->intAnnot[1]=0; - n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL; - return n; -} - -Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) { - if (cnf->size > cnf->maxsize) { - resizeCNF(cnf, cnf->capacity << 1); - } - uint hashvalue=hashNode(type, numEdges, edges); - uint mask=cnf->mask; - uint index=hashvalue & mask; - Node **n_ptr; - for(;;index=(index+1)&mask) { - n_ptr=&cnf->node_array[index]; - if (*n_ptr!=NULL) { - if ((*n_ptr)->hashCode==hashvalue) { - if (compareNodes(*n_ptr, type, numEdges, edges)) { - Edge e={*n_ptr}; - return e; - } - } - } else { - break; - } - } - *n_ptr=allocNode(type, numEdges, edges, hashvalue); - Edge e={*n_ptr}; - return e; -} - -uint hashNode(NodeType type, uint numEdges, Edge * edges) { - uint hashvalue=type ^ numEdges; - for(uint i=0;i> 29); //rotate left by 3 bits - } - return (uint) hashvalue; -} - -bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) { - if (node->flags.type!=type || node->numEdges != numEdges) - return false; - Edge *nodeedges=node->edges; - for(uint i=0;inode_ptr)-((uintptr_t)e2->node_ptr); -} - -Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) { - qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction); - int initindex=0; - while(initindexenableMatching && lowindex==2 && - isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) && - getNodeType(edges[0]) == NodeType_AND && - getNodeType(edges[1]) == NodeType_AND && - getNodeSize(edges[0]) == 2 && - getNodeSize(edges[1]) == 2) { - Edge * e0edges=getEdgeArray(edges[0]); - Edge * e1edges=getEdgeArray(edges[1]); - if (sameNodeOppSign(e0edges[0], e1edges[0])) { - return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1])); - } else if (sameNodeOppSign(e0edges[0], e1edges[1])) { - return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0])); - } else if (sameNodeOppSign(e0edges[1], e1edges[0])) { - return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1])); - } else if (sameNodeOppSign(e0edges[1], e1edges[1])) { - return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0])); - } - } - - return createNode(cnf, NodeType_AND, lowindex, edges); -} - -Edge constraintAND2(CNF * cnf, Edge left, Edge right) { - Edge edges[2]={left, right}; - return constraintAND(cnf, 2, edges); -} - -Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) { - Edge array[2]; - array[0]=left; - array[1]=constraintNegate(right); - Edge eand=constraintAND(cnf, 2, array); - return constraintNegate(eand); -} - -Edge constraintIFF(CNF * cnf, Edge left, Edge right) { - bool negate=!sameSignEdge(left, right); - Edge lpos=getNonNeg(left); - Edge rpos=getNonNeg(right); - - Edge e; - if (equalsEdge(lpos, rpos)) { - e=E_True; - } else if (ltEdge(lpos, rpos)) { - Edge edges[]={lpos, rpos}; - e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges); - } else { - Edge edges[]={rpos, lpos}; - e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges); - } - if (negate) - e=constraintNegate(e); - return e; -} - -Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) { - if (isNegEdge(cond)) { - cond=constraintNegate(cond); - Edge tmp=thenedge; - thenedge=elseedge; - elseedge=tmp; - } - - bool negate = isNegEdge(thenedge); - if (negate) { - thenedge=constraintNegate(thenedge); - elseedge=constraintNegate(elseedge); - } - - Edge result; - if (equalsEdge(cond, E_True)) { - result=thenedge; - } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) { - result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge}); - } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) { - result=constraintIMPLIES(cnf, cond, thenedge); - } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) { - result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge}); - } else if (equalsEdge(thenedge, elseedge)) { - result=thenedge; - } else if (sameNodeOppSign(thenedge, elseedge)) { - if (ltEdge(cond, thenedge)) { - result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge}); - } else { - result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond}); - } - } else { - Edge edges[]={cond, thenedge, elseedge}; - result=createNode(cnf, NodeType_ITE, 3, edges); - } - if (negate) - result=constraintNegate(result); - return result; -} - -void addConstraint(CNF *cnf, Edge constraint) { - pushVectorEdge(&cnf->constraints, constraint); -} - -Edge constraintNewVar(CNF *cnf) { - uint varnum=cnf->varcount++; - Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) }; - return e; -} - -int solveCNF(CNF *cnf) { - countPass(cnf); - convertPass(cnf, false); - finishedClauses(cnf->solver); - return solve(cnf->solver); -} - -bool getValueCNF(CNF *cnf, Edge var) { - Literal l=getEdgeVar(var); - bool isneg=(l<0); - l=abs(l); - return isneg ^ getValueSolver(cnf->solver, l); -} - -void countPass(CNF *cnf) { - uint numConstraints=getSizeVectorEdge(&cnf->constraints); - VectorEdge *ve=allocDefVectorEdge(); - for(uint i=0; iconstraints, i)); - } - deleteVectorEdge(ve); -} - -void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) { - //Skip constants and variables... - if (edgeIsVarConst(eroot)) - return; - - clearVectorEdge(stack);pushVectorEdge(stack, eroot); - - bool isMatching=cnf->enableMatching; - - while(getSizeVectorEdge(stack) != 0) { - Edge e=lastVectorEdge(stack); popVectorEdge(stack); - bool polarity=isNegEdge(e); - Node *n=getNodePtrFromEdge(e); - if (getExpanded(n, polarity)) { - if (n->flags.type == NodeType_IFF || - n->flags.type == NodeType_ITE) { - Edge pExp={n->ptrAnnot[polarity]}; - getNodePtrFromEdge(pExp)->intAnnot[0]++; - } else { - n->intAnnot[polarity]++; - } - } else { - setExpanded(n, polarity); - - if (n->flags.type == NodeType_ITE|| - n->flags.type == NodeType_IFF) { - n->intAnnot[polarity]=0; - Edge cond=n->edges[0]; - Edge thenedge=n->edges[1]; - Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2]; - thenedge=constraintNegateIf(thenedge, !polarity); - elseedge=constraintNegateIf(elseedge, !polarity); - thenedge=constraintAND2(cnf, cond, thenedge); - cond=constraintNegate(cond); - elseedge=constraintAND2(cnf, cond, elseedge); - thenedge=constraintNegate(thenedge); - elseedge=constraintNegate(elseedge); - cnf->enableMatching=false; - Edge succ1=constraintAND2(cnf, thenedge, elseedge); - n->ptrAnnot[polarity]=succ1.node_ptr; - cnf->enableMatching=isMatching; - pushVectorEdge(stack, succ1); - if (getExpanded(n, !polarity)) { - Edge succ2={(Node *)n->ptrAnnot[!polarity]}; - Node *n1=getNodePtrFromEdge(succ1); - Node *n2=getNodePtrFromEdge(succ2); - n1->ptrAnnot[0]=succ2.node_ptr; - n2->ptrAnnot[0]=succ1.node_ptr; - n1->ptrAnnot[1]=succ2.node_ptr; - n2->ptrAnnot[1]=succ1.node_ptr; - } - } else { - n->intAnnot[polarity]=1; - for (uint i=0;inumEdges;i++) { - Edge succ=n->edges[i]; - succ=constraintNegateIf(succ, polarity); - if(!edgeIsVarConst(succ)) { - pushVectorEdge(stack, succ); - } - } - } - } - } -} - -void convertPass(CNF *cnf, bool backtrackLit) { - uint numConstraints=getSizeVectorEdge(&cnf->constraints); - VectorEdge *ve=allocDefVectorEdge(); - for(uint i=0; iconstraints, i), backtrackLit); - } - deleteVectorEdge(ve); -} - -void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) { - Node *nroot=getNodePtrFromEdge(root); - - if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) { - root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]}; - } - - if (edgeIsConst(root)) { - if (isNegEdge(root)) { - //trivally unsat - Edge newvar=constraintNewVar(cnf); - Literal var=getEdgeVar(newvar); - Literal clause[] = {var}; - addArrayClauseLiteral(cnf->solver, 1, clause); - clause[0]=-var; - addArrayClauseLiteral(cnf->solver, 1, clause); - return; - } else { - //trivially true - return; - } - } else if (edgeIsVarConst(root)) { - Literal clause[] = { getEdgeVar(root)}; - addArrayClauseLiteral(cnf->solver, 1, clause); - return; - } - - clearVectorEdge(stack);pushVectorEdge(stack, root); - while(getSizeVectorEdge(stack)!=0) { - Edge e=lastVectorEdge(stack); - Node *n=getNodePtrFromEdge(e); - - if (edgeIsVarConst(e)) { - popVectorEdge(stack); - continue; - } else if (n->flags.type==NodeType_ITE || - n->flags.type==NodeType_IFF) { - popVectorEdge(stack); - if (n->ptrAnnot[0]!=NULL) - pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]}); - if (n->ptrAnnot[1]!=NULL) - pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]}); - continue; - } - - bool needPos = (n->intAnnot[0] > 0); - bool needNeg = (n->intAnnot[1] > 0); - if ((!needPos || n->flags.cnfVisitedUp & 1) && - (!needNeg || n->flags.cnfVisitedUp & 2)) { - popVectorEdge(stack); - } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) || - (needNeg && !(n->flags.cnfVisitedDown & 2))) { - if (needPos) - n->flags.cnfVisitedDown|=1; - if (needNeg) - n->flags.cnfVisitedDown|=2; - for(uint i=0; inumEdges; i++) { - Edge arg=n->edges[i]; - arg=constraintNegateIf(arg, isNegEdge(e)); - pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE - } - } else { - popVectorEdge(stack); - produceCNF(cnf, e); - } - } - CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)]; - if (isProxy(cnfExp)) { - Literal l=getProxy(cnfExp); - Literal clause[] = {l}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } else if (backtrackLit) { - Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root)); - Literal clause[] = {l}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } else { - outputCNF(cnf, cnfExp); - } - - if (!((intptr_t) cnfExp & 1)) { - deleteCNFExpr(cnfExp); - nroot->ptrAnnot[isNegEdge(root)] = NULL; - } -} - - -Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) { - Literal l = 0; - Node * n = getNodePtrFromEdge(e); - - if (n->flags.cnfVisitedUp & (1<ptrAnnot[!isNeg]; - if (isProxy(otherExp)) - l = -getProxy(otherExp); - } else { - Edge semNeg={(Node *) n->ptrAnnot[isNeg]}; - Node * nsemNeg=getNodePtrFromEdge(semNeg); - if (nsemNeg != NULL) { - if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) { - CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg]; - if (isProxy(otherExp)) - l = -getProxy(otherExp); - } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) { - CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg]; - if (isProxy(otherExp)) - l = getProxy(otherExp); - } - } - } - - if (l == 0) { - Edge newvar = constraintNewVar(cnf); - l = getEdgeVar(newvar); - } - // Output the constraints on the auxiliary variable - constrainCNF(cnf, l, exp); - deleteCNFExpr(exp); - - n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1); - - return l; -} - -void produceCNF(CNF * cnf, Edge e) { - CNFExpr* expPos = NULL; - CNFExpr* expNeg = NULL; - Node *n = getNodePtrFromEdge(e); - - if (n->intAnnot[0] > 0) { - expPos = produceConjunction(cnf, e); - } - - if (n->intAnnot[1] > 0) { - expNeg = produceDisjunction(cnf, e); - } - - /// @todo Propagate constants across semantic negations (this can - /// be done similarly to the calls to propagate shown below). The - /// trick here is that we need to figure out how to get the - /// semantic negation pointers, and ensure that they can have CNF - /// produced for them at the right point - /// - /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false) - - // propagate from positive to negative, negative to positive - if (!propagate(cnf, & expPos, expNeg, true)) - propagate(cnf, & expNeg, expPos, true); - - // The polarity heuristic entails visiting the discovery polarity first - if (isPosEdge(e)) { - saveCNF(cnf, expPos, e, false); - saveCNF(cnf, expNeg, e, true); - } else { - saveCNF(cnf, expNeg, e, true); - saveCNF(cnf, expPos, e, false); - } -} - -bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) { - if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) { - if (*dest == NULL) { - *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); - } else if (isProxy(*dest)) { - bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); - if (alwaysTrue) { - Literal clause[] = {getProxy(*dest)}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } else { - Literal clause[] = {-getProxy(*dest)}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } - - *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); - } else { - clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); - } - return true; - } - return false; -} - -void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) { - Node *n=getNodePtrFromEdge(e); - n->flags.cnfVisitedUp |= (1 << sign); - if (exp == NULL || isProxy(exp)) return; - - if (exp->litSize == 1) { - Literal l = getLiteralLitVector(&exp->singletons, 0); - deleteCNFExpr(exp); - n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1); - } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) { - introProxy(cnf, e, exp, sign); - } else { - n->ptrAnnot[sign] = exp; - } -} - -void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) { - if (alwaysTrueCNF(expr)) { - return; - } else if (alwaysFalseCNF(expr)) { - Literal clause[] = {-lcond}; - addArrayClauseLiteral(cnf->solver, 1, clause); - return; - } - - for(uint i=0;isingletons);i++) { - Literal l=getLiteralLitVector(&expr->singletons,i); - Literal clause[] = {-lcond, l}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } - for(uint i=0;iclauses);i++) { - LitVector *lv=getVectorLitVector(&expr->clauses,i); - addClauseLiteral(cnf->solver, -lcond); //Add first literal - addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest - } -} - -void outputCNF(CNF *cnf, CNFExpr *expr) { - for(uint i=0;isingletons);i++) { - Literal l=getLiteralLitVector(&expr->singletons,i); - Literal clause[] = {l}; - addArrayClauseLiteral(cnf->solver, 1, clause); - } - for(uint i=0;iclauses);i++) { - LitVector *lv=getVectorLitVector(&expr->clauses,i); - addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); - } -} - -CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) { - clearVectorEdge(&cnf->args); - - *largestEdge = (Edge) {(Node*) NULL}; - CNFExpr* largest = NULL; - Node *n=getNodePtrFromEdge(e); - int i = n->numEdges; - while (i != 0) { - Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg); - Node * narg = getNodePtrFromEdge(arg); - - if (edgeIsVarConst(arg)) { - pushVectorEdge(&cnf->args, arg); - continue; - } - - if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) { - arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]}; - } - - if (narg->intAnnot[isNegEdge(arg)] == 1) { - CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; - if (!isProxy(argExp)) { - if (largest == NULL) { - largest = argExp; - * largestEdge = arg; - continue; - } else if (argExp->litSize > largest->litSize) { - pushVectorEdge(&cnf->args, *largestEdge); - largest = argExp; - * largestEdge = arg; - continue; - } - } - } - pushVectorEdge(&cnf->args, arg); - } - - if (largest != NULL) { - Node *nlargestEdge=getNodePtrFromEdge(*largestEdge); - nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL; - } - - return largest; -} - -void printCNF(Edge e) { - if (edgeIsVarConst(e)) { - Literal l=getEdgeVar(e); - printf ("%d", l); - return; - } - bool isNeg=isNegEdge(e); - if (edgeIsConst(e)) { - if (isNeg) - printf("T"); - else - printf("F"); - return; - } - Node *n=getNodePtrFromEdge(e); - if (isNeg) - printf("!"); - switch(getNodeType(e)) { - case NodeType_AND: - printf("and"); - break; - case NodeType_ITE: - printf("ite"); - break; - case NodeType_IFF: - printf("iff"); - break; - } - printf("("); - for(uint i=0;inumEdges;i++) { - Edge e=n->edges[i]; - if (i!=0) - printf(" "); - printCNF(e); - } - printf(")"); -} - -CNFExpr * produceConjunction(CNF * cnf, Edge e) { - Edge largestEdge; - - CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge); - if (accum == NULL) accum = allocCNFExprBool(true); - - int i = getSizeVectorEdge(&cnf->args); - while (i != 0) { - Edge arg = getVectorEdge(&cnf->args, --i); - if (edgeIsVarConst(arg)) { - conjoinCNFLit(accum, getEdgeVar(arg)); - } else { - Node *narg=getNodePtrFromEdge(arg); - CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; - - bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0); - if (isProxy(argExp)) { // variable has been introduced - conjoinCNFLit(accum, getProxy(argExp)); - } else { - conjoinCNFExpr(accum, argExp, destroy); - if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL; - } - } - } - - return accum; -} - -#define CLAUSE_MAX 3 - -CNFExpr* produceDisjunction(CNF *cnf, Edge e) { - Edge largestEdge; - CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge); - if (accum == NULL) - accum = allocCNFExprBool(false); - - // This is necessary to check to make sure that we don't start out - // with an accumulator that is "too large". - - /// @todo Strictly speaking, introProxy doesn't *need* to free - /// memory, then this wouldn't have to reallocate CNFExpr - - /// @todo When this call to introProxy is made, the semantic - /// negation pointer will have been destroyed. Thus, it will not - /// be possible to use the correct proxy. That should be fixed. - - // at this point, we will either have NULL, or a destructible expression - if (getClauseSizeCNF(accum) > CLAUSE_MAX) - accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge))); - - int i = getSizeVectorEdge(&cnf->args); - while (i != 0) { - Edge arg=getVectorEdge(&cnf->args, --i); - Node *narg=getNodePtrFromEdge(arg); - if (edgeIsVarConst(arg)) { - disjoinCNFLit(accum, getEdgeVar(arg)); - } else { - CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)]; - - bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0); - if (isProxy(argExp)) { // variable has been introduced - disjoinCNFLit(accum, getProxy(argExp)); - } else if (argExp->litSize == 0) { - disjoinCNFExpr(accum, argExp, destroy); - } else { - // check to see if we should introduce a proxy - int aL = accum->litSize; // lits in accum - int eL = argExp->litSize; // lits in argument - int aC = getClauseSizeCNF(accum); // clauses in accum - int eC = getClauseSizeCNF(argExp); // clauses in argument - - if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) { - disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg))); - } else { - disjoinCNFExpr(accum, argExp, destroy); - if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL; - } - } - } - } - - return accum; -} diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h deleted file mode 100644 index 89ea40f..0000000 --- a/src/Backend/nodeedge.h +++ /dev/null @@ -1,212 +0,0 @@ -#ifndef NODEEDGE_H -#define NODEEDGE_H -#include "classlist.h" -#include "vector.h" - -#define NEGATE_EDGE 1 -#define EDGE_IS_VAR_CONSTANT 2 -#define VAR_SHIFT 2 -#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT) - -typedef int Literal; - -struct Edge; -typedef struct Edge Edge; - -struct Node; -typedef struct Node Node; - -struct Edge { - Node * node_ptr; -}; - -VectorDef(Edge, Edge) - -enum NodeType { - NodeType_AND, - NodeType_ITE, - NodeType_IFF -}; - -typedef enum NodeType NodeType; - -struct NodeFlags { - NodeType type:2; - int varForced:1; - int wasExpanded:2; - int cnfVisitedDown:2; - int cnfVisitedUp:2; -}; - -typedef struct NodeFlags NodeFlags; - -struct Node { - NodeFlags flags; - uint numEdges; - uint hashCode; - uint intAnnot[2]; - void * ptrAnnot[2]; - Edge edges[]; -}; - -#define DEFAULT_CNF_ARRAY_SIZE 256 -#define LOAD_FACTOR 0.25 - -struct CNF { - uint varcount; - uint capacity; - uint size; - uint mask; - uint maxsize; - bool enableMatching; - Node ** node_array; - IncrementalSolver * solver; - VectorEdge constraints; - VectorEdge args; -}; - -typedef struct CNF CNF; - -struct CNFExpr; -typedef struct CNFExpr CNFExpr; - -static inline bool getExpanded(Node *n, int isNegated) { - return n->flags.wasExpanded & (1<flags.wasExpanded |= (1<flags.type; -} - -static inline bool equalsEdge(Edge e1, Edge e2) { - return e1.node_ptr == e2.node_ptr; -} - -static inline bool ltEdge(Edge e1, Edge e2) { - return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr; -} - -static inline uint getNodeSize(Edge e) { - Node * n=getNodePtrFromEdge(e); - return n->numEdges; -} - -static inline Edge * getEdgeArray(Edge e) { - Node * n=getNodePtrFromEdge(e); - return n->edges; -} - -static inline Edge getNonNeg(Edge e) { - Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))}; - return enew; -} - -static inline bool edgeIsConst(Edge e) { - return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT; -} - -static inline bool edgeIsNull(Edge e) { - return e.node_ptr == NULL; -} - -static inline bool edgeIsVarConst(Edge e) { - return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT; -} - -static inline Edge constraintNegateIf(Edge e, bool negate) { - Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ negate)}; - return eret; -} - -static inline Literal getEdgeVar(Edge e) { - int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT); - return isNegEdge(e) ? -val : val; -} - -static inline bool isProxy(CNFExpr *expr) { - return (bool) (((intptr_t) expr) & 1); -} - -static inline Literal getProxy(CNFExpr *expr) { - return (Literal) (((intptr_t) expr) >> 1); -} - -CNF * createCNF(); -void deleteCNF(CNF * cnf); - -uint hashNode(NodeType type, uint numEdges, Edge * edges); -Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode); -bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges); -Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges); -Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges); -Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges); -Edge constraintOR2(CNF * cnf, Edge left, Edge right); -Edge constraintAND2(CNF * cnf, Edge left, Edge right); -Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right); -Edge constraintIFF(CNF * cnf, Edge left, Edge right); -Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge); -Edge constraintNewVar(CNF *cnf); -void countPass(CNF *cnf); -void countConstraint(CNF *cnf, VectorEdge * stack, Edge e); -void addConstraint(CNF *cnf, Edge constraint); -int solveCNF(CNF *cnf); -bool getValueCNF(CNF *cnf, Edge var); -void printCNF(Edge e); - -void convertPass(CNF *cnf, bool backtrackLit); -void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit); -void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp); -void produceCNF(CNF * cnf, Edge e); -CNFExpr * produceConjunction(CNF * cnf, Edge e); -CNFExpr* produceDisjunction(CNF *cnf, Edge e); -bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate); -void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign); -CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge); -Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg); -void outputCNF(CNF *cnf, CNFExpr *expr); - -Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT}; -Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)}; -#endif diff --git a/src/Backend/orderpair.c b/src/Backend/orderpair.c index 109fc53..4db56ca 100644 --- a/src/Backend/orderpair.c +++ b/src/Backend/orderpair.c @@ -1,7 +1,7 @@ #include "orderpair.h" -OrderPair* allocOrderPair(uint64_t first, uint64_t second, Constraint * constraint){ +OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint){ OrderPair* pair = (OrderPair*) ourmalloc(sizeof(OrderPair)); pair->first = first; pair->second = second; diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h index bdffb15..05c8ffa 100644 --- a/src/Backend/orderpair.h +++ b/src/Backend/orderpair.h @@ -10,14 +10,15 @@ #include "classlist.h" #include "mymemory.h" +#include "constraint.h" struct OrderPair{ uint64_t first; uint64_t second; - Constraint *constraint; + Edge constraint; }; -OrderPair* allocOrderPair(uint64_t first, uint64_t second, Constraint * constraint); +OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint); void deleteOrderPair(OrderPair* pair); #endif /* ORDERPAIR_H */ diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index fa1d513..5c41571 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -16,18 +16,18 @@ SATEncoder * allocSATEncoder() { SATEncoder *This=ourmalloc(sizeof (SATEncoder)); This->varcount=1; - This->satSolver = allocIncrementalSolver(); + This->cnf=createCNF(); return This; } void deleteSATEncoder(SATEncoder *This) { - deleteIncrementalSolver(This->satSolver); + deleteCNF(This->cnf); ourfree(This); } -Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64_t value) { - generateElementEncodingVariables(encoder, getElementEncoding(This)); - switch(getElementEncoding(This)->type){ +Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { + generateElementEncodingVariables(This, getElementEncoding(elem)); + switch(getElementEncoding(elem)->type){ case ONEHOT: //FIXME ASSERT(0); @@ -36,7 +36,7 @@ Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64 ASSERT(0); break; case BINARYINDEX: - return getElementValueBinaryIndexConstraint(This, value); + return getElementValueBinaryIndexConstraint(This, elem, value); break; case ONEHOTBINARY: ASSERT(0); @@ -48,33 +48,19 @@ Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64 ASSERT(0); break; } - return NULL; + return E_BOGUS; } -Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) { - ASTNodeType type = GETELEMENTTYPE(This); + +Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) { + ASTNodeType type = GETELEMENTTYPE(elem); ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); - ElementEncoding* elemEnc = getElementEncoding(This); + ElementEncoding* elemEnc = getElementEncoding(elem); for(uint i=0; iencArraySize; i++){ if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){ - return generateBinaryConstraint(elemEnc->numVars, - elemEnc->variables, i); + return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i); } } - return NULL; -} - -void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver) { - VectorConstraint* simplified = simplifyConstraint(c); - uint size = getSizeVectorConstraint(simplified); - for(uint i=0; itype==TRUE) - continue; - ASSERT(simp->type!=FALSE); - dumpConstraint(simp, satSolver); - freerecConstraint(simp); - } - deleteVectorConstraint(simplified); + return E_BOGUS; } void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) { @@ -82,16 +68,13 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) { uint size=getSizeVectorBoolean(constraints); for(uint i=0;isatSolver); - //FIXME: When do we want to delete constraints? Should we keep an array of them - // and delete them later, or it would be better to just delete them right away? + Edge c= encodeConstraintSATEncoder(This, constraint); + printCNF(c); + addConstraint(This->cnf, c); } } -Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { +Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { switch(GETBOOLEANTYPE(constraint)) { case ORDERCONST: return encodeOrderSATEncoder(This, (BooleanOrder *) constraint); @@ -107,50 +90,41 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { } } -void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) { +void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) { for(uint i=0;ivarcount); - Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++); - setNegConstraint(var, varneg); - setNegConstraint(varneg, var); - return var; +Edge getNewVarSATEncoder(SATEncoder *This) { + return constraintNewVar(This->cnf); } -Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) { - if (constraint->var == NULL) { +Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) { + if (edgeIsNull(constraint->var)) { constraint->var=getNewVarSATEncoder(This); } return constraint->var; } -Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) { - Constraint * array[getSizeArrayBoolean(&constraint->inputs)]; +Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) { + Edge array[getSizeArrayBoolean(&constraint->inputs)]; for(uint i=0;iinputs);i++) array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i)); switch(constraint->op) { case L_AND: - return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array); + return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array); case L_OR: - return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array); + return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array); case L_NOT: ASSERT( getSizeArrayBoolean(&constraint->inputs)==1); - return negateConstraint(array[0]); - case L_XOR: { + return constraintNegate(array[0]); + case L_XOR: ASSERT( getSizeArrayBoolean(&constraint->inputs)==2); - Constraint * nleft=negateConstraint(cloneConstraint(array[0])); - Constraint * nright=negateConstraint(cloneConstraint(array[1])); - return allocConstraint(OR, - allocConstraint(AND, array[0], nright), - allocConstraint(AND, nleft, array[1])); - } + return constraintXOR(This->cnf, array[0], array[1]); case L_IMPLIES: ASSERT( getSizeArrayBoolean( &constraint->inputs)==2); - return allocConstraint(IMPLIES, array[0], array[1]); + return constraintIMPLIES(This->cnf, array[0], array[1]); default: model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op); exit(-1); @@ -158,7 +132,7 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) } -Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { +Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { switch( constraint->order->type){ case PARTIAL: return encodePartialOrderSATEncoder(This, constraint); @@ -167,10 +141,10 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) { +Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) { bool negate = false; OrderPair flipped; if (pair->first > pair->second) { @@ -179,7 +153,7 @@ Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, Ord flipped.second=pair->first; pair = &flipped; //FIXME: accessing a local variable from outside of the function? } - Constraint * constraint; + Edge constraint; if (!containsBoolConst(table, pair)) { constraint = getNewVarSATEncoder(This); OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint); @@ -187,71 +161,66 @@ Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, Ord } else constraint = getBoolConst(table, pair)->constraint; if (negate) - return negateConstraint(constraint); + return constraintNegate(constraint); else return constraint; } -Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){ +Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){ ASSERT(boolOrder->order->type == TOTAL); if(boolOrder->order->boolsToConstraints == NULL){ initializeOrderHashTable(boolOrder->order); - return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); + createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); } HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints; - OrderPair pair={boolOrder->first, boolOrder->second, NULL}; - Constraint *constraint = getPairConstraint(This, boolToConsts, & pair); + OrderPair pair={boolOrder->first, boolOrder->second, E_NULL}; + Edge constraint = getPairConstraint(This, boolToConsts, & pair); return constraint; } -Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ ASSERT(order->type == TOTAL); VectorInt* mems = order->set->members; HashTableBoolConst* table = order->boolsToConstraints; uint size = getSizeVectorInt(mems); - Constraint* constraints [size*size]; uint csize =0; for(uint i=0; icnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); } } } - return allocArrayConstraint(AND, csize, constraints); } -Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){ +Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){ ASSERT(pair->first!= pair->second); - Constraint* constraint= getBoolConst(table, pair)->constraint; + Edge constraint = getBoolConst(table, pair)->constraint; if(pair->first > pair->second) return constraint; else - return negateConstraint(constraint); + return constraintNegate(constraint); } -Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){ - //FIXME: first we should add the the constraint to the satsolver! - ASSERT(constIJ!= NULL && constJK != NULL && constIK != NULL); - Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)}; - Constraint * loop1= allocArrayConstraint(OR, 3, carray); - Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK}; - Constraint * loop2= allocArrayConstraint(OR, 3,carray2 ); - return allocConstraint(AND, loop1, loop2); +Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){ + Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; + Edge loop1= constraintOR(This->cnf, 3, carray); + Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK}; + Edge loop2= constraintOR(This->cnf, 3, carray2 ); + return constraintAND2(This->cnf, loop1, loop2); } -Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ +Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ // FIXME: we can have this implementation for partial order. Basically, // we compute the transitivity between two order constraints specified by the client! (also can be used // when client specify sparse constraints for the total order!) @@ -261,7 +230,7 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const if( containsBoolConst(boolToConsts, boolOrder) ){ return getBoolConst(boolToConsts, boolOrder); } else { - Constraint* constraint = getNewVarSATEncoder(This); + Edge constraint = getNewVarSATEncoder(This); putBoolConst(boolToConsts,boolOrder, constraint); VectorBoolean* orderConstrs = &boolOrder->order->constraints; uint size= getSizeVectorBoolean(orderConstrs); @@ -269,7 +238,7 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST ); BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i); BooleanOrder* newBool; - Constraint* first, *second; + Edge first, second; if(tmp->second==boolOrder->first){ newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second); first = encodeTotalOrderSATEncoder(This, tmp); @@ -281,16 +250,16 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const second = encodeTotalOrderSATEncoder(This, tmp); }else continue; - Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool); + Edge transConstr= encodeTotalOrderSATEncoder(This, newBool); generateTransOrderConstraintSATEncoder(This, first, second, transConstr ); } return constraint; } */ - return NULL; + return E_BOGUS; } -Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { +Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { switch(GETPREDICATETYPE(constraint->predicate) ){ case TABLEPRED: return encodeTablePredicateSATEncoder(This, constraint); @@ -299,10 +268,10 @@ Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * con default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ +Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ switch(constraint->encoding.type){ case ENUMERATEIMPLICATIONS: case ENUMERATEIMPLICATIONSNEGATE: @@ -313,14 +282,14 @@ Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries); FunctionEncodingType encType = constraint->encoding.type; uint size = getSizeVectorTableEntry(entries); - Constraint* constraints[size]; + Edge constraints[size]; for(uint i=0; ioutput!= true) @@ -329,28 +298,25 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic continue; ArrayElement* inputs = &constraint->inputs; uint inputNum =getSizeArrayElement(inputs); - Constraint* carray[inputNum]; + Edge carray[inputNum]; for(uint j=0; jinputs[j]); - ASSERT(tmpc!= NULL); + Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]); if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){ - Constraint* func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el); - ASSERT(func!=NULL); - carray[j] = allocConstraint(AND, func, tmpc); + Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el); + carray[j] = constraintAND2(This->cnf, func, tmpc); } else { carray[j] = tmpc; } - ASSERT(carray[j]!= NULL); } - constraints[i]=allocArrayConstraint(AND, inputNum, carray); + constraints[i]=constraintAND(This->cnf, inputNum, carray); } - Constraint* result= allocArrayConstraint(OR, size, constraints); + Edge result=constraintOR(This->cnf, size, constraints); //FIXME: if it didn't match with any entry - return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result); + return encType==ENUMERATEIMPLICATIONS? result: constraintNegate(result); } -Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ +Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ switch(constraint->encoding.type){ case ENUMERATEIMPLICATIONS: return encodeEnumOperatorPredicateSATEncoder(This, constraint); @@ -360,10 +326,10 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ +Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED); PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; ASSERT(predicate->op == EQUALS); //For now, we just only support equals @@ -371,32 +337,29 @@ Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPre uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members); uint64_t commonElements [size]; getEqualitySetIntersection(predicate, &size, commonElements); - Constraint* carray[size]; + Edge carray[size]; Element* elem1 = getArrayElement( &constraint->inputs, 0); - Constraint *elemc1 = NULL, *elemc2 = NULL; + Edge elemc1 = E_NULL, elemc2 = E_NULL; if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN) elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1); Element* elem2 = getArrayElement( &constraint->inputs, 1); if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN) elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2); for(uint i=0; icnf, arg1, arg2); } //FIXME: the case when there is no intersection .... - Constraint* result = allocArrayConstraint(OR, size, carray); - ASSERT(result!= NULL); - if(elemc1!= NULL) - result = allocConstraint(AND, result, elemc1); - if(elemc2 != NULL) - result = allocConstraint (AND, result, elemc2); + Edge result = constraintOR(This->cnf, size, carray); + if (!edgeIsNull(elemc1)) + result = constraintAND2(This->cnf, result, elemc1); + if (!edgeIsNull(elemc2)) + result = constraintAND2(This->cnf, result, elemc2); return result; } -Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){ +Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){ switch(GETFUNCTIONTYPE(This->function)){ case TABLEFUNC: return encodeTableElementFunctionSATEncoder(encoder, This); @@ -405,10 +368,10 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ +Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ switch(getElementFunctionEncoding(This)->type){ case ENUMERATEIMPLICATIONS: return encodeEnumTableElemFunctionSATEncoder(encoder, This); @@ -419,17 +382,17 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun default: ASSERT(0); } - return NULL; + return E_BOGUS; } -Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ +Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC); ASSERT(getSizeArrayElement(&This->inputs)==2 ); ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) ); ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) ); - Constraint* carray[elem1->encArraySize*elem2->encArraySize]; + Edge carray[elem1->encArraySize*elem2->encArraySize]; uint size=0; - Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var; + Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var; for(uint i=0; iencArraySize; i++){ if(isinUseElement(elem1, i)){ for( uint j=0; jencArraySize; j++){ @@ -439,15 +402,12 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element elem2->encodingArray[j], &isInRange); //FIXME: instead of getElementValueConstraint, it might be useful to have another function // that doesn't iterate over encodingArray and treats more efficient ... - Constraint* valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]); - ASSERT(valConstrIn1 != NULL); - Constraint* valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]); - ASSERT(valConstrIn2 != NULL); - Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result); - if(valConstrOut == NULL) + Edge valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]); + Edge valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]); + Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result); + if(edgeIsNull(valConstrOut)) continue; //FIXME:Should talk to brian about it! - Constraint* OpConstraint = allocConstraint(IMPLIES, - allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut); + Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut); switch( ((FunctionOperator*)This->function)->overflowbehavior ){ case IGNORE: if(isInRange){ @@ -459,31 +419,23 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element break; case FLAGFORCESOVERFLOW: if(isInRange){ - Constraint* const1 = allocConstraint(IMPLIES, - allocConstraint(AND, valConstrIn1, valConstrIn2), - negateConstraint(overFlowConstraint)); - carray[size++] = allocConstraint(AND, const1, OpConstraint); + Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint)); + carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint); } break; case OVERFLOWSETSFLAG: if(isInRange){ carray[size++] = OpConstraint; } else{ - carray[size++] = allocConstraint(IMPLIES, - allocConstraint(AND, valConstrIn1, valConstrIn2), - overFlowConstraint); + carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint); } break; case FLAGIFFOVERFLOW: if(isInRange){ - Constraint* const1 = allocConstraint(IMPLIES, - allocConstraint(AND, valConstrIn1, valConstrIn2), - negateConstraint(overFlowConstraint)); - carray[size++] = allocConstraint(AND, const1, OpConstraint); - }else{ - carray[size++] = allocConstraint(IMPLIES, - allocConstraint(AND, valConstrIn1, valConstrIn2), - overFlowConstraint); + Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint)); + carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint); + } else { + carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint); } break; case NOOVERFLOW: @@ -500,29 +452,28 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element } } } - return allocArrayConstraint(AND, size, carray); + return constraintAND(encoder->cnf, size, carray); } -Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ +Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); ArrayElement* elements= &This->inputs; Table* table = ((FunctionTable*) (This->function))->table; uint size = getSizeVectorTableEntry(&table->entries); - Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries - for(uint i=0; ientries, i); - uint inputNum =getSizeArrayElement(elements); - Constraint* carray[inputNum]; + uint inputNum = getSizeArrayElement(elements); + Edge carray[inputNum]; for(uint j=0; jinputs[j]); - ASSERT(carray[j]!= NULL); } - Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output); - ASSERT(output!= NULL); - Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output); + Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output); + Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output); constraints[i]=row; } - Constraint* result = allocArrayConstraint(OR, size, constraints); + Edge result = constraintOR(encoder->cnf, size, constraints); return result; } + diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 0ada52b..0d6999f 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -4,38 +4,38 @@ #include "classlist.h" #include "structs.h" #include "inc_solver.h" +#include "constraint.h" struct SATEncoder { uint varcount; - IncrementalSolver* satSolver; + CNF * cnf; }; SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This); -Constraint * getNewVarSATEncoder(SATEncoder *This); -void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray); -Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); -Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); -Constraint * createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order); -Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair); -Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK); -Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); -Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); -Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); -Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); -Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge getNewVarSATEncoder(SATEncoder *This); +void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge*carray); +Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); +Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order); +Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair); +Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK); +Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); +Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); +Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value); -Constraint * getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value); +Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value); +Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value); -Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This); -Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); -Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); -Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This); -void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver); +Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This); +Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This); #endif diff --git a/src/Collections/structs.c b/src/Collections/structs.c index 0453231..29c7abe 100644 --- a/src/Collections/structs.c +++ b/src/Collections/structs.c @@ -5,7 +5,6 @@ VectorImpl(Table, Table *, 4); VectorImpl(Set, Set *, 4); VectorImpl(Boolean, Boolean *, 4); -VectorImpl(Constraint, Constraint *, 4); VectorImpl(Function, Function *, 4); VectorImpl(Predicate, Predicate *, 4); VectorImpl(Element, Element *, 4); diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 8700459..86addfb 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -13,7 +13,6 @@ ArrayDef(Set, Set *); VectorDef(Table, Table *); VectorDef(Set, Set *); VectorDef(Boolean, Boolean *); -VectorDef(Constraint, Constraint *); VectorDef(Function, Function *); VectorDef(Predicate, Predicate *); VectorDef(Element, Element *); diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c index a5158ab..2989b3b 100644 --- a/src/Encoders/elementencoding.c +++ b/src/Encoders/elementencoding.c @@ -35,7 +35,7 @@ void allocInUseArrayElement(ElementEncoding *This, uint size) { void allocElementConstraintVariables(ElementEncoding* This, uint numVars){ This->numVars = numVars; - This->variables = ourmalloc(sizeof(Constraint*) * numVars); + This->variables = ourmalloc(sizeof(Edge) * numVars); } void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){ diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index d51f5fa..797f301 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -2,6 +2,7 @@ #define ELEMENTENCODING_H #include "classlist.h" #include "naiveencoder.h" +#include "constraint.h" enum ElementEncodingType { ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL @@ -12,7 +13,7 @@ typedef enum ElementEncodingType ElementEncodingType; struct ElementEncoding { ElementEncodingType type; Element * element; - Constraint ** variables;/* List Variables Used To Encode Element */ + Edge * variables;/* List Variables Used To Encode Element */ uint64_t * encodingArray; /* List the Variables in the appropriate order */ uint64_t * inUseArray;/* Bitmap to track variables in use */ uint encArraySize; diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c index ddad6d7..06b83bb 100644 --- a/src/Test/testcnf.c +++ b/src/Test/testcnf.c @@ -1,4 +1,4 @@ -#include "nodeedge.h" +#include "constraint.h" #include int main(int numargs, char ** argv) { diff --git a/src/classlist.h b/src/classlist.h index c02268d..4f44aff 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -21,10 +21,6 @@ typedef struct CSolver CSolver; struct SATEncoder; typedef struct SATEncoder SATEncoder; - -struct Constraint; -typedef struct Constraint Constraint; - typedef struct BooleanOrder BooleanOrder; typedef struct BooleanVar BooleanVar; typedef struct BooleanLogic BooleanLogic; diff --git a/src/csolver.c b/src/csolver.c index 1d31e42..d903044 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -175,8 +175,7 @@ void startEncoding(CSolver* solver){ naiveEncodingDecision(solver); SATEncoder* satEncoder = allocSATEncoder(); encodeAllSATEncoder(solver, satEncoder); - finishedClauses(satEncoder->satSolver); - int result= solve(satEncoder->satSolver); + int result= solveCNF(satEncoder->cnf); model_print("sat_solver's result:%d\n", result); //For now, let's just delete it, and in future for doing queries //we may need it.