b_interpreter_components

apply_binding_to_substitution([],_,_,[]).

apply_binding_to_substitution([TV/TE|T],Var,Expr,[TV/TE2|NT]) :-
    \+ occurs_in_expr(TV,Expr), % otherwise we get a cyclic substitution --> fail
    replace_id_by_expr(TE,Var,Expr,TE2),
    apply_binding_to_substitution(T,Var,Expr,NT).

apply_subst([],X,X).

apply_subst([Var/Expr|T],E,NewE) :-
    (replace_id_by_expr(E,Var,Expr,E2) % replace identifier Var by expression Expr
    -> %apply_to_tail(T,Var,Expr,NT), % apply binding to tail of substitution
    apply_subst(T,E2,NewE)
    ; add_internal_error('Call failed: ',apply_subst([Var/Expr|T],E,NewE)),NewE=E).

assert_det_solution_for_constant(Var,Val) :-
    (value_too_large(Val) -> PVal = '$TOO_LARGE' ,debug_println(4,not_storing(Var))
    ; pack_value(Val,PVal)
    %,translate:translate_bvalue_with_limit(Val,200,VS),format(' STORING ---> ~w = ~w~n',[Var,VS])
    ),
    assertz(det_solution_for_constant_packed(Var,PVal)).

assert_skipped_failed_conjunct(ComponentNr,BE) :- assert_skipped_unsat_conjunct,
    assertz(unsat_conjunct_inside_component(ComponentNr,BE,false,'')),
    (preferences:get_preference(provide_trace_information,false) -> true
    ; add_message(b_interpreter_components,' *** INCONSISTENCY DETECTED, SKIPPING COMPONENT NR: ',ComponentNr, BE),
    (debug_mode(on) -> print_bexpr_with_limit(BE,500) ; print_bexpr_with_limit(BE,150)), nl
).

assert_skipped_unknown_conjunct :-
    (skipped_unsat_conjunct(_) -> true ; assertz(skipped_unsat_conjunct(unknown))).

assert_skipped_unknown_conjunct(ComponentNr,BE,Reason) :- assert_skipped_unknown_conjunct,
    assertz(unsat_conjunct_inside_component(ComponentNr,BE,unknown,Reason)),
    ((Reason=abort_error; Reason=well_definedness_error)
    -> assert_unsat_component_abort_error(ComponentNr)
    ; true),
    (preferences:get_preference(provide_trace_information,false) -> true
    ; get_reason_msg(Reason,MSG),format(' *** Skipping predicate due to ~w:',[MSG]),
    write(' '),print_bexpr_with_limit(BE,150),nl,
    format('~n *** Predicate is unknown~n *** COMPONENT NUMBER: ~w~n',[ComponentNr])
).

assert_skipped_unsat_conjunct :-
    (skipped_unsat_conjunct(false) -> true
    ; retractall(skipped_unsat_conjunct(_)), assertz(skipped_unsat_conjunct(false))).

assert_unknown(ComponentNr,BE,Reason,Ai,Ao) :- % print(assert_unknown(ComponentNr,Reason)),nl,
    assert_skipped_unknown_conjunct(ComponentNr,BE,Reason),Ai=Ao.

assert_unsat_component_abort_error(X) :- \+ unsat_component_abort_error(X),
    assertz(unsat_component_abort_error(X)),
    debug_println(19,unsat_component_abort_error(X)).

augment_ids([],[]).

augment_ids([ID|T],[b(identifier(ID),_,_)|TT]) :- augment_ids(T,TT).

b_trace_test_components(Properties,ConstantsState,TypedVals) :-
    %format('b_trace_test_components(~w,~w,~w)',[Properties,ConstantsState,TypedVals]),
    b_trace_test_components(Properties,ConstantsState,TypedVals,all).

b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables) :-
    b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,[]).

b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts) :-
    b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,no_wf_available).

b_trace_test_components2([],_ConstantsState,TypedVals,_,_,Nr,ResWF,OuterWF) :-
    (TypedVals=[]
    -> print_trace_message(finished_processing_component_predicates),
    ResWF=[]
    ; print_trace_message_with_typed_vals('Enumerating Identifiers without constraints: ',TypedVals),
    init_wait_flags(WF0,[b_tighter_enumerate_values]),
    copy_wait_flag_call_stack_info(OuterWF,WF0,WF),
    b_tighter_enumerate_all_values(TypedVals,WF), ResWF=[wf_comp(WF,Nr)]).

b_trace_test_components2([component(Pred,ComponentVars)|T],ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,
    Nr,ResWF,OuterWF) :-
    N1 is Nr+1,
    ( RelevantVariables\=all, ComponentVars\= all,
    lists_are_disjoint(RelevantVariables,ComponentVars)
    -> print_trace_message(skipping_irrelevant_component(Nr,ComponentVars)),
    b_trace_test_components2(T,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,N1,ResWF,OuterWF)
    ; %% print(checking_component_properties(Nr,ComponentVars)),nl,
    %% print(component(Nr)),nl, translate:nested_print_bexpr_as_classicalb(Pred),debug:nl_time,
    ResWF = [wf_comp(WF,Nr)|TWF],
    init_wait_flags(WF0,[wf_comp(Nr)]),
    copy_wait_flag_call_stack_info(OuterWF,WF0,WF),
    (preferences:preference(use_chr_solver,true) -> attach_chr_integer_inequality_to_wf_store(WF) ; true),
    (ComponentVars=all -> InTypedVals=TypedVals, OutTypedVals=[], ProjectedState=ConstantsState
    ; project_typed_vals(TypedVals,ComponentVars,InTypedVals,OutTypedVals),
    project_state(ConstantsState,ComponentVars,ProjectedState) % relevant, e.g., for exists which may wait on state becoming ground
    ),
    observe_state(InTypedVals,WF,Nr),
    reset_tracetest_for_component,
    predicate_level_optimizations(Pred,OPred),
    %%nl,nl,print(component(Nr,ComponentVars,ProjectedState)),nl,nl,translate:print_bexpr(Pred),nl,nl,
    %%start_ms_timer(T1),
    b_tracetest_boolean_expression(OPred,[],ProjectedState,WF,Nr),
    % Skipping can only occur in this call above, not in enumeration phase
    %% stop_ms_timer_with_debug_msg(T1,b_tracetest_boolean_expression(Nr)),
    %print(done_comp(Nr,WF,ComponentVars)),nl,
    (skipped_unsat_conjunct(FalseOrUnknown)
    -> store_unsat_component_nr(Nr,FalseOrUnknown), % can be unknown due to an enumeration warning, cf. test 1390
    %print('UNSAT: '),translate:nested_print_bexpr(Pred),nl,nl,
    allow_skipping_over_components % check if we allow skipping over unsat components to
    % maybe find as many values for constants as possible (partial setup_constants),...
    % Note: in Disprover mode or solve_predicate (REPL) we can stop and fail straightaway
    ; %print_bt_message(setup_enumerating_constants(Nr)), %%(TypedVals)),
    b_tighter_enumerate_values(InTypedVals,DoNotEnumVars,WF),
    (preferences:get_preference(disprover_mode,false) -> true
    ; ground_wait_flag0(WF) % ensure that we give each component the chance to run WF0 inconsistency checks
    %, print(finished_wf0_grounding_in_disprover_mode(Nr)),nl
    )
    ),
    % we could ground waitflag 1 (deterministic computations) ?
    b_trace_test_components2(T,ConstantsState,OutTypedVals,RelevantVariables,DoNotEnumVars,N1,TWF,OuterWF)
).

b_trace_test_components_wf(Properties,ConstantsState,TypedVals,WF) :-
    b_trace_test_components_wf(Properties,ConstantsState,TypedVals,all,[],WF).

