dev.pl

bast(RawString, BAst) :-
    bast(RawString, _, BAst).

bast(RawString, UntypedAst, BAst) :-
    atom_codes(RawString, RawCodes),
    parsercall:parse_formula(RawCodes, UntypedAst),
    btypechecker:env_empty(Env),
    btypechecker:btype_ground([UntypedAst], Env, [], _, [BAst], _).

bcompile(Ast, Compiled) :-
    find_identifier_uses(Ast, [], UsedIds),
    temporary_set_preference(data_validation_mode, true),
    b_compile(Ast, UsedIds, [], [], Compiled, no_wf_available),
    reset_temporary_preference(data_validation_mode).

check_fuzz(Ast, CleanWd) :-
    banditfuzz:report_ast(Ast),
    clean_up_pred(Ast, [], CNewPred),
    welldef:ensure_wd(CNewPred, WdPred),
    banditfuzz:report_ast('Ensured WD', WdPred),
    clean_up_pred(WdPred, [], CleanWd),
    banditfuzz:report_ast('Cleaned', CleanWd),
    !,
    report_validity(CleanWd),
    report_wd_problems(CleanWd).

check_wd_enforcement(PredString) :-
    bast(PredString, BAst),
    wd_clean_pred(BAst, _).

fuzz_list(0, _) :- !.

fuzz_list(N, Options) :-
    error_manager:enter_new_error_scope(Scope),
    ( bf_env:env(Options, Env),
    fuzz_conjuncts(Env, _, BExpr),
    % Prepare and make WD
    clean_up_pred(BExpr, [], CNewPred),
    welldef:ensure_wd(CNewPred, WdPred),
    clean_up_pred(WdPred, [], CleanWd),
    % Prepare printing
    set_print_type_infos(all),
    find_typed_identifier_uses(CleanWd, Ids),
    add_normal_typing_predicates(Ids, CleanWd, FullyTypedAst),
    print_bexpr(FullyTypedAst)
    ; true
    ),
    error_manager:exit_error_scope(Scope, _),
    format('~n', []),
    N1 is N - 1,
    fuzz_list(N1, Options).

fuzz_or_mute(Options, Ast) :-
    bf_env:env(Options, Env),
    fuzz_conjuncts(4, Env, FuzzEnv, Fuzz),
    write('Fuzzing initial pred...'), nl,
    check_fuzz(Fuzz, _),
    % Find random node.
    allowed_expressions(Env, AllowedExpr),
    allowed_predicates(Env, AllowedPreds),
    allowed_leafs(Env, AllowedLeafs),
    append(AllowedExpr, AllowedPreds, AllowedInnerNodes),
    append(AllowedLeafs, AllowedInnerNodes, AllowedNodes),
    random:random_member(Node:_, AllowedNodes),
    Node =.. [Name|_],
    format('Mutating with ~q~n', [Name]),
    mutations:fuzz_or_mutate(Fuzz, Name, FuzzEnv, _, Ast).

fuzz_test(0, _) :- !.

fuzz_test(N, Options) :-
    getrand(Rand),
    format('~w samples left~nRandom state: ~w~n', [N, Rand]),
    error_manager:enter_new_error_scope(Scope),
    ( bf_env:env(Options, Env),
    fuzz_conjuncts(Env, _, BExpr),
    check_fuzz(BExpr, _)
    ; format('! Failed to generate a valid B expression.~n', [])
    ),
    error_manager:exit_error_scope(Scope, ErrorOccured),
    (ErrorOccured -> write('! Errors outside of check_ast/1 occured'), nl; true),
    format('Rerun with: setrand(~w), fuzz_test(1, ~w).~n', [Rand, Options]),
    format('---~n', []),
    N1 is N - 1,
    fuzz_test(N1, Options).

mutation_test(0, _) :- !.

mutation_test(N, Options) :-
    getrand(Rand),
    format('~w samples left~nRandom state: ~w~n', [N, Rand]),
    error_manager:enter_new_error_scope(Scope),
    (fuzz_or_mute(Options, BExpr),
    check_fuzz(BExpr, _)
    ; format('! Failed to generate a valid B expression.~n', [])
    ),
    error_manager:exit_error_scope(Scope, ErrorOccured),
    (ErrorOccured -> write('! Errors outside of check_ast/1 occured'), nl; true),
    format('Rerun with: setrand(~w), mutation_test(1, ~w).~n', [Rand, Options]),
    format('---~n', []),
    N1 is N - 1,
    mutation_test(N1, Options).

no_contradictions(_, _, [], []).

no_contradictions(V, Solver, [V2 | Rs], [Other | Rest]) :-
    solvercalls:contradiction(V, V2),
    format('! CONTRADICTION FOUND:~n', []),
    format('! ~w: ~w~n', [Solver, V]),
    format('! ~w: ~w~n', [Other, V2]),
    no_contradictions(V, Solver, Rs, Rest).

no_contradictions(V, Solver, [_ | Rs], [_ | Rest]) :-
    no_contradictions(V, Solver, Rs, Rest).

redo_with(new, _, _, ResPred) :-
    bf_env:env(E), % empty environment is not realistic but only impacts IDs anyway.
    fuzz(4, pred, E, _, ResPred).

redo_with(mutate, Inner, Ast, ResPred) :-
    bf_env:env(E), % empty environment is not realistic but only impacts IDs anyway.
    fuzz_or_mutate(Ast, Inner, E, _, ResPred).

redo_with(Seed, Outer, Inner, Ast, Result) :-
    setrand(Seed),
    redo_with(Outer, Inner, Ast, Raw),
    banditfuzz:wd_clean_report_pred(Raw, Result).

replay_mutations([], Result, _, Result).

replay_mutations([Mut-Seed | Mutations], Ast, Env, Result) :-
    setrand(Seed),
    fuzz_or_mutate(Ast, Mut, Env, NextEnv, NextPred),
    wd_clean_pred(NextPred, Clean),
    replay_mutations(Mutations, Clean, NextEnv, Result).

replay_with(InitialSeed, MutationSequence, Result) :-
    setrand(InitialSeed),
    bf_env:env(E),
    fuzz(4, pred, E, Env, InitialPred),
    wd_clean_pred(InitialPred, Clean),
    replay_mutations(MutationSequence, Clean, Env, Result).

report_validity(Ast) :-
    report_validity(Ast, _).

report_validity(Ast, valid) :-
    banditfuzz:valid_ast(Ast),
    !,
    write('Ast passes through check_ast/1'), nl.

report_validity(_, invalid) :-
    write('! Ast rejected by check_ast/1'), nl.

report_wd_problems(Ast) :-
    analyse_wd_for_expr(Ast, _, Res),
    Res == 'TRUE', !,
    write('AST is WD (passes through well_def_analyser/3)'), nl.

report_wd_problems(_) :-
    write('! Ast is not WD (rejected by well_def_analyser/3)'), nl.

single_solve(Solver-Options, Ast, Result, Time) :-
    format('Solving with ~w-~q~n', [Solver, Options]),
    solvercalls:solve_timed(Solver, Options, Ast, Result, Time),
    format('Solving result=~w, time=~w~n', [Result, Time]),
    !.

single_solve(_-_, _, error, -1) :-
    format('Solving of predicate failed.~n', []).

solve_bexpr(Solvers, Ast) :-
    solve_bexpr(Solvers, Ast, Results),
    validate_results(Results, Solvers).

solve_bexpr([], _, []).

solve_bexpr([Solver | Solvers], Ast, [Result | Results]) :-
    single_solve(Solver, Ast, Result, _),
    solve_bexpr(Solvers, Ast, Results).

solver_test(0, _, _) :- !, write('Done.'), nl.

solver_test(N, Solvers, Options) :-
    %preferences:set_preference(trace_upon_error,true),
    getrand(Rand),
    format('~w samples left~nRandom state: ~w~n', [N, Rand]),
    error_manager:enter_new_error_scope(Scope),
    ( bf_env:env(Env),
    fuzz(4, pred, Env, _, BExpr),
    check_fuzz(BExpr, CleanWd),
    solve_bexpr(Solvers, CleanWd)
    ; format('! Failed to generate a valid B expression.~n', [])
    ),
    error_manager:exit_error_scope(Scope, ErrorOccured),
    (ErrorOccured -> write('! Errors outside of check_ast/1 occured'), nl; true),
    format('Rerun with: setrand(~w), solver_test(1, ~q, ~w).~n', [Rand, Solvers, Options]),
    format('---~n', []),
    N1 is N - 1,
    solver_test(N1, Solvers, Options).

validate_results([], []).

validate_results([Res | Results], [Solver | Solvers]) :-
    no_contradictions(Res, Solver, Results, Solvers),
    validate_results(Results, Solvers).

wd_clean_pred(NewPred, ResPred) :-
    clean_up_pred(NewPred, [], CNewPred),
    ensure_wd(CNewPred, WdPred),
    clean_up_pred(WdPred, [], ResPred),
    banditfuzz:report_ast('Cleaned', ResPred).