Modul Tree

Jan Burse, erstellt 20. Okt 2018
/**
* The SAT solver allows denoting Boolean value expressions. These
* expressions can contain native Prolog variables. Boolean expressions
* are posted to the SAT solver via the predicate sat/1. Internally
* the SAT constraint is normalized into a BDD tree. The resulting
* BDD tree is automatically shown by the top-level:
*
* Example:
* ?- sat(X#Y).
* sat((X->(Y->0;1);Y->1;0))
*
* BDD tree reductions and attribute variable hooks guard the interaction
* between SAT con-straints. Currently the following inference rule sets
* have been implemented for Boolean value expressions:
*
* * Forward Checking
*
* The forward checking consists of the two inference rules constant
* elimination and constant back propagation. Where permitted SAT
* constraints are replaced by native Prolog unification. It is also
* allowed mixing native Prolog unification =/2 with SAT constraints:
*
* Examples:
* ?- X=Y, sat(X+Y).
* X = 1,
* Y = 1
* ?- sat(X+Y), X=Y.
* X = 1,
* Y = 1
*
* Warranty & Liability
* To the extent permitted by applicable law and unless explicitly
* otherwise agreed upon, XLOG Technologies GmbH makes no warranties
* regarding the provided information. XLOG Technologies GmbH assumes
* no liability that any problems might be solved with the information
* provided by XLOG Technologies GmbH.
*
* Rights & License
* All industrial property rights regarding the information - copyright
* and patent rights in particular - are the sole property of XLOG
* Technologies GmbH. If the company was not the originator of some
* excerpts, XLOG Technologies GmbH has at least obtained the right to
* reproduce, change and translate the information.
*
* Reproduction is restricted to the whole unaltered document. Reproduction
* of the information is only allowed for non-commercial uses. Selling,
* giving away or letting of the execution of the library is prohibited.
* The library can be distributed as part of your applications and libraries
* for execution provided this comment remains unchanged.
*
* Restrictions
* Only to be distributed with programs that add significant and primary
* functionality to the library. Not to be distributed with additional
* software intended to replace any components of the library.
*
* Trademarks
* Jekejeke is a registered trademark of XLOG Technologies GmbH.
*/
:- package(library(jekmin/reference/finite)).
:- module(tree, []).
:- use_module(library(basic/lists)).
:- use_module(library(term/unify)).
:- use_module(library(experiment/trail)).
:- use_module(library(minimal/assume)).
:- use_module(library(experiment/ref)).
:- public infix(#).
:- op(500, yfx, #).
:- public prefix(~).
:- op(300, fy, ~).
/********************************************************/
/* Expressions */
/********************************************************/
/**
* expr_tree(E, T):
* The predicate succeeds in T with the tree of the expression E.
*/
% expr_tree(+Expr, -Tree)
/**
* V (SAT):
* A native Prolog variable V represents a Boolean variable.
*/
var(X), !,
R = node3(Y,[Y],one,zero).
/**
* 0 (SAT):
* 1 (SAT):
* The constant 0 or 1 represents a Boolean constant.
*/
R = zero.
R = one.
/**
* ~ A (SAT):
* If A is an expression then the negation ~A is also an expression.
*/
expr_tree(~A, R) :- !,
expr_tree(A, P),
tree_not(P, R).
/**
* A + B (SAT):
* If A and B are expressions then the disjunction A+B is also an expression.
*/
expr_tree(A+B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_or(P, Q, R).
/**
* A * B (SAT):
* If A and B are expressions then the conjunction A*B is also an expression.
*/
expr_tree(A*B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_and(P, Q, R).
/**
* A =< B (SAT):
* If A and B are expressions then the implication A=<B is also an expression.
*/
expr_tree(A=<B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_imply(P, Q, R).
/**
* A >= B (SAT):
* If A and B are expressions then the implication B=<A is also an expression.
*/
expr_tree(A>=B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_imply(Q, P, R).
/**
* A > B (SAT):
* If A and B are expressions then the difference A>B is also an expression.
*/
expr_tree(A>B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_diff(P, Q, R).
/**
* A < B (SAT):
* If A and B are expressions then the difference B>A is also an expression.
*/
expr_tree(A<B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_diff(Q, P, R).
/**
* A =:= B (SAT):
* If A and B are expressions then the equality A=:=B is also an expression.
*/
expr_tree(A=:=B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_equiv(P, Q, R).
/**
* A # B (SAT):
* If A and B are expressions then the xor A#B is also an expression.
*/
expr_tree(A#B, R) :- !,
expr_tree(A, P),
expr_tree(B, Q),
tree_xor(P, Q, R).
/**
* A -> B; C (SAT):
* If A, B and C are expressions then the if-then-else A->B;C is also an expression.
*/
expr_tree((A->B;C), S) :- !,
expr_tree(A, P),
expr_tree(B, Q),
expr_tree(C, R),
tree_ite(Q, R, P, S).
/**
* V^A (SAT):
* If V is a native Prolog variable and A is an expression then the Boolean existential quantification V^A is also an expression.
*/
expr_tree(X^A, R) :- !,
expr_tree(A, P),
tree_exists(P, Y, R).
throw(error(type_error(sat_expr,E),_)).
/**
* expr_pretty(T, E):
* The predicate succeeds in E with the expression of the tree T.
*/
% expr_pretty(+Tree, -Expr)
expr_pretty(zero, R) :- !,
R = 0.
expr_pretty(one, R) :- !,
R = 1.
expr_pretty(node3(X,_,A,B), R) :-
R = (Y->C;D).
/*****************************************************************/
/* Connectives */
/*****************************************************************/
/**
* tree_not(P, Q):
* The predicate succeeds in Q with the P complemented.
*/
% tree_not(+Tree, -Tree)
:- private tree_not/2.
tree_not(zero, R) :- !,
R = one.
tree_not(one, R) :- !,
R = zero.
tree_not(node3(X,W,A,B), node3(X,W,C,D)) :-
tree_not(A, C),
tree_not(B, D).
/**
* tree_and(P, Q, R):
* The predicate succeeds in R with the boolean and of P and Q.
*/
% tree_and(+Tree, +Tree, -Tree)
tree_and(zero, _, R) :- !,
R = zero.
tree_and(_, zero, R) :- !,
R = zero.
tree_and(one, A, R) :- !,
R = A.
tree_and(A, one, R) :- !,
R = A.
tree_and(node3(X,_,A,B), N, R) :-
N = node3(Y,_,_,_),
X < Y, !,
tree_and(A, N, E),
tree_and(B, N, F),
tree_make(E, F, X, R).
tree_and(node3(X,_,A,B), node3(X,_,C,D), R) :- !,
tree_and(A, C, E),
tree_and(B, D, F),
tree_make(E, F, X, R).
tree_and(N, node3(Y,_,C,D), R) :-
tree_and(N, C, E),
tree_and(N, D, F),
tree_make(E, F, Y, R).
/**
* tree_or(P, Q, R):
* The predicate succeeds in R with the boolean or of P and Q.
*/
% tree_or(+Tree, +Tree, -Tree)
:- private tree_or/3.
tree_or(one, _, R) :- !,
R = one.
tree_or(_, one, R) :- !,
R = one.
tree_or(zero, A, R) :- !,
R = A.
tree_or(A, zero, R) :- !,
R = A.
tree_or(node3(X,_,A,B), N, R) :-
N = node3(Y,_,_,_),
X < Y, !,
tree_or(A, N, E),
tree_or(B, N, F),
tree_make(E, F, X, R).
tree_or(node3(X,_,A,B), node3(X,_,C,D), R) :- !,
tree_or(A, C, E),
tree_or(B, D, F),
tree_make(E, F, X, R).
tree_or(N, node3(Y,_,C,D), R) :-
tree_or(N, C, E),
tree_or(N, D, F),
tree_make(E, F, Y, R).
/**
* tree_imply(P, Q, R):
* The predicate succeeds in R with the boolean conditional of P and Q.
*/
% tree_imply(+Tree, +Tree, -Tree)
:- private tree_imply/3.
tree_imply(zero, _, R) :- !,
R = one.
tree_imply(A, zero, R) :- !,
tree_not(A, R).
tree_imply(one, A, R) :- !,
R = A.
tree_imply(_, one, R) :- !,
R = one.
tree_imply(node3(X,_,A,B), N, R) :-
N = node3(Y,_,_,_),
X < Y, !,
tree_imply(A, N, E),
tree_imply(B, N, F),
tree_make(E, F, X, R).
tree_imply(node3(X,_,A,B), node3(X,_,C,D), R) :- !,
tree_imply(A, C, E),
tree_imply(B, D, F),
tree_make(E, F, X, R).
tree_imply(N, node3(Y,_,C,D), R) :-
tree_imply(N, C, E),
tree_imply(N, D, F),
tree_make(E, F, Y, R).
/**
* tree_equiv(P, Q, R):
* The predicate succeeds in R with the boolean bi-conditional of P and Q.
*/
% tree_equiv(+Tree, +Tree, -Tree)
tree_equiv(one, A, R) :- !,
R = A.
tree_equiv(A, one, R) :- !,
R = A.
tree_equiv(zero, A, R) :- !,
tree_not(A, R).
tree_equiv(A, zero, R) :- !,
tree_not(A, R).
tree_equiv(node3(X,_,A,B), N, R) :-
N = node3(Y,_,_,_),
X < Y, !,
tree_equiv(A, N, E),
tree_equiv(B, N, F),
tree_make(E, F, X, R).
tree_equiv(node3(X,_,A,B), node3(X,_,C,D), R) :- !,
tree_equiv(A, C, E),
tree_equiv(B, D, F),
tree_make(E, F, X, R).
tree_equiv(N, node3(Y,_,C,D), R) :-
tree_equiv(N, C, E),
tree_equiv(N, D, F),
tree_make(E, F, Y, R).
/**
* tree_xor(P, Q, R):
* The predicate succeeds in R with the boolean difference of P and Q.
*/
:- private tree_diff/3.
tree_diff(P, Q, R) :-
tree_imply(P, Q, A),
tree_not(A, R).
/**
* tree_xor(P, Q, R):
* The predicate succeeds in R with the boolean xor of P and Q.
*/
:- private tree_xor/3.
tree_xor(P, Q, R) :-
tree_equiv(P, Q, A),
tree_not(A, R).
/**
* tree_ite(Q, R, P, S):
* The predicate succeeds in S with the boolean if-then-else of P, Q and R.
*/
% tree_ite(+Tree, +Tree, +Tree, -Tree)
tree_ite(Q, R, P, S) :-
tree_imply(P, Q, A),
tree_or(P, R, B),
tree_and(A, B, S).
/*****************************************************************/
/* Quantifiers */
/*****************************************************************/
/**
* tree_exists(Q, P, R):
* The predicate succeeds in R with existential removing the variable P from Q.
*/
% tree_exists(+Tree, +Index, -Tree)
tree_exists(zero, _, R) :- !,
R = zero.
tree_exists(one, _, R) :- !,
R = one.
tree_exists(node3(Y,_,A,B), X, R) :-
Y < X, !,
tree_exists(A, X, C),
tree_exists(B, X, D),
tree_make(C, D, Y, R).
tree_exists(node3(X,_,A,B), X, R) :- !,
tree_or(A, B, R).
tree_exists(N, _, N).
/**
* tree_one(Q, P, R):
* The predicate succeeds in R with substituting 1 for the variable P in Q.
*/
% tree_one(+Tree, +Index,-Tree)
tree_one(zero, _, R) :- !,
R = zero.
tree_one(one, _, R) :- !,
R = one.
tree_one(node3(Y,_,A,B), X, R) :-
Y < X, !,
tree_one(A, X, C),
tree_one(B, X, D),
tree_make(C, D, Y, R).
tree_one(node3(X,_,A,_), X, R) :- !,
R = A.
tree_one(N, _, N).
/**
* tree_zero(Q, P, R):
* The predicate succeeds in R with substituting 0 for the variable P in Q.
*/
% tree_zero(+Tree, +Index, -Tree)
tree_zero(zero, _, R) :- !,
R = zero.
tree_zero(one, _, R) :- !,
R = one.
tree_zero(node3(Y,_,A,B), X, R) :-
Y < X, !,
tree_zero(A, X, C),
tree_zero(B, X, D),
tree_make(C, D, Y, R).
tree_zero(node3(X,_,_,B), X, R) :- !,
R = B.
tree_zero(N, _, N).
/*****************************************************************/
/* Generate Index */
/*****************************************************************/
:- private cache_index/2.
:- thread_local cache_index/2.
/**
* gen_index(K, W):
* The predicate succeeds in N with a new index for the base B.
*/
% gen_index(+Key, -Value)
:- public gen_index/2.
W is H+1,
R = W.
R = 1.
/*****************************************************************/
/* Variable Lookup */
/*****************************************************************/
:- private cache_var/2.
:- thread_local cache_var/2.
/**
* var_map_new(X, Y):
* The predicate succeeds in Y with new mapping of X.
*/
% var_map_new(+Variable, -Index)
get_attr(X, tree, var_index(Y)), !,
R = Y.
gen_index(var_map, Y),
H = wrap(X),
put_attr(X, tree, var_index(Y)),
R = Y.
/**
* var_map_back(X, Y):
* The predicate succeeds in Y with the unmapping of X.
*/
% var_map_back(+Index, -Variable)
cache_var(X, H),
sys_melt_var(H, wrap(Y)).
/*****************************************************************/
/* Tree Make */
/*****************************************************************/
/**
* tree_make(A, B, X, R):
* The predicate succeeds in R with a new tree (X->A;B).
*/
% tree_make(+Tree, +Tree, +Index, -Tree)
:- private tree_make/4.
tree_make(A, A, _, R) :- !,
R = A.
tree_make(A, B, X, node3(X,[X|W],A,B)) :-
expr_vars(A, U),
expr_vars(B, V),
vars_union(U, V, W).
/**
* vars_union(U, V, W):
* The predicate succeeds in W with the union of the variables U and V.
*/
% vars_union(+List, +List, -List)
vars_union([], X, R) :- !,
R = X.
vars_union(X, [], R) :- !,
R = X.
vars_union([X|L], [Y|M], R) :-
X < Y, !,
vars_union(L, [Y|M], S),
R = [X|S].
vars_union([X|L], [X|M], R) :- !,
vars_union(L, M, S),
R = [X|S].
vars_union(L, [Y|M], [Y|S]) :-
vars_union(L, M, S).
/**
* expr_vars(T, L):
* The predicate succeeds in L with the variable
* indexes in the tree T.
*/
% expr_vars(+Tree, -List)
:- public expr_vars/2.
expr_vars(zero, R) :- !,
R = [].
expr_vars(one, R) :- !,
R = [].
expr_vars(node3(_,W,_,_), W).
/*****************************************************************/
/* Unify Hook */
/*****************************************************************/
/**
* attr_unify_hook(A, W):
* The predicate is called when a varable with attribute
* term A got the value W assigned.
*/
% attr_unify_hook(+Attr, +Term)
:- public attr_unify_hook/2.
/*****************************************************************/
/* Goals Hook */
/*****************************************************************/
/**
* attribute_goals(V, I, O):
* The predicate is called when the goal list I of
* the variable V is required. The list should end in O.
*/
% attribute_goals(+Variable, -List, +List)
:- public attribute_goals/3.
attribute_goals(_, R, R).

Kommentare