dpllt_solver_tests

Imports	Exports
Name: solve_predicate/3 Module: solver_interface Name: clean_up_pred/3 Module: b_ast_cleanup Name: module_info/2 Module: module_information	Name: run_tests/1

Imports

Exports

Name: solve_predicate/3

Module: solver_interface

Name: clean_up_pred/3

Module: b_ast_cleanup

Name: module_info/2

Module: module_information

Name: run_tests/1

Predicates

Predicates:

fuzzy_verify_solver/0

prob_accepts_result/2

solve_clean_predicate/3

test/2

verify_dpllt_solutions_with_prob/1

fuzzy_verify_solver/0

test(extend_candidate_impls_acc_less, [true(NewAcc == candidate_impls(integer([Ast]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),integer,[]),
    Arg2 = b(integer(7),integer,[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_non_ground, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_no_identifier, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq, [true(NewAcc == candidate_impls(integer([Ast]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),integer,[]),
    Arg2 = b(integer(7),integer,[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq_non_ground, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq_no_identifier, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset, [true(NewAcc == candidate_impls(integer([]),set([Ast])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_non_ground, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_no_identifier, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict, [true(NewAcc == candidate_impls(integer([]),set([Ast])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict_non_ground, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict_no_identifier, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_equal, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(equal(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_member, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(integer),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(member(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(pred, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_member_non_ground_type, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(integer),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(member(Arg1,Arg2),pred,[]),
    dpllt_solver:extend_candidate_impls_acc(_Type, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_add, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(integer(1),integer,[]),
    Arg2 = b(integer(1),integer,[]),
    Ast = b(add(Arg1,Arg2),integer,[]),
    dpllt_solver:extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_overwrite, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
    Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
    Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
    dpllt_solver:extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_overwrite_non_ground_type, [true(NewAcc == candidate_impls(integer([]),set([])))]) :-
    dpllt_solver:empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
    Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
    Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
    dpllt_solver:extend_candidate_impls_acc(_Type, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

verify_dpllt_solutions_with_prob/1

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file extension('prolog_fuzzer/fuzzing') does not exist
! goal: absolute_file_name(extension('prolog_fuzzer/fuzzing'),_3665,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/dpllt_solver/dpllt_solver_tests.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc('dpllt_solver/dpllt_solver') does not exist
! goal: absolute_file_name(probsrc('dpllt_solver/dpllt_solver'),_4065,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/dpllt_solver/dpllt_solver_tests.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(solver_interface) does not exist
! goal: absolute_file_name(probsrc(solver_interface),_273,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/dpllt_solver/dpllt_solver_tests.pl')])

Name: =/2
Name: solve_clean_predicate/3	Module: dpllt_solver_tests
Name: ==/2
Name: ground/1
Name: !

Name: extend_candidate_impls_acc/7	Module: dpllt_solver
Name: =/2
Name: empty_candidate_impls_acc/1	Module: dpllt_solver

Name: prob_accepts_result/2	Module: dpllt_solver_tests
Name: !
Name: dpllt_solve_predicate/2	Module: foo_error