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 * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
  32         BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
  33         GETBOOLEANTYPE(This)= PREDICATEOP;
  34         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  35         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  36         This->predicate=predicate;
  37         initArrayInitElement(&This->inputs, inputs, numInputs);
  38         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  39
  40         for(uint i=0;i<numInputs;i++) {
  41                 pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
  42         }
  43         initPredicateEncoding(&This->encoding, (Boolean *) This);
  44         This->undefStatus = undefinedStatus;
  45         return & This->base;
  46 }
  47
  48 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
  49         BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
  50         GETBOOLEANTYPE(This) = LOGICOP;
  51         GETBOOLEANVALUE(This) = BV_UNDEFINED;
  52         GETBOOLEANPOLARITY(This) = P_UNDEFINED;
  53         This->op = op;
  54         initDefVectorBoolean(GETBOOLEANPARENTS(This));
  55         initArrayInitBoolean(&This->inputs, array, asize);
  56         pushVectorBoolean(solver->allBooleans, (Boolean *) This);
  57         return & This->base;
  58 }
  59
  60 void deleteBoolean(Boolean * This) {
  61         switch(GETBOOLEANTYPE(This)){
  62                 case PREDICATEOP:{
  63                         BooleanPredicate *bp=(BooleanPredicate *)This;
  64                         deleteInlineArrayElement(& bp->inputs );
  65                         deleteFunctionEncoding(& bp->encoding);
  66                         break;
  67                 }
  68                 case LOGICOP:{
  69                         BooleanLogic* bl = (BooleanLogic*) This;
  70                         deleteInlineArrayBoolean(&bl->inputs);
  71                         break;
  72                 }
  73                 default:
  74                         break;
  75         }
  76         deleteVectorArrayBoolean(GETBOOLEANPARENTS(This));
  77         ourfree(This);
  78 }
  79
  80
  81 Polarity negatePolarity(Polarity This){
  82         switch(This){
  83                 case P_UNDEFINED:
  84                 case P_BOTHTRUEFALSE:
  85                         return This;
  86                 case P_TRUE:
  87                         return P_FALSE;
  88                 case P_FALSE:
  89                         return P_TRUE;
  90                 default:
  91                         ASSERT(0);
  92         }
  93 }
  94
  95 BooleanValue negateBooleanValue(BooleanValue This){
  96         switch(This){
  97                 case BV_UNDEFINED:
  98                 case BV_UNKNOWN:
  99                         return This;
 100                 case BV_MUSTBETRUE:
 101                         return BV_MUSTBEFALSE;
 102                 case BV_MUSTBEFALSE:
 103                         return BV_MUSTBETRUE;
 104                 default:
 105                         ASSERT(0);
 106         }
 107 }
 108