Benchmarks/bool.chr

   1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   2 %%
   3 %% Thom Fruehwirth ECRC 1991-1993
   4 %% 910528 started boolean,and,or constraints
   5 %% 910904 added xor,neg constraints
   6 %% 911120 added imp constraint
   7 %% 931110 ported to new release
   8 %% 931111 added card constraint
   9 %% 961107 Christian Holzbaur, SICStus mods
  10 %%
  11 %% ported to hProlog by Tom Schrijvers June 2003
  12
  13
  14 :- module(bool,[main/0,main/1]).
  15
  16 :- use_module( library(chr)).
  17
  18 :- use_module(library(lists)).
  19
  20 :- constraints boolean/1, and/3, or/3, xor/3, neg/2, imp/2, labeling/0, card/4.
  21
  22
  23 boolean(0) <=> true.
  24 boolean(1) <=> true.
  25
  26 labeling, boolean(A)#Pc <=>
  27 ( A=0 ; A=1),
  28 labeling
  29 pragma passive(Pc).
  30
  31
  32 %% and/3 specification
  33 %%and(0,0,0).
  34 %%and(0,1,0).
  35 %%and(1,0,0).
  36 %%and(1,1,1).
  37
  38 and(0,X,Y) <=> Y=0.
  39 and(X,0,Y) <=> Y=0.
  40 and(1,X,Y) <=> Y=X.
  41 and(X,1,Y) <=> Y=X.
  42 and(X,Y,1) <=> X=1,Y=1.
  43 and(X,X,Z) <=> X=Z.
  44 %%and(X,Y,X) <=> imp(X,Y).
  45 %%and(X,Y,Y) <=> imp(Y,X).
  46 and(X,Y,A) \ and(X,Y,B) <=> A=B.
  47 and(X,Y,A) \ and(Y,X,B) <=> A=B.
  48
  49 labeling, and(A,B,C)#Pc <=>
  50 label_and(A,B,C),
  51 labeling
  52 pragma passive(Pc).
  53
  54 label_and(0,X,0).
  55 label_and(1,X,X).
  56
  57
  58 %% or/3 specification
  59 %%or(0,0,0).
  60 %%or(0,1,1).
  61 %%or(1,0,1).
  62 %%or(1,1,1).
  63
  64 or(0,X,Y) <=> Y=X.
  65 or(X,0,Y) <=> Y=X.
  66 or(X,Y,0) <=> X=0,Y=0.
  67 or(1,X,Y) <=> Y=1.
  68 or(X,1,Y) <=> Y=1.
  69 or(X,X,Z) <=> X=Z.
  70 %%or(X,Y,X) <=> imp(Y,X).
  71 %%or(X,Y,Y) <=> imp(X,Y).
  72 or(X,Y,A) \ or(X,Y,B) <=> A=B.
  73 or(X,Y,A) \ or(Y,X,B) <=> A=B.
  74
  75 labeling, or(A,B,C)#Pc <=>
  76 label_or(A,B,C),
  77 labeling
  78 pragma passive(Pc).
  79
  80 label_or(0,X,X).
  81 label_or(1,X,1).
  82
  83
  84 %% xor/3 specification
  85 %%xor(0,0,0).
  86 %%xor(0,1,1).
  87 %%xor(1,0,1).
  88 %%xor(1,1,0).
  89
  90 xor(0,X,Y) <=> X=Y.
  91 xor(X,0,Y) <=> X=Y.
  92 xor(X,Y,0) <=> X=Y.
  93 xor(1,X,Y) <=> neg(X,Y).
  94 xor(X,1,Y) <=> neg(X,Y).
  95 xor(X,Y,1) <=> neg(X,Y).
  96 xor(X,X,Y) <=> Y=0.
  97 xor(X,Y,X) <=> Y=0.
  98 xor(Y,X,X) <=> Y=0.
  99 xor(X,Y,A) \ xor(X,Y,B) <=> A=B.
 100 xor(X,Y,A) \ xor(Y,X,B) <=> A=B.
 101
 102 labeling, xor(A,B,C)#Pc <=>
 103 label_xor(A,B,C),
 104 labeling
 105 pragma passive(Pc).
 106
 107 label_xor(0,X,X).
 108 label_xor(1,X,Y):- neg(X,Y).
 109
 110
 111 %% neg/2 specification
 112 %%neg(0,1).
 113 %%neg(1,0).
 114
 115 neg(0,X) <=> X=1.
 116 neg(X,0) <=> X=1.
 117 neg(1,X) <=> X=0.
 118 neg(X,1) <=> X=0.
 119 neg(X,X) <=> fail.
 120 neg(X,Y) \ neg(Y,Z) <=> X=Z.
 121 neg(X,Y) \ neg(Z,Y) <=> X=Z.
 122 neg(Y,X) \ neg(Y,Z) <=> X=Z.
 123 %% Interaction with other boolean constraints
 124 neg(X,Y) \ and(X,Y,Z) <=> Z=0.
 125 neg(Y,X) \ and(X,Y,Z) <=> Z=0.
 126 neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
 127 neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
 128 neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
 129 neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
 130 neg(X,Y) \ or(X,Y,Z) <=> Z=1.
 131 neg(Y,X) \ or(X,Y,Z) <=> Z=1.
 132 neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
 133 neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
 134 neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
 135 neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
 136 neg(X,Y) \ xor(X,Y,Z) <=> Z=1.
 137 neg(Y,X) \ xor(X,Y,Z) <=> Z=1.
 138 neg(X,Z) \ xor(X,Y,Z) <=> Y=1.
 139 neg(Z,X) \ xor(X,Y,Z) <=> Y=1.
 140 neg(Y,Z) \ xor(X,Y,Z) <=> X=1.
 141 neg(Z,Y) \ xor(X,Y,Z) <=> X=1.
 142 neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
 143 neg(Y,X) , imp(X,Y) <=> X=0,Y=1.
 144
 145 labeling, neg(A,B)#Pc <=>
 146 label_neg(A,B),
 147 labeling
 148 pragma passive(Pc).
 149
 150 label_neg(0,1).
 151 label_neg(1,0).
 152
 153
 154 %% imp/2 specification (implication)
 155 %%imp(0,0).
 156 %%imp(0,1).
 157 %%imp(1,1).
 158
 159 imp(0,X) <=> true.
 160 imp(X,0) <=> X=0.
 161 imp(1,X) <=> X=1.
 162 imp(X,1) <=> true.
 163 imp(X,X) <=> true.
 164 imp(X,Y),imp(Y,X) <=> X=Y.
 165
 166 labeling, imp(A,B)#Pc <=>
 167 label_imp(A,B),
 168 labeling
 169 pragma passive(Pc).
 170
 171 label_imp(0,X).
 172 label_imp(1,1).
 173
 174
 175
 176 %% Boolean cardinality operator
 177 %% card(A,B,L,N) constrains list L of length N to have between A and B 1s
 178
 179
 180 card(A,B,L):-
 181         length(L,N),
 182         A=<B,0=<B,A=<N,                         %0=<N
 183         card(A,B,L,N).
 184
 185 %% card/4 specification
 186 %%card(A,B,[],0):- A=<0,0=<B.
 187 %%card(A,B,[0|L],N):-
 188 %%              N1 is N-1,
 189 %%              card(A,B,L,N1).
 190 %%card(A,B,[1|L],N):-
 191 %%              A1 is A-1, B1 is B-1, N1 is N-1,
 192 %%              card(A1,B1,L,N1).
 193
 194 triv_sat @ card(A,B,L,N) <=> A=<0,N=<B | true. % trivial satisfaction
 195 pos_sat @ card(N,B,L,N) <=> set_to_ones(L).     % positive satisfaction
 196 neg_sat @ card(A,0,L,N) <=> set_to_zeros(L). % negative satisfaction
 197 pos_red @ card(A,B,L,N) <=> b_delete(X,L,L1),X==1 | % positive reduction
 198 A1 is A-1, B1 is B-1, N1 is N-1,
 199 card(A1,B1,L1,N1).
 200 neg_red @ card(A,B,L,N) <=> b_delete(X,L,L1),X==0 | % negative reduction
 201 N1 is N-1,
 202 card(A,B,L1,N1).
 203 %% special cases with two variables
 204 card2nand @ card(0,1,[X,Y],2) <=> and(X,Y,0).
 205 card2neg @ card(1,1,[X,Y],2) <=> neg(X,Y).
 206 card2or @ card(1,2,[X,Y],2) <=> or(X,Y,1).
 207
 208 b_delete( X, [X|L],  L).
 209 b_delete( Y, [X|Xs], [X|Xt]) :-
 210         b_delete( Y, Xs, Xt).
 211
 212 labeling, card(A,B,L,N)#Pc <=>
 213 label_card(A,B,L,N),
 214 labeling
 215 pragma passive(Pc).
 216
 217 label_card(A,B,[],0):- A=<0,0=<B.
 218 label_card(A,B,[0|L],N):-
 219         %N1 is N-1,
 220         card(A,B,L).
 221 label_card(A,B,[1|L],N):-
 222         A1 is A-1, B1 is B-1, %N1 is N-1,
 223         card(A1,B1,L).
 224
 225 set_to_ones([]).
 226 set_to_ones([1|L]):-
 227         set_to_ones(L).
 228
 229 set_to_zeros([]).
 230 set_to_zeros([0|L]):-
 231         set_to_zeros(L).
 232
 233
 234
 235 %% Auxiliary predicates
 236
 237 :- op(100,xfy,#).
 238
 239 solve_bool(A,C) :- var(A), !, A=C.
 240 solve_bool(A,C) :- atomic(A), !, A=C.
 241 solve_bool(A * B, C) :- !,
 242         solve_bool(A,A1),
 243         solve_bool(B,B1),
 244         and(A1,B1,C).
 245 solve_bool(A + B, C) :- !,
 246         solve_bool(A,A1),
 247         solve_bool(B,B1),
 248         or(A1,B1,C).
 249 solve_bool(A # B, C) :- !,
 250         solve_bool(A,A1),
 251         solve_bool(B,B1),
 252         xor(A1,B1,C).
 253 solve_bool(not(A),C) :- !,
 254         solve_bool(A,A1),
 255         neg(A1,C).
 256 solve_bool((A -> B), C) :- !,
 257         solve_bool(A,A1),
 258         solve_bool(B,B1),
 259         imp(A1,B1),C=1.
 260 solve_bool(A = B, C) :- !,
 261         solve_bool(A,A1),
 262         solve_bool(B,B1),
 263         A1=B1,C=1.
 264
 265 %% Labeling
 266 label_bool([]).
 267 label_bool([X|L]) :-
 268         ( X=0;X=1),
 269         label_bool(L).
 270
 271 /*                              % no write macros in SICStus and hProlog
 272
 273 bool_portray(and(A,B,C),Out):- !, Out = (A*B = C).
 274 bool_portray(or(A,B,C),Out):- !, Out = (A+B = C).
 275 bool_portray(xor(A,B,C),Out):- !, Out = (A#B = C).
 276 bool_portray(neg(A,B),Out):- !, Out = (A= not(B)).
 277 bool_portray(imp(A,B),Out):- !, Out = (A -> B).
 278 bool_portray(card(A,B,L,N),Out):- !, Out = card(A,B,L).
 279
 280 :- define_macro(type(compound),bool_portray/2,[write]).
 281 */
 282
 283 /* end of handler bool */
 284
 285 half_adder(X,Y,S,C) :-
 286         xor(X,Y,S),
 287         and(X,Y,C).
 288
 289 full_adder(X,Y,Ci,S,Co) :-
 290         half_adder(X,Y,S1,Co1),
 291         half_adder(Ci,S1,S,Co2),
 292         or(Co1,Co2,Co).
 293
 294 main :-
 295         main(60000).
 296
 297 main(N) :-
 298         cputime(X),
 299         adder(N),
 300         cputime(Now),
 301         Time is Now - X,
 302         write(bench(bool, N, Time, 0, hprolog)),write('.'),nl.
 303
 304 adder(N) :-
 305         length(Ys,N),
 306         add(N,Ys).
 307
 308 add(N,[Y|Ys]) :-
 309         half_adder(1,Y,0,C),
 310         add0(Ys,C).
 311
 312 add0([],1).
 313 add0([Y|Ys],C) :-
 314         full_adder(0,Y,C,1,NC),
 315         add1(Ys,NC).
 316
 317 add1([],0).
 318 add1([Y|Ys],C) :-
 319         full_adder(1,Y,C,0,NC),
 320         add0(Ys,NC).
 321