quantifier_instantiation

check_quantifier_limit(Options, Len, Kind, Span, NewOptions) :-
    select(instantiate_quantifier_limit(Limit),Options,NO),
    Len \== 0,
    !,
    ( Len =< Limit
    -> perfmessage(good(Kind),expanding_quantifier(Len,limit(Limit)),Span),
    NewLimit is Limit // Len,
    NewOptions = [instantiate_quantifier_limit(NewLimit)|NO]
    ; perfmessage(Kind,not_expanding_quantifier(Kind,Len,limit(Limit)),Span),
    fail
).

check_quantifier_limit(O, _, _, _, O).

compute_instantiations_from_compset(Kind,Options,CompSet, Bindings, PrecomputedVals,Options,Span) :-
    ground_bexpr(CompSet), % should now be always true
    temporary_set_preference(strict_raise_enum_warnings, false),
    enter_new_error_scope(ScopeID, compute_instantiations_from_compset),
    ( true
    ; clear_enumeration_warning_in_error_scope(ScopeID),
    fail
    ),
    (member(expansion_time_out(Val),Options) -> TimeOutVal=Val ; TimeOutVal=100),
    % things like !i.(i:dom(f) => f(x)=TRUE) cannot be expanded if f not fully known at the moment
    (debug_mode(on) -> format('Trying to expand (timeout ~w ms): ',[TimeOutVal]),translate:print_bexpr(CompSet),nl ; true),
    call_cleanup(safe_time_out(
    (b_compute_expression_nowf(CompSet, [], Bindings, TPrecomputedVals,
    'SMT quantifier precomputation', 0), !,
    (enumeration_warning_occured_in_error_scope
    -> perfmessage(Kind,not_expanding_quantifier_due_to_enum_warning(Kind),Span)
    ; true)
    ),
    TimeOutVal, TimeOutRes),
    (exit_error_scope(ScopeID, _, compute_instantiations_from_compset),
    reset_temporary_preference(strict_raise_enum_warnings))),
    (TimeOutRes == time_out
    -> perfmessage(Kind,not_expanding_quantifier_due_to_timeout(Kind,TimeOutVal),Span),
    fail
    ; true),
    !,
    expand_computed_val(TPrecomputedVals,Kind,Options,PrecomputedVals,Span).

contains_quantifiers(b(E,pred,_)) :- contains_quantifiers_e(E).

contains_quantifiers_e(negation(A)) :- contains_quantifiers(A).

contains_quantifiers_e(conjunct(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)).

contains_quantifiers_e(disjunct(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)).

contains_quantifiers_e(implication(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)).

contains_quantifiers_e(equivalence(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)).

contains_quantifiers_e(forall(_,_,_)).

contains_quantifiers_e(exists(_,_)).

convert_to_couple(b(value(V),couple(T1,T2),I), [BV1,BV2]) :-
    nonvar(V),
    V = (V1,V2),
    !,
    BV1 = b(value(V1),T1,I),
    BV2 = b(value(V2),T2,I).

convert_to_couple(b(couple(V1,V2),_,_), [V1,V2]).

couples_to_list_of_tuples([], _, []).

couples_to_list_of_tuples([b(value(ValueCouple),CoupleType,_)|T], RTIDS, [ListOfAsts|NT]) :-
    value_couple_to_list_of_asts(ValueCouple, RTIDS, CoupleType, ListOfAsts),
    couples_to_list_of_tuples(T, RTIDS, NT).

create_cartesian_product_list(ListOfValues1, ListOfValues2, ListOfPairs) :-
    create_cartesian_product_list(ListOfValues1, ListOfValues2, [], ListOfPairs).

create_cartesian_product_list([], _, Acc, Acc).

create_cartesian_product_list([Val1|T], ListOfValues2, Acc, ListOfPairs) :-
    create_cartesian_product_list_val(Val1, ListOfValues2, Acc, NAcc),
    create_cartesian_product_list(T, ListOfValues2, NAcc, ListOfPairs).

create_cartesian_product_list_val(_, [], Acc, Acc).

create_cartesian_product_list_val(ValList, [Val2|T], Acc, NAcc) :-
    is_list(ValList),
    !,
    append(ValList, [Val2], NValList),
    create_cartesian_product_list_val(ValList, T, [NValList|Acc], NAcc).

create_cartesian_product_list_val(Val1, [Val2|T], Acc, NAcc) :-
    create_cartesian_product_list_val(Val1, T, [[Val1,Val2]|Acc], NAcc).

create_global_state_bindings([], []).

create_global_state_bindings([Id|T], [bind(Id,Val)|NT]) :-
    lookup_global_constant(Id, Val),
    create_global_state_bindings(T, NT).

