初学者向けCHRの使い方まとめ/Constraint_Solver のバックアップ(No.2)

バックアップ一覧
差分を表示
現在との差分を表示
ソースを表示
初学者向けCHRの使い方まとめ/Constraint_Solver へ行く。
- 1 (2019-02-18 (月) 10:11:04)
- 2 (2019-02-18 (月) 12:39:53)
- 3 (2019-02-18 (月) 16:18:25)
- 4 (2019-02-19 (火) 10:30:17)

例題目録 †

例題目録
boolean.pl
equations_gauss.pl

boolean.pl †

コード

:- 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).

を出力してくる。

↑

equations_gauss.pl †

コード

:- 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).