ast_optimizer_for_smt

assert_ground_id_value(ScopeId, b(Eq,pred,_)) :-
    ( Eq = equal(Id,GroundAst)
    ; Eq = equal(GroundAst,Id)
    ),
    Id = b(identifier(IdName),_,_),
    get_texpr_expr(GroundAst, GroundVal),
    is_ground_b_value(GroundVal),
    !,
    asserta(id_ground_value(ScopeId,IdName,GroundAst)).

assert_ground_id_value(ScopeId, b(equal(Id1,Id2),pred,_)) :-
    Id1 = b(identifier(IdName1),_,_),
    Id2 = b(identifier(IdName2),_,_),
    !,
    asserta(id_equality(ScopeId,IdName1,IdName2)).

assert_ground_id_value(_, _).

assert_ground_id_values(ScopeId, Ast) :-
    conjunction_to_list(Ast, List),
    maplist(assert_ground_id_value(ScopeId), List).

assert_state_id_values(_, NoState) :-
    NoState == no_state, !.

assert_state_id_values(_, []).

assert_state_id_values(TypedIds, [bind(IdName,Value)|T]) :-
    ( member(b(identifier(IdName),TType,_), TypedIds)
    -> Type = TType
    ; infer_value_type(Value, Type)
    ),
    asserta(id_ground_value(0,IdName,b(value(Value),Type,[]))),
    assert_state_id_values(TypedIds, T).

binary_connective(conjunct(A,B),conjunct,A,B).

binary_connective(disjunct(A,B),disjunct,A,B).

binary_connective(implication(A,B),implication,A,B).

binary_connective(equivalence(A,B),equivalence,A,B).

compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, CartList) :-
    compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, [], CartList).

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

compute_cartesian_product(InTypeA, InTypeB, [H|T], SetB, Acc, CartList) :-
    compute_single_cartesian_product(InTypeA, InTypeB, H, SetB, Acc, NAcc),
    compute_cartesian_product(InTypeA, InTypeB, T, SetB, NAcc, CartList).

compute_ground_lambda(LambdaId, Domain, Range, ScopeIds, Options, ComputedSet) :-
    rewrite_set_to_list_of_asts(Domain, ScopeIds, Options, LoAsts),
    ( member(instantiate_sets_limit(SetLimit), Options)
    -> length(LoAsts, Len),
    Len =< SetLimit
    ; true
    ),
    get_texpr_type(Range, RT),
    find_identifier_uses(Range, [], UsedIds),
    LambdaId = b(identifier(LambdaIdName),_,_),
    LoAsts = [b(_,DT,_)|_],
    ( UsedIds = []
    -> % for instance, %i.(i : 1 .. 10|0)
    findall(b(couple(A,Range),couple(DT,RT),[]),
    member(A, LoAsts),
    ComputedSet)
    ; % for instance, %i.(i : 1 .. 10|i + i)
    UsedIds = [LambdaIdName],
    findall(b(couple(A,ComputedRange),couple(DT,RT),[]),
    ( member(A, LoAsts),
    b_compute_expression_nowf(A, [], [], DomValue,'SMT precomputation',0),
    b_compute_expression_nowf(Range, [bind(LambdaIdName,DomValue)], [], Res,'SMT precomputation',0),
    ComputedRange = b(value(Res),RT,[])
    ),
    ComputedSet)
).

compute_inverse([], []).

compute_inverse(List, InvList) :-
    List = [Couple|_],
    get_texpr_type(Couple, CoupleType),
    CoupleType = couple(A,B),
    compute_inverse(couple(B,A), List, [], InvList).

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

compute_inverse(InvCoupleType, [Couple|T], Acc, InvList) :-
    get_elements_of_couple(Couple, A, B),
    compute_inverse(InvCoupleType, T, [b(couple(B,A),InvCoupleType,[])|Acc], InvList).

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

compute_single_cartesian_product(InTypeA, InTypeB, H, [H2|T], Acc, NAcc) :-
    Couple = b(couple(H,H2),couple(InTypeA, InTypeB),[]),
    NAcc1 = [Couple|Acc],
    compute_single_cartesian_product(InTypeA, InTypeB, H, T, NAcc1, NAcc).

