120 Lines

11 Predicates

Imported Modules: lists bsyntaxtree kodkod_tools

1 Exports

3 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: get_texpr_set_type/2 Module: bsyntaxtree Name: replace_ids_by_exprs/4 Module: bsyntaxtree	Name: apply_rewriting_rules/2

Imports

Exports

Name: module_info/2

Module: module_information

Name: get_texpr_set_type/2

Module: bsyntaxtree

Name: replace_ids_by_exprs/4

Module: bsyntaxtree

Name: apply_rewriting_rules/2

Predicates

Predicates:

apply_rewriting_rules/2

apply_rewriting_rules_post/3

apply_rewriting_rules_pre/3

convert_element_to_pair/3

convert_elements_to_pairs/3

create_integer_with_analysis/2

create_kk_tpred/2

element_analysis/2

kodkod_rewrite_membership/4

kodkod_rewrite_post/3

kodkod_rewrite_pre/3

apply_rewriting_rules/2

apply_rewriting_rules(TExpr,NTExpr) :-
    remove_bt(TExpr,Expr,NExpr,NTExpr),
    get_texpr_info(TExpr,Info),
    apply_rewriting_rules_pre(Expr,Info,IExpr),
    syntaxtransformation(IExpr,Subs,_,NSubs,Expr1),
    maplist(apply_rewriting_rules,Subs,NSubs),
    apply_rewriting_rules_post(Expr1,Info,NExpr).

Calls:

Name: apply_rewriting_rules_post/3	Module: kodkod_rewrite
Name: maplist/3	Module: foo_error
Name: syntaxtransformation/5	Module: foo_error
Name: apply_rewriting_rules_pre/3	Module: kodkod_rewrite
Name: get_texpr_info/2	Module: foo_error
Name: remove_bt/4	Module: foo_error

apply_rewriting_rules_post/3

apply_rewriting_rules_post(Expr,Info,NExpr) :-
kodkod_rewrite_post(Expr,Info,Expr1),!,
apply_rewriting_rules_post(Expr1,Info,NExpr).

apply_rewriting_rules_post(Expr,_,Expr).

Calls:

Name: RECURSIVE_CALL/3	Module: kodkod_rewrite
Name: !
Name: kodkod_rewrite_post/3	Module: kodkod_rewrite

Called:

Name: apply_rewriting_rules/2

Module: kodkod_rewrite

apply_rewriting_rules_pre/3

apply_rewriting_rules_pre(Expr,Info,NExpr) :-
kodkod_rewrite_pre(Expr,Info,Expr1),!,
apply_rewriting_rules_pre(Expr1,Info,NExpr).

apply_rewriting_rules_pre(Expr,_,Expr).

Calls:

Name: RECURSIVE_CALL/3	Module: kodkod_rewrite
Name: !
Name: kodkod_rewrite_pre/3	Module: kodkod_rewrite

Called:

Name: apply_rewriting_rules/2

Module: kodkod_rewrite

convert_element_to_pair/3

convert_element_to_pair(Elem,Index,Pair) :-
    Range = irange(Index,Index),
    create_texpr(integer(Index),integer,[analysis([interval:Range])],TIndex),
    get_texpr_type(Elem,Type),
    get_texpr_info(Elem,EInfo),
    findall(right(Scope):Info,
    ( memberchk(analysis(AInfos),EInfo),member(Scope:Info,AInfos)),
    RInfos),
    create_texpr(couple(TIndex,Elem),couple(integer,Type),[analysis([left(interval):Range|RInfos])],Pair).

Calls:

Name: create_texpr/4	Module: foo_error
Name: findall/3
Name: get_texpr_info/2	Module: foo_error
Name: get_texpr_type/2	Module: foo_error
Name: =/2

Called:

Name: convert_elements_to_pairs/3

Module: kodkod_rewrite

convert_elements_to_pairs/3

convert_elements_to_pairs([],_,[]).

convert_elements_to_pairs([Elem|Erest],Index,[Pair|Prest]) :-
    convert_element_to_pair(Elem,Index,Pair),
    I2 is Index + 1,
    convert_elements_to_pairs(Erest,I2,Prest).

Calls:

Name: RECURSIVE_CALL/3	Module: kodkod_rewrite
Name: is/2
Name: convert_element_to_pair/3	Module: kodkod_rewrite

Called:

Name: kodkod_rewrite_post/3

Module: kodkod_rewrite

create_integer_with_analysis/2

create_integer_with_analysis(I,Expr) :-
create_texpr(integer(I),integer,[analysis([interval:irange(I,I)])],Expr).

Calls:

Name: create_texpr/4

Module: foo_error

Called:

Name: kodkod_rewrite_membership/4

Module: kodkod_rewrite

create_kk_tpred/2

create_kk_tpred(Pred,TPred) :-
create_texpr(Pred,pred,[kodkod],TPred).

Calls:

Name: create_texpr/4

Module: foo_error

Called:

Name: kodkod_rewrite_membership/4	Module: kodkod_rewrite
Name: kodkod_rewrite_pre/3	Module: kodkod_rewrite

element_analysis/2

element_analysis(SetInfo,[analysis(MemberInfo)]) :-
    findall( S:R,
    ( member(analysis(Analysis), SetInfo),
    member(elem(S):R,Analysis)),
    MemberInfo).

Calls:

Name: findall/3

Called:

Name: kodkod_rewrite_post/3	Module: kodkod_rewrite
Name: kodkod_rewrite_pre/3	Module: kodkod_rewrite

kodkod_rewrite_membership/4

kodkod_rewrite_membership(pow_subset(Set),Elem,_,subset(Elem,Set)).

kodkod_rewrite_membership(fin_subset(Set),Elem,_,subset(Elem,Set)).

kodkod_rewrite_membership(relations(A,B),Elem,_,subset(Elem,Cartesian)) :-
    create_kk_tpred(cartesian_product(A,B),Cartesian).

kodkod_rewrite_membership(pow1_subset(Set),Elem,ElemInfo,conjunct(Subset,Exists)) :-
    get_texpr_set_type(Set,Type),
    create_texpr(identifier('___elem'),Type,[kodkod|ElemInfo],Id),
    create_kk_tpred(subset(Elem,Set),Subset),
    create_kk_tpred(exists([Id],Member),Exists),
    create_kk_tpred(member(Id,Set),Member).

kodkod_rewrite_membership(fin1_subset(Set),Elem,Info,Pred) :-
    kodkod_rewrite_membership(pow1_subset(Set),Elem,Info,Pred).

kodkod_rewrite_membership(interval(A,B),Elem,_,conjunct(Lower,Upper)) :-
    create_kk_tpred(less_equal(A,Elem),Lower),
    create_kk_tpred(less_equal(Elem,B),Upper).

kodkod_rewrite_membership(integer_set('NATURAL'),Elem,_,less_equal(Zero,Elem)) :-
    create_integer_with_analysis(0,Zero).

kodkod_rewrite_membership(integer_set('NATURAL1'),Elem,_,less_equal(One,Elem)) :-
    create_integer_with_analysis(1,One).

Calls:

Name: create_integer_with_analysis/2	Module: kodkod_rewrite
Name: create_kk_tpred/2	Module: kodkod_rewrite
Name: RECURSIVE_CALL/4	Module: kodkod_rewrite
Name: create_texpr/4	Module: foo_error
Name: get_texpr_set_type/2	Module: bsyntaxtree

Called:

Name: kodkod_rewrite_pre/3

Module: kodkod_rewrite

kodkod_rewrite_post/3

kodkod_rewrite_post(interval(A,B),Info,comprehension_set([TmpId],Predicate)) :- !,
    element_analysis(Info,ElemInfo),
    unique_identifier(TId),
    create_texpr(identifier(TId),integer,ElemInfo,TmpId),
    create_texpr(less_equal(A,TmpId),pred,[],Left),
    create_texpr(less_equal(TmpId,B),pred,[],Right),
    conjunct_predicates([Left,Right],Predicate).

kodkod_rewrite_post(sequence_extension(Elems),_Info,set_extension(Pairs)) :- !,
    convert_elements_to_pairs(Elems,1,Pairs).

