src/AST/boolean.c

   1 #include "boolean.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "element.h"
   5 #include "order.h"
   6
   7 Boolean* allocBooleanVar(VarType t) {
   8         BooleanVar* This=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
   9         GETBOOLEANTYPE(This)=BOOLEANVAR;
  10         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  11         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  12         This->vtype=t;
  13         This->var=E_NULL;
  14         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  15         return & This->base;
  16 }
  17
  18 Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
  19         BooleanOrder* This=(BooleanOrder *) ourmalloc(sizeof (BooleanOrder));
  20         GETBOOLEANTYPE(This)=ORDERCONST;
  21         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  22         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  23         This->order=order;
  24         This->first=first;
  25         This->second=second;
  26         pushVectorBoolean(&order->constraints, &This->base);
  27         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  28         return & This -> base;
  29 }
  30
  31 Boolean * allocBooleanInterOrder(Order * order1, uint64_t first,Order* order2, uint64_t second){
  32         BooleanInterOrder* This=(BooleanInterOrder *) ourmalloc(sizeof (BooleanInterOrder));
  33         GETBOOLEANTYPE(This)=INTERORDERCONST;
  34         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  35         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  36         This->order1=order1;
  37         This->order2 = order2;
  38         This->first=first;
  39         This->second=second;
  40         pushVectorBoolean(&order1->constraints, &This->base);
  41         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  42         return & This -> base;
  43 }
  44
  45 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
  46         BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
  47         GETBOOLEANTYPE(This)= PREDICATEOP;
  48         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  49         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  50         This->predicate=predicate;
  51         initArrayInitElement(&This->inputs, inputs, numInputs);
  52         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  53
  54         for(uint i=0;i<numInputs;i++) {
  55                 pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
  56         }
  57         initPredicateEncoding(&This->encoding, (Boolean *) This);
  58         This->undefStatus = undefinedStatus;
  59         return & This->base;
  60 }
  61
  62 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
  63         BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
  64         GETBOOLEANTYPE(This) = LOGICOP;
  65         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  66         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  67         This->op = op;
  68         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  69         initArrayInitBoolean(&This->inputs, array, asize);
  70         pushVectorBoolean(solver->allBooleans, (Boolean *) This);
  71         return & This->base;
  72 }
  73
  74 void deleteBoolean(Boolean * This) {
  75         switch(GETBOOLEANTYPE(This)){
  76                 case PREDICATEOP:{
  77                         BooleanPredicate *bp=(BooleanPredicate *)This;
  78                         deleteInlineArrayElement(& bp->inputs );
  79                         deleteFunctionEncoding(& bp->encoding);
  80                         break;
  81                 }
  82                 case LOGICOP:{
  83                         BooleanLogic* bl = (BooleanLogic*) This;
  84                         deleteInlineArrayBoolean(&bl->inputs);
  85                         break;
  86                 }
  87                 default:
  88                         break;
  89         }
  90         deleteVectorArrayBoolean(GETBOOLEANPARENTS(This));
  91         ourfree(This);
  92 }
  93
  94
  95 Polarity negatePolarity(Polarity This){
  96         switch(This){
  97                 case P_UNDEFINED:
  98                 case P_BOTHTRUEFALSE:
  99                         return This;
 100                 case P_TRUE:
 101                         return P_FALSE;
 102                 case P_FALSE:
 103                         return P_TRUE;
 104                 default:
 105                         ASSERT(0);
 106         }
 107 }
 108
 109 BooleanValue negateBooleanValue(BooleanValue This){
 110         switch(This){
 111                 case BV_UNDEFINED:
 112                 case BV_UNKNOWN:
 113                         return This;
 114                 case BV_MUSTBETRUE:
 115                         return BV_MUSTBEFALSE;
 116                 case BV_MUSTBEFALSE:
 117                         return BV_MUSTBETRUE;
 118                 default:
 119                         ASSERT(0);
 120         }
 121 }
 122