b_compile2(Exp,_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,WF) :- var(Exp), !,
add_internal_error_wf(b_compiler,'Variable Expression: ',Exp,unknown,WF),
NExpr=Exp, FullyKnown=false.
b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known
b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known
b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
b_compile2(boolean_false,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_false), FullyKnown=true.
b_compile2(boolean_true,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_true), FullyKnown=true.
b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
NExpr=value(Val),
(known_value(Val) -> % ground(Val) -> known_value ?
FullyKnown=true ; FullyKnown=false).
b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false).
b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
( ord_member(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl,
NExpr = lazy_lookup_pred(Id), FullyKnown=false
; compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown,WF)
).
b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
( ord_member(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl,
NExpr = lazy_lookup_expr(Id), FullyKnown=false
; compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown,WF)
).
b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
( FullyKnownA=true, FullyKnownB=true,
NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
-> (equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity)
; generate_equality(NExprA,NExprB,NExpr)
).
b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
( FullyKnownA=true, FullyKnownB=true,
NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
-> %print(computing_neq(VA,VB)),nl,
(kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth)
%, print(result(NExpr)),nl
; NExpr = not_equal(NExprA,NExprB)
).
b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never evaluated in b_compile1
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
(NExprB = b(value(X),BT,BI)
-> (X==[], always_well_defined(A) -> NExpr = falsity
; b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
% check if we can decide membership (e.g., 1:{1})
(quick_test_membership1(NExprA,X,PRes)
-> convert_pred_res(PRes,NExpr)
% TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below
% However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16})
% ; (get_texpr_id(NExprA,IDA),
% get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info),
% print(rename(IDB,IDA,Info)),nl,
% bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr)
; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El
-> get_texpr_type(NExprA,TA),
generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
; get_template_for_filter_cannot_match(NExprA,VA)
-> filter_cannot_match(X,VA,NewX,Filtered),
% (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl),
(Filtered=false -> NExpr = member(NExprA,NExprB)
; (NewX==[], always_well_defined(A)) -> NExpr = falsity
; custom_explicit_sets:singleton_set(NewX,El)
-> get_texpr_type(NExprA,TA),
%nl,print(create_equal(NExprA,FullyKnownA,El,FullyKnownB,NExprB)),nl,nl,
generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
; NExpr = member(NExprA, b(value(NewX),BT,BI))
)
% end fo filtering
; NExpr = member(NExprA,NExprB)
)
% , print('compile: '),print(NExpr),nl
)
; NExpr = member(NExprA,NExprB),
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
).
b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never evaluated in b_compile1
b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
(NExprB = b(value(X),_,_)
-> (X==[], always_well_defined(A) -> NExpr = truth
; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(quick_test_membership1(NExprA,X,PRes)
-> convert_neg_pred_res(PRes,NExpr)
; NExpr = not_member(NExprA,NExprB))
)
; NExpr = not_member(NExprA,NExprB),
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
).
b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
(is_lazy_extension_function_for_fun_app(Fun)
-> Eval1=false % extension function applications treated lazily
% TO DO: first evaluate B, if known then only evaluate relevant part of extension function
; Eval1=Eval),
b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF),
combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
%tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl,
(FullyKnown2=true, preferences:preference(find_abort_values,false),
% check if we have enough information to apply a partially specified function as a list
% e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers !
can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF)
-> NExpr = ResultExpr,
(FullyKnown12=true -> FullyKnown=true
; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true
; FullyKnown = false)
; %tools_printing:print_term_summary(cannot_apply_function(FullyKnown2,NExprA,NExprB)),nl,
%translate:print_bexpr(NExprA),nl, translate:print_bexpr(NExprB),nl,
NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12).
b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never automatically evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(is_falsity(NExprA) -> NExpr = falsity
;
% TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters
% also: try and detect unsatisfiable predicates beforehand
b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
(is_falsity(NExprB) -> NExpr = falsity
; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr)
; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr)
; NExpr = conjunct(NExprA,NExprB))
).
b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never automatically evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(is_truth(NExprA) -> NExpr = truth
; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
(is_truth(NExprB) -> NExpr = truth
; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr)
; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr)
; NExpr = disjunct(NExprA,NExprB))
).
b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never automatically evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(is_falsity(NExprA) -> NExpr = truth
; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), get_texpr_expr(NExprB,NExpr)
; NExpr = implication(NExprA,NExprB),
b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % B does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
% TO DO: add preference to force pre-computation everywhere and pass Eval instead of false to b_compile1; ditto for disjunction
).
b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never automatically evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
( get_negated_operator_expr(NExprA,NegatedA) -> NExpr = NegatedA
; NExpr = negation(NExprA)
).
b_compile2(if_then_else(A,B,C),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(is_falsity(NExprA) -> b_compile1(C,Parameters,LS,S,NExprC,Eval,FullyKnown,WF), get_texpr_expr(NExprC,NExpr)
; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), get_texpr_expr(NExprB,NExpr)
; NExpr = if_then_else(NExprA,NExprB,NExprC), FullyKnown=false,
b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % set Eval to false as we do not know if B will be needed
b_compile1(C,Parameters,LS,S,NExprC,false,_,WF) % ditto for C
).
b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
FullyKnown=false, % predicates never automatically evaluated in b_compile1
get_texpr_ids(ForallPara,AtomicIds),
add_parameters(Parameters,AtomicIds,NParameters),
b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF),
(is_falsity(NA) -> NExpr = truth
; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF),
(is_truth(NB) -> NExpr = truth
; NExpr = forall(ForallPara,NA,NB)
% TO DO ??: if we have an equality -> replace Body by value and remove quantifier
%,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl
)
).
b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
% First: we can try compute even if value not fully known !, we just need record field list
(get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true
; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA).
b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
%NExpr = couple(NExprA,NExprB),
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
(FullyKnown \== true, % evaluation will already combine the result
NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_)
-> NExpr = value((VA,VB))
; NExpr = couple(NExprA,NExprB)).
b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
(FullyKnown \= true, NExprA=b(value(VA),BT,BI),
NExprB=b(value(VB),_,_), nonvar(VB),
custom_explicit_sets:singleton_set(VB,VBX)
-> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl,
NExpr = image(b(value(NewVA),BT,BI),NExprB)
% TO DO: add case where VB==[] or VA==[] are the empty set
; NExpr = image(NExprA,NExprB)
). %, print('compile image: '),translate:print_bexpr(NExpr),nl.
b_compile2(composition(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
NExpr = composition(NExprA,NExprB),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
(FullyKnown=false, Eval=eval, performance_monitoring_on,
( FullyKnown1=true, NExprB=b(value(_),_,Info), large_known_value(NExprA,2)
-> true %translate:nested_print_bexpr(NExprB),nl
; FullyKnown2=true, NExprA=b(value(_),_,Info), large_known_value(NExprB,2)
-> true %translate:nested_print_bexpr(NExprA),nl
)
-> perfmessage(b_compiler,'Cannot compile relational composition (try lift it out of quantification)',Info)
; true).
b_compile2(assertion_expression(A,Msg,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
(is_truth(NExprA) -> % the ASSERT EXPR is redundant
%print(removed_assert),nl, translate:print_bexpr(B),nl,
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF),
get_texpr_expr(NExprB,NExpr)
; b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
FullyKnown=false, % we cannot get rid of WD condition
NExpr = assertion_expression(NExprA,Msg,NExprB)
).
b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
(FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known
-> FullyKnown = true, NExpr = value(Domain)
; FullyKnown = FullyKnown1, NExpr = domain(NExprA)).
b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
(FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known
-> FullyKnown = true, NExpr = value(Range)
; FullyKnown = FullyKnown1, NExpr = range(NExprA)).
b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false,
maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List),
b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF).
b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !,
FullyKnown = false,
b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF).
b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
% TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr
!,
def_get_texpr_id(Operation,op(OperationName)),
FullyKnown = false,
b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
TopLevel=false,
b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel),
bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2),
get_texpr_ids(OpFormalParameters,OpIds),
add_parameters(Parameters,OpIds,InnerParas),
b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine
% Note: global state S should be valid for all machines in currently loaded specification
get_texpr_ids(OpCallResults,OpRIds),
add_parameters(Parameters,OpRIds,LocalKnownParas),
simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals),
split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas,
FreshOpParas,FreshCallVals,
ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras
% print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl,
(FreshOpParas=[] -> get_texpr_expr(NBody,Let1)
; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1),
Let1 = let(FreshOpParas,Equality1,NBody)),
(ClashOpParas = []
-> InlinedOpCall = Let1
; %nl,print(clash(ClashOpParas)),nl,
maplist(create_fresh_id,ClashOpParas,FreshCopy),
create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids
create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids
get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)],
Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])),
InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo]))
).
b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
functor(Expr,BOP,2),
binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation
arg(1,Expr,A),
FullyKnown=false, % predicates never evaluated in b_compile1
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
arg(2,Expr,B),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
(eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result)
-> NExpr = Result
; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB)
).
b_compile2(external_function_call(ExtFun,Args),_Parameters,LS,_S,NExpr,_Eval,FullyKnown,_WF) :-
expects_unevaluated_args(ExtFun),
memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS), % this is an optimize call
!,
debug_format(9,'Not compiling external function call to ~w~n',[ExtFun]),
NExpr=external_function_call(ExtFun,Args),
FullyKnown=false.
b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
functor(Expr,BOP,2),
kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation
arg(1,Expr,A),
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown),
arg(2,Expr,B),
b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB).
b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
functor(Expr,UOP,1),
kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation
arg(1,Expr,A),
b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF),
functor(NExpr,UOP,1), arg(1,NExpr,NExprA).
b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE
%hit_profiler:add_profile_hit(Expr),
syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
get_texpr_ids(Names,Ids),
add_parameters(Parameters,Ids,NParameters),
b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF).