初学者向けCHRの使い方まとめ/Constraint_Solver
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
単語検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
トップページ:[[初学者向けCHRの使い方まとめ]]
*例題目録 [#vc82f401]
#contents
*boolean.pl [#ub7ae437]
コード
:- 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...
%% 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 c...
%% 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(...
このプログラムは、各種の論理関数(boolean,and,or,xor,neg,i...
例えば
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).
という制約と矛盾しないように変数の値を選択されることにな...
または、
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
の記述によってor制約が消滅しC=1に変換される。
さらに、
labeling \ neg(A,B) <=> label_neg(A,B).
label_neg(0,1).
label_neg(1,0).
という規則及び公理(この名前の述語が合致しなければならない...
A = 0, B = 1, C = 1, labeling.
A = 1, B = 0, C = 1, labeling.
の二通りになる。(SWI-prologはすべての解を網羅するため)
labeling制約がない場合、
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
が発火したところで処理が止まり、
C = 1, neg(A,B).
を出力してくる。
*equations_gauss.pl [#f662fca4]
コード
:- 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 Coeffi...
%% eq/2
%% curly brackets as wrapper to avoid name clash with bu...
%% {}/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) | C...
%% 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. Hol...
%% 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 ari...
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), addp...
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(...
normpoly([A-B] eq C, E0) :- normpoly([A] eq C,E), normpo...
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,...
normpoly([X*A] eq 0, E0) :-
safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,...
normpoly([X/A] eq 0, E0) :-
safe_is(A1,1/A), normpoly([X] eq 0, E), multpoly(A1,...
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; retai...
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) :- o...
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) :- o...
addpoly([A*X|P] eq C, Q eq D, P0 eq C0).
%% multpoly(M,E, E0): multiply polynomial equation with ...
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).
こちらはガウスの消去法により連立一次方程式を解くSolverで...
%% Auxiliary predicates
以降の記述はSWI-prologの述語(CHRで言う伝播規則のような動...
入力例1として、
{2+2*X+4*Y+2*Z=0, 4+2*X+4*Y+4*Z=0, 1+2*X+3*Z=0}.
を与える。
この入力はまず、splitルールによって
{2+2*X+4*Y+2*Z=0},
{4+2*X+4*Y+4*Z=0},
{1+2*X+3*Z=0}.
と変換される。その後、normalizeルール及びAPによって
[2*X,4*Y,2*Z] eq -2,
[2*X,4*Y,4*Z] eq -4,
[2*X,3*Z] eq -1.
となり、eliminateルールとAPによって
[2*X,4*Y,2*Z] eq -2,
[2*Z] eq -2,
[2*X,3*Z] eq -1.
に変換されて、bindルール及びprologのライブラリにあるis/2 ...
[2*X,4*Y,2*Z] eq -2,
[2*X,3*Z] eq-1.
となり、boundルールによってZ項は右辺に移項され、
[2*X,4*Y] eq 0,
[2*X] eq 2.
となる。再びbindルール及びboundルールが発火して、X=1.0で...
[4*Y] eq -2.
となる。当然これもbindルールで変換され、Y=-0.5で束縛され...
結果、束縛された変数である
X=1.0, Y=-0.5, Z=-1.0.
が解として出力される。このようにしてこのSolverは連立一次...
*interval.pl [#zcb4bd6c]
コード
:- module(interval, [(::)/2, le/2, eq/2, ne/2, add/3, mu...
split0/1, split/1, label/1]).
:- use_module( library(chr)).
% for domain constraints
:- op( 700,xfx,'::').
:- op( 600,xfx,':').
% for inequality constraints
:- op( 700,xfx,le).
:- op( 700,xfx,ne).
:- op( 700,xfx,eq).
%% Deprecated syntax used for SICStus 3.x
%handler interval.
%constraints
%% Syntax for SWI / SICStus 4.x
:- chr_constraint
% X::Min:Max - X is between the numbers Min and Max, inc...
% X must always be an unbound variable(!), and Min and M...
% (i.e. ground) arithmetic expressions (or numbers)
(::)/2,
le/2, eq/2, ne/2, add/3, mult/3,
% int(X) says that X is an integer (default is a real)
int/1,
% bool(X) says that X is a boolean (default is a real)
bool/1,
split0/1,
split/1,
label/1, % repeated split/1
browse/1. % watch how domain of X evolves
% Auxiliary -----------------------------------
browse(X), X::A:B ==> write((X::A:B)),nl.
% define the smallest intervals you want to get:
% the smaller, the more precise, the longer the computat...
small(A:B) :- A+2.0e-05>=B.
% is zero part of A:B ?
withzero(A:B) :- A=<0, 0=<B.
% Intersection -------------------------------
redundant @ X::A:B \ X::C:D <=>
(C=<A, B=<D ; A<B,small(A:B), C<D,small(C:D)) | ...
intersect @ X::A:B , X::C:D <=>
X::max(A,C):min(B,D).
% Special Cases -------------------------------
failure @ _::A:B <=> A>B | fail.
compute @ X::A:B <=> \+ (number(A),number(B)) | C is A, ...
integer @ int(X), X::A:B ==> \+ (integer(A),integer(B)) |
C is integer(ceiling(A)), D is integer(floor(B)), ...
bool @ bool(X), X::_:B ==> B<1 | X::0:0.
bool @ bool(X), X::A:_ ==> A>0 | X::1:1.
bool @ bool(X) ==> X::0:1.
% Inequality -------------------------------
(le) @ X le Y, X::A:_, Y::_:D ==> Y::A:D, X::A:D.
(eq) @ X eq Y, X::A:B, Y::C:D ==> Y::A:B, X::C:D.
(ne) @ X ne Y, X::A:A, Y::A:A <=> fail.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> B=Y | X::A:B-1.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> B=Y | X::A:B-1.
% Addition X+Y=Z -------------------------------
add @ add(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
X::E-D:F-C, Y::E-B:F-A, Z::A+C:B+D.
% Multiplication X*Y=Z -------------------------------
mult_z @ mult(X,Y,Z), X::A:B, Y::C:D ==>
M1 is A*C, M2 is A*D, M3 is B*C, M4 is B*D,
Z::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_y @ mult(X,Y,Z), X::A:B, Z::E:F ==>
\+ withzero(A:B) |
M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_x @ mult(Y,X,Z), X::A:B, Z::E:F ==>
\+ withzero(A:B) |
M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_xyz @ mult(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
withzero(A:B), withzero(C:D), \+ withzero(E:F) |
(A*C<E -> D>0, X::E/D:B ; true),
(B*D<E -> C<0, X::A:E/C ; true),
(F<A*D -> C<0, X::F/C:B ; true),
(F<B*C -> D>0, X::A:F/D ; true).
% Labeling ---------------------------------------------...
label @ split0(X), X::A:B <=> \+ small(A:B), A<0,0<B |
(X::A:0 ; X::0:B).
label @ split(X), X::A:B <=> \+ small(A:B) |
Half is (A+B)/2,
(X::A:Half ; X::Half:B).
label @ label(X), X::A:B <=> \+ small(A:B) |
Half is (A+B)/2,
(X::A:Half ; X::Half:B),
label(X).
これは数値に幅のある整数または実数の変数を扱うSolverであ...
例えば、1~3まであり得るXと2~4まであり得るYの和X+Yは3~7ま...
以下、入力例とその場合の動作である。
input
X::3:5, X::2:4.
intersectルールにより、 二つの制約は X::max(3,2):min(5,4)...
input
X le Y, X::3:5, Y::2:4.
le/2はless or equalを表す制約で、X=<Yの意味になる。
今回は伝播規則(le)が発火して、
Y::3:4, X::3:4
という制約が新たに生成される。
ここでintersectルールまたはrebundantルールが発火し、
X::3:4, X::3:5
という制約は
X::3:4
に書き換えられる。
また、
Y::3:4, Y::2:4
という制約も同じ2つのルールのどちらかによって
Y::3:4
に書き換えられる。
従って出力は
X le Y, X::3:4, Y::3:4
となる。
input
add(X,Y,Z), X::2:5, Y::3:4, Z::1:7
addは X+Y=Z の関係を表す制約である。
この入力に対しては伝播規則addが発火し、
X::1-4:7-3, Y::1-5:7-2, Z::2+3:4+5
則ち
X:: -3:4, Y:: -4:5, Z::5:9
という制約を生成する。
これが元々あった制約群と合わせてintersectルールまたはrebu...
X::2:4, Y::3:4, Z::5:7 となる。
数値が変化したためもう一度addルールは発火するが、結局inte...
add(X,Y,Z), X::2:4, Y::3:4, Z::5:7
となる。
mult(X,Y,Z), X:: -2:3, Y:: -3:4, Z:: -12: -9.
multはX*Y=Zの関係を表す制約である。
半角スペースが入っているのは - が :: と結合して違う名前の...
この入力に対して4つの伝播規則mult_z, mult_y, mult_xが一度...
mult_zにより、
M1=-2*-3=6, M2=-2*4=-8, M3=3*-3=-9, M4=3*4=12
を使って
Z:: -9:12
が生成され、
mult_yにより、
M1=-12/-2=6, M2=-12/3=-4, M3=-9/-2=4.5, M4=-9/3=-3
を使って
Y:: -4:6
が生成され、
mult_xにより、
M1=-12/-3=4, M2=-12/4=-3, M3=-9/-3=3, M4=-9/4=-2.25
を使って
X:: -3: 4
が生成される。
mult_xyzはwithzero制約がないので発火しない。
ここからintersectルールまたはrebundantルールによって、
X:: -2:3, X:: -3:4,
Y:: -3:4, Y:: -4:6,
Z:: -12: -9, Z:: -9:12,
という制約は
X:: -2:3, Y:: -3:4, Z:: -9: -9
に単純化される。これが出力となる。
input
A::(-3):3, B::(-3):3, C::4:4, mult(A,B,C), A eq B, label...
label/1はprologのライブラリにある述語でもあり、引数に与え...
3番目のlabelルールにより、Aの範囲は上限・下限の平均値でわ...
また、(eq)ルールとintersectまたはrebundantルールが実行さ...
その前後でmult(A,B,C)が発火し、結果Cが4を含まない範囲であ...
それを繰り返してでA,Bの範囲が狭まっていく。
これだけだと無限ループになるが、ある程度範囲が狭くなると...
small(A:B) :- A+2.0e-05>=B
が成功し、3番目のlabelルールが発火しなくなって止まる。
具体的に何回繰り返しているかは不明確なのでここでは省略す...
*rationaltree.pl [#h733a02a]
コード
:- module(rationaltree, [(~)/2, (#~)/2, neq_list/2, labe...
:- use_module(library(chr)).
:- use_module(library(lists)).
user:library_directory('.').
:- use_module(library(var_order)). % need stable orde...
:- op(700,xfx,(~)).
:- op(700,xfx,(#~)).
%% Deprecated syntax used for SICStus 3.x
%handler rationaltree.
%constraints (~)/2, (#~)/2, eq_list/2, neq_list/2, label...
%% Syntax for SWI / SICStus 4.x
:- chr_constraint (~)/2, (#~)/2, eq_list/2, neq_list/2, ...
% T1 ~ T2 means: term T1 is syntactically equal to term T2
% T1 #~ T2 means: term T1 is syntactically different fro...
eq_globalize @ T1 ~ T2 ==> var_order:globalize(...
neq_globalize @ T1 #~ T2 ==> var_order:globalize(...
eq_reflexivity @ X ~ X <=> true.
eq_orientation @ T ~ X <=> var(X), lss(X,T) | X...
eq_decomposition @ T1 ~ T2 <=> nonvar(T1),nonvar(T2...
same_functions(T1,T2).
eq_confrontation @ X ~ T1 \ X ~ T2 <=> var(X), lss(...
T1 ~ T2.
neq_reflexivity @ X #~ X <=> fail.
neq_orientation @ T #~ X <=> var(X), lss(X,T) | X...
neq_decomposition @ T1 #~ T2 <=> nonvar(T1), nonvar(T...
different_functions(...
neq_confrontation @ X ~ T1 \ X #~ T2 <=> T1 #~ T2.
% two same-length lists must be equal,
% i.e., every pair of elements must be equal
eq_list([],[]) <=> true.
eq_list([X|L1],[Y|L2]) <=> X ~ Y, eq_list(L1,L2).
% two same-length lists must not be equal,
% i.e., at least one pair of elements must be different
neq_list([],[]) <=> fail.
neq_list([X],[Y]) <=> X #~ Y.
neq_list([X|L1],[X|L2]) <=> neq_list(L1,L2).
neq_list([X|L1],[Y|L2]), X~Y <=> neq_list(L1,L2).
% label
label \ neq_list([X|L1],[Y|L2])#Id <=> true |
(X #~ Y ; X ~ Y, neq_list(L1,L2))
pragma passive(Id).
%% Auxiliary
% lss(X,Y): X is smaller than Y by term-size order
lss(X,Y) :- var(X),var(Y), var_order:var_compare(<,X,Y)....
lss(X,Y) :- var(X),nonvar(Y).
lss(X,Y) :- nonvar(X),nonvar(Y), termsize(X,M),termsize(...
% leq(X,Y): X is smaller-eq than Y by term-size order
leq(X,Y) :- \+ lss(Y,X).
% functions must be equal
same_functions(T1,T2) :-
T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), eq_lis...
% functions must be different
different_functions(T1,T2) :-
T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), !, neq...
different_functions(_,_).
% termsize
termsize_list([],0).
termsize_list([X|L],N) :- termsize(X,N1), termsize_list(...
termsize(X,0) :- var(X).
termsize(T,1) :- atom(T).
termsize(T,N) :- compound(T), T=..L, termsize_list(L,N).
このコードは、「RationalTree」の同一性、筆者が読んだ限り...
関数の名前が同じで、引数の数と、その引数が同じ構造の関数...
以下入力と動作の例。
入力
f(X,b)~f(a,Y).
「~」は二つの関数が同じ構造であることを示す制約である。
eq_globalizeルールによって変数にid属性(順序付けのための性...
f(X,b)~f(a,Y).
は
same_functions(T1,T2).
に変換され、prolog述語によって関数名を先頭、引数が後に続...
eq_list(L1,L2)制約の判定は
eq_list([],[]) <=> true.
eq_list([X|L1],[Y|L2]) <=> X~Y, eq_list(L1,L2).
の二つのルールで定義されていて、各変数について X~Y である...
eq_reflexivity @ X~X <=> true.
というルールが存在し、それによって判定される。入力中の変...
X~a, Y~b.
が出力される。
入力
f(a,b)~f(X).
に対しては、上と同様の流れでsame_functions(f(a,b),f(X))の...
same_length([a,b],[X])がfailしてnoを出力される。
入力
X~f(X), X~f(f(X)).
に対しては、eq_confrontationルールが発火して
X~f(X), f(X)~f(f(X)).
と変換され、eq_decomposition,same_functions及びeq_listル...
X~f(X), X~f(X).
となる。これがさらにeq_confrontationルールにより、
X~f(X), f(X)~f(X).
となった上で、eq_decomposition,same_functions,eq_list,eq_...
X~f(X).
となる。
入力
f(a,X,c)#~f(a,b,Y), X#~Y, label.
に対しては、関数は変数でないため、
neq_decompositionルールが発火。
different_functions(f(a,X,c),f(a,b,Y)), X#~Y, label.
からprolog記述を経由して
neq_list([a,X,c],[a,b,Y]), X#~Y, label.
となる。
neq_listに関する規則とeq_reflexivityルールにより、
neq_list([X,c],[b,Y]), X#~Y, label.
となったところで
label \ neq_list([X|L1],[Y|L2])#Id <=> true | (X#~Y ; X~...
pragma passive(Id).
の記述(pragma以下はprologの記述と思われるが詳細不明、とに...
label, X#~b, X#~Y.
が出力され、別解を探させるとバックトラックしX#~bではなく ...
neq_list([c],[Y]), X#~Y, X~b, label.
X#~Y, X~b, c#~Y, label.
となった後、neq_orientationルールにより、
X#~Y, X~b, Y#~c, label.
そしてneq_confrontationルールにより
b#~Y, X~b, Y#~c, label.
もう一度のneq_orientationルールにより
Y#~b, Y#~c, X~b, label.
という解を出力して解を網羅し終わる。
終了行:
トップページ:[[初学者向けCHRの使い方まとめ]]
*例題目録 [#vc82f401]
#contents
*boolean.pl [#ub7ae437]
コード
:- 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...
%% 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 c...
%% 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(...
このプログラムは、各種の論理関数(boolean,and,or,xor,neg,i...
例えば
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).
という制約と矛盾しないように変数の値を選択されることにな...
または、
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
の記述によってor制約が消滅しC=1に変換される。
さらに、
labeling \ neg(A,B) <=> label_neg(A,B).
label_neg(0,1).
label_neg(1,0).
という規則及び公理(この名前の述語が合致しなければならない...
A = 0, B = 1, C = 1, labeling.
A = 1, B = 0, C = 1, labeling.
の二通りになる。(SWI-prologはすべての解を網羅するため)
labeling制約がない場合、
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
が発火したところで処理が止まり、
C = 1, neg(A,B).
を出力してくる。
*equations_gauss.pl [#f662fca4]
コード
:- 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 Coeffi...
%% eq/2
%% curly brackets as wrapper to avoid name clash with bu...
%% {}/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) | C...
%% 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. Hol...
%% 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 ari...
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), addp...
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(...
normpoly([A-B] eq C, E0) :- normpoly([A] eq C,E), normpo...
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,...
normpoly([X*A] eq 0, E0) :-
safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,...
normpoly([X/A] eq 0, E0) :-
safe_is(A1,1/A), normpoly([X] eq 0, E), multpoly(A1,...
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; retai...
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) :- o...
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) :- o...
addpoly([A*X|P] eq C, Q eq D, P0 eq C0).
%% multpoly(M,E, E0): multiply polynomial equation with ...
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).
こちらはガウスの消去法により連立一次方程式を解くSolverで...
%% Auxiliary predicates
以降の記述はSWI-prologの述語(CHRで言う伝播規則のような動...
入力例1として、
{2+2*X+4*Y+2*Z=0, 4+2*X+4*Y+4*Z=0, 1+2*X+3*Z=0}.
を与える。
この入力はまず、splitルールによって
{2+2*X+4*Y+2*Z=0},
{4+2*X+4*Y+4*Z=0},
{1+2*X+3*Z=0}.
と変換される。その後、normalizeルール及びAPによって
[2*X,4*Y,2*Z] eq -2,
[2*X,4*Y,4*Z] eq -4,
[2*X,3*Z] eq -1.
となり、eliminateルールとAPによって
[2*X,4*Y,2*Z] eq -2,
[2*Z] eq -2,
[2*X,3*Z] eq -1.
に変換されて、bindルール及びprologのライブラリにあるis/2 ...
[2*X,4*Y,2*Z] eq -2,
[2*X,3*Z] eq-1.
となり、boundルールによってZ項は右辺に移項され、
[2*X,4*Y] eq 0,
[2*X] eq 2.
となる。再びbindルール及びboundルールが発火して、X=1.0で...
[4*Y] eq -2.
となる。当然これもbindルールで変換され、Y=-0.5で束縛され...
結果、束縛された変数である
X=1.0, Y=-0.5, Z=-1.0.
が解として出力される。このようにしてこのSolverは連立一次...
*interval.pl [#zcb4bd6c]
コード
:- module(interval, [(::)/2, le/2, eq/2, ne/2, add/3, mu...
split0/1, split/1, label/1]).
:- use_module( library(chr)).
% for domain constraints
:- op( 700,xfx,'::').
:- op( 600,xfx,':').
% for inequality constraints
:- op( 700,xfx,le).
:- op( 700,xfx,ne).
:- op( 700,xfx,eq).
%% Deprecated syntax used for SICStus 3.x
%handler interval.
%constraints
%% Syntax for SWI / SICStus 4.x
:- chr_constraint
% X::Min:Max - X is between the numbers Min and Max, inc...
% X must always be an unbound variable(!), and Min and M...
% (i.e. ground) arithmetic expressions (or numbers)
(::)/2,
le/2, eq/2, ne/2, add/3, mult/3,
% int(X) says that X is an integer (default is a real)
int/1,
% bool(X) says that X is a boolean (default is a real)
bool/1,
split0/1,
split/1,
label/1, % repeated split/1
browse/1. % watch how domain of X evolves
% Auxiliary -----------------------------------
browse(X), X::A:B ==> write((X::A:B)),nl.
% define the smallest intervals you want to get:
% the smaller, the more precise, the longer the computat...
small(A:B) :- A+2.0e-05>=B.
% is zero part of A:B ?
withzero(A:B) :- A=<0, 0=<B.
% Intersection -------------------------------
redundant @ X::A:B \ X::C:D <=>
(C=<A, B=<D ; A<B,small(A:B), C<D,small(C:D)) | ...
intersect @ X::A:B , X::C:D <=>
X::max(A,C):min(B,D).
% Special Cases -------------------------------
failure @ _::A:B <=> A>B | fail.
compute @ X::A:B <=> \+ (number(A),number(B)) | C is A, ...
integer @ int(X), X::A:B ==> \+ (integer(A),integer(B)) |
C is integer(ceiling(A)), D is integer(floor(B)), ...
bool @ bool(X), X::_:B ==> B<1 | X::0:0.
bool @ bool(X), X::A:_ ==> A>0 | X::1:1.
bool @ bool(X) ==> X::0:1.
% Inequality -------------------------------
(le) @ X le Y, X::A:_, Y::_:D ==> Y::A:D, X::A:D.
(eq) @ X eq Y, X::A:B, Y::C:D ==> Y::A:B, X::C:D.
(ne) @ X ne Y, X::A:A, Y::A:A <=> fail.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> B=Y | X::A:B-1.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> B=Y | X::A:B-1.
% Addition X+Y=Z -------------------------------
add @ add(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
X::E-D:F-C, Y::E-B:F-A, Z::A+C:B+D.
% Multiplication X*Y=Z -------------------------------
mult_z @ mult(X,Y,Z), X::A:B, Y::C:D ==>
M1 is A*C, M2 is A*D, M3 is B*C, M4 is B*D,
Z::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_y @ mult(X,Y,Z), X::A:B, Z::E:F ==>
\+ withzero(A:B) |
M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_x @ mult(Y,X,Z), X::A:B, Z::E:F ==>
\+ withzero(A:B) |
M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),ma...
mult_xyz @ mult(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
withzero(A:B), withzero(C:D), \+ withzero(E:F) |
(A*C<E -> D>0, X::E/D:B ; true),
(B*D<E -> C<0, X::A:E/C ; true),
(F<A*D -> C<0, X::F/C:B ; true),
(F<B*C -> D>0, X::A:F/D ; true).
% Labeling ---------------------------------------------...
label @ split0(X), X::A:B <=> \+ small(A:B), A<0,0<B |
(X::A:0 ; X::0:B).
label @ split(X), X::A:B <=> \+ small(A:B) |
Half is (A+B)/2,
(X::A:Half ; X::Half:B).
label @ label(X), X::A:B <=> \+ small(A:B) |
Half is (A+B)/2,
(X::A:Half ; X::Half:B),
label(X).
これは数値に幅のある整数または実数の変数を扱うSolverであ...
例えば、1~3まであり得るXと2~4まであり得るYの和X+Yは3~7ま...
以下、入力例とその場合の動作である。
input
X::3:5, X::2:4.
intersectルールにより、 二つの制約は X::max(3,2):min(5,4)...
input
X le Y, X::3:5, Y::2:4.
le/2はless or equalを表す制約で、X=<Yの意味になる。
今回は伝播規則(le)が発火して、
Y::3:4, X::3:4
という制約が新たに生成される。
ここでintersectルールまたはrebundantルールが発火し、
X::3:4, X::3:5
という制約は
X::3:4
に書き換えられる。
また、
Y::3:4, Y::2:4
という制約も同じ2つのルールのどちらかによって
Y::3:4
に書き換えられる。
従って出力は
X le Y, X::3:4, Y::3:4
となる。
input
add(X,Y,Z), X::2:5, Y::3:4, Z::1:7
addは X+Y=Z の関係を表す制約である。
この入力に対しては伝播規則addが発火し、
X::1-4:7-3, Y::1-5:7-2, Z::2+3:4+5
則ち
X:: -3:4, Y:: -4:5, Z::5:9
という制約を生成する。
これが元々あった制約群と合わせてintersectルールまたはrebu...
X::2:4, Y::3:4, Z::5:7 となる。
数値が変化したためもう一度addルールは発火するが、結局inte...
add(X,Y,Z), X::2:4, Y::3:4, Z::5:7
となる。
mult(X,Y,Z), X:: -2:3, Y:: -3:4, Z:: -12: -9.
multはX*Y=Zの関係を表す制約である。
半角スペースが入っているのは - が :: と結合して違う名前の...
この入力に対して4つの伝播規則mult_z, mult_y, mult_xが一度...
mult_zにより、
M1=-2*-3=6, M2=-2*4=-8, M3=3*-3=-9, M4=3*4=12
を使って
Z:: -9:12
が生成され、
mult_yにより、
M1=-12/-2=6, M2=-12/3=-4, M3=-9/-2=4.5, M4=-9/3=-3
を使って
Y:: -4:6
が生成され、
mult_xにより、
M1=-12/-3=4, M2=-12/4=-3, M3=-9/-3=3, M4=-9/4=-2.25
を使って
X:: -3: 4
が生成される。
mult_xyzはwithzero制約がないので発火しない。
ここからintersectルールまたはrebundantルールによって、
X:: -2:3, X:: -3:4,
Y:: -3:4, Y:: -4:6,
Z:: -12: -9, Z:: -9:12,
という制約は
X:: -2:3, Y:: -3:4, Z:: -9: -9
に単純化される。これが出力となる。
input
A::(-3):3, B::(-3):3, C::4:4, mult(A,B,C), A eq B, label...
label/1はprologのライブラリにある述語でもあり、引数に与え...
3番目のlabelルールにより、Aの範囲は上限・下限の平均値でわ...
また、(eq)ルールとintersectまたはrebundantルールが実行さ...
その前後でmult(A,B,C)が発火し、結果Cが4を含まない範囲であ...
それを繰り返してでA,Bの範囲が狭まっていく。
これだけだと無限ループになるが、ある程度範囲が狭くなると...
small(A:B) :- A+2.0e-05>=B
が成功し、3番目のlabelルールが発火しなくなって止まる。
具体的に何回繰り返しているかは不明確なのでここでは省略す...
*rationaltree.pl [#h733a02a]
コード
:- module(rationaltree, [(~)/2, (#~)/2, neq_list/2, labe...
:- use_module(library(chr)).
:- use_module(library(lists)).
user:library_directory('.').
:- use_module(library(var_order)). % need stable orde...
:- op(700,xfx,(~)).
:- op(700,xfx,(#~)).
%% Deprecated syntax used for SICStus 3.x
%handler rationaltree.
%constraints (~)/2, (#~)/2, eq_list/2, neq_list/2, label...
%% Syntax for SWI / SICStus 4.x
:- chr_constraint (~)/2, (#~)/2, eq_list/2, neq_list/2, ...
% T1 ~ T2 means: term T1 is syntactically equal to term T2
% T1 #~ T2 means: term T1 is syntactically different fro...
eq_globalize @ T1 ~ T2 ==> var_order:globalize(...
neq_globalize @ T1 #~ T2 ==> var_order:globalize(...
eq_reflexivity @ X ~ X <=> true.
eq_orientation @ T ~ X <=> var(X), lss(X,T) | X...
eq_decomposition @ T1 ~ T2 <=> nonvar(T1),nonvar(T2...
same_functions(T1,T2).
eq_confrontation @ X ~ T1 \ X ~ T2 <=> var(X), lss(...
T1 ~ T2.
neq_reflexivity @ X #~ X <=> fail.
neq_orientation @ T #~ X <=> var(X), lss(X,T) | X...
neq_decomposition @ T1 #~ T2 <=> nonvar(T1), nonvar(T...
different_functions(...
neq_confrontation @ X ~ T1 \ X #~ T2 <=> T1 #~ T2.
% two same-length lists must be equal,
% i.e., every pair of elements must be equal
eq_list([],[]) <=> true.
eq_list([X|L1],[Y|L2]) <=> X ~ Y, eq_list(L1,L2).
% two same-length lists must not be equal,
% i.e., at least one pair of elements must be different
neq_list([],[]) <=> fail.
neq_list([X],[Y]) <=> X #~ Y.
neq_list([X|L1],[X|L2]) <=> neq_list(L1,L2).
neq_list([X|L1],[Y|L2]), X~Y <=> neq_list(L1,L2).
% label
label \ neq_list([X|L1],[Y|L2])#Id <=> true |
(X #~ Y ; X ~ Y, neq_list(L1,L2))
pragma passive(Id).
%% Auxiliary
% lss(X,Y): X is smaller than Y by term-size order
lss(X,Y) :- var(X),var(Y), var_order:var_compare(<,X,Y)....
lss(X,Y) :- var(X),nonvar(Y).
lss(X,Y) :- nonvar(X),nonvar(Y), termsize(X,M),termsize(...
% leq(X,Y): X is smaller-eq than Y by term-size order
leq(X,Y) :- \+ lss(Y,X).
% functions must be equal
same_functions(T1,T2) :-
T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), eq_lis...
% functions must be different
different_functions(T1,T2) :-
T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), !, neq...
different_functions(_,_).
% termsize
termsize_list([],0).
termsize_list([X|L],N) :- termsize(X,N1), termsize_list(...
termsize(X,0) :- var(X).
termsize(T,1) :- atom(T).
termsize(T,N) :- compound(T), T=..L, termsize_list(L,N).
このコードは、「RationalTree」の同一性、筆者が読んだ限り...
関数の名前が同じで、引数の数と、その引数が同じ構造の関数...
以下入力と動作の例。
入力
f(X,b)~f(a,Y).
「~」は二つの関数が同じ構造であることを示す制約である。
eq_globalizeルールによって変数にid属性(順序付けのための性...
f(X,b)~f(a,Y).
は
same_functions(T1,T2).
に変換され、prolog述語によって関数名を先頭、引数が後に続...
eq_list(L1,L2)制約の判定は
eq_list([],[]) <=> true.
eq_list([X|L1],[Y|L2]) <=> X~Y, eq_list(L1,L2).
の二つのルールで定義されていて、各変数について X~Y である...
eq_reflexivity @ X~X <=> true.
というルールが存在し、それによって判定される。入力中の変...
X~a, Y~b.
が出力される。
入力
f(a,b)~f(X).
に対しては、上と同様の流れでsame_functions(f(a,b),f(X))の...
same_length([a,b],[X])がfailしてnoを出力される。
入力
X~f(X), X~f(f(X)).
に対しては、eq_confrontationルールが発火して
X~f(X), f(X)~f(f(X)).
と変換され、eq_decomposition,same_functions及びeq_listル...
X~f(X), X~f(X).
となる。これがさらにeq_confrontationルールにより、
X~f(X), f(X)~f(X).
となった上で、eq_decomposition,same_functions,eq_list,eq_...
X~f(X).
となる。
入力
f(a,X,c)#~f(a,b,Y), X#~Y, label.
に対しては、関数は変数でないため、
neq_decompositionルールが発火。
different_functions(f(a,X,c),f(a,b,Y)), X#~Y, label.
からprolog記述を経由して
neq_list([a,X,c],[a,b,Y]), X#~Y, label.
となる。
neq_listに関する規則とeq_reflexivityルールにより、
neq_list([X,c],[b,Y]), X#~Y, label.
となったところで
label \ neq_list([X|L1],[Y|L2])#Id <=> true | (X#~Y ; X~...
pragma passive(Id).
の記述(pragma以下はprologの記述と思われるが詳細不明、とに...
label, X#~b, X#~Y.
が出力され、別解を探させるとバックトラックしX#~bではなく ...
neq_list([c],[Y]), X#~Y, X~b, label.
X#~Y, X~b, c#~Y, label.
となった後、neq_orientationルールにより、
X#~Y, X~b, Y#~c, label.
そしてneq_confrontationルールにより
b#~Y, X~b, Y#~c, label.
もう一度のneq_orientationルールにより
Y#~b, Y#~c, X~b, label.
という解を出力して解を網羅し終わる。
ページ名: