1 #include "polarityassignment.h"
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);
15 void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
16 Boolean *bdst = dst.getBoolean();
17 Boolean *bsrc = src.getBoolean();
18 bool isNegated = dst.isNegated() ^ src.isNegated();
19 Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
20 updatePolarity(bdst, p);
23 void updateEdgePolarity(BooleanEdge dst, Polarity p) {
24 Boolean *bdst = dst.getBoolean();
25 bool isNegated = dst.isNegated();
28 updatePolarity(bdst, p);
31 bool updatePolarity(Boolean *This, Polarity polarity) {
32 Polarity oldpolarity = This->polarity;
33 Polarity newpolarity = (Polarity) (This->polarity | polarity);
34 This->polarity = newpolarity;
35 return newpolarity != oldpolarity;
38 void updateMustValue(Boolean *This, BooleanValue value) {
39 This->boolVal = (BooleanValue) (This->boolVal | value);
42 void computePolarity(Boolean *This, Polarity polarity) {
43 if (updatePolarity(This, polarity)) {
49 return computePredicatePolarity((BooleanPredicate *)This);
51 return computeLogicOpPolarity((BooleanLogic *)This);
58 void computePredicatePolarity(BooleanPredicate *This) {
59 if (This->undefStatus) {
60 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
64 void computeLogicOpPolarity(BooleanLogic *This) {
65 Polarity child = computeLogicOpPolarityChildren(This);
66 uint size = This->inputs.getSize();
67 for (uint i = 0; i < size; i++) {
68 BooleanEdge b = This->inputs.get(i);
69 computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
73 BooleanValue negateBooleanValue(BooleanValue This) {
79 return BV_MUSTBEFALSE;
87 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
90 return This->polarity;
93 return P_BOTHTRUEFALSE;
100 Polarity negatePolarity(Polarity This) {
103 case P_BOTHTRUEFALSE: