b_interpreter_check

add_predicate(_Pred,_Var,no_avl,NewAVL) :- !, NewAVL=no_avl.

add_predicate(Pred,Var,AVL,NewAVL) :- (avl_store(Pred,AVL,Var,NewAVL) -> true ; NewAVL=no_avl). %pred_var(Var),NewAVL).

apply_unary_minus(unary_minus(A),A).

apply_unary_minus(Nr,MNr) :- number(Nr), MNr is -Nr.

arithmetic_op(less(LHS,RHS),'<',LHS,RHS).

arithmetic_op(less_equal(LHS,RHS),'<=',LHS,RHS).

arithmetic_op(greater(LHS,RHS),'<',RHS,LHS).

arithmetic_op(greater_equal(LHS,RHS),'<=',RHS,LHS).

b_check_boolean_expression(b(Expr,_,Infos),LS,S,WF,Res) :-
    (composed(Expr) -> empty_avl(Ai)
    ; Ai = no_avl), % simple expression: no sharing is possible: no need to register expressions
    b_check_boolean_expression2(Expr,Infos,LS,S,wfwd(WF,pred_true,pred_true),Res,Ai,_).

b_check_boolean_expression(E,LS,S,WF,Res,Ai,Ao) :-
    % add information about WD context: wfwd(WF_store, ExpectedVal, Val)
    % when Val becomes nonvar: if Val==ExpectedVal we need the value of E, otherwise it should be discarded
    b_check_boolean_expression1(E,LS,S,wfwd(WF,pred_true,pred_true),Res,Ai,Ao).

b_check_boolean_expression0(WDE,WDV,Expr,LS,S,WF,Res,Ai,Ao) :-
    b_check_boolean_expression1(Expr,LS,S,wfwd(WF,WDE,WDV),Res,Ai,Ao).

b_check_boolean_expression1(b(Expr,_,Infos),LS,S,WFD,Res,Ai,Ao) :- WFD=wfwd(_WF,WDE,WDV),!,
    % print('check : '), translate:print_bexpr(b(Expr,pred,Infos)),nl,
    %when(nonvar(Res), (print(Res), print(' <--> '),translate:print_bexpr(b(Expr,pred,Infos)),nl)),
    (nonvar(WDV),WDE \= WDV
    -> Ai=Ao,
    (var(Res) -> Res=pred_false ; true)
    ; b_check_boolean_expression2(Expr,Infos,LS,S,WFD,Res,Ai,Ao)).

b_check_boolean_expression1(b(Expr,T,Infos),LS,S,WFD,Res,Ai,Ao) :- !,
    add_internal_error('Illegal WFWD info: ',b_check_boolean_expression1(b(Expr,T,Infos),LS,S,WFD,Res,Ai,Ao)),
    b_check_boolean_expression2(Expr,Infos,LS,S,wfwd(WFD,pred_true,pred_true),Res,Ai,Ao).

b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao) :-
    add_internal_error('Boolean expression not properly wrapped: ',b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao)),
    b_check_boolean_expression2(E,[],LS,S,WFD,Res,Ai,Ao).

