| 901 | } |
| 902 | |
| 903 | void |
| 904 | clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y, |
| 905 | int n, IntPropLevel) { |
| 906 | using namespace Int; |
| 907 | if ((n < 0) || (n > 1)) |
| 908 | throw NotZeroOne("Int::rel"); |
| 909 | GECODE_POST; |
| 910 | switch (o) { |
| 911 | case BOT_AND: |
| 912 | if (n == 0) { |
| 913 | ViewArray<NegBoolView> xv(home,x.size()); |
| 914 | for (int i=0; i<x.size(); i++) { |
| 915 | NegBoolView nxi(x[i]); xv[i]=nxi; |
| 916 | } |
| 917 | ViewArray<BoolView> yv(home,y); |
| 918 | xv.unique(); yv.unique(); |
| 919 | GECODE_ES_FAIL((Bool::ClauseTrue<NegBoolView,BoolView> |
| 920 | ::post(home,xv,yv))); |
| 921 | } else { |
| 922 | for (int i=0; i<x.size(); i++) { |
| 923 | BoolView b(x[i]); GECODE_ME_FAIL(b.one(home)); |
| 924 | } |
| 925 | for (int i=0; i<y.size(); i++) { |
| 926 | BoolView b(y[i]); GECODE_ME_FAIL(b.zero(home)); |
| 927 | } |
| 928 | } |
| 929 | break; |
| 930 | case BOT_OR: |
| 931 | if (n == 0) { |
| 932 | for (int i=0; i<x.size(); i++) { |
| 933 | BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home)); |
| 934 | } |
| 935 | for (int i=0; i<y.size(); i++) { |
| 936 | BoolView b(y[i]); GECODE_ME_FAIL(b.one(home)); |
| 937 | } |
| 938 | } else { |
| 939 | ViewArray<BoolView> xv(home,x); |
| 940 | ViewArray<NegBoolView> yv(home,y.size()); |
| 941 | for (int i=0; i<y.size(); i++) { |
| 942 | NegBoolView nyi(y[i]); yv[i]=nyi; |
| 943 | } |
| 944 | xv.unique(); yv.unique(); |
| 945 | GECODE_ES_FAIL((Bool::ClauseTrue<BoolView,NegBoolView> |
| 946 | ::post(home,xv,yv))); |
| 947 | } |
| 948 | break; |
| 949 | default: |
| 950 | throw IllegalOperation("Int::clause"); |
| 951 | } |
| 952 | } |
| 953 | |
| 954 | void |
| 955 | clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y, |
no test coverage detected