#Ignoring netbeans configs
nbproject/
+sat_solver
+setup.sh
#Ignoring binary files
src/bin/
src/lib_cons_comp.so
/src/mymemory.cc
.*
-*.dSYM
\ No newline at end of file
+*.dSYM
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;
}
#include "structs.h"
#include "astnode.h"
#include "functionencoding.h"
+#include "constraint.h"
/**
This is a little sketchy, but apparently legit.
struct BooleanVar {
Boolean base;
VarType vtype;
- Constraint * var;
+ Edge var;
};
struct BooleanLogic {
return &This->base;
}
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange){
+ uint64_t result = 0;
+ switch( func->op){
+ case ADD:
+ result = var1+ var2;
+ break;
+ case SUB:
+ result = var1 - var2;
+ break;
+ default:
+ ASSERT(0);
+ }
+ *isInRange = existsInSet(func->range, result);
+ return result;
+}
+
void deleteFunction(Function* This){
switch(GETFUNCTIONTYPE(This)){
case TABLEFUNC:
Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior);
Function* allocFunctionTable (Table* table);
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInrange);
void deleteFunction(Function* This);
#endif
allocInlineDefVectorBoolean(& order->constraints);
order->type=type;
allocOrderEncoding(& order->order, order);
- order->boolsToConstraints = allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+ order->boolsToConstraints = NULL;
return order;
}
+void initializeOrderHashTable(Order* order){
+ order->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+}
+
void addOrderConstraint(Order* order, BooleanOrder* constraint){
pushVectorBoolean( &order->constraints, (Boolean*) constraint);
}
void deleteOrder(Order* order){
deleteVectorArrayBoolean(& order->constraints);
deleteOrderEncoding(& order->order);
- deleteHashTableBoolConst(order->boolsToConstraints);
+ if(order->boolsToConstraints!= NULL) {
+ resetAndDeleteHashTableBoolConst(order->boolsToConstraints);
+ deleteHashTableBoolConst(order->boolsToConstraints);
+ }
ourfree(order);
}
};
Order* allocOrder(OrderType type, Set * set);
+void initializeOrderHashTable(Order * order);
void addOrderConstraint(Order* order, BooleanOrder* constraint);
void setOrderEncodingType(Order* order, OrderEncodingType type);
void deleteOrder(Order* order);
return tmp;
}
+bool existsInSet(Set* set, uint64_t element){
+ if(set->isRange){
+ return element >= set->low && element <= set->high;
+ }else {
+ uint size = getSizeVectorInt(set->members);
+ for(uint i=0; i< size; i++){
+ if(element == getVectorInt(set->members, i))
+ return true;
+ }
+ return false;
+ }
+}
+
uint getSetSize(Set* set){
if(set->isRange){
return set->high- set->low+1;
Set *allocSet(VarType t, uint64_t * elements, uint num);
Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);
+bool existsInSet(Set* set, uint64_t element);
uint getSetSize(Set* set);
void deleteSet(Set *set);
#endif/* SET_H */
}
void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result){
- ASSERT(getSizeArrayElement( &table->domains) == inputSize);
+ ASSERT(getSizeArraySet( &table->domains) == inputSize);
pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result));
}
--- /dev/null
+#include "cnfexpr.h"
+#include <stdio.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.
+*/
+
+#define LITCAPACITY 4
+#define MERGESIZE 5
+
+VectorImpl(LitVector, LitVector *, 4)
+
+static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
+
+LitVector * allocLitVector() {
+ LitVector *This=ourmalloc(sizeof(LitVector));
+ initLitVector(This);
+ return This;
+}
+
+void initLitVector(LitVector *This) {
+ This->size=0;
+ This->capacity=LITCAPACITY;
+ This->literals=ourmalloc(This->capacity * sizeof(Literal));
+}
+
+LitVector *cloneLitVector(LitVector *orig) {
+ LitVector *This=ourmalloc(sizeof(LitVector));
+ This->size=orig->size;
+ This->capacity=orig->capacity;
+ This->literals=ourmalloc(This->capacity * sizeof(Literal));
+ memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
+ return This;
+}
+
+void clearLitVector(LitVector *This) {
+ This->size=0;
+}
+
+void freeLitVector(LitVector *This) {
+ ourfree(This->literals);
+}
+
+void deleteLitVector(LitVector *This) {
+ freeLitVector(This);
+ ourfree(This);
+}
+
+Literal getLiteralLitVector(LitVector *This, uint index) {
+ return This->literals[index];
+}
+
+void setLiteralLitVector(LitVector *This, uint index, Literal l) {
+ This->literals[index]=l;
+}
+
+void addLiteralLitVector(LitVector *This, Literal l) {
+ Literal labs = abs(l);
+ uint vec_size=This->size;
+ uint searchsize=boundedSize(vec_size);
+ uint i=0;
+ for (; i < searchsize; i++) {
+ Literal curr = This->literals[i];
+ Literal currabs = abs(curr);
+ if (currabs > labs)
+ break;
+ if (currabs == labs) {
+ if (curr == -l)
+ This->size = 0; //either true or false now depending on whether this is a conj or disj
+ return;
+ }
+ }
+ if ((++This->size) >= This->capacity) {
+ This->capacity <<= 1;
+ This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
+ }
+
+ if (vec_size < MERGESIZE) {
+ memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
+ This->literals[i]=l;
+ } else {
+ This->literals[vec_size]=l;
+ }
+}
+
+CNFExpr * allocCNFExprBool(bool isTrue) {
+ CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+ This->litSize=0;
+ This->isTrue=isTrue;
+ allocInlineVectorLitVector(&This->clauses, 2);
+ initLitVector(&This->singletons);
+ return This;
+}
+
+CNFExpr * allocCNFExprLiteral(Literal l) {
+ CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+ This->litSize=1;
+ This->isTrue=false;
+ allocInlineVectorLitVector(&This->clauses, 2);
+ initLitVector(&This->singletons);
+ addLiteralLitVector(&This->singletons, l);
+ return This;
+}
+
+void clearCNFExpr(CNFExpr *This, bool isTrue) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
+ clearVectorLitVector(&This->clauses);
+ clearLitVector(&This->singletons);
+ This->litSize=0;
+ This->isTrue=isTrue;
+}
+
+void deleteCNFExpr(CNFExpr *This) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
+ deleteVectorArrayLitVector(&This->clauses);
+ freeLitVector(&This->singletons);
+ ourfree(This);
+}
+
+void conjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0 && !This->isTrue) //Handle False
+ return;
+
+ This->litSize-=getSizeLitVector(&This->singletons);
+ addLiteralLitVector(&This->singletons, l);
+ uint newsize=getSizeLitVector(&This->singletons);
+ if (newsize==0)
+ clearCNFExpr(This, false); //We found a conflict
+ else
+ This->litSize+=getSizeLitVector(&This->singletons);
+}
+
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ if (destroy) {
+ ourfree(This->singletons.literals);
+ ourfree(This->clauses.array);
+ This->litSize=expr->litSize;
+ This->singletons.literals=expr->singletons.literals;
+ This->singletons.capacity=expr->singletons.capacity;
+ This->clauses.size=expr->clauses.size;
+ This->clauses.array=expr->clauses.array;
+ This->clauses.capacity=expr->clauses.capacity;
+ ourfree(expr);
+ } else {
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ addLiteralLitVector(&This->singletons, l);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+ }
+ This->litSize=expr->litSize;
+ }
+}
+
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ if (expr->litSize==0) {
+ if (!This->isTrue) {
+ clearCNFExpr(This, false);
+ }
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ if (This->litSize==0) {
+ if (This->isTrue) {
+ copyCNF(This, expr, destroy);
+ } else if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ uint litSize=This->litSize;
+ litSize-=getSizeLitVector(&expr->singletons);
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ addLiteralLitVector(&This->singletons, l);
+ if (getSizeLitVector(&This->singletons)==0) {
+ //Found conflict...
+ clearCNFExpr(This, false);
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ }
+ litSize+=getSizeLitVector(&expr->singletons);
+ if (destroy) {
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ litSize+=getSizeLitVector(lv);
+ pushVectorLitVector(&This->clauses, lv);
+ }
+ clearVectorLitVector(&expr->clauses);
+ deleteCNFExpr(expr);
+ } else {
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ litSize+=getSizeLitVector(lv);
+ pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+ }
+ }
+ This->litSize=litSize;
+}
+
+void disjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0) {
+ if (!This->isTrue) {
+ This->litSize++;
+ addLiteralLitVector(&This->singletons, l);
+ }
+ return;
+ }
+
+ uint litSize=0;
+ uint newindex=0;
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ LitVector * lv=getVectorLitVector(&This->clauses, i);
+ addLiteralLitVector(lv, l);
+ uint newSize=getSizeLitVector(lv);
+ if (newSize!=0) {
+ setVectorLitVector(&This->clauses, newindex++, lv);
+ } else {
+ deleteLitVector(lv);
+ }
+ litSize+=newSize;
+ }
+ setSizeVectorLitVector(&This->clauses, newindex);
+
+ bool hasSameSingleton=false;
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ Literal lsing=getLiteralLitVector(&This->singletons, i);
+ if (lsing == l) {
+ hasSameSingleton=true;
+ } else if (lsing != -l) {
+ //Create new LitVector with both l and lsing
+ LitVector *newlitvec=allocLitVector();
+ addLiteralLitVector(newlitvec, l);
+ addLiteralLitVector(newlitvec, lsing);
+ litSize+=2;
+ pushVectorLitVector(&This->clauses, newlitvec);
+ }
+ }
+ clearLitVector(&This->singletons);
+ if (hasSameSingleton) {
+ addLiteralLitVector(&This->singletons, l);
+ litSize++;
+ } else if (litSize==0) {
+ This->isTrue=true;//we are true
+ }
+ This->litSize=litSize;
+}
+
+#define MERGETHRESHOLD 2
+LitVector * mergeLitVectors(LitVector *This, LitVector *expr) {
+ uint maxsize=This->size+expr->size+MERGETHRESHOLD;
+ LitVector *merged=ourmalloc(sizeof(LitVector));
+ merged->literals=ourmalloc(sizeof(Literal)*maxsize);
+ merged->capacity=maxsize;
+ uint thisSize=boundedSize(This->size);
+ uint exprSize=boundedSize(expr->size);
+ uint iThis=0, iExpr=0, iMerge=0;
+ Literal lThis=This->literals[iThis];
+ Literal lExpr=expr->literals[iExpr];
+ Literal thisAbs=abs(lThis);
+ Literal exprAbs=abs(lExpr);
+
+ while(iThis<thisSize && iExpr<exprSize) {
+ if (thisAbs<exprAbs) {
+ merged->literals[iMerge++]=lThis;
+ lThis=This->literals[++iThis];
+ thisAbs=abs(lThis);
+ } else if(thisAbs>exprAbs) {
+ merged->literals[iMerge++]=lExpr;
+ lExpr=expr->literals[++iExpr];
+ exprAbs=abs(lExpr);
+ } else if(lThis==lExpr) {
+ merged->literals[iMerge++]=lExpr;
+ lExpr=expr->literals[++iExpr];
+ exprAbs=abs(lExpr);
+ lThis=This->literals[++iThis];
+ thisAbs=abs(lThis);
+ } else if(lThis==-lExpr) {
+ merged->size=0;
+ return merged;
+ }
+ }
+ if (iThis < thisSize) {
+ memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize-iThis) * sizeof(Literal));
+ iMerge += (thisSize-iThis);
+ }
+ if (iExpr < exprSize) {
+ memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize-iExpr) * sizeof(Literal));
+ iMerge += (exprSize-iExpr);
+ }
+ merged->size=iMerge;
+ return merged;
+}
+
+LitVector * mergeLitVectorLiteral(LitVector *This, Literal l) {
+ LitVector *copy=cloneLitVector(This);
+ addLiteralLitVector(copy, l);
+ return copy;
+}
+
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ /** Handle the special cases */
+ if (expr->litSize == 0) {
+ if (expr->isTrue) {
+ clearCNFExpr(This, true);
+ }
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ } else if (This->litSize == 0) {
+ if (!This->isTrue) {
+ copyCNF(This, expr, destroy);
+ } else if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ } else if (expr->litSize == 1) {
+ disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ } else if (destroy && This->litSize == 1) {
+ Literal l=getLiteralLitVector(&This->singletons,0);
+ copyCNF(This, expr, true);
+ disjoinCNFLit(This, l);
+ return;
+ }
+
+ /** Handle the full cross product */
+ uint mergeIndex=0;
+ uint newCapacity=getClauseSizeCNF(This)*getClauseSizeCNF(expr);
+ LitVector ** mergeArray=ourmalloc(newCapacity*sizeof(LitVector*));
+ uint singleIndex=0;
+ /** First do the singleton, clause pairs */
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ Literal lThis=getLiteralLitVector(&This->singletons, i);
+ for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);j++) {
+ LitVector * lExpr=getVectorLitVector(&expr->clauses, j);
+ LitVector * copy=cloneLitVector(lExpr);
+ addLiteralLitVector(copy, lThis);
+ if (getSizeLitVector(copy)==0) {
+ deleteLitVector(copy);
+ } else {
+ mergeArray[mergeIndex++]=copy;
+ }
+ }
+ }
+
+ /** Next do the clause, singleton pairs */
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal lExpr=getLiteralLitVector(&expr->singletons, i);
+ for(uint j=0;j<getSizeVectorLitVector(&This->clauses);j++) {
+ LitVector * lThis=getVectorLitVector(&This->clauses, j);
+ LitVector * copy=cloneLitVector(lThis);
+ addLiteralLitVector(copy, lExpr);
+ if (getSizeLitVector(copy)==0) {
+ deleteLitVector(copy);
+ } else {
+ mergeArray[mergeIndex++]=copy;
+ }
+ }
+ }
+
+ /** Next do the clause, clause pairs */
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ LitVector * lThis=getVectorLitVector(&This->clauses, i);
+ for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);j++) {
+ LitVector * lExpr=getVectorLitVector(&expr->clauses, j);
+ LitVector * merge=mergeLitVectors(lThis, lExpr);
+ if (getSizeLitVector(merge)==0) {
+ deleteLitVector(merge);
+ } else {
+ mergeArray[mergeIndex++]=merge;
+ }
+ }
+ deleteLitVector(lThis);//Done with this litVector
+ }
+
+ /** Finally do the singleton, singleton pairs */
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ Literal lThis=getLiteralLitVector(&This->singletons, i);
+ for(uint j=0;j<getSizeLitVector(&expr->singletons);j++) {
+ Literal lExpr=getLiteralLitVector(&expr->singletons, j);
+ if (lThis==lExpr) {
+ //We have a singleton still in the final result
+ setLiteralLitVector(&This->singletons, singleIndex++, lThis);
+ } else if (lThis!=-lExpr) {
+ LitVector *mergeLV=allocLitVector();
+ addLiteralLitVector(mergeLV, lThis);
+ addLiteralLitVector(mergeLV, lExpr);
+ mergeArray[mergeIndex++]=mergeLV;
+ }
+ }
+ }
+
+ ourfree(This->clauses.array);
+ setSizeLitVector(&This->singletons, singleIndex);
+ This->clauses.capacity=newCapacity;
+ This->clauses.array=mergeArray;
+ This->clauses.size=mergeIndex;
+ if (destroy)
+ deleteCNFExpr(expr);
+}
+
+void printCNFExpr(CNFExpr *This) {
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ if (i!=0)
+ printf(" ^ ");
+ Literal l=getLiteralLitVector(&This->singletons,i);
+ printf ("%d",l);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&This->clauses,i);
+ printf(" ^ (");
+ for(uint j=0;j<getSizeLitVector(lv);j++) {
+ if (j!=0)
+ printf(" v ");
+ printf("%d", getLiteralLitVector(lv, j));
+ }
+ printf(")");
+ }
+}
--- /dev/null
+#ifndef CNFEXPR_H
+#define CNFEXPR_H
+#include "classlist.h"
+#include "vector.h"
+
+typedef int Literal;
+
+
+struct LitVector {
+ uint size;
+ uint capacity;
+ Literal *literals;
+};
+typedef struct LitVector LitVector;
+
+VectorDef(LitVector, LitVector *)
+
+struct CNFExpr {
+ uint litSize;
+ bool isTrue;
+ VectorLitVector clauses;
+ LitVector singletons;
+};
+
+typedef struct CNFExpr CNFExpr;
+
+LitVector * allocLitVector();
+void initLitVector(LitVector *This);
+void clearLitVector(LitVector *This);
+void freeLitVector(LitVector *This);
+LitVector *cloneLitVector(LitVector *orig);
+void deleteLitVector(LitVector *This);
+void addLiteralLitVector(LitVector *This, Literal l);
+Literal getLiteralLitVector(LitVector *This, uint index);
+void setLiteralLitVector(LitVector *This, uint index, Literal l);
+LitVector * mergeLitVectorLiteral(LitVector *This, Literal l);
+LitVector * mergeLitVectors(LitVector *This, LitVector *expr);
+
+static inline uint getSizeLitVector(LitVector *This) {return This->size;}
+static inline void setSizeLitVector(LitVector *This, uint size) {This->size=size;}
+
+CNFExpr * allocCNFExprBool(bool isTrue);
+CNFExpr * allocCNFExprLiteral(Literal l);
+void deleteCNFExpr(CNFExpr *This);
+void clearCNFExpr(CNFExpr *This, bool isTrue);
+void printCNFExpr(CNFExpr *This);
+
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
+static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}
+static inline bool alwaysFalseCNF(CNFExpr * This) {return (This->litSize==0) && !This->isTrue;}
+static inline uint getLitSizeCNF(CNFExpr * This) {return This->litSize;}
+static inline uint getClauseSizeCNF(CNFExpr * This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
+void conjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
+
+#endif
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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 <string.h>
+#include <stdlib.h>
#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);
-}
-
-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;i<This->numoperandsorvar;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;i<cnf->capacity;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;
- ourfree(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;i<oldCapacity;i++) {
+ Node *n=old_array[i];
+ uint hashCode=n->hashCode;
+ 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;i<This->numoperandsorvar;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<numEdges;i++) {
+ hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
+ hashvalue = (hashvalue << 3) | (hashvalue >> 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;i<This->numoperandsorvar;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;i<numEdges;i++) {
+ if (!equalsEdge(nodeedges[i], edges[i]))
+ return false;
+ }
+ return true;
+}
+
+Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
+ Edge edgearray[numEdges];
+
+ for(uint i=0; i<numEdges; i++) {
+ edgearray[i]=constraintNegate(edges[i]);
+ }
+ Edge eand=constraintAND(cnf, numEdges, edgearray);
+ return constraintNegate(eand);
+}
+
+Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
+ Edge lneg=constraintNegate(left);
+ Edge rneg=constraintNegate(right);
+ Edge eand=constraintAND2(cnf, lneg, rneg);
+ return constraintNegate(eand);
+}
+
+int comparefunction(const Edge * e1, const Edge * e2) {
+ return ((uintptr_t)e1->node_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(initindex<numEdges && equalsEdge(edges[initindex], E_True))
+ initindex++;
+
+ uint remainSize=numEdges-initindex;
+
+ if (remainSize == 0)
+ return E_True;
+ else if (remainSize == 1)
+ return edges[initindex];
+ else if (equalsEdge(edges[initindex], E_False))
+ return E_False;
+
+ /** De-duplicate array */
+ uint lowindex=0;
+ edges[lowindex]=edges[initindex++];
+
+ for(;initindex<numEdges;initindex++) {
+ Edge e1=edges[lowindex];
+ Edge e2=edges[initindex];
+ if (sameNodeVarEdge(e1, e2)) {
+ if (!sameSignEdge(e1, e2)) {
+ return E_False;
}
- printConstraint(This->operands[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:
- 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;i<This->numoperandsorvar;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; i<numConstraints;i++) {
+ countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
}
+ deleteVectorEdge(ve);
}
-Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) {
- Constraint *carray[numvars];
- for(uint j=0;j<numvars;j++) {
- carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
- value=value>>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;i<n->numEdges;i++) {
+ Edge succ=n->edges[i];
+ if(!edgeIsVarConst(succ)) {
+ succ=constraintNegateIf(succ, polarity);
+ 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; i<numConstraints;i++) {
+ convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, 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<numvars;j++) {
- if ((val&1)==1)
- orarray[ori++]=negateConstraint(vars[j]);
- val=val>>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; i<n->numEdges; 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;i<numvars;i++) {
- array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
- array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
+
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
+ Literal l = 0;
+ Node * n = getNodePtrFromEdge(e);
+
+ if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) n->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);
}
- return allocArrayConstraint(AND, numvars*2, array);
+ // 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;i<getSizeVectorConstraint(from);i++) {
- Constraint *c=getVectorConstraint(from, i);
- if (c->type==TRUE)
- continue;
- if (c->type==FALSE) {
- for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
- freerecConstraint(getVectorConstraint(from,j));
- for(uint j=0;j<getSizeVectorConstraint(to);j++)
- freerecConstraint(getVectorConstraint(to, j));
- clearVectorConstraint(to);
- pushVectorConstraint(to, &ctrue);
- deleteVectorConstraint(from);
- return true;
+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));
}
- 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;i<This->numoperandsorvar;i++) {
- VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
- if (mergeandfree(vec, subvec)) {
- for(uint j=i+1;j<This->numoperandsorvar;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;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ Literal clause[] = {-lcond, l};
+ addArrayClauseLiteral(cnf->solver, 2, clause);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);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;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ Literal clause[] = {l};
+ addArrayClauseLiteral(cnf->solver, 1, clause);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);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;i<This->numoperandsorvar;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;j<This->numoperandsorvar;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;j<This->numoperandsorvar;j++)
- if (j!=i)
- array[index++]=This->operands[j];
- for(uint j=0;j<c->numoperandsorvar;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;j<This->numoperandsorvar;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;i<n->numEdges;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;j<c->numoperandsorvar;j++) {
- //copy other elements
- for(uint k=0;k<This->numoperandsorvar;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;i<This->numoperandsorvar;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<numvars;j++) {
+ carray[j]=((value&1)==1) ? vars[j] : constraintNegate(vars[j]);
+ value=value>>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<numvars;j++) {
+ if ((val&1)==1)
+ orarray[ori++]=constraintNegate(vars[j]);
+ val=val>>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<numvars;i++) {
+ array[i]=constraintIFF(cnf, var1[i], var2[i]);
}
+ return constraintAND(cnf, numvars, array);
}
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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;
+
+struct Edge {
+ Node * node_ptr;
+};
+
+VectorDef(Edge, Edge)
+
+enum NodeType {
+ NodeType_AND,
+ NodeType_ITE,
+ NodeType_IFF
+};
+
+typedef enum NodeType NodeType;
-enum ConstraintType {
- TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS
+struct NodeFlags {
+ NodeType type:2;
+ int varForced:1;
+ int wasExpanded:2;
+ int cnfVisitedDown:2;
+ int cnfVisitedUp:2;
};
-typedef enum ConstraintType CType;
+typedef struct NodeFlags NodeFlags;
-struct Constraint {
- CType type;
- uint numoperandsorvar;
- Constraint ** operands;
- Constraint *neg;
+struct Node {
+ NodeFlags flags;
+ uint numEdges;
+ uint hashCode;
+ uint intAnnot[2];
+ void * ptrAnnot[2];
+ Edge edges[];
};
-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);
-
-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 * simplify(Constraint * c);
-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);
-
-extern Constraint ctrue;
-extern Constraint cfalse;
-
-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);
+#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<<isNegated);
+}
+
+static inline void setExpanded(Node *n, int isNegated) {
+ n->flags.wasExpanded |= (1<<isNegated);
+}
+
+static inline Edge constraintNegate(Edge e) {
+ Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+ return enew;
+}
+
+static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
+ return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
+}
+
+static inline bool sameSignEdge(Edge e1, Edge e2) {
+ return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool sameNodeOppSign(Edge e1, Edge e2) {
+ return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
+}
+
+static inline bool isNegEdge(Edge e) {
+ return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
+}
+
+static inline bool isPosEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool isNodeEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
+}
+
+static inline bool isNegNodeEdge(Edge e) {
+ return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
+}
+
+static inline Node * getNodePtrFromEdge(Edge e) {
+ return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
+}
+
+static inline NodeType getNodeType(Edge e) {
+ Node * n=getNodePtrFromEdge(e);
+ return n->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);
+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);
+
+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
#define SATSOLVER "sat_solver"
#include <fcntl.h>
#include "common.h"
+#include <string.h>
IncrementalSolver * allocIncrementalSolver() {
IncrementalSolver *This=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
ourfree(This->buffer);
if (This->solution != NULL)
ourfree(This->solution);
+ ourfree(This);
}
void resetSolver(IncrementalSolver * This) {
}
}
+void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) {
+ uint index=0;
+ while(true) {
+ uint bufferspace=IS_BUFFERSIZE-This->offset;
+ uint numtowrite=numliterals-index;
+ if (bufferspace > numtowrite) {
+ memcpy(&This->buffer[This->offset], &literals[index], numtowrite*sizeof(int));
+ This->offset+=numtowrite;
+ This->buffer[This->offset++]=0; //have one extra spot always
+ if (This->offset==IS_BUFFERSIZE) {//Check if full
+ flushBufferSolver(This);
+ }
+ return;
+ } else {
+ memcpy(&This->buffer[This->offset], &literals[index], bufferspace*sizeof(int));
+ This->offset+=bufferspace;
+ index+=bufferspace;
+ flushBufferSolver(This);
+ }
+ }
+}
+
void finishedClauses(IncrementalSolver * This) {
addClauseLiteral(This, 0);
}
waitpid(This->solver_pid, &status, 0);
}
}
+bool first=true;
void flushBufferSolver(IncrementalSolver * This) {
ssize_t bytestowrite=sizeof(int)*This->offset;
ssize_t byteswritten=0;
+ for(uint i=0;i<This->offset;i++) {
+ if (first)
+ printf("(");
+ if (This->buffer[i]==0) {
+ printf(")\n");
+ first=true;
+ } else {
+ if (!first)
+ printf(" + ");
+ first=false;
+ printf("%d", This->buffer[i]);
+ }
+ }
do {
ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
if (n == -1) {
IncrementalSolver * allocIncrementalSolver();
void deleteIncrementalSolver(IncrementalSolver * This);
void addClauseLiteral(IncrementalSolver * This, int literal);
+void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals);
void finishedClauses(IncrementalSolver * This);
void freeze(IncrementalSolver * This, int variable);
int solve(IncrementalSolver * This);
+++ /dev/null
-#include "nodeedge.h"
-#include <string.h>
-#include <stdlib.h>
-
-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);
- return cnf;
-}
-
-void deleteCNF(CNF * cnf) {
- for(uint i=0;i<cnf->capacity;i++) {
- Node *n=cnf->node_array[i];
- if (n!=NULL)
- ourfree(n);
- }
- 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;i<oldCapacity;i++) {
- Node *n=old_array[i];
- uint hashCode=n->hashCode;
- 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->numEdges=numEdges;
- n->flags.type=type;
- n->hashCode=hashcode;
- 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<numEdges;i++) {
- hashvalue ^= (uint) edges[i].node_ptr;
- hashvalue = (hashvalue << 3) | (hashvalue >> 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;i<numEdges;i++) {
- if (!equalsEdge(nodeedges[i], edges[i]))
- return false;
- }
- return true;
-}
-
-Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
- Edge edgearray[numEdges];
-
- for(uint i=0; i<numEdges; i++) {
- edgearray[i]=constraintNegate(edges[i]);
- }
- Edge eand=constraintAND(cnf, numEdges, edgearray);
- return constraintNegate(eand);
-}
-
-Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
- Edge lneg=constraintNegate(left);
- Edge rneg=constraintNegate(right);
- Edge eand=constraintAND2(cnf, left, right);
- return constraintNegate(eand);
-}
-
-int comparefunction(const Edge * e1, const Edge * e2) {
- return ((uintptr_t)e1->node_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(initindex<numEdges && equalsEdge(edges[initindex], E_True))
- initindex++;
-
- uint remainSize=numEdges-initindex;
-
- if (remainSize == 0)
- return E_True;
- else if (remainSize == 1)
- return edges[initindex];
- else if (equalsEdge(edges[initindex], E_False))
- return E_False;
-
- /** De-duplicate array */
- uint lowindex=0;
- edges[lowindex++]=edges[initindex++];
-
- for(;initindex<numEdges;initindex++) {
- Edge e1=edges[lowindex];
- Edge e2=edges[initindex];
- if (sameNodeVarEdge(e1, e2)) {
- if (!sameSignEdge(e1, e2)) {
- return E_False;
- }
- } else
- edges[lowindex++]=edges[initindex];
- }
- if (lowindex==1)
- return edges[0];
-
- if (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]));
- }
- }
-
- return createNode(cnf, NodeType_AND, numEdges, 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;
-}
-
-Edge constraintNewVar(CNF *cnf) {
- uint varnum=cnf->varcount++;
- Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
- return e;
-}
+++ /dev/null
-#ifndef NODEEDGE_H
-#define NODEEDGE_H
-#include "classlist.h"
-
-#define NEGATE_EDGE 1
-#define EDGE_IS_VAR_CONSTANT 2
-#define VAR_SHIFT 2
-#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
-
-struct Edge;
-typedef struct Edge Edge;
-
-struct Node;
-typedef struct Node Node;
-
-struct Edge {
- Node * node_ptr;
-};
-
-enum NodeType {
- NodeType_AND,
- NodeType_ITE,
- NodeType_IFF
-};
-
-typedef enum NodeType NodeType;
-
-struct NodeFlags {
- NodeType type:2;
-};
-
-typedef struct NodeFlags NodeFlags;
-
-struct Node {
- NodeFlags flags;
- uint numEdges;
- uint hashCode;
- Edge edges[];
-};
-
-#define DEFAULT_CNF_ARRAY_SIZE 256
-#define LOAD_FACTOR 0.25
-#define enableMatching 1
-
-struct CNF {
- uint varcount;
- uint capacity;
- uint size;
- uint mask;
- uint maxsize;
- Node ** node_array;
-};
-
-typedef struct CNF CNF;
-
-static inline Edge constraintNegate(Edge e) {
- Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
- return enew;
-}
-
-static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
- return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
-}
-
-static inline bool sameSignEdge(Edge e1, Edge e2) {
- return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
-}
-
-static inline bool sameNodeOppSign(Edge e1, Edge e2) {
- return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
-}
-
-static inline bool isNegEdge(Edge e) {
- return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
-}
-
-static inline bool isNodeEdge(Edge e) {
- return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
-}
-
-static inline bool isNegNodeEdge(Edge e) {
- return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
-}
-
-static inline Node * getNodePtrFromEdge(Edge e) {
- return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
-}
-
-static inline NodeType getNodeType(Edge e) {
- Node * n=getNodePtrFromEdge(e);
- return n->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;
-}
-
-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);
-
-Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
-Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
-#endif
#include "orderpair.h"
-OrderPair* allocOrderPair(uint64_t first, uint64_t second){
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint){
OrderPair* pair = (OrderPair*) ourmalloc(sizeof(OrderPair));
pair->first = first;
pair->second = second;
+ pair->constraint = constraint;
return pair;
}
+
void deleteOrderPair(OrderPair* pair){
ourfree(pair);
-}
\ No newline at end of file
+}
#include "classlist.h"
#include "mymemory.h"
+#include "constraint.h"
struct OrderPair{
uint64_t first;
uint64_t second;
+ Edge constraint;
};
-OrderPair* allocOrderPair(uint64_t first, uint64_t second);
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint);
void deleteOrderPair(OrderPair* pair);
#endif /* ORDERPAIR_H */
SATEncoder * allocSATEncoder() {
SATEncoder *This=ourmalloc(sizeof (SATEncoder));
This->varcount=1;
+ This->cnf=createCNF();
return This;
}
void deleteSATEncoder(SATEncoder *This) {
+ deleteCNF(This->cnf);
ourfree(This);
}
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
- /** We really should not walk the free list to generate constraint
- variables...walk the constraint tree instead. Or even better
- yet, just do this as you need to during the encodeAllSATEncoder
- walk. */
-
-// FIXME!!!!(); // Make sure Hamed sees comment above
-
- uint size = getSizeVectorElement(csolver->allElements);
- for(uint i=0; i<size; i++){
- Element* element = getVectorElement(csolver->allElements, i);
- generateElementEncodingVariables(This,getElementEncoding(element));
- }
-}
-
-
-Constraint * getElementValueConstraint(Element* This, uint64_t value) {
- 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);
break;
case UNARY:
ASSERT(0);
break;
case BINARYINDEX:
- ASSERT(0);
+ return getElementValueBinaryIndexConstraint(This, elem, value);
break;
case ONEHOTBINARY:
- return getElementValueBinaryIndexConstraint(This, value);
+ ASSERT(0);
break;
case BINARYVAL:
ASSERT(0);
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; i<elemEnc->encArraySize; 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;
+ return E_BOGUS;
}
void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
uint size=getSizeVectorBoolean(constraints);
for(uint i=0;i<size;i++) {
Boolean *constraint=getVectorBoolean(constraints, i);
- encodeConstraintSATEncoder(This, constraint);
+ Edge c= encodeConstraintSATEncoder(This, constraint);
+ printCNF(c);
+ printf("\n");
+ addConstraint(This->cnf, c);
}
-
-// FIXME: Following line for element!
-// size = getSizeVectorElement(csolver->allElements);
-// for(uint i=0; i<size; i++){
-// Element* element = getVectorElement(csolver->allElements, i);
-// switch(GETELEMENTTYPE(element)){
-// case ELEMFUNCRETURN:
-// encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
-// break;
-// default:
-// continue;
-// //ElementSets that aren't used in any constraints/functions
-// //will be eliminated.
-// }
-// }
}
-Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
switch(GETBOOLEANTYPE(constraint)) {
case ORDERCONST:
return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
}
}
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) {
for(uint i=0;i<num;i++)
carray[i]=getNewVarSATEncoder(encoder);
}
-Constraint * getNewVarSATEncoder(SATEncoder *This) {
- Constraint * var=allocVarConstraint(VAR, This->varcount);
- 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;i<getSizeArrayBoolean(&constraint->inputs);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(constraint->numArray==1);
- return negateConstraint(array[0]);
- case L_XOR: {
- ASSERT(constraint->numArray==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]));
- }
+ ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
+ return constraintNegate(array[0]);
+ case L_XOR:
+ ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
+ return constraintXOR(This->cnf, array[0], array[1]);
case L_IMPLIES:
- ASSERT(constraint->numArray==2);
- return allocConstraint(IMPLIES, array[0], array[1]);
+ ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
+ return constraintIMPLIES(This->cnf, array[0], array[1]);
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
}
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
+Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
switch( constraint->order->type){
case PARTIAL:
return encodePartialOrderSATEncoder(This, constraint);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
+Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+ bool negate = false;
+ OrderPair flipped;
+ if (pair->first > pair->second) {
+ negate=true;
+ flipped.first=pair->second;
+ flipped.second=pair->first;
+ pair = &flipped; //FIXME: accessing a local variable from outside of the function?
+ }
+ Edge constraint;
+ if (!containsBoolConst(table, pair)) {
+ constraint = getNewVarSATEncoder(This);
+ OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
+ putBoolConst(table, paircopy, paircopy);
+ } else
+ constraint = getBoolConst(table, pair)->constraint;
+ if (negate)
+ return constraintNegate(constraint);
+ else
+ return constraint;
+
+}
-Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
ASSERT(boolOrder->order->type == TOTAL);
- HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
- OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second);
- if( !containsBoolConst(boolToConsts, pair) ){
+ if(boolOrder->order->boolsToConstraints == NULL){
+ initializeOrderHashTable(boolOrder->order);
createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
}
- Constraint* constraint = getOrderConstraint(boolToConsts, pair);
- deleteOrderPair(pair);
+ HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+ OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
+ Edge constraint = getPairConstraint(This, boolToConsts, & pair);
return constraint;
}
VectorInt* mems = order->set->members;
HashTableBoolConst* table = order->boolsToConstraints;
uint size = getSizeVectorInt(mems);
+ uint csize =0;
for(uint i=0; i<size; i++){
uint64_t valueI = getVectorInt(mems, i);
for(uint j=i+1; j<size;j++){
uint64_t valueJ = getVectorInt(mems, j);
- OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
- ASSERT(!containsBoolConst(table, pairIJ));
- Constraint* constIJ = getNewVarSATEncoder(This);
- putBoolConst(table, pairIJ, constIJ);
+ OrderPair pairIJ = {valueI, valueJ};
+ Edge constIJ=getPairConstraint(This, table, & pairIJ);
for(uint k=j+1; k<size; k++){
uint64_t valueK = getVectorInt(mems, k);
- OrderPair* pairJK = allocOrderPair(valueJ, valueK);
- OrderPair* pairIK = allocOrderPair(valueI, valueK);
- Constraint* constJK, *constIK;
- if(!containsBoolConst(table, pairJK)){
- constJK = getNewVarSATEncoder(This);
- putBoolConst(table, pairJK, constJK);
- }
- if(!containsBoolConst(table, pairIK)){
- constIK = getNewVarSATEncoder(This);
- putBoolConst(table, pairIK, constIK);
- }
- generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
+ OrderPair pairJK = {valueJ, valueK};
+ OrderPair pairIK = {valueI, valueK};
+ Edge constIK = getPairConstraint(This, table, & pairIK);
+ Edge constJK = getPairConstraint(This, table, & pairJK);
+ addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
}
}
}
}
-Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
ASSERT(pair->first!= pair->second);
- Constraint* constraint= getBoolConst(table, pair);
- ASSERT(constraint!= NULL);
+ 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!
- 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!)
- ASSERT(boolOrder->order->type == PARTIAL);
+ ASSERT(constraint->order->type == PARTIAL);
/*
HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
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);
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);
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);
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:
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; i<size; i++){
TableEntry* entry = getVectorTableEntry(entries, i);
if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
continue;
ArrayElement* inputs = &constraint->inputs;
uint inputNum =getSizeArrayElement(inputs);
- Constraint* carray[inputNum];
- Element* el = getArrayElement(inputs, i);
+ Edge carray[inputNum];
for(uint j=0; j<inputNum; j++){
- carray[j] = getElementValueConstraint(el, entry->inputs[j]);
+ Element* el = getArrayElement(inputs, j);
+ Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
+ if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
+ Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
+ carray[j] = constraintAND2(This->cnf, func, tmpc);
+ } else {
+ carray[j] = tmpc;
+ }
}
- 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);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
- ASSERT(GETPREDICATETYPE(constraint)==OPERATORPRED);
+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
//getting maximum size of in common elements between two sets!
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);
+ 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; i<size; i++){
-
- carray[i] = allocConstraint(AND, getElementValueConstraint(elem1, commonElements[i]),
- getElementValueConstraint(elem2, commonElements[i]) );
+ Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
+ Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
+ carray[i] = constraintAND2(This->cnf, arg1, arg2);
}
//FIXME: the case when there is no intersection ....
- return allocArrayConstraint(OR, size, carray);
+ 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);
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);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
- //FIXME: for now it just adds/substracts inputs exhustively
- return NULL;
+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) );
+ Edge carray[elem1->encArraySize*elem2->encArraySize];
+ uint size=0;
+ Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
+ for(uint i=0; i<elem1->encArraySize; i++){
+ if(isinUseElement(elem1, i)){
+ for( uint j=0; j<elem2->encArraySize; j++){
+ if(isinUseElement(elem2, j)){
+ bool isInRange = false;
+ uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
+ 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 ...
+ 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!
+ Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
+ switch( ((FunctionOperator*)This->function)->overflowbehavior ){
+ case IGNORE:
+ if(isInRange){
+ carray[size++] = OpConstraint;
+ }
+ break;
+ case WRAPAROUND:
+ carray[size++] = OpConstraint;
+ break;
+ case FLAGFORCESOVERFLOW:
+ if(isInRange){
+ 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++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
+ }
+ break;
+ case FLAGIFFOVERFLOW:
+ if(isInRange){
+ 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:
+ if(!isInRange){
+ ASSERT(0);
+ }
+ carray[size++] = OpConstraint;
+ break;
+ default:
+ ASSERT(0);
+ }
+
+ }
+ }
+ }
+ }
+ 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; i<size; i++){
+ Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
+ for(uint i=0; i<size; i++) {
TableEntry* entry = getVectorTableEntry(&table->entries, i);
- uint inputNum =getSizeArrayElement(elements);
- Element* el= getArrayElement(elements, i);
- Constraint* carray[inputNum];
+ uint inputNum = getSizeArrayElement(elements);
+ Edge carray[inputNum];
for(uint j=0; j<inputNum; j++){
- carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+ Element* el= getArrayElement(elements, j);
+ carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
}
- Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
- getElementValueBinaryIndexConstraint((Element*)This, entry->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;
}
+
#include "classlist.h"
#include "structs.h"
+#include "inc_solver.h"
+#include "constraint.h"
struct SATEncoder {
uint varcount;
+ CNF * cnf;
};
SATEncoder * allocSATEncoder();
void deleteSATEncoder(SATEncoder *This);
-void initializeConstraintVars(CSolver* csolver, 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);
+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);
-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 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(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);
+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
bool contains ## Name(const HashTable ## Name * tab, _Key key); \
void resize ## Name(HashTable ## Name * tab, unsigned int newsize); \
double getLoadFactor ## Name(HashTable ## Name * tab); \
- unsigned int getCapacity ## Name(HashTable ## Name * tab);
+ unsigned int getCapacity ## Name(HashTable ## Name * tab); \
+ void resetAndDeleteHashTable ## Name(HashTable ## Name * tab);
-#define HashTableImpl(Name, _Key, _Val, hash_function, equals) \
+#define HashTableImpl(Name, _Key, _Val, hash_function, equals, freefunction) \
HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \
HashTable ## Name * tab = (HashTable ## Name *)ourmalloc(sizeof(HashTable ## Name)); \
tab->table = (struct hashlistnode ## Name *)ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \
tab->size = 0; \
return tab; \
} \
- \
- void deleteHashTable ## Name(HashTable ## Name * tab) { \
+ \
+ void deleteHashTable ## Name(HashTable ## Name * tab) { \
ourfree(tab->table); \
if (tab->zero) \
ourfree(tab->zero); \
ourfree(tab); \
} \
- \
+ \
+ void resetAndDeleteHashTable ## Name(HashTable ## Name * tab) { \
+ for(uint i=0;i<tab->capacity;i++) { \
+ struct hashlistnode ## Name * bin=&tab->table[i]; \
+ if (bin->key!=NULL) { \
+ bin->key=NULL; \
+ if (bin->val!=NULL) { \
+ freefunction(bin->val); \
+ bin->val=NULL; \
+ } \
+ } \
+ } \
+ if (tab->zero) { \
+ if (tab->zero->val != NULL) \
+ freefunction(tab->zero->val); \
+ ourfree(tab->zero); \
+ tab->zero=NULL; \
+ } \
+ tab->size=0; \
+ } \
+ \
void reset ## Name(HashTable ## Name * tab) { \
memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \
if (tab->zero) { \
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);
return key1 == key2;
}
-inline unsigned int order_pair_hash_Function(OrderPair* This){
- uint64_t x=This->first^This->second;
- uint64_t a=This->first&This->second;
- return (uint)((x<<4)^(a));
+static inline unsigned int order_pair_hash_Function(OrderPair* This){
+ return (uint) (This->first << 2) ^ This->second;
}
-inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
+static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
return key1->first== key2->first && key1->second == key2->second;
}
-HashTableImpl(BoolConst, OrderPair *, Constraint *, order_pair_hash_Function, order_pair_equals);
+HashTableImpl(BoolConst, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);
ArrayDef(Boolean, Boolean *);
ArrayDef(Set, Set *);
-
-VectorDef(Table, Table *, 4);
-VectorDef(Set, Set *, 4);
-VectorDef(Boolean, Boolean *, 4);
-VectorDef(Constraint, Constraint *, 4);
-VectorDef(Function, Function *, 4);
-VectorDef(Predicate, Predicate *, 4);
-VectorDef(Element, Element *, 4);
-VectorDef(Order, Order *, 4);
-VectorDef(TableEntry, TableEntry *, 4);
-VectorDef(ASTNode, ASTNode *, 4);
-VectorDef(Int, uint64_t, 4);
-
-
+VectorDef(Table, Table *);
+VectorDef(Set, Set *);
+VectorDef(Boolean, Boolean *);
+VectorDef(Function, Function *);
+VectorDef(Predicate, Predicate *);
+VectorDef(Element, Element *);
+VectorDef(Order, Order *);
+VectorDef(TableEntry, TableEntry *);
+VectorDef(ASTNode, ASTNode *);
+VectorDef(Int, uint64_t);
HashTableDef(Void, void *, void *);
-HashTableDef(BoolConst, OrderPair *, Constraint *);
+HashTableDef(BoolConst, OrderPair *, OrderPair *);
HashSetDef(Void, void *);
#define VECTOR_H
#include <string.h>
-#define VectorDef(name, type, defcap) \
+#define VectorDef(name, type) \
struct Vector ## name { \
uint size; \
uint capacity; \
Vector ## name * allocDefVector ## name(); \
Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
void pushVector ## name(Vector ## name *vector, type item); \
- type getVector ## name(Vector ## name *vector, uint index); \
+ type lastVector ## name(Vector ## name *vector); \
+ void popVector ## name(Vector ## name *vector); \
+ type getVector ## name(Vector ## name *vector, uint index); \
void setVector ## name(Vector ## name *vector, uint index, type item); \
uint getSizeVector ## name(Vector ## name *vector); \
+ void setSizeVector ## name(Vector ## name *vector, uint size); \
void deleteVector ## name(Vector ## name *vector); \
void clearVector ## name(Vector ## name *vector); \
void deleteVectorArray ## name(Vector ## name *vector); \
Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
tmp->size = 0; \
tmp->capacity = capacity; \
- tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity); \
+ tmp->array = (type *) ourmalloc(sizeof(type) * capacity); \
return tmp; \
} \
Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \
memcpy(tmp->array, array, capacity * sizeof(type)); \
return tmp; \
} \
- void pushVector ## name(Vector ## name *vector, type item) { \
- if (vector->size >= vector->capacity) { \
- uint newcap=vector->capacity * 2; \
- vector->array=(type *)ourrealloc(vector->array, newcap); \
+ void popVector ## name(Vector ## name *vector) { \
+ vector->size--; \
+ } \
+ type lastVector ## name(Vector ## name *vector) { \
+ return vector->array[vector->size-1]; \
+ } \
+ void setSizeVector ## name(Vector ## name *vector, uint size) { \
+ if (size <= vector->size) { \
+ vector->size=size; \
+ return; \
+ } else if (size > vector->capacity) { \
+ vector->array=(type *)ourrealloc(vector->array, size * sizeof(type)); \
+ vector->capacity=size; \
+ } \
+ bzero(&vector->array[vector->size], (size-vector->size)*sizeof(type)); \
+ vector->size=size; \
+ } \
+ void pushVector ## name(Vector ## name *vector, type item) { \
+ if (vector->size >= vector->capacity) { \
+ uint newcap=vector->capacity << 1; \
+ vector->array=(type *)ourrealloc(vector->array, newcap * sizeof(type)); \
+ vector->capacity=newcap; \
} \
vector->array[vector->size++] = item; \
} \
void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
vector->size = 0; \
vector->capacity = capacity; \
- vector->array = (type *) ourcalloc(1, sizeof(type) * capacity); \
+ vector->array = (type *) ourmalloc(sizeof(type) * capacity); \
} \
void allocInlineDefVector ## name(Vector ## name * vector) { \
allocInlineVector ## name(vector, defcap); \
}
void allocInUseArrayElement(ElementEncoding *This, uint size) {
- This->inUseArray=ourcalloc(1, size >> 6);
+ uint bytes = ((size + ((1 << 9)-1)) >> 6)&~7;//Depends on size of inUseArray
+ This->inUseArray=ourcalloc(1, bytes);
}
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){
void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){
ASSERT(This->type!=ELEM_UNASSIGNED);
- ASSERT(This->variables==NULL);
+ if(This->variables!=NULL)
+ return;
switch(This->type){
case BINARYINDEX:
generateBinaryIndexEncodingVars(encoder, This);
#define ELEMENTENCODING_H
#include "classlist.h"
#include "naiveencoder.h"
+#include "constraint.h"
enum ElementEncodingType {
ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
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;
void deleteElementEncoding(ElementEncoding *This);
void allocEncodingArrayElement(ElementEncoding *This, uint size);
void allocInUseArrayElement(ElementEncoding *This, uint size);
-//FIXME
-//uint addNewVariableToEncodingArray(ElementEncoding* This, uint64_t var);
static inline bool isinUseElement(ElementEncoding *This, uint offset) {
return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
}
DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
-CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections
+CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend
all: $(OBJECTS) ../bin/run.sh
Order * o=createOrder(solver, TOTAL, s);
Boolean * oc=orderConstraint(solver, o, 1, 2);
addBoolean(solver, oc);
+
+ uint64_t set2[] = {2, 3};
+ Set* rangef1 = createSet(solver, 1, set2, 2);
+ Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
+
+ Table* table = createTable(solver, domain, 2, s);
+ uint64_t row1[] = {0, 1};
+ uint64_t row2[] = {1, 1};
+ uint64_t row3[] = {2, 1};
+ uint64_t row4[] = {1, 2};
+ addTableEntry(solver, table, row1, 2, 0);
+ addTableEntry(solver, table, row2, 2, 1);
+ addTableEntry(solver, table, row3, 2, 2);
+ addTableEntry(solver, table, row4, 2, 2);
+ Function * f2 = completeTable(solver, table); //its range would be as same as s
+
+ Boolean* overflow = getBooleanVar(solver , 2);
+ Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
+ Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
+ Set* domain2[] = {s,rangef1};
+ Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
+ Element* inputs2 [] = {e4, e3};
+ Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
+ addBoolean(solver, pred);
+
+ startEncoding(solver);
deleteSolver(solver);
}
export LD_LIBRARY_PATH=../bin
# For Mac OSX
export DYLD_LIBRARY_PATH=../bin
+# For sat_solver
+export PATH=.:$PATH
$@
--- /dev/null
+#include "constraint.h"
+#include <stdio.h>
+
+int main(int numargs, char ** argv) {
+ CNF *cnf=createCNF();
+ Edge v1=constraintNewVar(cnf);
+ Edge v2=constraintNewVar(cnf);
+ Edge v3=constraintNewVar(cnf);
+ Edge v4=constraintNewVar(cnf);
+ Edge v5=constraintNewVar(cnf);
+
+ Edge nv1=constraintNegate(v1);
+ Edge nv2=constraintNegate(v2);
+ Edge nv3=constraintNegate(v3);
+ Edge nv4=constraintNegate(v4);
+
+ Edge c1=constraintAND2(cnf, v1, nv2);
+ Edge c2=constraintAND2(cnf, v3, nv4);
+ Edge c3=constraintAND2(cnf, nv1, v2);
+ Edge c4=constraintAND2(cnf, nv3, v4);
+ Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+ printCNF(cor);
+ printf("\n");
+ addConstraint(cnf, cor);
+ int value=solveCNF(cnf);
+ if (value==1) {
+ bool v1v=getValueCNF(cnf, v1);
+ bool v2v=getValueCNF(cnf, v2);
+ bool v3v=getValueCNF(cnf, v3);
+ bool v4v=getValueCNF(cnf, v4);
+ printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
+ } else
+ printf("%d\n",value);
+ deleteCNF(cnf);
+}
struct SATEncoder;
typedef struct SATEncoder SATEncoder;
-
-struct Constraint;
-typedef struct Constraint Constraint;
-
typedef struct BooleanOrder BooleanOrder;
typedef struct BooleanVar BooleanVar;
typedef struct BooleanLogic BooleanLogic;
--- /dev/null
+#include "common.h"
+
+void assert_hook(void)
+{
+ model_print("Add breakpoint to line %u in file %s.\n", __LINE__, __FILE__);
+}
\ No newline at end of file
#endif
#ifndef CONFIG_ASSERT
-//#define CONFIG_ASSERT
+#define CONFIG_ASSERT
#endif
#endif
return constraint;
}
-void encode(CSolver* solver){
+void startEncoding(CSolver* solver){
naiveEncodingDecision(solver);
SATEncoder* satEncoder = allocSATEncoder();
- initializeConstraintVars(solver, satEncoder);
encodeAllSATEncoder(solver, satEncoder);
+ 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.
deleteSATEncoder(satEncoder);
-}
\ No newline at end of file
+}
Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
/** When everything is done, the client calls this function and then csolver starts to encode*/
-void encode(CSolver*);
+void startEncoding(CSolver*);
#endif
projects / satune.git / commitdiff