1 #include "polarityassignment.h"
4 void computePolarities(CSolver *This) {
5 HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
6 while(hasNextBoolean(iterator)) {
7 Boolean *boolean = nextBoolean(iterator);
8 updatePolarity(boolean, P_TRUE);
9 updateMustValue(boolean, BV_MUSTBETRUE);
10 computePolarityAndBooleanValue(boolean);
12 deleteIterBoolean(iterator);
15 void updatePolarity(Boolean *This, Polarity polarity) {
16 This->polarity |= polarity;
19 void updateMustValue(Boolean *This, BooleanValue value) {
20 This->boolVal |= value;
23 void computePolarityAndBooleanValue(Boolean *This) {
24 switch (GETBOOLEANTYPE(This)) {
29 return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
31 return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
37 void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
38 updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
39 computePolarityAndBooleanValue(This->undefStatus);
42 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
43 computeLogicOpBooleanValue(This);
44 computeLogicOpPolarity(This);
45 uint size = getSizeArrayBoolean(&This->inputs);
46 for (uint i = 0; i < size; i++) {
47 computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
51 Polarity negatePolarity(Polarity This) {
65 BooleanValue negateBooleanValue(BooleanValue This) {
71 return BV_MUSTBEFALSE;
79 void computeLogicOpPolarity(BooleanLogic *This) {
80 Polarity parentpolarity = GETBOOLEANPOLARITY(This);
84 uint size = getSizeArrayBoolean(&This->inputs);
85 for (uint i = 0; i < size; i++) {
86 Boolean *tmp = getArrayBoolean(&This->inputs, i);
87 updatePolarity(tmp, parentpolarity);
92 Boolean *tmp = getArrayBoolean(&This->inputs, 0);
93 updatePolarity(tmp, negatePolarity(parentpolarity));
97 updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
98 updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
102 Boolean *left = getArrayBoolean(&This->inputs, 0);
103 updatePolarity(left, negatePolarity( parentpolarity));
104 Boolean *right = getArrayBoolean(&This->inputs, 1);
105 updatePolarity(right, parentpolarity);
113 void computeLogicOpBooleanValue(BooleanLogic *This) {
114 BooleanValue parentbv = GETBOOLEANVALUE(This);
117 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
118 uint size = getSizeArrayBoolean(&This->inputs);
119 for (uint i = 0; i < size; i++) {
120 updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
126 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
127 uint size = getSizeArrayBoolean(&This->inputs);
128 for (uint i = 0; i < size; i++) {
129 updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
135 updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
138 //implies is really an or with the first term negated
139 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
140 uint size = getSizeArrayBoolean(&This->inputs);
141 updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
142 updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);