Commit after resolving conflicts
authorHamed <hamed.gorjiara@gmail.com>
Tue, 20 Jun 2017 18:12:02 +0000 (11:12 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Tue, 20 Jun 2017 18:12:02 +0000 (11:12 -0700)
17 files changed:
design/notes.txt
src/AST/boolean.c
src/AST/boolean.h
src/AST/element.c
src/AST/element.h
src/AST/function.c
src/AST/function.h
src/AST/ops.h
src/Backend/constraint.h
src/Backend/satencoder.c [new file with mode: 0644]
src/Backend/satencoder.h [new file with mode: 0644]
src/Encoders/elementencoding.c
src/Encoders/functionencoding.c
src/Encoders/orderencoding.c [new file with mode: 0644]
src/Encoders/orderencoding.h [new file with mode: 0644]
src/classlist.h
src/csolver.c

index 1159c96..ce399c3 100644 (file)
@@ -6,3 +6,6 @@
 
 (4) Might need to indicate what variables we can query about in
 future?
+
+(5) Could simplify output of functions...  Maybe several outputs have
+same effect...
index 0d3e892..831a200 100644 (file)
@@ -6,6 +6,7 @@ Boolean* allocBoolean(VarType t) {
        BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
        GETBOOLEANTYPE(tmp)=BOOLEANVAR;
        tmp->vtype=t;
+       tmp->var=NULL;
        return & tmp->base;
 }
 
index fd59a21..0222fc7 100644 (file)
@@ -25,6 +25,7 @@ struct BooleanOrder {
 struct BooleanVar {
        Boolean base;
        VarType vtype;
+       Constraint * var;
 };
 
 struct BooleanLogic {
index 903256d..3746d25 100644 (file)
@@ -1,11 +1,12 @@
 #include "element.h"
 #include "structs.h"
-
-Element *allocElementSet(Set * s) {
-       ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet));
+//FIXME: ELEMENTSET?
+Element *allocElement(Set * s) {
+       Element * tmp=(Element *)ourmalloc(sizeof(Element));
        GETELEMENTTYPE(tmp)= ELEMSET;
        tmp->set=s;
-       return &tmp->base;
+       tmp->encoding=NULL;
+       return tmp;
 }
 
 Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus){
index 4119b7d..0a23d88 100644 (file)
@@ -7,8 +7,11 @@
 
 #define GETELEMENTTYPE(o) (((Element*)o)->type)
 
+//FIXME:TALK ABOUT ELEMENT
 struct Element {
-       ElementType type;
+       ElementType type;
+       Set * set;
+       ElementEncoding * encoding;
 };
 
 struct ElementSet {
@@ -23,7 +26,7 @@ struct ElementFunction{
     Boolean * overflowstatus;
 };
 
-Element * allocElementSet(Set *s);
+Element * allocElement(Set *s);
 Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus);
 void deleteElement(Element *This);
 #endif
index c9d0717..c816363 100644 (file)
@@ -4,30 +4,31 @@
 
 
 Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior){
-    FunctionOperator* This = (FunctionOperator*) ourmalloc(sizeof(FunctionOperator));
-    GETFUNCTIONTYPE(This)=OPERATORFUNC;
-    This->domains = allocVectorArraySet(numDomain, domain);
-    This->op=op;
-    This->overflowbehavior = overflowbehavior;
-    This->range=range;
-    return  &This->base;
+       FunctionOperator* This = (FunctionOperator*) ourmalloc(sizeof(FunctionOperator));
+       GETFUNCTIONTYPE(This)=OPERATORFUNC;
+       This->domains = allocVectorArraySet(numDomain, domain);
+       This->op=op;
+       This->overflowbehavior = overflowbehavior;
+       This->range=range;
+       return &This->base;
 }
 
 Function* allocFunctionTable (Table* table){
-    FunctionTable* This = (FunctionTable*) ourmalloc(sizeof(FunctionTable));
-    GETFUNCTIONTYPE(This)=TABLEFUNC;
-    This->table = table;
+       FunctionTable* This = (FunctionTable*) ourmalloc(sizeof(FunctionTable));
+       GETFUNCTIONTYPE(This)=TABLEFUNC;
+       This->table = table;
+       return &This->base;
 }
 
 void deleteFunction(Function* This){
-    switch( GETFUNCTIONTYPE(This)){
+       switch(GETFUNCTIONTYPE(This)){
        case TABLEFUNC:
-           ourfree((FunctionTable*)This);
-           break;
+               ourfree((FunctionTable*)This);
+               break;
        case OPERATORFUNC:
-           ourfree((FunctionOperator*) This);
-           break;
+               ourfree((FunctionOperator*) This);
+               break;
        default:
-           ASSERT(0);
-    }
+               ASSERT(0);
+       }
 }
index e22ec75..3f2a1a9 100644 (file)
@@ -5,7 +5,6 @@
 #include "ops.h"
 #include "structs.h"
 
-
 #define GETFUNCTIONTYPE(o) (((Function*)o)->type)
 
 struct Function{
index adbef8d..9fa2966 100644 (file)
@@ -1,6 +1,6 @@
 #ifndef OPS_H
 #define OPS_H
-enum LogicOp {AND, OR, NOT, XOR, IMPLIES};
+enum LogicOp {L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES};
 typedef enum LogicOp LogicOp;
 
 enum ArithOp {ADD, SUB};
index 4b59812..d6e7e86 100644 (file)
@@ -33,15 +33,15 @@ Constraint * allocVarConstraint(CType t, uint var);
 void deleteConstraint(Constraint *);
 void printConstraint(Constraint * c);
 void dumpConstraint(Constraint * c, IncrementalSolver *solver);
-uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
+inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
 VectorConstraint * simplify(Constraint * c);
-CType getType(Constraint * c) {return c->type;}
-bool isFalse(Constraint * c) {return c->type==FALSE;}
-bool isTrue(Constraint * c) {return c->type==TRUE;}
+inline CType getType(Constraint * c) {return c->type;}
+inline bool isFalse(Constraint * c) {return c->type==FALSE;}
+inline bool isTrue(Constraint * c) {return c->type==TRUE;}
 void internalfreeConstraint(Constraint * c);
 void freerecConstraint(Constraint * c);
 Constraint * cloneConstraint(Constraint * c);
-void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
+inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
 Constraint *negateConstraint(Constraint * c);
 
 extern Constraint ctrue;
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
new file mode 100644 (file)
index 0000000..0eb2346
--- /dev/null
@@ -0,0 +1,79 @@
+#include "satencoder.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "constraint.h"
+
+SATEncoder * allocSATEncoder() {
+       SATEncoder *This=ourmalloc(sizeof (SATEncoder));
+       This->varcount=1;
+       return This;
+}
+
+void deleteSATEncoder(SATEncoder *This) {
+       ourfree(This);
+}
+
+void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
+       VectorBoolean *constraints=csolver->constraints;
+       uint size=getSizeVectorBoolean(constraints);
+       for(uint i=0;i<size;i++) {
+               Boolean *constraint=getVectorBoolean(constraints, i);
+               encodeConstraintSATEncoder(This, constraint);
+       }
+}
+
+Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+       switch(constraint->btype) {
+       case ORDERCONST:
+               return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
+       case BOOLEANVAR:
+               return encodeVarSATEncoder(This, (BooleanVar *) constraint);
+       case LOGICOP:
+               return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
+       }
+}
+
+Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
+       return NULL;
+}
+
+Constraint * getNewVarSATEncoder(SATEncoder *This) {
+       Constraint * var=allocVarConstraint(VAR, This->varcount);
+       Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
+       setNegConstraint(var, varneg);
+       setNegConstraint(varneg, var);
+       return var;
+}
+
+Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
+       if (constraint->var == NULL) {
+               constraint->var=getNewVarSATEncoder(This);
+       }
+       return constraint->var;
+}
+
+Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
+       Constraint *left=encodeConstraintSATEncoder(This, constraint->left);
+       Constraint *right=NULL;
+       if (constraint->right!=NULL)
+               right=encodeConstraintSATEncoder(This, constraint->right);
+       switch(constraint->op) {
+       case L_AND:
+               return allocConstraint(AND, left, right);
+       case L_OR:
+               return allocConstraint(OR, left, right);
+       case L_NOT:
+               return negateConstraint(allocConstraint(OR, left, NULL));
+       case L_XOR: {
+               Constraint * nleft=negateConstraint(cloneConstraint(left));
+               Constraint * nright=negateConstraint(cloneConstraint(right));
+               return allocConstraint(OR,
+                                                                                                        allocConstraint(AND, left, nright),
+                                                                                                        allocConstraint(AND, nleft, right));
+       }
+       case L_IMPLIES:
+               return allocConstraint(IMPLIES, left, right);
+       }
+       return NULL;
+}
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
new file mode 100644 (file)
index 0000000..ea5de8b
--- /dev/null
@@ -0,0 +1,20 @@
+#ifndef SATENCODER_H
+#define SATENCODER_H
+
+#include "classlist.h"
+
+struct SATEncoder {
+       uint varcount;
+};
+
+
+SATEncoder * allocSATEncoder();
+void deleteSATEncoder(SATEncoder *This);
+void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
+Constraint * getNewVarSATEncoder(SATEncoder *This);
+Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
+Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
+Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
+Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
+
+#endif
index fb2ce4a..08385db 100644 (file)
@@ -1,7 +1,7 @@
 #include "elementencoding.h"
 
 ElementEncoding * allocElementEncoding(ElementEncodingType type, Element *element) {
-       ElementEncoding * This=(ElementEncoding *)ourmalloc(sizeof(ElementEncoding));
+       ElementEncoding * This=ourmalloc(sizeof(ElementEncoding));
        This->element=element;
        This->type=type;
        This->variables=NULL;
index 4520fa0..d0f8c3d 100644 (file)
@@ -1,14 +1,14 @@
 #include "functionencoding.h"
 
 FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function) {
-       FunctionEncoding * This=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding));
+       FunctionEncoding * This=ourmalloc(sizeof(FunctionEncoding));
        This->op.function=function;
        This->type=type;
        return This;
 }
 
 FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate) {
-       FunctionEncoding * This=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding));
+       FunctionEncoding * This=ourmalloc(sizeof(FunctionEncoding));
        This->op.predicate=predicate;
        This->type=type;
        return This;