b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,OuterWF) :-
    % we now treat all TypedVals as local variables:
    % ensure that we count them in predicate_components/predicate_identifiers
    % (in case they clash with global identifiers)!
    %start_ms_timer(T0),
    maplist(get_typedval_id,TypedVals,LocalVars),
    extract_do_not_enum_ids_from_predicate(Properties,DoNotEnumVars),
    (preferences:get_preference(partition_predicates,true)
    -> predicate_components_in_scope(Properties,LocalVars,Components),
    length(Components,Len), print_trace_message(nr_of_components(Len))
    ; predicate_identifiers_in_scope(Properties,LocalVars,PropVars),
    Components = [component(Properties,PropVars)], Len=1
    ),
    retractall(nr_of_components(_)),assertz(nr_of_components(Len)),
    reset_observe_state,
    %stop_ms_timer_with_debug_msg(T0,b_trace_test_components_preprocessing),
    b_trace_test_components2(Components,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,1,WFList,OuterWF),
    get_unsat_component(WFList,Components,UnsatConjuncts).

b_tracetest_boolean_expression(BE,LS,S,WF,ComponentNr) :- %print(catch(ComponentNr)),nl,
    empty_avl(Ai),
    catch_enumeration_warning_exceptions_and_wd_failures(
    b_tracetest_boolean_expression1(BE,LS,S,WF,ComponentNr,Ai,_Ao),
    % this should not backtrack (without WF0 set); otherwise we may get problems with error blocks nesting
    assert_skipped_unknown_conjunct(ComponentNr,BE,enumeration_warning),
    true, % true: add exceptions as event errors
    assert_skipped_unknown_conjunct(ComponentNr,BE,well_definedness_error), % for WD error
    component(ComponentNr)). % Source argument for debugging

b_tracetest_boolean_expression1(b(Expr,_,Infos),LS,S,WF,ComponentNr,Ai,Ao) :-
    b_tracetest_boolean_expression2(Expr,Infos,LS,S,WF,ComponentNr,Ai,Ao).

b_tracetest_boolean_expression2(Conjunct,Info,LocalState,State,WF,ComponentNr,Ai,Ao) :-
    is_a_conjunct_or_neg_disj(b(Conjunct,pred,Info),LHS,RHS),
    % also detects: not(A or B) <=> not(A) & not(B) and not(A=>B) <=> A & not(B)
    % \+(Info = [try_smt|_]),
    !,
    %% print('check lhs of conjunct: '), translate:print_bexpr(LHS),nl,
    b_tracetest_boolean_expression1(LHS,LocalState,State,WF,ComponentNr,Ai,Aii),
    %% print('check rhs of conjunct: '), translate:print_bexpr(RHS),nl,
    b_tracetest_boolean_expression1(RHS,LocalState,State,WF,ComponentNr,Aii,Ao).

b_tracetest_boolean_expression2(BE,Infos,LS,S,WF,ComponentNr,Ai,Ao) :-
    (get_preference(provide_trace_information,true)
    -> format('~n ====> (~w) ',[ComponentNr]),
    print_bexpr_with_limit(b(BE,pred,Infos),250),nl
    ; true),
    if(safe_b_test_boolean_expression(ComponentNr,b(BE,pred,Infos),LS,S,WF,Ai,Ao),
    true,
    (assert_skipped_failed_conjunct(ComponentNr,b(BE,pred,Infos)),
    Ai=Ao)).

compose_with_subst(Subst,Var,Expr,[Var/NewExpr|ModSubst]) :-
    apply_subst(Subst,Expr,NewExpr),
    \+ occurs_in_expr(Var,NewExpr), % otherwise cyclic
    apply_binding_to_substitution(Subst,Var,NewExpr,ModSubst).

conjunct_components(C,Parameters,Res,Simplify,NrComponents) :-
    conjunct_components2(C,Parameters,List,Simplify,0,NrComponents),
    conjunct_predicates_with_pos_info(List,Res).

conjunct_components2([],_Parameters,[],_,Nr,Nr). % :- (Parameters=[] -> true ; print(unused_existential_var(Parameters)),nl).

