bf_env

add_all_ids(Env, [], Env) :- !.

add_all_ids(Env, [Id:Type|Ids], NewEnv) :-
    add_id_use(Env, Id, Type, InterEnv),
    add_all_ids(InterEnv, Ids, NewEnv).

add_id_use(Env, Name, Type, NewEnv) :-
    Env = env(A1, A2, Local-Global, C),
    NewEnv = env(A1, A2, Local-[Name:Type | Global], C).

add_option(Option, Env, NewEnv) :-
    Option =.. [Key, Value], !,
    add_option(Key, Value, Env, NewEnv).

add_option(Option, Env, NewEnv) :-
    Option =.. [Key], !,
    supported_option(Key, Default),
    member(Default, [true, false]),
    add_option(Key, true, Env, NewEnv)
    ;
    format_error('Option ~w is not boolean but no value supplied.~n', [Key]),
    fail.

add_option(Option, Env, NewEnv) :-
    Option =.. [Key | Values], !,
    add_option(Key, Values, Env, NewEnv).

add_option(Key, Value, env(A, B, C, Ops), env(A, B, C, NewOps)) :-
    supported_option(Key, Default),
    verify_value_match(Value, Default), !,
    avl:avl_store(Key, Ops, Value, NewOps).

add_option(Key, Value, _, _) :-
    supported_option(Key, _), !,
    warn_wrong_value_type(Key, Value),
    fail.

add_option(Key, _, _, _) :-
    format_error('! BF env: Unrecognized Option \'~w\'.', [Key]),
    fail.

allowed_expressions(env(_, [_, Allowed], _, _), AllowedCopy) :-
    % Need to copy term. Otherwise, if user binds variables in the allowed list, it pollutes the OG data.
    bi_copy_term(Allowed, AllowedCopy).

allowed_leafs(env(Allowed, _, _, _), AllowedCopy) :-
    % Need to copy term. Otherwise, if user binds variables in the allowed list, it pollutes the OG data.
    bi_copy_term(Allowed, AllowedCopy).

allowed_leafs(Env, Type, Allowed) :-
    allowed_leafs(Env, Leafs),
    findall(Ex:T, (member(Ex:T, Leafs), T = Type), Allowed).

allowed_nodes(Env, Type, Allowed) :-
    % Special case for predicates.
    Type == pred, !, % May not unify any unbound variables.
    allowed_predicates(Env, Allowed).

allowed_nodes(Env, Type, Allowed) :-
    allowed_expressions(Env, NonLeafs),
    findall(Ex:T,
    % Need to filter out cases where result will be cyclic term.
    (member(Ex:T, NonLeafs), T = Type, acyclic_term(T)),
    Allowed).

allowed_predicates(env(_, [Allowed, _], _, _), AllowedCopy) :-
    % Need to copy term. Otherwise, if user binds variables in the allowed list, it pollutes the OG data.
    bi_copy_term(Allowed, AllowedCopy).

apply_dependent_option(conjuncts_min(Min), ToSet, Env, NewEnv) :-
    processed_value(conjuncts_max, ToSet, Env, Max, Setter), Max < Min, !,
    format_error('! BF env: conjuncts_min(~w) > conjuncts_max(~w) (set by ~w). Updating Max to ~w.~n',
    [Min, Max, Setter, Min]),
    add_option(conjuncts_max(Min), Env, NewEnv).

apply_dependent_option(conjuncts_max(Max), ToSet, Env, NewEnv) :-
    processed_value(conjuncts_min, ToSet, Env, Min, Setter), Min > Max, !,
    format_error('! BF env: conjuncts_max(~w) < conjuncts_min(~w) (set by ~w). Updating Min to ~w.~n',
    [Max, Min, Setter, Max]),
    add_option(conjuncts_min(Max), Env, NewEnv).

apply_dependent_option(list_min(Min), ToSet, Env, NewEnv) :-
    processed_value(list_max, ToSet, Env, Max, Setter), Max < Min, !,
    format_error('! BF env: list_min(~w) > list_max(~w) (set by ~w). Updating Max to ~w.~n', [Min, Max, Setter, Min]),
    add_option(list_max(Min), Env, NewEnv).

apply_dependent_option(list_max(Max), ToSet, Env, NewEnv) :-
    processed_value(list_min, ToSet, Env, Min, Setter), Min > Max, !,
    format_error('! BF env: list_max(~w) < list_min(~w) (set by ~w). Updating Min to ~w.~n', [Max, Min, Setter, Max]),
    add_option(list_min(Max), Env, NewEnv).

apply_dependent_option(cnf, ToSet, Env, NewEnv) :-
    predicted_value(sat_only, ToSet, Env, false, Setter), !,
    (Setter = default
    -> format_error('! BF env: cnf(true) implicitly sets sat_only(true).~n', [])
    ; format_error('! BF env: Failed to set cnf(true). Requires sat_only(true) but was set to false by user.~n', []),
    fail
    ),
    apply_option(sat_only, Env, NewEnv).

apply_dependent_option(_, _, E, E).

apply_option(O, Env, Res) :-
    transform_if_needed(O, Env, Inter),
    add_option(O, Inter, Res).

apply_options([], E, E).

apply_options([O | Os], Env, ResEnv) :-
    apply_dependent_option(O, Os, Env, Dependent),
    apply_option(O, Dependent, Inter),
    apply_options(Os, Inter, ResEnv).

bi_copy_term(T1, T2) :-
    var(T1), !,
    copy_term(T2, T1).

bi_copy_term(T1, T2) :-
    copy_term(T1, T2).

clean_copy(env(A, B, _, C), env(A, B, []-[], C)).

delete_any([], _, []).

delete_any([D | Ds], Elem, Res) :-
    \+ \+ D = Elem, !, % Check if they would unify without actually unifying.
    delete_any(Ds, Elem, Res).

delete_any([D | Ds], Elem, [D | Res]) :-
    delete_any(Ds, Elem, Res).

disallow_node(Signature:Type, Env, NewEnv) :-
    !,
    Node = Signature:Type,
    allowed_leafs(Env, Leaves),
    allowed_predicates(Env, Preds),
    allowed_expressions(Env, Exprs),
    delete_any(Leaves, Node, RemLeaves),
    delete_any(Preds, Node, RemPreds),
    delete_any(Exprs, Node, RemExprs),
    with_leafs(Env, RemLeaves, Env2),
    with_predicates(Env2, RemPreds, Env3),
    with_expressions(Env3, RemExprs, NewEnv).

disallow_node(NodeName, Env, NewEnv) :-
    atom(NodeName), !,
    node_by_name(NodeName, Node),
    disallow_node(Node, Env, NewEnv).

disallow_node(Node, Env, NewEnv) :-
    % Node is a compound like `equals(A, A)`.
    has_type(Node, Type),
    disallow_node(Node:Type, Env, NewEnv).

disallow_nodes([], Env, Env).

disallow_nodes([N|Ns], Env, NewEnv) :-
    disallow_node(N, Env, InterEnv),
    disallow_nodes(Ns, InterEnv, NewEnv).

empty_id_scopes(env(_, _, []-[], _)).

env(Options, FinalEnv) :-
    findall(Expr:Type, fuzztypes:has_type(Expr, Type), Allowed),
    %% Split allowed AST nodes into leafs and non-leaves based on arity.
    findall(Ex:T, (member(Ex:T, Allowed), Ex =.. [_]), AllowedLeafs), % [_] forces arity 0.
    findall(Ex:T, (member(Ex:T, Allowed), Ex =.. [_,_|_]), AllowedNodes), % [_,_|_] forces arity >= 1.
    % Note: Need to add value types to the leafs as well.
    % We do that by adding Type:Type constructs.
    % Booleans are already covered by boolean_true:boolean and
    % boolean_false:boolean, so boolean:boolean is unnecessary.
    AllowedLeafsWithTypes = [integer:integer, real:real, string:string
    |AllowedLeafs],
    % We need to differentiate between predicates and expression.
    % Some expression only have a variable as type, allowing them to by any type.
    % Hence, we need to differentiate them from real predicates, as otherwise
    % they might unify rather faulty.
    split_preds_and_exprs(AllowedNodes, Preds, Exprs),
    allowed_leafs(Env, AllowedLeafsWithTypes),
    allowed_expressions(Env, Exprs),
    allowed_predicates(Env, Preds),
    empty_id_scopes(Env),
    with_empty_options(Env, Env2),
    apply_options(Options, Env2, FinalEnv), % See below.
    !.

env(Env) :-
    env([], Env).

has_option(Key, env(_, _, _, Options)) :-
    has_option(Key, env(_, _, _, Options), _).

has_option(Key, env(_, _, _, Options), Value) :-
    avl:avl_member(Key, Options, Value), !,
    Value \== false.

has_option(Key, _, Value) :-
    % Use default value.
    supported_option(Key, Default),
    Default \== false -> Value = Default.

leave_local_id_scope(env(A, B, []-Ids, C), env(A, B, []-Ids, C)).

leave_local_id_scope(env(A, B, [_|Ss]-Ids, C), env(A, B, Ss-Ids, C)).

new_id_probability(Env, Proba) :-
    has_option(new_id_proba, Env, Proba).

option_set_by_user(Key, env(_, _, _, Options), Value) :-
    % Check if option was set by user.
    avl:avl_member(Key, Options, Value), !.

predicted_value(OptionName, _, Env, Value, user) :-
    option_set_by_user(OptionName, Env, Value), !.

predicted_value(OptionName, ToSet, _, Value, user) :-
    member(FutureOption, ToSet),
    (FutureOption =.. [OptionName, Value]
    ; FutureOption =.. [OptionName], Value=true), !.

predicted_value(OptionName, _, _, Value, default) :-
    supported_option(OptionName, Value).

processed_value(OptionName, _, Env, Value, user) :-
    option_set_by_user(OptionName, Env, Value), !.

processed_value(OptionName, ToSet, _, Value, user) :-
    member(FutureOption, ToSet),
    (FutureOption =.. [OptionName, Value]
    ; FutureOption =.. [OptionName], Value=true), !, fail.

processed_value(OptionName, _, _, Value, default) :-
    supported_option(OptionName, Value).

real_node(less_equal_real(real,real), pred).

real_node(less_real(real,real), pred).

real_node(real_set, set(real)).

real_node(convert_real(integer), real).

real_node(convert_int_floor(real), integer).

real_node(convert_int_ceiling(real), integer).

real_node(add_real(real,real), real).

real_node(minus_real(real,real), real).

real_node(unary_minus_real(real), real).

real_node(multiplication_real(real,real), real).

real_node(div_real(real,real), real).

real_node(power_of_real(real,real), real).

real_node(max_real(set(real)), real).

real_node(min_real(set(real)), real).

real_node(general_sum(ids,pred,real), real).

real_node(general_product(ids,pred,real), real).

split_preds_and_exprs([], [], []).

split_preds_and_exprs([Ex:T|L], [Ex:T | Preds], Exprs) :-
    T == pred, !,
    split_preds_and_exprs(L, Preds, Exprs).

split_preds_and_exprs([Ex:T|L], Preds, [Ex:T | Exprs]) :-
    split_preds_and_exprs(L, Preds, Exprs).

supported_option(z3safe, false).

supported_option(size, 4). % Fuzzed AST depth.

supported_option(list_min, 1). % Minimum number of elements in a generated list.

supported_option(list_max, 4). % Maximum number of elements in a generated list.

supported_option(min_int, 0). % Minimum integer fuzzed. Also affects integer part of reals.

supported_option(max_int, 100). % Maximum integer fuzzed. Also affects integer part of reals.

supported_option(new_id_proba, 0.2). % Chance that a new identifier is introduced instead of reusing an old one.

supported_option(solutions_only, false). % BanditFuzz will ignore any calls resulting in timeouts or errors.

supported_option(min_one_solution, false). % BanditFuzz will ignore any calls no solver was able to solve.

supported_option(samp_size, 3). % Number of measurements taken per solver; average result will be used.

supported_option(port, 44644). % Port number for Prothon.

supported_option(conjuncts_min, 1). % Minimum number of conjuncts fuzzed.

supported_option(conjuncts_max, 1). % Maximum number of conjuncts fuzzed.

supported_option(use_reals, true). % Whether to make use of real numbers.

supported_option(use_strings, false). % Whether to make use of strings.

supported_option(sat_only, false). % Whether to only fuzz SAT formulae, i.e. only boolean variables. Implies use_reals(false) and use_strings(false).

supported_option(cnf, false). % Fuzzes only CNF formulae. Implies sat_only(true).

supported_option(var_max, none). % Maximum number of (top level) variables in a formula. If none, no limit is set.

transform_if_needed(z3safe, Env, Res) :- !,
    %% Only allow nodes for which a translation to SMT_LIB is supported.
    findall(Nogo:_, z3_unsupported_translation(Nogo), Z3Nogos),
    disallow_nodes(Z3Nogos, Env, Res).

transform_if_needed(use_reals(false), Env, Res) :- !,
    findall(Node:Type, real_node(Node, Type), RealNodes),
    disallow_nodes(RealNodes, Env, Res).

transform_if_needed(use_strings(false), Env, Res) :- !,
    disallow_node(string_set:set(string), Env, Res).

transform_if_needed(sat_only, Env, Res) :- !,
    with_leafs(Env, [boolean_true:boolean, boolean_false:boolean], BoolVars),
    with_expressions(BoolVars, [], BoolExprs),
    with_predicates(BoolExprs, [
    conjunct(pred,pred):pred,
    disjunct(pred,pred):pred,
    equal(boolean,boolean):pred
    ], Res).

transform_if_needed(cnf, Env, Res) :- !,
    with_predicates(Env, [
    disjunct(pred,pred):pred,
    equal(boolean,boolean):pred
    ], Res).

transform_if_needed(_, Env, Env).

used_ids(Env, Ids) :-
    var(Env), !,
    Env = env(_, _, []-Ids, _).

used_ids(env(_, _, Locals-Globals, _), Ids) :-
    append([Globals | Locals], Ids).

var_max_reached(Env) :-
    has_option(var_max, Env, Max),
    Max \== none, !,
    Env = env(_, _, _-Ids, _),
    length(Ids, Len),
    Len >= Max.

verify_value_match(true, Default) :- !, member(Default, [true, false]).

verify_value_match(false, Default) :- !, member(Default, [true, false]).

verify_value_match(_, Default) :- !, \+ member(Default, [true, false]).

warn_wrong_value_type(Key, Val) :-
    member(Val, [true, false]), !,
    format_error('! BF env: Option ~w is not boolean but received value ~w~n', [Key, Val]).

warn_wrong_value_type(Key, Val) :-
    format_error('! BF env: Option ~w is boolean but received value ~w~n', [Key, Val]).

with_empty_options(env(A, B, C, _), env(A, B, C, Ops)) :-
    avl:empty_avl(Ops).

with_expressions(env(A, [Preds, _], B, C), Exprs, env(A, [Preds, Exprs], B, C)).

with_id_probability(Env, Proba, NewEnv) :-
    add_option(new_id_proba(Proba), Env, NewEnv).

with_leafs(env(_, A, B, C), Leafs, env(Leafs, A, B, C)).

with_local_ids(env(A, B, L-Ids, C), NewIds, env(A, B, [NewIds|L]-Ids, C)).

with_predicates(env(A, [_, Exprs], B, C), Preds, env(A, [Preds, Exprs], B, C)).

z3_unsupported_translation(closure(_)).

z3_unsupported_translation(reflexive_closure(_)).

z3_unsupported_translation(general_concat(_)).

z3_unsupported_translation(general_product(_,_,_)).

z3_unsupported_translation(general_sum(_,_,_)).

z3_unsupported_translation(iteration(_,_)).

z3_unsupported_translation(power_of_real(_,_)).

z3_unsupported_translation(struct(_)).

z3_unsupported_translation(mu(_)).