construct_set_extension([],Res) :- !, Res=empty_set.

construct_set_extension(List,set_extension(List)).

get_elements_of_couple(b(couple(A,B),_,_), A, B).

get_elements_of_couple(b(value((A,B)),couple(TA,TB),[]), AstA, AstB) :-
    AstA = b(value(A),TA,[]),
    AstB = b(value(B),TB,[]).

is_a_list_of_values([]).

is_a_list_of_values([H|T]) :- is_a_value(H),is_a_list_of_values(T).

is_a_value(b(V,_,_)) :- is_a_value_aux(V).

is_a_value_aux(value(V)) :- ground_value(V).

is_a_value_aux(integer(_)).

is_a_value_aux(boolean_false).

is_a_value_aux(boolean_true).

is_a_value_aux(string(_)).

is_a_value_aux(real(_)).

is_a_value_aux(empty_set).

is_a_value_aux(empty_sequence).

is_a_value_aux(bool_set).

is_a_value_aux(max_int).

is_a_value_aux(min_int).

is_a_value_aux(couple(A,B)) :- is_a_value(A), is_a_value(B).

is_asserted_ground_value(IdName, _, GroundAst) :-
    id_ground_value(_, IdName, TGroundAst),
    !,
    GroundAst = TGroundAst.

is_asserted_ground_value(IdName, EqVals, GroundAst) :-
    % transitive equality
    (id_equality(_, IdName, EqIdName); id_equality(_, EqIdName, IdName)),
    \+ member(EqIdName, EqVals),
    !,
    is_asserted_ground_value(EqIdName, [EqIdName|EqVals], GroundAst).

is_ground_b_value(boolean_false).

is_ground_b_value(boolean_true).

is_ground_b_value(bool_set).

is_ground_b_value(empty_sequence).

is_ground_b_value(empty_set).

is_ground_b_value(integer(_)).

is_ground_b_value(int(_)).

is_ground_b_value(integer_set(_)).

is_ground_b_value(max_int).

is_ground_b_value(min_int).

is_ground_b_value(float_set).

is_ground_b_value(real(_)).

is_ground_b_value(real_set).

is_ground_b_value(string(_)).

is_ground_b_value(string_set).

is_ground_b_value(value(_)).

is_ground_b_value(interval(_,_)).

is_ground_b_value(set_extension(_)).

is_ground_b_value(identifier(EnumId)) :-
    b_get_named_machine_set(_, EnumIds),
    member(EnumId, EnumIds), !.

l_replace_ids_with_eq_ids_top_level([],[]).

l_replace_ids_with_eq_ids_top_level([H|T],[NH|NT]) :-
    replace_ids_with_eq_ids_top_level(H,NH),
    l_replace_ids_with_eq_ids_top_level(T,NT).

l_replace_ids_with_ground_values([],_,_,[]).

l_replace_ids_with_ground_values([H|T],ScopeId,Excl,[NH|NT]) :-
    replace_ids_with_ground_values(H,ScopeId,Excl,NH),
    l_replace_ids_with_ground_values(T,ScopeId,Excl,NT).

no_recursive_computation(set_extension(_)).

no_recursive_computation(sequence_extension(_)).

no_recursive_computation(value(_)).

precompute_values(Ast, Options, AstOpt) :-
    precompute_values3(Ast, [allow_recursive_call|Options], [], AstOpt).

precompute_values3(Ast, Options, ScopeIds, AstOpt) :-
    Ast = b(Expr,Type,Info), !,
    ( precompute_values_e(Expr, Type, Info, Options, ScopeIds, NExpr)
    -> safe_create_texpr(NExpr, Type, Info, AstOpt)
    ; add_internal_error('Call failed: ',precompute_values_e(Expr, Type, Info, Options, ScopeIds, _)),
    AstOpt = Ast
).

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

precompute_values_e(min_int, _, _, _, _, integer(MinInt)) :- !,
    get_preference(minint, MinInt).

precompute_values_e(max_int, _, _, _, _, integer(MaxInt)) :- !,
    get_preference(maxint, MaxInt).