conjunct_components2([component(Pred,ComponentVars)|T],Parameters,Res,Simplify,InNr,OutNr) :-
    augment_ids(ComponentVars,CV), % translate atomic id names into b(identifier(...
    tools:list_intersection(CV,Parameters,ExistParas), % TO DO: use ordsets
    (Simplify=true
    -> create_and_simplify_exists(ExistParas,Pred,EP) % no use in recursively calling construct_optimized_exists
    ; Simplify= no_cleanup_and_simplify
    -> create_exists(ExistParas,Pred,EP0), % avoid loops when called from ast_cleanup
    get_texpr_info(EP0,AllInfos0),
    (nonmember(nodeid(_),AllInfos0),ExistParas=[Par1|_]
    -> get_texpr_info(Par1,AllInfos1),extract_pos_infos(AllInfos1,PIs) % try and get position from ids
    ; PIs=[]), % we already have a position info
    add_texpr_infos(EP0,[partitioned_exists|PIs],EP) % add ,removed_typing ??
    ; create_unsimplified_exists(ExistParas,Pred,EP)
    ),
    (EP=b(truth,pred,[]) % or should we allow _ for Info field ??
    -> Res=TRes
    ; Res=[EP|TRes]),
    In1 is InNr+1,
    conjunct_components2(T,Parameters,TRes,Simplify,In1,OutNr).

construct_optimized_exists(Parameters,Body,Pred) :-
    construct_optimized_exists(Parameters,Body,Pred,true,_).

construct_optimized_exists(Parameters,Body,Pred,Simplify) :-
    construct_optimized_exists(Parameters,Body,Pred,Simplify,_).

construct_optimized_exists(Parameters,Body,Pred,Simplify,NrComponents) :-
    % we can actually do more: first project out all conjuncts which do not have any variables in common with Parameters
    % #x.(P(x) & Q) <=> #x.(P(x)) & Q
    % we can also use a stronger version of predicate components #(x,y).( P(x,v) & Q(v,y)) <=> #(x).P(x,v) & #(y).Q(v,y)
    get_texpr_ids(Parameters,PIDs),
    %print(constructing_optimized_exists(PIDs)),nl,
    LocalVars = PIDs,
    predicate_components_with_restriction(Body,LocalVars,PIDs,Components), % we focus partition decision on PIDs, not on all identifiers
    %length(Components,Len), print(nr_of_components_for_exists(Len,Components)),nl,
    conjunct_components(Components,Parameters,Pred,Simplify,NrComponents).

create_and_simplify_exists(Paras,Pred,ResultingPred) :-
    extract_equalities_in_quantifier(Paras,Pred,NewParas,NewPred),
    create_and_simplify_exists2(NewParas,NewPred,ResultingPred).

create_and_simplify_exists2([],Pred,R) :- !,R=Pred.

create_and_simplify_exists2(Parameters,Body,Res) :- create_unsimplified_exists(Parameters,Body,Res).

create_unsimplified_exists(Parameters,Body,Res) :-
    maplist(mark_generated_exists,Parameters,Para2), % mark that this is an artificially constructed; we now mark the exists
    create_exists(Para2,Body,Res1),
    add_texpr_info_if_new(Res1,removed_typing,Res2), % unconditionally add this info, avoid generating warnings in exists_body_warning, see test 625
    % and avoid useless_let_message
    % previously removed_typing was only added for disjuncts or implications
    clean_up_pred(Res2,[],Res). % also computes used_ids,

det_solution_for_constant(Var,Val) :-
    if(det_solution_for_constant_packed(Var,PVal),
    unpack_det_sol(Var,PVal,Val),
    (get_specification_description(properties,PROPS),
    ajoin([PROPS, ' are *not* true and no value was found (deterministically) for the following CONSTANT: '], Msg),
    add_message(det_value_not_found_for_constant,Msg,Var),
    fail)
).

det_solution_for_constant_was_stored :- (det_solution_for_constant_was_stored(_) -> true).

det_solution_for_constant_was_stored(Var) :- det_solution_for_constant_packed(Var,_).

extract_equalities2(b(conjunct(A,B),pred,Info),Ids,RemIds,Res) --> !,
    {Res=b(conjunct(PA,PB),pred,Info)},
    extract_equalities2(A, Ids,RemIds1,PA),
    extract_equalities2(B,RemIds1,RemIds,PB).

extract_equalities2(TEqual,Ids,RemIds,NewPred,InSubst,OutSubst) :-
    is_equality(TEqual,ID,E),
    % TODO: we could try and split equalities if possible; usually this is done by ast_cleanup though?
    %(bsyntaxtree:split_equality(TEqual,A,B) -> nl,print('COULD BE SPLIT: '),translate:print_bexpr(TEqual),nl ; true),
    same_id_is_member(ID,Ids,SID,RemIds),
    %\+ occurs_in_expr(SID,E), % not cyclic; we check it again after applyng InSubst to E below
    \+ in_subst_dom(SID,InSubst), % ensure we don't already have an equation for the same ID
    compose_with_subst(InSubst,SID,E,OutSubst), % we can compose with existing substitution without occurs-check problem
    always_well_defined_or_disprover_mode(E), % otherwise we may move evaluation of E forward !
    !,
    NewPred=b(truth,pred,[]).

extract_equalities2(X,Ids,Ids,X) --> [].

extract_equalities_in_quantifier(Parameters,Pred, ReducedParas,OutPred) :-
    extract_equalities2(Pred,Parameters,ReducedParas,NewPred,[],Subst),
    %sort(Subst,SortedSubst),
    %print(extracted(Subst)),nl,
    apply_subst(Subst,NewPred,OutPred).

get_binding_value(bind(Id,Value),Id,Value).

get_binding_value(typedval(Value,_Type,Id,_Trigger),Id,Value).

get_det_solution_for_constant_value_kind(Var,ValKind) :-
    det_solution_for_constant_packed(Var,PVal),
    (PVal = '$TOO_LARGE' -> ValKind='LARGE-VALUE'
    ; unpack_value(PVal,Val),
    (translate_bvalue_kind(Val,K) -> ValKind=K ; ValKind='UNKNOWN-VALUE')
).

get_reason_msg(enumeration_warning,R) :- !, R='ENUMERATION WARNING'.

get_reason_msg(M,M).

get_typedval_id(typedval(_Val,_Type,ID,_),ID).

get_unsat_component(_,Components,UnsatConjuncts) :-
    unsat_component_exists, !,
    debug_println(9,unsatisfiable_predicate),
    unsat_component(UnsatComponentNr,false),!,
    nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)).

