bf_runner

call_generate(b(RootNode,pred,[])) :-
    TwoSubPreds = [conjunct,disjunct,implication,equivalence],
    IntToPred = [less_equal,less,greater_equal,greater],
    SetToPred = [subset,subset_strict,not_subset,not_subset_strict],
    SeqToPred = [equal,not_equal],
    random_member(RootExpr, TwoSubPreds),
    random_member(LeftExpr, TwoSubPreds),
    random_member(RightExpr, TwoSubPreds),
    random_member(IntExpr, IntToPred),
    random_member(SetExpr, SetToPred),
    random_member(SeqExpr, SeqToPred),
    generate(prob_ast_pred([alph]), PredAST),
    generate(prob_ast_pred(SeqExpr,[alph,equal_seq]), SeqAST),
    generate(prob_ast_pred(IntExpr,[alph]), IntAST),
    generate(prob_ast_pred(SetExpr,[alph]), SetAST),
    LeftNode =.. [LeftExpr, PredAST, SeqAST],
    LeftAST =.. [b, LeftNode, pred, []],
    RightNode =.. [RightExpr, IntAST, SetAST],
    RightAST =.. [b, RightNode, pred, []],
    RootNode =.. [RootExpr, LeftAST, RightAST].

call_mutate(GrammarExpr, GrammarType, OldAST, MutationCancelled, AST) :-
    findall(A, mutate(GrammarExpr, GrammarType, OldAST, A), All_ASTs),
    (All_ASTs == []
    -> MutationCancelled = true,
    AST = none
    ; random_member(AST, All_ASTs)).

run_banditfuzz_iteration(SolverList, Operation, GrammarExpr, GrammarType, TimeOutValue, OldAST, TimePerSolver) :-
    TimeOutValue > 0,
    getrand(Seed),
    format(user_error,'Start BanditFuzz with seed ~w~n',[Seed]),
    (Operation == mutate
    -> call_mutate(GrammarExpr, GrammarType, OldAST, MutationCancelled, AST)
    ; call_generate(AST)),
    (MutationCancelled == true
    -> TimePerSolver = []
    ; time_per_solver(AST, SolverList, TimeOutValue, TimePerSolver)),
    %print_bexpr_stream(user_error, AST),
    translate_bexpression(AST, Pretty),
    format(user_error,'~nAST for Python = ~q~nPretty Printed = ~q~n', [AST, Pretty]).

run_banditfuzz_iteration(SolverList, Operation, GrammarExpr, GrammarType, TimeOutValue, OldAST, TimePerSolver, Seed) :-
    setrand(Seed),
    format(user_error,'Set seed ~w~n',[Seed]),
    run_banditfuzz_iteration(SolverList, Operation, GrammarExpr, GrammarType, TimeOutValue, OldAST, TimePerSolver).

test(call_mutate, [nondet]) :-
    call_mutate(disjunct(pred,pred), pred, b(conjunct(b(truth,pred,[]),b(falsity,pred,[])),pred,[]), _, b(disjunct(b(truth,pred,[]),b(falsity,pred,[])),pred,[])).

test(call_time_per_solver, [nondet]) :-
    AST = b(conjunct(b(truth,pred,[]),b(truth,pred,[])),pred,[]),
    time_per_solver(AST, [prob, kodkod, cdclt, z3, cvc4], 1000, Res),
    Res = [[cvc4,_,_,solution([])],[z3,_,_,solution([])],[cdclt,_,_,solution([])],[kodkod,_,_,solution([])],[prob,_,_,solution([])]].

test(call_time_per_solver_contradiction, [nondet]) :-
    AST = b(conjunct(b(truth,pred,[]),b(falsity,pred,[])),pred,[]),
    time_per_solver(AST, [prob, kodkod, cdclt, z3, cvc4], 1000, Res),
    Res = [[cvc4,_,_,contradiction_found],[z3,_,_,contradiction_found],[cdclt,_,_,contradiction_found],[kodkod,_,_,contradiction_found],[prob,_,_,contradiction_found]].

test_runner :-
    run_tests(runner).

time_per_solver(AST, SolverList, TimeOutValue, TimePerSolver) :-
    time_per_solver_acc(AST, SolverList, TimeOutValue, [], TimePerSolver).

time_per_solver_acc(_, [], _, Res, Res).

time_per_solver_acc(AST, [prob|Solvers], TimeOutValue, Acc, TimePerSolver) :-
    statistics(walltime,[Start,_]),
    time_out(solve_predicate(AST,_,Res),TimeOutValue,TimeOut),
    statistics(walltime,[End,_]),
    Time is End - Start,
    time_per_solver_acc(AST, Solvers, TimeOutValue, [[prob,Time,TimeOut,Res]|Acc], TimePerSolver).

time_per_solver_acc(AST, [kodkod|Solvers], TimeOutValue, Acc, TimePerSolver) :-
    statistics(walltime,[Start,_]),
    time_out(solve_predicate(AST,_,1,['KODKOD'],Res),TimeOutValue,TimeOut),
    statistics(walltime,[End,_]),
    Time is End - Start,
    time_per_solver_acc(AST, Solvers, TimeOutValue, [[kodkod,Time,TimeOut,Res]|Acc], TimePerSolver).

time_per_solver_acc(AST, [cdclt|Solvers], TimeOutValue, Acc, TimePerSolver) :-
    statistics(walltime,[Start,_]),
    time_out(cdclt_solve_predicate(AST,_,Res),TimeOutValue,TimeOut),
    statistics(walltime,[End,_]),
    Time is End - Start,
    time_per_solver_acc(AST, Solvers, TimeOutValue, [[cdclt,Time,TimeOut,Res]|Acc], TimePerSolver).

time_per_solver_acc(AST, [Solver|Solvers], TimeOutValue, Acc, TimePerSolver) :-
    member(Solver, [cvc4, z3]),
    statistics(walltime,[Start,_]),
    time_out(smt_solve_predicate(Solver, AST,_,Res),TimeOutValue,TimeOut),
    statistics(walltime,[End,_]),
    Time is End - Start,
    time_per_solver_acc(AST, Solvers, TimeOutValue, [[Solver,Time,TimeOut,Res]|Acc], TimePerSolver).