From fc1dd990c4a5d55165ff08da878fbda71dee83cf Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 19 Jun 2017 16:34:52 -0700 Subject: [PATCH] edits --- src/AST/ops.h | 2 +- src/Backend/constraint.h | 10 ++++---- src/Backend/satencoder.c | 50 +++++++++++++++++++++++++++++++++++- src/Backend/satencoder.h | 7 ++++- src/Encoders/orderencoding.c | 4 ++- src/Encoders/orderencoding.h | 11 ++++++-- 6 files changed, 73 insertions(+), 11 deletions(-) diff --git a/src/AST/ops.h b/src/AST/ops.h index 3541808..3b3e3c3 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -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}; diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 4b59812..d6e7e86 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -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 index a2f96d5..3b34c3a 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -1,6 +1,8 @@ #include "satencoder.h" #include "structs.h" #include "csolver.h" +#include "boolean.h" +#include "constraint.h" SATEncoder * allocSATEncoder() { SATEncoder *This=ourmalloc(sizeof (SATEncoder)); @@ -20,6 +22,52 @@ void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) { } } -void encodeConstraintSATEncoder(SATEncoder *This, Boolean *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); + case COMPARE: + return encodeCompareSATEncoder(This, (BooleanComp *) constraint); + } +} + +Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { + return NULL; +} + +Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) { + return NULL; +} + +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; +} +Constraint * encodeCompareSATEncoder(SATEncoder *This, BooleanComp * constraint) { + return NULL; } diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 9145e2b..a612930 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -11,5 +11,10 @@ struct SATEncoder { SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver); -void encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); +Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); +Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); +Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); +Constraint * encodeCompareSATEncoder(SATEncoder *This, BooleanComp * constraint); + #endif diff --git a/src/Encoders/orderencoding.c b/src/Encoders/orderencoding.c index fcef2f3..3cd78e1 100644 --- a/src/Encoders/orderencoding.c +++ b/src/Encoders/orderencoding.c @@ -1,7 +1,9 @@ #include "orderencoding.h" -OrderEncoding * allocOrderEncoding() { +OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order) { OrderEncoding *This=ourmalloc(sizeof(OrderEncoding)); + This->type=type; + This->order=order; return This; } diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h index c0e4c00..89c436a 100644 --- a/src/Encoders/orderencoding.h +++ b/src/Encoders/orderencoding.h @@ -2,11 +2,18 @@ #define ORDERENCODING_H #include "classlist.h" -struct OrderEncoding { +enum OrderEncodingType { + PAIRWISE +}; +typedef enum OrderEncodingType OrderEncodingType; + +struct OrderEncoding { + OrderEncodingType type; + Order *order; }; -OrderEncoding * allocOrderEncoding(); +OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order); void deleteOrderEncoding(OrderEncoding *This); #endif -- 2.34.1