expand_computed_val(global_set(GS),Kind,Options,Res,Span) :-
    % for deferred sets: we check list_contains_unfixed_deferred_set_id above
    (enumerated_set(GS) -> true
    ; member(instantiate_deferred_sets,Options), % Z3 cannot deal with deferred set values, see test 2063
    perfmessage(Kind,not_expanding_quantifier_with_global_deferred_set(Kind),GS,Span)
    ),!,
    try_expand_and_convert_to_avl_with_check(global_set(GS),Res,quantifier_instantiation(Kind)).

expand_computed_val(Closure,Kind,Options,Res,Span) :-
    is_interval_closure(Closure,Low,Up),
    number(Low), number(Up),
    Card is Up-Low+1,
    (member(instantiate_quantifier_limit(Lim),Options) -> true ; Lim=200),
    (Lim >= Card -> true
    ; perfmessage(Kind,not_expanding_interval(Kind,Card,limit(Lim)),Low:Up,Span),
    fail
    ),
    try_expand_and_convert_to_avl_with_check(Closure,Res,quantifier_instantiation(Kind)).

expand_computed_val(Val,_,_,Val,_).

filter_lhs_distinct_from_ids(LHS, IdNames, RelevantLHS, RestLHS) :-
    conjunction_to_list(LHS, List),
    list_to_ord_set(IdNames,SIds),
    split_list(irrelevant_or_non_ground_conjunct(SIds),List,TList,RList),
    conjunct_predicates(RList, RelevantLHS),
    conjunct_predicates(TList, RestLHS).

finite_base_type(boolean,b(boolean_set,set(boolean),[])).

finite_base_type(couple(TA,TB),b(cartesian_product(VA,VB),set(couple(TA,TB)),[])) :-
    finite_base_type(TA,VA),
    finite_base_type(TB,VB).

get_couple_type_for_ids([TID1], Type1) :- !, get_texpr_type(TID1, Type1).

get_couple_type_for_ids([TID1,TID2|T], CType) :-
    get_texpr_type(TID1, Type1),
    get_texpr_type(TID2, Type2),
    get_couple_type_for_ids(T, couple(Type1,Type2), CType).

get_couple_type_for_ids([], CType, CType).

get_couple_type_for_ids([TID|T], Acc, CType) :-
    get_texpr_type(TID, Type),
    get_couple_type_for_ids(T, couple(Acc,Type), CType).

get_id_names([], []).

get_id_names([b(identifier(IdName),_,_)|T], [IdName|NT]) :-
    get_id_names(T, NT).

get_instantiation_value([_], List, Res) :- !, Res=[Val],
    member(Val,List).

get_instantiation_value(L, List, ValList) :-
    length(L, Len),
    Len > 1,
    length(ValList, Len),
    member(ValList, List).

get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS) :-
    MEM = b(member(b(IdTerm,IdType,_),Set),pred,_),
    select_member_in_conjunction(MEM, LHS, RestLHS).

get_member_for_id(_Id,IdType,LHS,Set,Rest) :- Rest=LHS,
    (IdType = global(GS)
    -> Set = b(value(global_set(GS)),set(IdType),[]) % we have a finite enumerated or def. set as type
    ; IdType = boolean
    -> Set = b(boolean_set,set(IdType),[])
).

instantiate_exists_to_list(TIDs,LHS,Info,Options,Bodies) :-
    instantiate_quantifier_to_list(TIDs,LHS,exists,Info,Options,[],_NOptions,Bodies).

instantiate_paras_by_membership([TID], LHS, _, _, Options, [Id], ScopeIds, ListOfValues, RestLHS) :-
    get_texpr_id(TID, Id),
    ( get_texpr_id(TID2, Id),
    is_membership_or_equality(MEM, TID2, Set),
    select_member_in_conjunction(MEM, LHS, TRestLHS)
    ; get_texpr_type(TID, Type),
    finite_base_type(Type, Set),
    TRestLHS = LHS
    ),
    rewrite_set_to_list_of_asts(Set, [Id|ScopeIds], Options, TListOfValues),
    !,
    ListOfValues = TListOfValues,
    RestLHS = TRestLHS.

instantiate_paras_by_membership([TID1,TID2], LHS, _Kind, _, Options, [Id1,Id2], ScopeIds, ListOfPairs, RestLHS) :-
    get_texpr_id(TID1, Id1),
    get_texpr_id(TID2, Id2),
    Couple = b(couple(A,B),_,_), get_texpr_id(A,Id1), get_texpr_id(B,Id2),
    MEM = b(member(Couple,Set),pred,_),
    select_member_in_conjunction(MEM, LHS, RestLHS),
    rewrite_set_to_list_of_asts(Set, [Id1,Id2|ScopeIds], Options, ListOfValues),
    maplist(convert_to_couple, ListOfValues, ListOfPairs),
    !.

instantiate_paras_by_membership(TIDS, LHS, _, _, Options, IdNames, ScopeIds, ListOfTuples, RestLHS) :-
    % !(x1,..xn).(x1:S1 & .. & xn:Sn & RestLHS => BODY) | #(x1,..xn).(x1:S1 & .. & xn:Sn & RestLHS)
    instantiate_paras_possible_nary_member(TIDS, LHS, IdNames, [], ScopeIds, Options, TListOfTuples, TRestLHS),
    !,
    ListOfTuples = TListOfTuples,
    RestLHS = TRestLHS.

instantiate_paras_comp_set(TIDS, LHS, Kind, Info, Options, IdNames, _ScopeIds, ListOfTuples, RestLHS) :-
    % any other quantifier where domains are, e.g., defined in nested couples such as !(a,b,c).(0|->1|-a|->b|->c : S => BODY), also for exists
    get_couple_type_for_ids(TIDS, CType),
    get_id_names(TIDS, TIdNames),
    filter_lhs_distinct_from_ids(LHS, TIdNames, RelevantLHS, RestLHS),
    CompSet = b(comprehension_set(TIDS,RelevantLHS),set(CType),[]),
    find_identifier_uses(CompSet, [], UsedIds),
    ( create_global_state_bindings(UsedIds, Bindings)
    -> true
    ; % cannot instantiate due to free variables that are not quantified
    fail
    ),
    % Default timeout 100ms, can be overridden with expansion_time_out option
    % write('TRY EXPANDING: '),nl,translate:print_bexpr(CompSet),nl,
    compute_instantiations_from_compset(Kind,Options,CompSet, Bindings, PrecomputedVals,Options, Info),
    !,
    IdNames = TIdNames,
    ( PrecomputedVals == []
    -> ListOfTuples = [] % no instantiation found, quantifier is false/true
    ; PrecomputedVals = avl_set(Avl),
    avl_to_list(Avl, AvlList),
    avl_list_to_list_of_asts(CType, AvlList, [], ListOfValues),
    (TIDS = [_] % single identifier
    -> ListOfTuples=ListOfValues
    ; reverse(TIDS, RTIDS),
    couples_to_list_of_tuples(ListOfValues, RTIDS, ListOfTuples)
)
).

instantiate_paras_possible(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS) :-
    \+ possibly_reject_unfixed_deferred_set_id(TIDs, Options),
    (nonmember(instantiate_precisely_only,Options),
    instantiate_paras_by_membership(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS)
    ;
    instantiate_paras_comp_set(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS)).

instantiate_paras_possible(TIDS, LHS, Kind, _, _Span, _, _, _, _) :-
    TIDS = [TID1|_],
    get_texpr_id(TID1,Id1),
    perfmessage_bexpr(Kind, ['Quantifier (',Kind,' over ',Id1,', ...) expansion not possible: '], LHS),
    fail.

instantiate_paras_possible_nary_member([], RestLHS, [], LAcc, _, _, LAcc, RestLHS).

instantiate_paras_possible_nary_member([TID|T], LHS, [Id|IdNames], LAcc, ScopeIds, Options, ListOfPairs, RestLHS) :-
    get_texpr_id(TID,Id),
    TID = b(IdTerm,IdType,_),
    get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS1),
    NScopeIds = [Id|ScopeIds],
    rewrite_set_to_list_of_asts(Set, NScopeIds, Options, ListOfValues),
    ( LAcc == []
    -> instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, ListOfValues, NScopeIds, Options, ListOfPairs, RestLHS)
    ; create_cartesian_product_list(LAcc, ListOfValues, NLAcc),
    instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, NLAcc, NScopeIds, Options, ListOfPairs, RestLHS)
).

instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, Res) :-
    instantiate_paras_possible(TIDs, LHS, forall, Info, Options, Ids, ScopeIds, List, RestLHS),
    ( List == []
    -> % no instantiation found, universal quantification is true
    Res = b(truth,pred,[])
    ; length(List,Len),
    check_quantifier_limit(Options, Len, forall, Info, NOptions),
    !,
    create_implication(RestLHS, RHS, BODY),% translate:nested_print_bexpr(BODY),nl,
    % Note: it is important that List contains only ground values; otherwise findall will copy variables:
    findall(Vals, get_instantiation_value(Ids, List, Vals),Vs),
    maplist(replace_ids_by_exprs(BODY,Ids),Vs,Bodies),
    Bodies \== [],
    %Bodies = [B1|_], translate:print_bexpr(B1),nl,
    conjunct_predicates(Bodies, Res)
).

instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, Res) :-
    instantiate_quantifier_to_list(TIDs,LHS,exists,Info,Options,ScopeIds,NOptions,Bodies),
    disjunct_predicates(Bodies, Res).

instantiate_quantifier_to_list(TIDs,LHS,Kind,Info,Options,ScopeIds,NOptions,Bodies) :-
    instantiate_paras_possible(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, BODY),
    ( List == []
    -> % no instantiation found, existential quantification is false
    Bodies = [] % falsity for disjunction
    ; length(List,Len),
    check_quantifier_limit(Options, Len, Kind, Info, NOptions),
    !,
    findall(Vals, get_instantiation_value(Ids, List, Vals),Vs),
    maplist(replace_ids_by_exprs(BODY,Ids),Vs,Bodies),
    Bodies \== []
).

instantiate_quantifiers(Options, Ast, AstOpt) :-
    instantiate_quantifiers(Options, [], Ast, AstOpt). %bsyntaxtree:check_ast(AstOpt).

instantiate_quantifiers(Options, ScopeIds, Ast, AstOpt) :-
    Ast = b(Expr,Type,Info),
    !,
    (%contains_no_quantifiers(Expr) -> AstOpt=Ast
    Type \= pred -> AstOpt = Ast % do we want to instantiate quantifiers inside set comprehensions / bool ...?
    ; instantiate_quantifiers_e(Expr, Type, Info, Options, ScopeIds, NExpr)
    -> safe_create_texpr(NExpr, Type, Info, AstOpt)
    ; add_internal_error('Call failed: ',instantiate_quantifiers_e(Expr, Type, Info, Options, ScopeIds, _)),
    AstOpt=Ast
).

instantiate_quantifiers(_, _, L, R) :-
    add_internal_error('Not a B AST:',instantiate_quantifiers(_, _, L, R) ),
    R = L.

instantiate_quantifiers_e(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, Res) :-
    instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, TRes),
    ( TRes == truth
    -> Res = truth % no instantiation found, universal quantification is true
    ; contains_quantifiers_e(impliation(LHS,RHS)) -> instantiate_quantifiers(NOptions, ScopeIds, TRes, b(Res,pred,_))
    ; get_texpr_expr(TRes,Res) % no quantifiers, no need to traverse
).

instantiate_quantifiers_e(exists(TIDs,LHS), pred, Info, Options, ScopeIds, Res) :-
    instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, TRes),
    ( TRes == falsity
    -> Res = falsity % no instantiation found, existential quantification is false
    ; contains_quantifiers(LHS) -> instantiate_quantifiers(NOptions, ScopeIds, TRes, b(Res,pred,_))
    ; get_texpr_expr(TRes,Res) % no quantifiers, no need to traverse
).

instantiate_quantifiers_e(Expr, _, _, Options, ScopeIds, Res) :-
    % TODO: only proceed if we do not have a top-level exists/forall
    %hit_profiler:add_profile_hit(Expr),
    syntaxtransformation_det(Expr,Subs,_,NSubs,NExpr),
    !,
    %maplist(instantiate_quantifiers(Options, ScopeIds),Subs,NSubs),
    l_instantiate_quantifiers(Subs,Options,ScopeIds,NSubs),
    Res = NExpr.

instantiate_quantifiers_e(Expr, _, _, _, ScopeIds, Res) :-
    add_internal_error('Unknown AST node:', instantiate_quantifiers_e(Expr, _, _, _, ScopeIds, Res)),
    Res = Expr.

irrelevant_or_non_ground_conjunct(_,Conj) :- \+ ground_bexpr(Conj),!.

irrelevant_or_non_ground_conjunct(IdNames,Conj) :-
    find_identifier_uses(Conj, [], UsedIds),
    \+ ord_intersect(UsedIds, IdNames).

l_instantiate_quantifiers([],_,_,[]).

l_instantiate_quantifiers([S1|TS],Options,ScopeIds,[NS1|NTS]) :-
    instantiate_quantifiers(Options,ScopeIds,S1,NS1),
    l_instantiate_quantifiers(TS,Options,ScopeIds,NTS).

possibly_reject_unfixed_deferred_set_id(TIDS, Options) :-
    member(not_instantiate_unfixed_deferred_sets, Options),
    list_contains_unfixed_deferred_set_id(TIDS).

value_couple_to_list_of_asts((VCouple,Value), [_|TRTIDS], couple(CoupleType,VType), ListOfAsts) :-
    VCouple = (_,_),
    !,
    value_couple_to_list_of_asts(VCouple, TRTIDS, CoupleType, TListOfAst),
    append(TListOfAst, [b(value(Value),VType,[])], ListOfAsts).

value_couple_to_list_of_asts((Value1,Value2), [_], couple(VType1,VType2), ListOfAsts) :-
    ListOfAsts = [b(couple(b(value(Value1),VType1,[]),b(value(Value2),VType2,[])),couple(VType1,VType2),[])].

value_couple_to_list_of_asts((Value1,Value2), [_,_], couple(VType1,VType2), ListOfAsts) :-
    ListOfAsts = [b(value(Value1),VType1,[]),b(value(Value2),VType2,[])].