diff --git a/src/Encoders/orderencoding.c b/src/Encoders/orderencoding.c
new file mode 100644 (file)
index 0000000..3cd78e1
--- /dev/null
@@ -0,0 +1,12 @@
+#include "orderencoding.h"
+
+OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order) {
+       OrderEncoding *This=ourmalloc(sizeof(OrderEncoding));
+       This->type=type;
+       This->order=order;
+       return This;
+}
+
+void deleteOrderEncoding(OrderEncoding *This) {
+       ourfree(This);
+}
diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
new file mode 100644 (file)
index 0000000..89c436a
--- /dev/null
@@ -0,0 +1,19 @@
+#ifndef ORDERENCODING_H
+#define ORDERENCODING_H
+#include "classlist.h"
+
+enum OrderEncodingType {
+       PAIRWISE
+};
+
+typedef enum OrderEncodingType OrderEncodingType;
+
+struct OrderEncoding {
+       OrderEncodingType type;
+       Order *order;
+};
+
+OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order);
+void deleteOrderEncoding(OrderEncoding *This);
+
+#endif
index 14f43f8..3306ffe 100644 (file)
@@ -18,6 +18,9 @@
 
 struct CSolver;
 typedef struct CSolver CSolver;
+struct SATEncoder;
+typedef struct SATEncoder SATEncoder;
+
 
 struct Constraint;
 typedef struct Constraint Constraint;