precompute_values_e(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, Res) :-
    member(instantiate_quantifier_limit(L), Options),
    L \== 0,
    instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, TRes),
    ( TRes == truth
    -> Res = truth % no instantiation found, universal quantification is true
    ; precompute_values3(TRes, NOptions, [], b(Res,pred,_)) % TODO: check this, what about ScopeIDs?
).

precompute_values_e(exists(TIDs,LHS), pred, Info, Options, ScopeIds, Res) :-
    member(instantiate_quantifier_limit(L), Options),
    L \== 0,
    instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, TRes),
    ( TRes == falsity
    -> Res = falsity % no instantiation found, existential quantification is false
    ; precompute_values3(TRes, NOptions, [], b(Res,pred,_)) % TODO: check this, what about ScopeIDs?
).

precompute_values_e(comprehension_set([Id,LambdaRes],Body), _, _, Options, ScopeIds, SetExtension) :-
    % e.g., %(i : 1..3|0)
    LambdaRes = b(identifier('_lambda_result_'),_,_),
    Body = b(conjunct(Member,LambdaEq),pred,_),
    remove_all_infos(Id, CId),
    remove_all_infos(LambdaRes, CLambdaRes),
    Member = b(member(CId,Domain),pred,_),
    LambdaEq = b(equal(CLambdaRes,RangeVal),pred,_),
    compute_ground_lambda(Id, Domain, RangeVal, ScopeIds, Options, ComputedSet),
    !,
    construct_set_extension(ComputedSet,SetExtension).

precompute_values_e(interval(A,B), _, _, Options, ScopeIds, SetExtension) :-
    rewrite_set_to_list_of_asts(b(interval(A,B),set(integer),[]), ScopeIds, Options, List),
    !,
    construct_set_extension(List,SetExtension).

precompute_values_e(Pow, _, _, Options, ScopeIds, Precomputed) :-
    SetAst = b(set_extension(List),set(Type),[]),
    ( Pow = pow_subset(Arg),
    PowAst = b(pow_subset(SetAst),set(set(Type)),[])
    ; Pow = pow1_subset(Arg),
    PowAst = b(pow1_subset(SetAst),set(set(Type)),[])
    ),
    rewrite_set_to_list_of_asts(Arg, ScopeIds, Options, List),
    is_a_list_of_values(List),
    length(List, Len),
    ( Pow = pow_subset(Arg)
    -> PowCard is 2**Len
    ; PowCard is 2**Len - 1
    ),
    ( member(instantiate_sets_limit(SetLimit), Options)
    -> PowCard =< SetLimit
    ; true
    ),
    List = [b(_,Type,_)|_],
    !,
    b_compute_expression_nowf(PowAst, [], [], TPrecomputedVal,'SMT precomputation',0),
    normalise_value_for_var(solver_result, force, TPrecomputedVal, PrecomputedVal),
    Precomputed = value(PrecomputedVal).

precompute_values_e(reverse(Arg), _, _, Options, ScopeIds, SetExtension) :-
    rewrite_set_to_list_of_asts(Arg, ScopeIds, Options, List),
    is_a_list_of_values(List),
    compute_inverse(List, InvList),
    !,
    construct_set_extension(InvList,SetExtension).

precompute_values_e(cartesian_product(SetA,SetB), _, _, Options, ScopeIds, SetExtension) :-
    rewrite_set_to_list_of_asts(SetA, ScopeIds, Options, ListA),
    rewrite_set_to_list_of_asts(SetB, ScopeIds, Options, ListB),
    get_texpr_type(SetA, set(InTypeA)),
    get_texpr_type(SetB, set(InTypeB)),
    compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, CartList),
    !,
    construct_set_extension(CartList,SetExtension).

precompute_values_e(BOP, _Type, _Info, Options, ScopeIds, Res) :-
    binary_connective(BOP,F,A,B),
    !,
    binary_connective(Res,F,NA,NB),
    precompute_values_non_recursive(Options, ScopeIds, A, NA),
    precompute_values_non_recursive(Options, ScopeIds, B, NB). % we ignore allow_recursive_call option; all optimisations are local

