return & This -> base;
}
-Boolean * allocBooleanInterOrder(Order * order1, uint64_t first,Order* order2, uint64_t second){
- BooleanInterOrder* This=(BooleanInterOrder *) ourmalloc(sizeof (BooleanInterOrder));
- GETBOOLEANTYPE(This)=INTERORDERCONST;
- GETBOOLEANVALUE(This) = BV_UNDEFINED;
- GETBOOLEANPOLARITY(This) = P_UNDEFINED;
- This->order1=order1;
- This->order2 = order2;
- This->first=first;
- This->second=second;
- pushVectorBoolean(&order1->constraints, &This->base);
- initDefVectorBoolean(GETBOOLEANPARENTS(This));
- return & This -> base;
-}
-
Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
GETBOOLEANTYPE(This)= PREDICATEOP;
uint64_t second;
};
-//I don't like the name, we may want to change it later --HG
-struct BooleanInterOrder{
- Boolean base;
- Order* order1;
- uint64_t first;
- Order* order2;
- uint64_t second;
-};
-
struct BooleanVar {
Boolean base;
VarType vtype;
Boolean * allocBooleanVar(VarType t);
Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
-Boolean * allocBooleanInterOrder(Order * order1, uint64_t first,Order* order2, uint64_t second);
Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
void deleteBoolean(Boolean * This);
enum PredicateType {TABLEPRED, OPERATORPRED};
typedef enum PredicateType PredicateType;
-enum ASTNodeType {INTERORDERCONST, ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
typedef enum ASTNodeType ASTNodeType;
enum Polarity {P_UNDEFINED, P_TRUE, P_FALSE, P_BOTHTRUEFALSE};
typedef struct SATEncoder SATEncoder;
typedef struct BooleanOrder BooleanOrder;
-typedef struct BooleanInterOrder BooleanInterOrder;
typedef struct BooleanVar BooleanVar;
typedef struct BooleanLogic BooleanLogic;
typedef struct BooleanPredicate BooleanPredicate;
return constraint;
}
-Boolean * interOrderConstraint(CSolver * This, Order * order1, uint64_t first, Order* order2, uint64_t second){
- Boolean* constraint = allocBooleanInterOrder(order1, first, order2, second);
- pushVectorBoolean(This->allBooleans, constraint);
- return constraint;
-}
-
int startEncoding(CSolver* This){
naiveEncodingDecision(This);
SATEncoder* satEncoder = This->satEncoder;
/** This function instantiates a boolean on two items in an order. */
Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
-Boolean * interOrderConstraint(CSolver *, Order * order1, uint64_t first, Order* order2, uint64_t second);
-
/** When everything is done, the client calls this function and then csolver starts to encode*/
int startEncoding(CSolver*);