@@ -36,7 +39,6 @@ typedef struct IncrementalSolver IncrementalSolver;
 
 struct Set;
 typedef struct Set Set;
-
 typedef struct Set MutableSet;
 
 typedef struct ElementFunction ElementFunction;
@@ -66,6 +68,9 @@ typedef struct ElementEncoding ElementEncoding;
 struct FunctionEncoding;
 typedef struct FunctionEncoding FunctionEncoding;
 
+struct OrderEncoding;
+typedef struct OrderEncoding OrderEncoding;
+
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 
index 2ec12db..b35680c 100644 (file)
@@ -30,33 +30,38 @@ void deleteSolver(CSolver *This) {
        for(uint i=0;i<size;i++) {
                deleteBoolean(getVectorBoolean(This->allBooleans, i));
        }
-
        deleteVectorBoolean(This->allBooleans);
 
        size=getSizeVectorSet(This->allSets);
        for(uint i=0;i<size;i++) {
                deleteSet(getVectorSet(This->allSets, i));
        }
-
        deleteVectorSet(This->allSets);
 
        size=getSizeVectorElement(This->allElements);
        for(uint i=0;i<size;i++) {
                deleteElement(getVectorElement(This->allElements, i));
        }
+       deleteVectorElement(This->allElements);
+
        size=getSizeVectorTable(This->allTables);
        for(uint i=0;i<size;i++) {
                deleteTable(getVectorTable(This->allTables, i));
        }
+       deleteVectorTable(This->allTables);
+       
        size=getSizeVectorPredicate(This->allPredicates);
        for(uint i=0;i<size;i++) {
                deletePredicate(getVectorPredicate(This->allPredicates, i));
        }
+       deleteVectorPredicate(This->allPredicates);
+
        size=getSizeVectorOrder(This->allOrders);
        for(uint i=0;i<size;i++) {
                deleteOrder(getVectorOrder(This->allOrders, i));
        }
        deleteVectorOrder(This->allOrders);
+       
        size=getSizeVectorFunction(This->allFunctions);
        for(uint i=0;i<size;i++) {
                deleteFunction(getVectorFunction(This->allFunctions, i));
@@ -94,7 +99,7 @@ uint64_t createUniqueItem(CSolver *solver, MutableSet * set) {
 }
 
 Element * getElementVar(CSolver *This, Set * set) {
-       Element * element=allocElementSet(set);
+       Element * element=allocElement(set);
        pushVectorElement(This->allElements, element);
        return element;
 }