This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/LGPL/chr/Benchmarks/bool.chr
vsc a247b1b8ec include CHR benchmarks
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1958 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2007-10-16 23:18:30 +00:00

324 lines
6.4 KiB
Plaintext

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Thom Fruehwirth ECRC 1991-1993
%% 910528 started boolean,and,or constraints
%% 910904 added xor,neg constraints
%% 911120 added imp constraint
%% 931110 ported to new release
%% 931111 added card constraint
%% 961107 Christian Holzbaur, SICStus mods
%%
%% ported to hProlog by Tom Schrijvers June 2003
:- module(bool,[main/0,main/1]).
:- use_module( library(chr)).
:- use_module(library(lists)).
:- chr_constraint boolean/1, and/3, or/3, xor/3, neg/2, imp/2, labeling/0, card/4.
boolean(0) <=> true.
boolean(1) <=> true.
labeling, boolean(A)#Pc <=>
( A=0 ; A=1),
labeling
pragma passive(Pc).
%% and/3 specification
%%and(0,0,0).
%%and(0,1,0).
%%and(1,0,0).
%%and(1,1,1).
and(0,X,Y) <=> Y=0.
and(X,0,Y) <=> Y=0.
and(1,X,Y) <=> Y=X.
and(X,1,Y) <=> Y=X.
and(X,Y,1) <=> X=1,Y=1.
and(X,X,Z) <=> X=Z.
%%and(X,Y,X) <=> imp(X,Y).
%%and(X,Y,Y) <=> imp(Y,X).
and(X,Y,A) \ and(X,Y,B) <=> A=B.
and(X,Y,A) \ and(Y,X,B) <=> A=B.
labeling, and(A,B,C)#Pc <=>
label_and(A,B,C),
labeling
pragma passive(Pc).
label_and(0,X,0).
label_and(1,X,X).
%% or/3 specification
%%or(0,0,0).
%%or(0,1,1).
%%or(1,0,1).
%%or(1,1,1).
or(0,X,Y) <=> Y=X.
or(X,0,Y) <=> Y=X.
or(X,Y,0) <=> X=0,Y=0.
or(1,X,Y) <=> Y=1.
or(X,1,Y) <=> Y=1.
or(X,X,Z) <=> X=Z.
%%or(X,Y,X) <=> imp(Y,X).
%%or(X,Y,Y) <=> imp(X,Y).
or(X,Y,A) \ or(X,Y,B) <=> A=B.
or(X,Y,A) \ or(Y,X,B) <=> A=B.
labeling, or(A,B,C)#Pc <=>
label_or(A,B,C),
labeling
pragma passive(Pc).
label_or(0,X,X).
label_or(1,X,1).
%% xor/3 specification
%%xor(0,0,0).
%%xor(0,1,1).
%%xor(1,0,1).
%%xor(1,1,0).
xor(0,X,Y) <=> X=Y.
xor(X,0,Y) <=> X=Y.
xor(X,Y,0) <=> X=Y.
xor(1,X,Y) <=> neg(X,Y).
xor(X,1,Y) <=> neg(X,Y).
xor(X,Y,1) <=> neg(X,Y).
xor(X,X,Y) <=> Y=0.
xor(X,Y,X) <=> Y=0.
xor(Y,X,X) <=> Y=0.
xor(X,Y,A) \ xor(X,Y,B) <=> A=B.
xor(X,Y,A) \ xor(Y,X,B) <=> A=B.
labeling, xor(A,B,C)#Pc <=>
label_xor(A,B,C),
labeling
pragma passive(Pc).
label_xor(0,X,X).
label_xor(1,X,Y):- neg(X,Y).
%% neg/2 specification
%%neg(0,1).
%%neg(1,0).
neg(0,X) <=> X=1.
neg(X,0) <=> X=1.
neg(1,X) <=> X=0.
neg(X,1) <=> X=0.
neg(X,X) <=> fail.
neg(X,Y) \ neg(Y,Z) <=> X=Z.
neg(X,Y) \ neg(Z,Y) <=> X=Z.
neg(Y,X) \ neg(Y,Z) <=> X=Z.
%% Interaction with other boolean constraints
neg(X,Y) \ and(X,Y,Z) <=> Z=0.
neg(Y,X) \ and(X,Y,Z) <=> Z=0.
neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(X,Y) \ or(X,Y,Z) <=> Z=1.
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(X,Y) \ xor(X,Y,Z) <=> Z=1.
neg(Y,X) \ xor(X,Y,Z) <=> Z=1.
neg(X,Z) \ xor(X,Y,Z) <=> Y=1.
neg(Z,X) \ xor(X,Y,Z) <=> Y=1.
neg(Y,Z) \ xor(X,Y,Z) <=> X=1.
neg(Z,Y) \ xor(X,Y,Z) <=> X=1.
neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
neg(Y,X) , imp(X,Y) <=> X=0,Y=1.
labeling, neg(A,B)#Pc <=>
label_neg(A,B),
labeling
pragma passive(Pc).
label_neg(0,1).
label_neg(1,0).
%% imp/2 specification (implication)
%%imp(0,0).
%%imp(0,1).
%%imp(1,1).
imp(0,X) <=> true.
imp(X,0) <=> X=0.
imp(1,X) <=> X=1.
imp(X,1) <=> true.
imp(X,X) <=> true.
imp(X,Y),imp(Y,X) <=> X=Y.
labeling, imp(A,B)#Pc <=>
label_imp(A,B),
labeling
pragma passive(Pc).
label_imp(0,X).
label_imp(1,1).
%% Boolean cardinality operator
%% card(A,B,L,N) constrains list L of length N to have between A and B 1s
card(A,B,L):-
length(L,N),
A=<B,0=<B,A=<N, %0=<N
card(A,B,L,N).
%% card/4 specification
%%card(A,B,[],0):- A=<0,0=<B.
%%card(A,B,[0|L],N):-
%% N1 is N-1,
%% card(A,B,L,N1).
%%card(A,B,[1|L],N):-
%% A1 is A-1, B1 is B-1, N1 is N-1,
%% card(A1,B1,L,N1).
triv_sat @ card(A,B,L,N) <=> A=<0,N=<B | true. % trivial satisfaction
pos_sat @ card(N,B,L,N) <=> set_to_ones(L). % positive satisfaction
neg_sat @ card(A,0,L,N) <=> set_to_zeros(L). % negative satisfaction
pos_red @ card(A,B,L,N) <=> b_delete(X,L,L1),X==1 | % positive reduction
A1 is A-1, B1 is B-1, N1 is N-1,
card(A1,B1,L1,N1).
neg_red @ card(A,B,L,N) <=> b_delete(X,L,L1),X==0 | % negative reduction
N1 is N-1,
card(A,B,L1,N1).
%% special cases with two variables
card2nand @ card(0,1,[X,Y],2) <=> and(X,Y,0).
card2neg @ card(1,1,[X,Y],2) <=> neg(X,Y).
card2or @ card(1,2,[X,Y],2) <=> or(X,Y,1).
b_delete( X, [X|L], L).
b_delete( Y, [X|Xs], [X|Xt]) :-
b_delete( Y, Xs, Xt).
labeling, card(A,B,L,N)#Pc <=>
label_card(A,B,L,N),
labeling
pragma passive(Pc).
label_card(A,B,[],0):- A=<0,0=<B.
label_card(A,B,[0|L],N):-
%N1 is N-1,
card(A,B,L).
label_card(A,B,[1|L],N):-
A1 is A-1, B1 is B-1, %N1 is N-1,
card(A1,B1,L).
set_to_ones([]).
set_to_ones([1|L]):-
set_to_ones(L).
set_to_zeros([]).
set_to_zeros([0|L]):-
set_to_zeros(L).
%% Auxiliary predicates
:- op(100,xfy,#).
solve_bool(A,C) :- var(A), !, A=C.
solve_bool(A,C) :- atomic(A), !, A=C.
solve_bool(A * B, C) :- !,
solve_bool(A,A1),
solve_bool(B,B1),
and(A1,B1,C).
solve_bool(A + B, C) :- !,
solve_bool(A,A1),
solve_bool(B,B1),
or(A1,B1,C).
solve_bool(A # B, C) :- !,
solve_bool(A,A1),
solve_bool(B,B1),
xor(A1,B1,C).
solve_bool(not(A),C) :- !,
solve_bool(A,A1),
neg(A1,C).
solve_bool((A -> B), C) :- !,
solve_bool(A,A1),
solve_bool(B,B1),
imp(A1,B1),C=1.
solve_bool(A = B, C) :- !,
solve_bool(A,A1),
solve_bool(B,B1),
A1=B1,C=1.
%% Labeling
label_bool([]).
label_bool([X|L]) :-
( X=0;X=1),
label_bool(L).
/* % no write macros in SICStus and hProlog
bool_portray(and(A,B,C),Out):- !, Out = (A*B = C).
bool_portray(or(A,B,C),Out):- !, Out = (A+B = C).
bool_portray(xor(A,B,C),Out):- !, Out = (A#B = C).
bool_portray(neg(A,B),Out):- !, Out = (A= not(B)).
bool_portray(imp(A,B),Out):- !, Out = (A -> B).
bool_portray(card(A,B,L,N),Out):- !, Out = card(A,B,L).
:- define_macro(type(compound),bool_portray/2,[write]).
*/
/* end of handler bool */
half_adder(X,Y,S,C) :-
xor(X,Y,S),
and(X,Y,C).
full_adder(X,Y,Ci,S,Co) :-
half_adder(X,Y,S1,Co1),
half_adder(Ci,S1,S,Co2),
or(Co1,Co2,Co).
main :-
main(60000).
main(N) :-
cputime(X),
adder(N),
cputime(Now),
Time is Now - X,
write(bench(bool, N, Time, 0, hprolog)),write('.'),nl.
adder(N) :-
length(Ys,N),
add(N,Ys).
add(N,[Y|Ys]) :-
half_adder(1,Y,0,C),
add0(Ys,C).
add0([],1).
add0([Y|Ys],C) :-
full_adder(0,Y,C,1,NC),
add1(Ys,NC).
add1([],0).
add1([Y|Ys],C) :-
full_adder(1,Y,C,0,NC),
add0(Ys,NC).
%cputime(Time) :-
% statistics(runtime, [_,Time]).