1 #include "polarityassignment.h"
4 void computePolarities(CSolver *This) {
5 HSIteratorBoolean *iterator=This->getConstraints();
6 while(iterator->hasNext()) {
7 Boolean *boolean = iterator->next();
8 updatePolarity(boolean, P_TRUE);
9 updateMustValue(boolean, BV_MUSTBETRUE);
10 computePolarityAndBooleanValue(boolean);
15 void updatePolarity(Boolean *This, Polarity polarity) {
16 This->polarity = (Polarity) (This->polarity | polarity);
19 void updateMustValue(Boolean *This, BooleanValue value) {
20 This->boolVal = (BooleanValue) (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 if (This->undefStatus != NULL) {
39 updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
40 computePolarityAndBooleanValue(This->undefStatus);
44 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
45 computeLogicOpBooleanValue(This);
46 computeLogicOpPolarity(This);
47 uint size = This->inputs.getSize();
48 for (uint i = 0; i < size; i++) {
49 computePolarityAndBooleanValue(This->inputs.get(i));
53 Polarity negatePolarity(Polarity This) {
67 BooleanValue negateBooleanValue(BooleanValue This) {
73 return BV_MUSTBEFALSE;
81 void computeLogicOpPolarity(BooleanLogic *This) {
82 Polarity parentpolarity = GETBOOLEANPOLARITY(This);
86 uint size = This->inputs.getSize();
87 for (uint i = 0; i < size; i++) {
88 Boolean *tmp = This->inputs.get(i);
89 updatePolarity(tmp, parentpolarity);
94 Boolean *tmp = This->inputs.get(0);
95 updatePolarity(tmp, negatePolarity(parentpolarity));
99 updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
100 updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
104 Boolean *left = This->inputs.get(0);
105 updatePolarity(left, negatePolarity( parentpolarity));
106 Boolean *right = This->inputs.get(1);
107 updatePolarity(right, parentpolarity);
115 void computeLogicOpBooleanValue(BooleanLogic *This) {
116 BooleanValue parentbv = GETBOOLEANVALUE(This);
119 if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
120 uint size = This->inputs.getSize();
121 for (uint i = 0; i < size; i++) {
122 updateMustValue(This->inputs.get(i), parentbv);
128 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
129 uint size = This->inputs.getSize();
130 for (uint i = 0; i < size; i++) {
131 updateMustValue(This->inputs.get(i), parentbv);
137 updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
140 //implies is really an or with the first term negated
141 if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
142 uint size = This->inputs.getSize();
143 updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
144 updateMustValue(This->inputs.get(1), parentbv);