kodkod_rewrite_post(general_sum([TId],Pred,Expr),_Info,general_sum([TId],NPred,Expr)) :-
    get_texpr_id(TId,Id), get_texpr_id(TElem,Id),
    extract_finite_integer_range(TId,[],IRange),
    \+ get_texpr_expr(Pred,member(TElem,_TSet)),!,
    write('rewritten\n'),
    create_texpr(comprehension_set([TId],Pred),set(integer),[analysis([elem(interval):IRange])],
    TCompSet),
    create_texpr(member(TId,TCompSet),pred,[],NPred).

Calls:

Name: create_texpr/4	Module: foo_error
Name: write/1
Name: !
Name: get_texpr_expr/2	Module: foo_error
Name: not/1
Name: extract_finite_integer_range/3	Module: foo_error
Name: get_texpr_id/2	Module: foo_error
Name: convert_elements_to_pairs/3	Module: kodkod_rewrite
Name: conjunct_predicates/2	Module: foo_error
Name: unique_identifier/1	Module: foo_error
Name: element_analysis/2	Module: kodkod_rewrite

Called:

Name: apply_rewriting_rules_post/3

Module: kodkod_rewrite

kodkod_rewrite_pre/3

kodkod_rewrite_pre(let_expression(Ids,Exprs,Body),_,Res) :- !, % expand LET expression
    replace_ids_by_exprs(Body,Ids,Exprs,b(NewBody,_,I2)),
    (kodkod_rewrite_pre(NewBody,I2,Res2) -> Res=Res2; Res = NewBody).

kodkod_rewrite_pre(let_predicate(Ids,Exprs,Body),_,Res) :- !, % expand LET predicate
    replace_ids_by_exprs(Body,Ids,Exprs,b(NewBody,_,I2)),
    (kodkod_rewrite_pre(NewBody,I2,Res2) -> Res=Res2; Res = NewBody).

kodkod_rewrite_pre(not_equal(A,B),_,negation(Equal)) :- !,
    create_kk_tpred(equal(A,B),Equal).

kodkod_rewrite_pre(member(Elem,Powset),_,Result) :-
    get_texpr_expr(Powset,PExpr),
    get_texpr_info(Elem,ElemInfo),
    kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Result),
    !.

kodkod_rewrite_pre(subset(Subset,Powset),_,forall([Elem],TPre,TCond)) :-
    get_texpr_info(Subset,Info),
    get_texpr_set_type(Subset,ElemType),
    unique_identifier(TId),
    element_analysis(Info,ElemInfo),
    create_texpr(identifier(TId),ElemType,ElemInfo,Elem),
    get_texpr_expr(Powset,PExpr),
    kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Cond),!,
    create_texpr(member(Elem,Subset),pred,[],TPre),
    create_texpr(Cond,pred,[],TCond).

kodkod_rewrite_pre(size(Seq),_,card(Seq)) :- !.

Calls:

Name: !
Name: create_texpr/4	Module: foo_error
Name: kodkod_rewrite_membership/4	Module: kodkod_rewrite
Name: get_texpr_expr/2	Module: foo_error
Name: element_analysis/2	Module: kodkod_rewrite
Name: unique_identifier/1	Module: foo_error
Name: get_texpr_set_type/2	Module: bsyntaxtree
Name: get_texpr_info/2	Module: foo_error
Name: create_kk_tpred/2	Module: kodkod_rewrite
Name: =/2
Name: RECURSIVE_CALL/3	Module: kodkod_rewrite
Name: ->/3
Name: replace_ids_by_exprs/4	Module: bsyntaxtree

Called:

Name: apply_rewriting_rules_pre/3

Module: kodkod_rewrite

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod_rewrite.pl')])

kodkod_rewrite

prob_prolog/src/kodkod/kodkod_rewrite.pl

Modules

Predicates of kodkod_rewrite

Module Information

120 Lines

11 Predicates

Imported Modules: lists bsyntaxtree kodkod_tools

1 Exports

3 specified Imports

Predicates:

apply_rewriting_rules/2

apply_rewriting_rules_post/3

apply_rewriting_rules_pre/3

convert_element_to_pair/3

convert_elements_to_pairs/3

create_integer_with_analysis/2

create_kk_tpred/2

element_analysis/2

kodkod_rewrite_membership/4

kodkod_rewrite_post/3

kodkod_rewrite_pre/3

Determinacy Checker: