Add directories per analysis
[satune.git] / src / ASTAnalyses / Polarity / polarityassignment.cc
1 #include "polarityassignment.h"
2 #include "csolver.h"
3
4 void computePolarities(CSolver *This) {
5         SetIteratorBooleanEdge *iterator = This->getConstraints();
6         while (iterator->hasNext()) {
7                 BooleanEdge boolean = iterator->next();
8                 Boolean *b = boolean.getBoolean();
9                 bool isNegated = boolean.isNegated();
10                 computePolarity(b, isNegated ? P_FALSE : P_TRUE);
11         }
12         delete iterator;
13 }
14
15 bool updatePolarity(Boolean *This, Polarity polarity) {
16         Polarity oldpolarity = This->polarity;
17         Polarity newpolarity = (Polarity) (This->polarity | polarity);
18         This->polarity = newpolarity;
19         return newpolarity != oldpolarity;
20 }
21
22 void updateMustValue(Boolean *This, BooleanValue value) {
23         This->boolVal = (BooleanValue) (This->boolVal | value);
24 }
25
26 void computePolarity(Boolean *This, Polarity polarity) {
27         if (updatePolarity(This, polarity)) {
28                 switch (This->type) {
29                 case BOOLEANVAR:
30                 case ORDERCONST:
31                         return;
32                 case PREDICATEOP:
33                         return computePredicatePolarity((BooleanPredicate *)This);
34                 case LOGICOP:
35                         return computeLogicOpPolarity((BooleanLogic *)This);
36                 default:
37                         ASSERT(0);
38                 }
39         }
40 }
41
42 void computePredicatePolarity(BooleanPredicate *This) {
43         if (This->undefStatus) {
44                 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
45         }
46 }
47
48 void computeLogicOpPolarity(BooleanLogic *This) {
49         Polarity child=computeLogicOpPolarityChildren(This);
50         uint size = This->inputs.getSize();
51         for (uint i = 0; i < size; i++) {
52                 BooleanEdge b=This->inputs.get(i);
53                 computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
54         }
55 }
56
57 Polarity negatePolarity(Polarity This) {
58         switch (This) {
59         case P_UNDEFINED:
60         case P_BOTHTRUEFALSE:
61                 return This;
62         case P_TRUE:
63                 return P_FALSE;
64         case P_FALSE:
65                 return P_TRUE;
66         default:
67                 ASSERT(0);
68         }
69 }
70
71 BooleanValue negateBooleanValue(BooleanValue This) {
72         switch (This) {
73         case BV_UNDEFINED:
74         case BV_UNSAT:
75                 return This;
76         case BV_MUSTBETRUE:
77                 return BV_MUSTBEFALSE;
78         case BV_MUSTBEFALSE:
79                 return BV_MUSTBETRUE;
80         default:
81                 ASSERT(0);
82         }
83 }
84
85 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
86         switch (This->op) {
87         case SATC_AND: {
88                 return This->polarity;
89         }
90         case SATC_IFF: {
91                 return P_BOTHTRUEFALSE;
92         }
93         default:
94                 ASSERT(0);
95         }
96 }