b_check_boolean_expression2(truth,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_true, Ai=Ao.

b_check_boolean_expression2(falsity,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_false, Ai=Ao.

b_check_boolean_expression2(negation(BExpr),_,LocalState,State,WFD,Res,Ai,Ao) :- !,
    (can_negate_expression(BExpr,NBExpr)
    -> /* avoid introducing negate propagator; maybe not necessary */
    b_check_boolean_expression1(NBExpr,LocalState,State,WFD,Res,Ai,Ao)
    ; negate(NR,Res),
    b_check_boolean_expression1(BExpr,LocalState,State,WFD,NR,Ai,Ao)).

b_check_boolean_expression2(conjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
    normalise_conjunct2(conjunct(LHS,RHS),CInfo,NormRes,[]),
    construct_norm_conjunct2(NormRes,NC,Info),
    b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(norm_conjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
    construct_norm_conjunct(RHS,NC),
    conjoin(LR,RR,Res,LHS,NC,WF),
    b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
    propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_false), % if WDE/=WDV then set GuardFlag to pred_false; indicating to RHS that it is not needed also
    b_check_boolean_expression0(pred_true,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).

b_check_boolean_expression2(implication(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !, imply(LR,RR,Res),
    b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
    propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_false),
    b_check_boolean_expression0(pred_true,GuardFlag,RHS,LocalState,State,WF,RR,Aii,Ao).

b_check_boolean_expression2(equivalence(LHS,RHS),_,LocalState,State,WFD,Res,Ai,Ao) :- !, equiv(LR,RR,Res),
    b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
    b_check_boolean_expression1(RHS,LocalState,State,WFD,RR,Aii,Ao).

b_check_boolean_expression2(disjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
    normalise_disjunct2(disjunct(LHS,RHS),CInfo,NormRes,[]),
    construct_norm_disjunct2(NormRes,NC,Info),
    b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(norm_disjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
    construct_norm_disjunct(RHS,NC),
    disjoin(LR,RR,Res,LHS,NC,WF),
    b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
    propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_true),
    b_check_boolean_expression0(pred_false,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).

b_check_boolean_expression2(let_predicate(Ids,AssignmentExprs,Pred),_Info,LocalState,State,WFD,Res,Ai,Ao) :-
    !,
    wd_set_up_localstate_for_let(Ids,AssignmentExprs,LocalState,State,LetState,WFD),
    b_check_boolean_expression1(Pred,LetState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(lazy_let_pred(Id,AssignmentExpr,Pred),_I,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
    set_up_localstate([Id],[(Trigger,IdValue)],LocalState,LetState),
    b_interpreter:lazy_compute_expression(Trigger,AssignmentExpr,LocalState,State,IdValue,WF,Ai),
    b_check_boolean_expression1(Pred,LetState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao).

b_check_boolean_expression2(lazy_lookup_pred(Id),Info,LocalState,_State,WFD,Res,Ai,Ao) :- !, Ai=Ao,
    store:lookup_value_for_existing_id(Id,LocalState,(Trigger,Value)), % should normally only occur in LocalState; value introduced by lazy_let
    wd_delay(((Trigger,Value) = (pred_true,Res)),
    Res,b(lazy_lookup_pred(Id),pred,Info),WFD).

b_check_boolean_expression2(value(V),_Info,_LocalState,_State,_WFD,Res,Ai,Ao) :- !, % this can occur when lazy_lookup_pred gets compiled by b_compiler
    Res=V,Ai=Ao.

b_check_boolean_expression2(not_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    (negate_equal_false(LHS,RHS,LHS1,RHS1)
    -> /* X/=FALSE equivalent to X=TRUE */
    b_check_boolean_expression3_pos(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
    ; b_check_boolean_expression3_neg(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
).

b_check_boolean_expression2(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    (negate_equal_false(LHS,RHS,LHS1,RHS1)
    -> RHS1=b(boolean_true,boolean,[]), /* X/=FALSE equivalent to X=TRUE */
    b_check_boolean_expression3_neg(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
    ; b_check_boolean_expression3_pos(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
).

b_check_boolean_expression2(not_member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_neg(member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(not_subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_neg(subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(not_subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_neg(subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(greater(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_pos(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(greater_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_neg(less(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(less_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
    b_check_boolean_expression3_neg(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression2(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
    b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao).

b_check_boolean_expression3_neg(Pred,Infos,LocalState,State,WFD,NegRes,Ai,Ao) :-
    %print(register_neg_predicate(WFD,Infos,Pred)),nl,
    register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ao), negate(Res,NegRes),
    (Reused=true
    -> true
    ; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Res)
).

b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
    %print(register_predicate(WFD,Infos,Pred)),nl,portray_avl(Ai),nl,
    register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ao),
    (Reused=true
    -> true % , print(reused_pred(WFD,Infos)),nl, translate:print_bexpr(Pred),nl
    ; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Res)
).

b_check_boolean_expression4(equal(LHS,RHS),_,LocalState,State,WFD,EqRes) :- !,
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
    get_texpr_type(LHS,Type),
    equality_objects_with_type(Type,LHValue,RHValue,EqRes).

b_check_boolean_expression4(member(LHS,RHS),Info,LocalState,State,WFD,Res) :-
    %member_check_should_be_reified(LHS,RHS), % no longer need this: symbolic operators will be kept as closures if large ?!
    !,
    get_texpr_expr(RHS,ERHS),
    b_check_member_expression(ERHS,RHS,LHS,Info,LocalState,State,WFD,Res).

b_check_boolean_expression4(forall(Parameters,LHS,RHS),Info,LocalState,State,WFD,Res) :- !,
    if(b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,Res),true,
    (perfmessagecall(reify,cannot_reify_forall(Parameters),translate:print_bexpr(LHS),LHS),
    fail)).

b_check_boolean_expression4(exists(Parameters,Body),Info,LocalState,State,WFD,Res) :- !,
    if(b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,Res),true,
    (perfmessagecall(reify,cannot_reify_exists(Parameters),translate:print_bexpr(Body),Body),
    fail)).

b_check_boolean_expression4(subset(LHS,RHS),_,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
    subset_test(LHValue,RHValue,Res,WF).

b_check_boolean_expression4(subset_strict(LHS,RHS),_,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
    subset_strict_test(LHValue,RHValue,Res,WF).

b_check_boolean_expression4(external_pred_call(FunName,Args),Info,LocalState,State,WFD,Res) :-
    !,
    (external_fun_has_wd_condition(FunName)
    -> wd_delay_until_needed(WFD,b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res))
    ; b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res)).

b_check_boolean_expression4(freetype_case(FT,IsCase,Expr),_Infos,LocalState,State,WFD,Res) :- !,
    b_wd_compute_expression(Expr,LocalState,State,freeval(FT,ActualCase,_A),WFD),
    eq_atomic(IsCase,ActualCase,freeval_case,Res).

b_check_boolean_expression4(finite(Expr),_Infos,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(Expr,LocalState,State,ExprVal,WFD),
    kernel_objects:test_finite_set_wf(ExprVal,Res,WF).

b_check_boolean_expression4(partition(Expr,ListOfSets),_Infos,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(Expr,LocalState,State,ExprVal,WFD),
    b_wd_compute_expressions(ListOfSets,LocalState,State,PartitionList,WFD), % arg is a Prolog list, not a set
    kernel_objects:test_partition_wf(ExprVal,PartitionList,Res,WF).

b_check_boolean_expression4(Pred,_,LocalState,State,WFD,Res) :-
    arithmetic_op(Pred,Op,LHS,RHS),!,
    b_wd_compute_expression(LHS,LocalState,State,int(LHValue),WFD),
    % kernel_objects:basic_type2(integer,int(LHValue)),
    b_wd_compute_expression(RHS,LocalState,State,int(RHValue),WFD),
    % kernel_objects:basic_type2(integer,int(RHValue)),
    check_arithmetic_operator(Op,LHValue,RHValue,Res).

b_check_exists_wf(Parameters,Body,Info,LocalState,State,WF,PredRes) :-
    WFD=wfwd(WF,pred_true,pred_true), % we expect it to be in a context where the value will be needed
    b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,PredRes).

b_check_exists_wfwd(Parameters,Body,_Info,LocalState,State,WFD,PredRes) :-
    % could be generalised to take into consideration domain as restricted by Body
    small_quantifier_cardinality(Parameters,Body,LHS,RHS),
    % print(expanding_check_exists(_Card,Parameters)),nl, % portray_waitflags(WF),
    expand_quantifier(Parameters,LHS,List),
    % now compute a priority for the disjunction based on the number of case splits
    % relevant for tests 1358, 1746
    length(List,Len), % Note: if Len=1: the body must be true; no disjoin will be set up
    get_pow2_binary_choice_priority(Len,Prio),
    % if Len=2 -> we actually have just two possibilities T,_ and F,T; but we want Prio to start at 4 ?
    % if Len=3 -> we have T,_,_ ; F,T,_ ; F,F,T less possibilites if disjoin enumerated from left-to-right; TO DO: should we lower the priority taking this into account ?
    % TO DO: maybe we could directly set up an n-ary disjoin predicate ? if one disjunct true; remove case-splits on other disjuncts
    WFD=wfwd(WF,_,_),
    check_expanded_exists_quantifier(List,Prio,RHS, LocalState, State,WF,WFD,PredRes).

b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res) :-
    WFD=wfwd(WF,_,_),
    (do_not_evaluate_args(FunName) -> EvaluatedArgs=[]
    ; b_wd_compute_expressions(Args, LocalState,State, EvaluatedArgs, WFD)),
    call_external_predicate(FunName,Args,EvaluatedArgs,LocalState,State,Res,Info,WF).

b_check_forall_wf(Parameters,LHS,RHS,Info,LocalState,State,WF,PredRes) :-
    WFD=wfwd(WF,pred_true,pred_true), % we expect it to be in a context where the value will be needed
    b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes).

b_check_forall_wfwd(_Parameters,LHS,RHS,_Info,_LocalState,_State,_WFD,PredRes) :-
    (is_falsity(LHS) ; is_truth(RHS)),!, % quantifier always true
    PredRes = pred_true.

b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes) :-
    small_quantifier_cardinality(Parameters,LHS,LHS1,LHSRest),
    %print(expand(forall(Parameters))),nl,
    expand_quantifier(Parameters,LHS1,List), %print(List),nl,
    Body = b(implication(LHSRest,RHS),pred,Info),% translate:print_bexpr(Body),nl,
    WFD=wfwd(WF,_,_),
    check_expanded_forall_quantifier(List,Body, LocalState, State,WF,WFD,PredRes).

b_check_member_expression(pow_subset(RHS),_,LHS,_Info,LocalState,State,WFD,Res) :- !,
    b_check_boolean_expression4(subset(LHS,RHS),[],LocalState,State,WFD,Res).

b_check_member_expression(interval(Low,Up),_,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    % to do: should we also match interval value closure
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(Low,LocalState,State,LowValue,WFD),
    b_wd_compute_expression(Up,LocalState,State,UpValue,WFD),
    kernel_objects:test_in_nat_range_wf(LHValue,LowValue,UpValue,Res,WF).

b_check_member_expression(set_extension(SetExt),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    % rewrite x:{a,b,c} into x=a or x=b or x=c (is the opposite of rewrite_disjunct_to_member)
    % The rewrite_disjunct_to_member is good when we know a membership to be true; the disjunct is better for reification
    % Note: the problem is in particular when the result of the membership is not needed and an uninstantiated
    % variable is used in the set extension, example y:dom(f) => (x:{f(y),0} or f(y)=0)
    % print(mem_check_set_extension),print(' '),translate:print_bexpr(b(member(LHS,_RHS),pred,[])),nl,
    b_wd_compute_expressions(SetExt,LocalState,State,SetExtValues,WFD),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    get_texpr_type(LHS,Type),
    NewLHS = b(value(LHValue),Type,[]),
    (ground(SetExtValues)
    -> % better to use normal treatment, we can compute the entire set and translate it into an AVL tree
    maplist(construct_value(Type),SetExtValues,Vals),
    b_wd_compute_expression(b(set_extension(Vals),set(Type),[]),LocalState,State,RHValue,WFD),
    membership_test_wf(RHValue,LHValue,Res,WF),
    force_membership_test(Res,LHValue,RHValue,WF)
    ; maplist(construct_equality(NewLHS,Type),SetExtValues,Disjuncts),
    construct_norm_disjunct2(Disjuncts,NC,InfoNC),
    empty_avl(Ai),
    b_check_boolean_expression2(NC,InfoNC,LocalState,State,WFD,Res,Ai,_)
).

b_check_member_expression(closure(Relation),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(Relation,LocalState,State,RelValue,WFD),
    bsets_clp:in_closure1_membership_test_wf(LHValue,RelValue,Res,WF).

b_check_member_expression(partial_function(Dom,Range),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
    b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
    bsets_clp:partial_function_test_wf(LHValue,DomValue,RangeValue,Res,WF).

b_check_member_expression(total_function(Dom,Range),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
    b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
    bsets_clp:total_function_test_wf(LHValue,DomValue,RangeValue,Res,WF).

b_check_member_expression(partial_surjection(Dom,Range),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
    b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
    bsets_clp:partial_surjection_test_wf(LHValue,DomValue,RangeValue,Res,WF).

b_check_member_expression(_,RHS,LHS,_Info,LocalState,State,WFD,Res) :- WFD=wfwd(WF,_,_),
    b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
    b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
    membership_test_wf(RHValue,LHValue,Res,WF),
    force_membership_test(Res,LHValue,RHValue,WF).

b_compute_expression_delay(WDE,WDV,Expr,LocalState,State,Value,WF) :-
    (WDE==WDV
    -> % print('WD Evaluation: '), print(WDE),print(' =?= '), print(WDV), print(' '),translate:print_bexpr(Expr),nl,
    b_compute_expression(Expr,LocalState,State,Value,WF)
    ; %print(instantiate_to_any_value(Value,Expr)),nl,
    instantiate_to_any_value(Value,Expr,WF) % does not matter anyway; but there can be pending co-routines :-(
).

b_wd_compute_expression(Expr,LocalState,State,Value,wfwd(WF,WDE,WDV)) :- !,
    (nonvar(WDV)
    -> (WDE==WDV
    -> %print('REQUIRED: '), translate:print_bexpr(Expr),nl,
    if(b_compute_expression(Expr,LocalState,State,Value,WF), % TO DO: we could use fresh variable for Value
    true,
    (kernel_objects:unbound_value(Value), % we have a WD error, if nonvar it could be because we expect a wrong value
    translate:translate_bexpression_with_limit(Expr,TS),
    add_wd_error_span('Well-definedness error evaluating expression: ',TS,span_predicate(Expr,LocalState,State),WF)
    %Value = term(undefined),
    )
    )
    ; instantiate_to_any_value(Value,Expr,WF))
    ; always_well_defined(Expr) % should we use always_well_defined_or_disprover_mode ?; probably not because of failure of the entire computation!
    -> % print('ALWAYS WD: '), translate:print_bexpr(Expr),nl,
    b_compute_expression(Expr,LocalState,State,Value,WF)
    ; b_compiler:b_optimize(Expr,[],LocalState,State,CExpr,WF),
    % try compiling; this will inline values and may make the expression well_defined; relevant for test 2013
    (always_well_defined(CExpr)
    -> b_compute_expression(CExpr,LocalState,State,Value,WF)
    ; % print('DELAYING DUE TO WD: '), translate:print_bexpr(CExpr),nl,
    b_compute_expression_delay(WDE,WDV, CExpr,LocalState,State,Value,WF)
)
).

b_wd_compute_expression(Expr,LocalState,State,Value,WFD) :-
    add_internal_error('Illegal WFD value: ', b_wd_compute_expression(Expr,LocalState,State,Value,WFD)),fail.

b_wd_compute_expressions([], _, _, [],_WFD).

b_wd_compute_expressions([EXPRsHd|EXPRsTl],LocalState,State,[ValHd|ValTl],WFD) :-
    b_wd_compute_expression(EXPRsHd,LocalState,State,ValHd,WFD),
    b_wd_compute_expressions(EXPRsTl,LocalState,State,ValTl,WFD).

bget_functor(b(B,_,_),F,N) :- functor(B,F,N).

bget_functor(B,F,N) :- functor(B,F,N).

blocking_any_value_for_type(_,_,TYPE,V) :- any_value_for_type(TYPE,V). % , print(inst2(TYPE,V)),translate:print_bexpr(b(_B,TYPE,_I)),nl.

can_negate2(equal(A,B),not_equal(A,B)).

can_negate2(not_equal(A,B),equal(A,B)).

can_negate2(member(A,B),not_member(A,B)).

can_negate2(not_member(A,B),member(A,B)).

can_negate2(subset(A,B),not_subset(A,B)).

can_negate2(not_subset(A,B),subset(A,B)).

can_negate2(subset_strict(A,B),not_subset_strict(A,B)).

can_negate2(not_subset_strict(A,B),subset_strict(A,B)).

can_negate2(greater_equal(A,B),less(A,B)).

can_negate2(less(A,B),greater_equal(A,B)).

can_negate2(less_equal(A,B),greater(A,B)).

can_negate2(greater(A,B),less_equal(A,B)).

can_negate2(less_real(A,B),less_equal_real(B,A)).

can_negate2(less_equal_real(A,B),less_real(B,A)).

can_negate_expression(b(Expr,pred,I),b(NExpr,pred,I)) :- can_negate2(Expr,NExpr).

check_expanded_exists_quantifier([], _, _Body, _LS, _State,_WF,_WFD,Res) :-
    Res=pred_false.

check_expanded_exists_quantifier([LS1|TLS], Priority, Body, LS, State,WF,WFD,Res) :-
    (TLS = [] -> Res=Res1
    ; disjoin(Res1,TRes,Res,priority(Priority),priority(Priority),WF)), % was using Body instead of priority(Priority)
    empty_avl(InnerAi), % TO DO: maybe use no_avl ?
    append(LS1,LS,InnerLS),
    b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
    % Note: we do not need to guard against wd-definition from other instances inside a quantified expression
    check_expanded_exists_quantifier(TLS,Priority,Body,LS,State,WF,WFD,TRes).

check_expanded_forall_quantifier([], _Body, _LS, _State,_WF,_WFD,Res) :-
    Res=pred_true.

check_expanded_forall_quantifier([LS1|TLS], Body, LS, State,WF,WFD,Res) :-
    conjoin(Res1,TRes,Res,Body,Body,WF),
    empty_avl(InnerAi), % TO DO: maybe use no_avl ?
    append(LS1,LS,InnerLS),
    % Note: we do not need to guard against wd-definition from other instances inside a quantified expression
    % either all conjuncts can be evaluated or none
    % print(expand_forall(WFD)), translate:print_bexpr(Body),nl,
    b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
    %instantiate_wfwd_result(WDE,WDV,Res1),
    check_expanded_forall_quantifier(TLS,Body,LS,State,WF,WFD,TRes).

check_less(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
    (Res=pred_true -> less_than_direct(X,Y) ; less_than_equal_direct(Y,X)).

check_less(X,Y,Res) :-
    X < Y,!,/* we could call safe_less_than(X,Y), */
    Res=pred_true.

check_less(_,_,pred_false).

check_less_than_equal(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
    (Res=pred_true -> less_than_equal_direct(X,Y) ; less_than_direct(Y,X)).

check_less_than_equal(X,Y,Res) :- X =< Y,!,Res=pred_true.

check_less_than_equal(_,_,pred_false).

check_pred_truth_var(X) :- var(X),!.

check_pred_truth_var(pred_true) :- !.

check_pred_truth_var(pred_false) :- !.

check_pred_truth_var(X) :- add_internal_error('Illegal Predicate Truth Value: ',check_pred_truth_var(X)).

composed(negation(_)).

composed(conjunct(_,_)).

composed(disjunct(_,_)).

composed(implication(_,_)).

composed(equivalence(_,_)).

composed(let_predicate(_,_,_)).

composed(lazy_let_pred(_,_,_)).

conjoin(X,Y,Res,LHS,RHS,WF) :- % print(conjoin(X,Y,Res)),nl, translate:print_bexpr(LHS),nl,
    ( Res==pred_true -> X=pred_true,Y=pred_true
    ; X==pred_true -> Res=Y
    ; X==pred_false -> Res=pred_false
    ; Y==pred_true -> Res=X
    ; Y==pred_false -> Res=pred_false
    ; Res==pred_false -> conjoin_false0(X,Y,LHS,RHS,WF)
    ; add_error_fail(conjoin,'Illegal values: ', conjoin(X,Y,Res,LHS,RHS,WF))
).

conjoin_false(X,Y,LHS,_RHS,_LWF) :-
    ( X==pred_true -> pred_false=Y
    ; X==pred_false -> true
    ; Y==pred_true -> pred_false=X
    ; Y==pred_false -> true
    ; useless_to_force(LHS) ->
    ( % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(_RHS), print(' == FALSE '),nl,
    Y=pred_false
    ;
    (Y,X)=(pred_true,pred_false)
    )
    ; ( % print(forcing_conjoin_lhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == FALSE '),nl,
    X=pred_false
    ; % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == TRUE ; '), nl,
    (X,Y)=(pred_true,pred_false)
)
).

conjoin_false0(X,Y,_LHS,_RHS,_WF) :- X==Y,!,
    %print(conjoin_false_eqeq(X,Y)),nl, translate:print_bexpr(_LHS),nl,
    X=pred_false.

conjoin_false0(X,Y,_LHS,_RHS,_WF) :- % X & not(X) -> always false
    bool_negate_check(X,Y),!
. %,print(conjoin_false_neqeq(X,Y)),nl,translate:print_bexpr(_LHS),nl.

conjoin_false0(X,Y,LHS,RHS,WF) :-
    %%Prio=1,
    %%(preferences:preference(use_smt_mode,full) -> FullPrio=1.5 ;
    get_priority_of_boolean_expression(LHS,Prio),
    (preferences:preference(use_clpfd_solver,true) ->
    % relevant for tests 349, 362:
    count_number_of_conjuncts(RHS,NrC),
    FullPrio is Prio+(NrC-1)/10,
    get_wait_flag(FullPrio,conjoin,WF,LWF)
    ; % in non-clpfd mode: much less propagation going on, avoid explosion of choice points
    % tests 349, 362 fail with the following for CLPFD: TO DO investigate and use this also in CLPFD mode
    get_binary_choice_wait_flag_exp_backoff(Prio,not_conjunct,WF,LWF)
    ),
    conjoin_false(X,Y,LHS,RHS,LWF).

constrains_ID(b(E,_,_),AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList) :-
    constrains_ID_aux(E,AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList).

constrains_ID_aux(couple(A,B),AllParas,Parameters,RestParameters,(V1,V2),(Skel1,Skel2),Bind) :-
    constrains_ID(A,AllParas,Parameters,Rest1,V1,Skel1,Bind1),
    constrains_ID(B,AllParas,Rest1,RestParameters,V2,Skel2,Bind2),
    append(Bind1,Bind2,Bind). % TO DO: use DCGs

constrains_ID_aux(rec(F),AllParas,Parameters,RestParameters,record(SkelV),record(SkelU),Bind) :-
    constrains_ID_fields(F,AllParas,Parameters,RestParameters,SkelV,SkelU,Bind).

constrains_ID_aux(identifier(ID),AllParas,Parameters,RestParameters,_SkelV,SkelU,Bind) :-
    % TO DO: allow same id to appear multiple times in expression + allow to re-use parameters in another conjunct
    (select(TID,Parameters,RestParameters), get_texpr_id(TID,ID)
    -> Bind = [TID/SkelU]
    ; member(ID,AllParas), % we have already used/bound ID; we will use first occurence for skeleton/bind; this one is simply ignored
    % TO DO: we could try and see whether using the second occurence gives a better result
    RestParameters=Parameters, Bind=[]
).

constrains_ID_aux(value(V),_AllParas,P,P,V,_,[]) :- ground_value(V).% if not ground value we may not be able to compute all possible values for ID

constrains_ID_aux(boolean_true,_AllParas,P,P,pred_true,pred_true,[]). % needed ?? everything is compiled anway ?

constrains_ID_aux(boolean_false,_AllParas,P,P,pred_false,pred_false,[]). % needed ?? everything is compiled anway ?

constrains_ID_aux(add(A,B),AllParas,P,P,_,_,[]) :- % basically allow other Parameters or ground values
    constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).

constrains_ID_aux(minus(A,B),AllParas,P,P,_,_,[]) :- % TO DO: allow other binary/unary operators ?
    constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).

constrains_ID_fields([],_AllParas,P,P,[],[],[]).

constrains_ID_fields([field(Field,Val)|TF],AllParas,Parameters,RestParameters,
    [field(Field,SkelVal)|TSkelV],[field(Field,SkelUnify)|TSkelU],Bind) :-
    constrains_ID(Val,AllParas,Parameters,Rest1,SkelVal,SkelUnify,Bind1),
    constrains_ID_fields(TF,AllParas,Rest1,RestParameters,TSkelV,TSkelU,Bind2),
    append(Bind1,Bind2,Bind). % TO DO: use DCGs

construct_equality(NewLHS,Type,ElementV,Equality) :-
    Element = b(value(ElementV),Type,[]),
    safe_create_texpr(equal(NewLHS,Element),pred,Equality). %, translate:print_bexpr(Equality),nl.

construct_norm_conjunct(A,b(B,pred,Info)) :- construct_norm_conjunct2(A,B,Info).

construct_norm_conjunct2([],truth,[]).

construct_norm_conjunct2([H|T],Res,Info) :-
    (T==[] -> H=b(Res,pred,Info) ; Res=norm_conjunct(H,T),Info=[]).

construct_norm_disjunct(A,b(B,pred,Info)) :- construct_norm_disjunct2(A,B,Info).

construct_norm_disjunct2([],falsity,[]).

construct_norm_disjunct2([H|T],Res,Info) :-
    (T==[] -> H=b(Res,pred,Info) ; Res=norm_disjunct(H,T),Info=[]).

construct_value(Type,Val,b(value(Val),Type,[])).

count_number_of_conjuncts(b(Expr,_,_Infos),Prio) :- !,
    count_number_of_conjuncts2(Expr,Prio).

count_number_of_conjuncts(priority(_),Prio) :- !, Prio=1.

count_number_of_conjuncts(B,Prio) :-
    add_internal_error('Expression not wrapped: ',count_number_of_conjuncts(B,Prio)),Prio=1.

count_number_of_conjuncts2(conjunct(A,B),Nr) :- !, count_number_of_conjuncts(A,NA),
    count_number_of_conjuncts(B,NB), Nr is NA+NB.

count_number_of_conjuncts2(norm_conjunct(_,RHS),Res) :- length(RHS,Len),!,
    Res is Len+1.

count_number_of_conjuncts2(negation(A),Nr) :- !, count_number_of_disjuncts(A,Nr).

count_number_of_conjuncts2(_,1).

count_number_of_disjuncts(b(Expr,_,_Infos),Prio) :- !,
    count_number_of_disjuncts2(Expr,Prio).

count_number_of_disjuncts(priority(_),Prio) :- !, Prio=1.

count_number_of_disjuncts(B,Prio) :-
    add_internal_error('Expression not wrapped: ',count_number_of_disjuncts(B,Prio)),Prio=1.

count_number_of_disjuncts2(disjunct(A,B),Nr) :- !, count_number_of_disjuncts(A,NA),
    count_number_of_disjuncts(B,NB), Nr is NA+NB.

count_number_of_disjuncts2(norm_disjunct(_,RHS),Res) :- length(RHS,Len),!,
    Res is Len+1.

count_number_of_disjuncts2(negation(A),Nr) :- !, count_number_of_conjuncts(A,Nr).

count_number_of_disjuncts2(_,1).

disjoin(X,Y,Res,LHS,RHS,WF) :- %print(disjoin(X,Y,Res,WF)),nl, %% translate:print_bexpr(LHS),print(' or '),translate:print_bexpr(RHS),nl,
    ( Res==pred_false -> X=pred_false,Y=pred_false
    ; X==pred_true -> Res=pred_true
    ; X==pred_false -> Res=Y
    ; Y==pred_true -> Res=pred_true
    ; Y==pred_false -> Res=X
    ; Res==pred_true -> disjoin_true0(X,Y,LHS,RHS,WF)
    ; add_error_fail(disjoin,'Illegal values: ',disjoin(X,Y,Res,LHS,RHS,WF))
).