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 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;
22 void updateMustValue(Boolean *This, BooleanValue value) {
23 This->boolVal = (BooleanValue) (This->boolVal | value);
26 void computePolarity(Boolean *This, Polarity polarity) {
27 if (updatePolarity(This, polarity)) {
33 return computePredicatePolarity((BooleanPredicate *)This);
35 return computeLogicOpPolarity((BooleanLogic *)This);
42 void computePredicatePolarity(BooleanPredicate *This) {
43 if (This->undefStatus) {
44 computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
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);
57 Polarity negatePolarity(Polarity This) {
71 BooleanValue negateBooleanValue(BooleanValue This) {
77 return BV_MUSTBEFALSE;
85 Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
88 return This->polarity;
91 return P_BOTHTRUEFALSE;