get_unsat_component(WFList,Components,UnsatConjuncts) :-
    get_unsat_component_aux(WFList,Components,UnsatConjuncts).

get_unsat_component_aux(WFList,Components,UnsatConjuncts) :-
    print_trace_message(grounding_wait_flags), % Note: for unknown components we continue grounding
    l_ground_wait_flags(WFList),
    (unsat_component(UnsatComponentNr,Status)
    -> debug_println(19,unsat_component(UnsatComponentNr,Status)), UnsatConjuncts \== [],
    nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_))
    ; UnsatConjuncts=[]).

get_unsat_component_aux(_,Components,UnsatConjuncts) :-
    unsat_component(UnsatComponentNr,_),!,
    nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)).

in_subst_dom(X,[I/_|T]) :- (X=I -> true ; in_subst_dom(X,T)).

l_ground_wait_flags(WF) :-
    l_ground_wait_flags(WF,WFE,Result),
    (Result=false
    -> (!,fail) % Cut: to prevent backtracking to find other solutions for earlier components !
    % Assumption: each component is independent and finding other solution for earlier component would again lead to failure in last component checked by l_ground_wait_flags/2
    ; grd_ef(WFE)).

l_ground_wait_flags([],_,true).

l_ground_wait_flags([wf_comp(_,ComponentNr)|TWF],WFE,SatResult) :-
    unsat_component(ComponentNr,_),!, % We now longer try and ground unknown components
    l_ground_wait_flags(TWF,WFE,SatResult).