precompute_values_e(Expr, Type, Info, Options, ScopeIds, Res) :-
    syntaxtransformation(Expr, Subs, Names, NSubs, NExpr),
    ( Names \= []
    -> maplist(get_texpr_id, Names, IdNames),
    append(IdNames, ScopeIds, NScopeIds)
    ; NScopeIds = ScopeIds),
    !,
    maplist(precompute_values_non_recursive(Options, NScopeIds), Subs, NSubs),
    ( ( select(allow_recursive_call, Options, Options2),
    \+ no_recursive_computation(NExpr)
    )
    -> precompute_values_e(NExpr, Type, Info, Options2, NScopeIds, Res) % Warning: this can cause a quadratic processing time !
    ; Res = NExpr
).

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

precompute_values_non_recursive(Options, Ast, AstOpt) :-
    precompute_values_non_recursive(Options, [], Ast, AstOpt).

precompute_values_non_recursive(Options, ScopeIds, Ast, AstOpt) :-
    precompute_values3(Ast, Options, ScopeIds, AstOpt).

replace_ids_with_eq_ids_top_level(Pred, NPred) :-
    Pred = b(Expr,Type,Info),
    replace_ids_with_eq_ids_top_level_e(Expr, NExpr),
    NPred = b(NExpr,Type,Info).

replace_ids_with_eq_ids_top_level_e(identifier(IdName), NExpr) :-
    findall(A-B-C, id_equality(A,B,C), _),
    (id_equality(0, IdName, EqIdName); id_equality(0, EqIdName, IdName)),
    NExpr = identifier(EqIdName).

replace_ids_with_eq_ids_top_level_e(negation(TExpr), NExpr) :-
    !,
    replace_ids_with_eq_ids_top_level(TExpr, NTExpr),
    NExpr = negation(NTExpr).

replace_ids_with_eq_ids_top_level_e(Expr, NExpr) :-
    Expr \= identifier(_),
    syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
    !,
    l_replace_ids_with_eq_ids_top_level(Subs,NSubs).

replace_ids_with_eq_ids_top_level_e(Expr, Expr) :-
    Expr \= identifier(_).

replace_ids_with_ground_values(Ast, ScopeId, ExcludeScopeIds, AstOpt) :-
    Ast = b(Expr,Type,Info),
    \+ member(do_not_optimize_away, Info),
    !,
    replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr),
    AstOpt = b(NExpr,Type,Info).

replace_ids_with_ground_values(A, _, _, A).

replace_ids_with_ground_values_e(identifier(IdName), _, ExcludeScopeIds, NExpr) :-
    is_asserted_ground_value(IdName, [], GroundAst),
    !,
    ( \+ member(b(identifier(IdName),_,_), ExcludeScopeIds)
    -> get_texpr_expr(GroundAst, NExpr)
    ; NExpr = identifier(IdName)
).

replace_ids_with_ground_values_e(Eq, _, _, NEq) :-
    % do not remove ground equality since this will be the last occurrence of the variable
    ( Eq = equal(Id,GroundValOrId)
    ; Eq = equal(GroundValOrId,Id)
    ),
    ( Id = b(identifier(_),_,_),
    get_texpr_expr(GroundValOrId, GroundExpr),
    is_ground_b_value(GroundExpr)
    ; id_equality(_, Id, GroundValOrId)
    ; id_equality(_, GroundValOrId, Id)
    ),
    !,
    NEq = Eq.

replace_ids_with_ground_values_e(equal(Id1,Id2), _, ExcludeScopeIds, NEq) :-
    Id1 = b(identifier(IdName1),Type,_),
    Id2 = b(identifier(IdName2),Type,_),
    ( id_ground_value(_, IdName1, GroundAst1),
    \+ member(b(identifier(IdName1),Type,_), ExcludeScopeIds)
    -> NArg1 = GroundAst1
    ; NArg1 = Id1
    ),
    ( id_ground_value(_, IdName2, GroundAst2),
    \+ member(b(identifier(IdName2),Type,_), ExcludeScopeIds)
    -> NArg2 = GroundAst2
    ; NArg2 = Id2
    ),
    !,
    NEq = equal(NArg1,NArg2).

