トップページ:初学者向けCHRの使い方まとめ
コード
:- module(boolean, [boolean/1, and/3, or/3, xor/3, neg/2, imp/2, labeling/0, half_adder/4, full_adder/5]). :- use_module( library(chr)). %% Deprecated syntax used for SICStus 3.x %handler boolean. %constraints boolean/1, and/3, or/3, xor/3, neg/2, imp/2, % labeling/0, half_adder/4, full_adder/5. %% Syntax for SWI / SICStus 4.x :- chr_type bool ---> 0 ; 1. :- chr_constraint boolean(?bool), and(?bool,?bool,?bool), or(?bool,?bool,?bool), xor(?bool,?bool,?bool), neg(?bool,?bool), imp(?bool,?bool), labeling, half_adder(?bool,?bool,?bool,?bool), full_adder(?bool,?bool,?bool,?bool,?bool). boolean(0) <=> true. boolean(1) <=> true. labeling \ boolean(A) <=> A=0 ; A=1. %% and/3 specification %%and(0,0,0). %%and(0,1,0). %%and(1,0,0). %%and(1,1,1). and(0,_,Y) <=> Y=0. and(_,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,A) \ and(X,Y,B) <=> A=B. and(X,Y,A) \ and(Y,X,B) <=> A=B. labeling \ and(A,B,C) <=> label_and(A,B,C). label_and(0,_,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,_,Y) <=> Y=1. or(_,1,Y) <=> Y=1. or(X,X,Z) <=> X=Z. 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) <=> label_or(A,B,C). label_or(0,X,X). label_or(1,_,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) <=> label_xor(A,B,C). 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) <=> label_neg(A,B). label_neg(0,1). label_neg(1,0). %% imp/2 specification (implication) %%imp(0,0). %%imp(0,1). %%imp(1,1). imp(0,_) <=> true. imp(X,0) <=> X=0. imp(1,X) <=> X=1. imp(_,1) <=> true. imp(X,X) <=> true. imp(X,Y),imp(Y,X) <=> X=Y. labeling \ imp(A,B) <=> label_imp(A,B). label_imp(0,_). label_imp(1,1). %% half_adder/4: add bits X and Y, result in S and carry in C %% X+Y = S+2*C half_adder(X,Y,S,C) <=> xor(X,Y,S), and(X,Y,C). %% full_adder/5: add bits X, Y and Ci, result in S and carry in Co %% X+Y+Ci = S+2*Co full_adder(X,Y,Ci,S,Co) <=> half_adder(X,Y,S1,Co1), half_adder(Ci,S1,S,Co2), or(Co1,Co2,Co).
このプログラムは、各種の論理関数(boolean,and,or,xor,neg,imp,半加算器、全加算器)をシミュレートすることができ、入力に矛盾が無いことを確認しつつ、正しく解ける時の変数についての制約として得られたことを出力してくる。 例えば
and(0,1,A), xor(1,1,B).
という入力に対しては、
and(0,_,A) <=> A=0. xor(1,X,Y) <=> neg(X,Y). neg(1,X) <=> X=0.
という3つのルールから
A=0, B=0.
という出力が得られる。
neg(A,A).
という入力に対しては、
neg(X,X) <=> fail.
というルールのみが発火するため
no.
という結果(解なし)が得られる。
また、
neg(A,B), or(A,B,C), labeling.
という制約を入力すれば、
labeling \ or(A,B,C) <=> label_or(A,B,C).
というルールで生成されたlabel_or制約が
label_or(0,X,X). label_or(1,_,1).
という制約と矛盾しないように変数の値を選択されることになるため、出力は
A = 0, B = 1, C = 1, labeling. A = 1, B = 0, C = 1, labeling.
の二通りになる。(SWI-prologはすべての解を網羅するため)
labeling制約がない場合、CHRの機能だけではどのルールも発火しないはずだが、SWI-prologは解を網羅して分かったC = 1を使って
C = 1, neg(A,B).
を出力してくる。
コード
:- module(equations_gauss, [eq/2, {}/1]). :- use_module(library(chr)). :- use_module(library(lists)). user:library_directory('.'). :- use_module(library(var_order)). :- op(600,xfx,eq). %% Deprecated syntax used for SICStus 3.x %handler gauss. %constraints eq/2, {}/1. %% Syntax for SWI / SICStus 4.x :- chr_constraint eq/2, {}/1. %% Poly eq Const, where Poly is list of monomials Coefficient*Variable %% eq/2 %% curly brackets as wrapper to avoid name clash with built-in = %% {}/1 %% split system of equations split @ {E, F} <=> {E}, {F}. %% convert arbitrary polynomial equation to eq-notation normalize @ {A = B} <=> globalize([A-B]), normpoly([A-B] eq 0, Poly eq Const), Poly eq Const. %% 0=C zero @ [] eq C <=> zero(C). %% normalize first coefficient to 1 norm1 @ [A*X|P] eq C <=> notzero(A-1) | multpoly(1/A,P eq C,P2 eq C2), [1*X|P2] eq C2. %% const on left side (because of bound variable) bound @ P eq C <=> select(A*X, P, P0), number(X) | C0 is C-A*X, P0 eq C0. %% A*X = C => bind variable bind @ [A*X] eq C <=> var(X) | X is C/A. %% Gaussian elimination elimate @ [A*X|P] eq C \ Q eq D <=> select(B*X, Q, Q1) | multpoly(-B/A, P eq C, E), addpoly(E, Q1 eq D, Q0 eq D0), Q0 eq D0. %% Auxiliary predicates %% stable variable order based on chr/ordering by C. Holzbaur (var_order.pl) %% compare variables with var_compare ord_lss(X,Y) :- var_compare(<,X,Y). %% otherwise use Prolog standard order ord_lss(X,Y) :- nonvar(Y), X @< Y. %% numerical stabilty notzero(A) :- abs(A) > 0.000001. zero(A) :- abs(A) =< 0.000001. %% safe_is(X,Exp): X is Exp; fails, if Exp is not an arith. expression safe_is(X,Exp) :- on_exception(_, X is Exp, fail). %% normalize polynomial equation normpoly([X] eq C, [1*X] eq C) :- var(X), !. normpoly([X] eq C, [1*X] eq C) :- simple(X), \+ number(X). normpoly([A] eq C, [] eq C0) :- number(A), C0 is C-A. normpoly([A,B|P] eq C, E0) :- normpoly([A] eq 0,E1), normpoly([B|P] eq C,E2), addpoly(E1,E2,E0). normpoly([+A] eq 0, E0) :- normpoly([A] eq 0, E0). normpoly([-A] eq 0, E0) :- normpoly([A] eq 0, E1), multpoly(-1, E1, E0). normpoly([A+B] eq C, E0) :- normpoly([A] eq C,E), normpoly([B] eq 0,F), addpoly(E,F,E0). normpoly([A-B] eq C, E0) :- normpoly([A] eq C,E), normpoly([B] eq 0,F), multpoly(-1,F,F1), addpoly(E,F1,E0). normpoly([A*X] eq 0, E0) :- safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0). normpoly([X*A] eq 0, E0) :- safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0). normpoly([X/A] eq 0, E0) :- safe_is(A1,1/A), normpoly([X] eq 0, E), multpoly(A1,E,E0). normpoly([A] eq C, P0 eq C0) :- C\==0, normpoly([A] eq 0, P0 eq C1), C0 is C+C1. %% addpoly(E,F, E0): add polynomial equations %% requires: polynomials ordered + duplicate free; retains properties addpoly(P eq C, [] eq D, P eq C0) :- !, C0 is C+D. addpoly([] eq C, Q eq D, Q eq C0) :- !, C0 is C+D. addpoly([A*X|P] eq C, [B*Y|Q] eq D, E0) :- X==Y, !, A1 is A+B, addpoly(P eq C, Q eq D, P1 eq C1), (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1). addpoly([A*X|P] eq C, [B*Y|Q] eq D, [A*X|P0] eq C0) :- ord_lss(X,Y), !, addpoly(P eq C, [B*Y|Q] eq D, P0 eq C0). addpoly([A*X|P] eq C, [B*Y|Q] eq D, [B*Y|P0] eq C0) :- ord_lss(Y,X), !, addpoly([A*X|P] eq C, Q eq D, P0 eq C0). %% multpoly(M,E, E0): multiply polynomial equation with scalar multpoly(M, [] eq C, [] eq C0) :- C0 is M*C. multpoly(M, [A*X|P] eq C, E0) :- A1 is M*A, multpoly(M,P eq C,P1 eq C1), (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1).