l_ground_wait_flags([wf_comp(WF,ComponentNr)|TWF],WFE,SatResult) :-
    (debug_mode(off) -> true ; print(grounding_component(ComponentNr)),nl, start_ms_timer(Timer)),
    % print_bt_message(grounding_component(ComponentNr)), portray_waitflags(WF),nl,
    % maybe we should set up new error scope ? <--- TO DO
    if(ground_constraintprop_wait_flags(WF),
    ((pending_abort_error(WF) -> assert_unsat_component_abort_error(ComponentNr) ; true),
    (debug_mode(on) -> (pending_abort_error(WF) -> Msg='PENDING WD/ABORT ERROR'; Msg='true'),
    stop_ms_timer_with_msg(Timer,component(ComponentNr,Msg))
    ; true),
    get_enumeration_finished_wait_flag(WF,WFE), % bind enumeration finished to the global outer WFE flag
    l_ground_wait_flags(TWF,WFE,SatResult) % continue with other components
    ),
    ((debug_mode(on) -> print(unsatisfiable_component(ComponentNr)),nl,
    stop_ms_timer_with_msg(Timer,component(ComponentNr,'false')) ; true),
    store_unsat_component_nr(ComponentNr),
    SatResult=false)).

mark_generated_exists(TID1,TID2) :- add_texpr_info_if_new(TID1,generated_exists_parameter,TID2).

observe_state(Env,WF,ComponentNr) :-
    get_wait_flag0(WF,WF0), get_wait_flag1(observe_state,WF,WF1),
    (preferences:get_preference(provide_trace_information,true)
    -> when((ground(Env);nonvar(WF0)),print_success(WF0,ComponentNr,Env,WF))
    %% ,when(nonvar(WF1),(nl, print('Starting Phase 1'),nl, portray_waitflags(WF)))
    ; true),
    observe_state2(Env,WF0,WF1).

observe_state2([],_,_).

observe_state2([Binding|T],WF0,WF1) :- get_binding_value(Binding,VarID,Val),
    observe_variable(VarID,Val,WF0,WF1),observe_state2(T,WF0,WF1).

observe_variable(Var,Val,WF0,_WF1) :- preferences:get_preference(provide_trace_information,false),!,
    observe_variable_no_trace(Var,Val,WF0).

observe_variable(Var,Val,WF0,WF1) :-
    ground_value_check(Val,GrVal),
    observe_variable0_block(Var,Val,GrVal,WF0,WF1).

observe_variable0_block(Var,Val,GrVal,WF0,WF1) :-
    (var(GrVal) -> write(' :?: '), write(Var), write(' '), print_value_summary(Val),
    observe_variable1(Var,Val,WF1)
    ; (var(WF0) -> write('-->> ')
    ; write('--0-->> ')), % WF0/GrVal grounded at same time probably does not happen (often)
    write(Var),nl, write(' '),print_value_summary(Val),print_walltime,nl,
    assert_det_solution_for_constant(Var,Val)
).

observe_variable1(Var,Val,WF1) :- ground_value_check(Val,GV),
    observe_variable1_block(Var,Val,WF1,GV).

observe_variable1_block(Var,Val,_WF1,GV):-
    (nonvar(GV)
    -> write('--1-->> '), write(Var),nl, write(' '),print_value_summary(Val),
    assert_det_solution_for_constant(Var,Val)
    ; write(' :?1?: '), write(Var), write(' '), print_value_summary(Val)
%% , when(ground(Val), (print('--ground-->> '),print(Var),print(' '), print_value_summary(Val))) % comment in to see grounding
%% , external_functions:observe_state([bind(Var,Val)]) % comment in to observe values
%% , translate:print_bstate([bind(Var,Val)]),nl % comment in to print full value with CLP(FD) info
).

observe_variable_no_trace(Var,Val,WF0) :- nonvar(WF0),!, % important e.g. for test 1368
    (ground_value(Val) -> assert_det_solution_for_constant(Var,Val) ; true).

observe_variable_no_trace(Var,Val,WF0) :- ground_value_check(Val,GV),
    %tools_printing:print_term_summary(gr_val_check(Var,Val,GV)),nl,
    observe_variable_no_trace4(Var,GV,Val,WF0).