replace_ids_with_ground_values_e(set_extension([Id]), _, ExcludeScopeIds, NUnary) :-
    Id = b(identifier(IdName),_,_),
    \+ member(b(identifier(IdName),_,_), ExcludeScopeIds),
    !,
    ( id_ground_value(_, IdName, GroundVal)
    -> NUnary = set_extension([GroundVal])
    ; NUnary = set_extension([Id])
).

replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
    functor(Expr, Functor, 2),
    ( Functor = implication
    ; Functor = disjunct
    ),
    arg(1, Expr, Arg1),
    arg(2, Expr, Arg2),
    !,
    NScopeId is ScopeId + 1,
    assert_ground_id_values(NScopeId, Arg1),
    replace_ids_with_ground_values(Arg1, NScopeId, ExcludeScopeIds, NArg1),
    retract_ground_id_values_for_scope(NScopeId),
    assert_ground_id_values(NScopeId, Arg2),
    replace_ids_with_ground_values(Arg2, NScopeId, ExcludeScopeIds, NArg2),
    retract_ground_id_values_for_scope(NScopeId),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, NArg1),
    arg(2, NExpr, NArg2).

replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
    functor(Expr, Functor, 2),
    ( Functor = conjunct
    ; Functor = equivalence
    ),
    arg(1, Expr, Arg1),
    arg(2, Expr, Arg2),
    !,
    % ground ids already asserted for top-level conjunction
    replace_ids_with_ground_values(Arg1, ScopeId, ExcludeScopeIds, NArg1),
    replace_ids_with_ground_values(Arg2, ScopeId, ExcludeScopeIds, NArg2),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, NArg1),
    arg(2, NExpr, NArg2).

replace_ids_with_ground_values_e(negation(Pred), ScopeId, ExcludeScopeIds, NNeg) :-
    !,
    NScopeId is ScopeId + 1,
    assert_ground_id_values(NScopeId, Pred),
    replace_ids_with_ground_values(Pred, NScopeId, ExcludeScopeIds, NPred),
    retract_ground_id_values_for_scope(NScopeId),
    NNeg = negation(NPred).

replace_ids_with_ground_values_e(forall(Ids,Lhs,Rhs), ScopeId, ExcludeScopeIds, NForall) :-
    !,
    append(ExcludeScopeIds, Ids, NExcludeScopeIds),
    replace_ids_with_ground_values(Lhs, ScopeId, NExcludeScopeIds, NLhs),
    NScopeId is ScopeId + 1,
    assert_ground_id_values(NScopeId, Rhs),
    replace_ids_with_ground_values(Rhs, NScopeId, NExcludeScopeIds, NRhs),
    retract_ground_id_values_for_scope(NScopeId),
    NForall = forall(Ids,NLhs,NRhs).

replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
    functor(Expr, Functor, 2),
    ( Functor = exists
    ; Functor = comprehension_set
    ; Functor = lambda
    ; Functor = general_sum
    ; Functor = general_product
    ; Functor = quantified_union
    ; Functor = quantified_intersection
    ; Functor = event_b_comprehension_set
    ),
    !,
    arg(1, Expr, Ids),
    arg(2, Expr, Pred),
    NScopeId is ScopeId + 1,
    assert_ground_id_values(NScopeId, Pred),
    append(ExcludeScopeIds, Ids, NExcludeScopeIds),
    replace_ids_with_ground_values(Pred, NScopeId, NExcludeScopeIds, NPred),
    retract_ground_id_values_for_scope(NScopeId),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, Ids),
    arg(2, NExpr, NPred).

replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds,NExpr) :-
    syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
    !,
    append(Names, ExcludeScopeIds, NExcludeScopeIds),
    l_replace_ids_with_ground_values(Subs,ScopeId,NExcludeScopeIds,NSubs).

replace_ids_with_ground_values_e(Expr, _, _, Expr).

reset_optimizer_state :-
    retractall(id_ground_value(_,_,_)),
    retractall(id_equality(_,_,_)).

retract_ground_id_values_for_scope(ScopeId) :-
    retractall(id_ground_value(ScopeId,_,_)),
    retractall(id_equality(ScopeId,_,_)).