observe_variable_no_trace4(_,GV,_,_) :- var(GV),!.

observe_variable_no_trace4(Var,_,Val,_) :- assert_det_solution_for_constant(Var,Val). % this could be expensive !?

portray_unsat_components :- format('Unsat components~n',[]),
    unsat_component(Comp,Status),
    (unsat_component_abort_error(Comp) -> Abort='abort/well_definedness error' ; Abort=''),
    (unsat_component_enumeration_warning(Comp) -> EW='enumeration_warning' ; EW=''),
    format('* component: ~w -> ~w ~w ~w~n',[Comp,Status,Abort,EW]),
    unsat_conjunct_inside_component(Comp,BE,S,Reason),
    format(' -> reason for ~w: ~w : ',[S,Reason]), translate:print_bexpr_with_limit(BE,100),nl,
    fail.

portray_unsat_components.

print_success(WF0,ComponentNr,_,_WF) :- nonvar(WF0),!,
    debug_format(19,'~n-->> WF0 for component ~w grounded.~n',[ComponentNr]).

print_success(_,ComponentNr,Env,_WF) :-
    (Env=[]
    ->
    format('~n-->> SUCCESS; processed component ~w (no identifiers)~n',[ComponentNr])
    ; length(Env,NrVal),
    format('~n-->> SUCCESS; all ~w identifier(s) valued in component ~w~n',[NrVal,ComponentNr])
    ),
    (debug_mode(on)
    -> findall(V,member(typedval(_,_,V,_),Env),Vars),
    statistics(walltime,[W,_]), format('-->> (walltime: ~w ms) : identifiers = ~w~n',[W,Vars])
    ; true),
    %%,check_for_multiple_solutions(WF,ComponentNr) %% comment in to check for multiple solutions
    nl.

print_trace_message(Msg) :-
    (preference(provide_trace_information,false) -> true
    ; printsilent_message(Msg)).

print_trace_message_with_typed_vals(Msg,TypedVals) :-
    (preference(provide_trace_information,false) -> true
    ; printsilent_message(Msg),
    maplist(get_typedval_id,TypedVals,IDs),
    printsilent_message(IDs)
).

print_walltime :- statistics(walltime,[Tot,Delta]),
    (debug_mode(on) -> print(' '),tools:print_memory_used_wo_gc ; true),
    format(' ~w ms (Delta ~w ms) ',[Tot,Delta]).

project_state([],_,[]).

project_state([bind(VarID,Value)|Rest],ComponentVars,Out) :-
    (member(VarID,ComponentVars)
    -> Out=[bind(VarID,Value)|Out2]
    ; Out=Out2
    ), project_state(Rest,ComponentVars,Out2).

project_typed_vals([],_,[],[]).

project_typed_vals([typedval(Val,Type,VarID,EnumWarningInfos)|Rest],ComponentVars,In,Out) :-
    (member(VarID,ComponentVars)
    -> In = [typedval(Val,Type,VarID,EnumWarningInfos)|In2], Out2=Out
    ; Out = [typedval(Val,Type,VarID,EnumWarningInfos)|Out2], In2=In
    ), project_typed_vals(Rest,ComponentVars,In2,Out2).

reset_all_component_infos :-
    reset_unsat_component_info,
    reset_unsat_conjunct_inside_component_info,
    reset_observe_state.

reset_component_info(AllowSkip) :- retractall(allow_skipping_over_components),
    (AllowSkip==true -> assertz(allow_skipping_over_components) ; true),
    reset_unsat_component_info,
    reset_unsat_conjunct_inside_component_info.

reset_observe_state :- retractall(det_solution_for_constant_packed(_,_)).

reset_tracetest_for_component :- retractall(skipped_unsat_conjunct(_)). % to be called before trace checking a component

reset_unsat_component_info :-
    retractall(unsat_component(_,_)),
    retractall(unsat_component_enumeration_warning(_)),
    retractall(unsat_component_abort_error(_)).

reset_unsat_conjunct_inside_component_info :-
    retractall(skipped_unsat_conjunct(_)),
    retractall(unsat_conjunct_inside_component(_,_,_,_)).

safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :- %print(c(_ComponentNr,WF)),nl, translate:print_bexpr(BE),nl,
    preferences:get_preference(provide_trace_information,false),
    \+ abort_error_occured_in_error_scope,
    % avoid setting up new error scope for every conjunct with catch_enumeration_warning
    % BE is only displayed in TRACE_INFO mode anyway
    % can be a bottleneck, e.g., for :prob-file ../prob_examples/public_examples/Eval/Sudoku_SAT.eval
    !,
    if(b_test_boolean_expression(BE,LS,S,WF,Ai,Ao),true,
    (abort_error_occured_in_error_scope
    -> assert_unknown(ComponentNr,BE,abort_error,Ai,Ao)
    ; fail)
).

safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :-
    catch_enumeration_warning_exceptions_and_wd_failures(
    b_test_boolean_expression(BE,LS,S,WF,Ai,Ao), % this should not backtrack (without WF0 set);
    % otherwise we may get problems with error blocks nesting
    assert_unknown(ComponentNr,BE,enumeration_warning,Ai,Ao), % call when exception caught
    true, % true: add exceptions as event errors
    assert_unknown(ComponentNr,BE,well_definedness_error,Ai,Ao), % call when wd_error caught
    component(ComponentNr)). % Source argument for debugging

same_id_is_member(X,[H|T],SID,Rest) :-
    (same_id(X,H,SID) -> Rest=T ; Rest=[H|TR],same_id_is_member(X,T,SID,TR)).

store_unsat_component_nr(X) :- % use if you do not know if it is unknown or unsat
    %error_manager:print_error_scopes,
    (critical_enumeration_warning_occured_in_error_scope
    -> Res = unknown
    % should we also detect abort_error_occured_in_error_scope ?
    ; Res=false),
    store_unsat_component_nr(X,Res).

store_unsat_component_nr(X,FalseOrUnknown) :-
    debug_println(9,store_unsat_component_nr(X,FalseOrUnknown)),
    (unsat_component(X,false) -> true
    ; retractall(unsat_component(X,_)),assertz(unsat_component(X,FalseOrUnknown))
    ),
    (critical_enumeration_warning_occured_in_error_scope,
    \+ unsat_component_enumeration_warning(X)
    -> assertz(unsat_component_enumeration_warning(X)),
    debug_println(19,enumeration_warning_in_component(X))
    ; true),
    (abort_error_occured_in_error_scope
    -> assert_unsat_component_abort_error(X)
    ; true).

unpack_det_sol(Var,PVal,Val) :-
    (PVal = '$TOO_LARGE'
    -> ajoin(['The following CONSTANT was not stored due to its size (set preference ALLOW_INCOMPLETE_SETUP_CONSTANTS to TRUE to store all constants found): '], Msg),
    add_message(det_value_not_stored_for_constant,Msg,Var),
    fail
    ; unpack_value(PVal,Val)
).

unsat_component_exists :- unsat_component(_,false),!.

unsat_or_unknown_component_exists :- unsat_component(_,_),!.

uses_large_value(BExpr) :-
    map_over_bexpr(uses_large_value_aux,BExpr).

uses_large_value_aux(value(V)) :- value_too_large(V).

value_too_large(avl_set(A)) :-
    preference(allow_incomplete_partial_setup_constants,false), %if true we always store the value
    (preference(provide_trace_information,false) -> MaxH=7 ; MaxH=9),
    \+ avl_height_less_than(A,MaxH).

value_too_large((A,B)) :- (value_too_large(A) -> true ; value_too_large(B)).

value_too_large(rec(F)) :- member(field(_,FVal),F), value_too_large(FVal).

value_too_large(closure(P,T,B)) :-
    \+ custom_explicit_sets:is_interval_closure(P,T,B,_,_),
    preference(allow_incomplete_partial_setup_constants,false),
    uses_large_value(B).