test(integer_abstractions1) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:get_integer_interval_size(-128,127,IntervalSize) ,
b_synthesis_afta:split_and_assert_abstractions(integer,-128,127,IntervalSize) ,
findall(A,(b_synthesis_afta:abstraction(integer,b(integer(27),integer,[]),Abstr) , A = abstraction(integer,b(integer(27),integer,[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-128,-112),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-111,-95),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-94,-78),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-77,-61),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-60,-44),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-43,-27),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-26,-10),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(-9,7),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(8,24),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(25,41),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(42,58),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(59,75),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(76,92),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(93,109),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(110,126),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(27),integer,[]),b(member(b(integer(27),integer,[]),b(interval(127,127),set(integer),[])),pred,[synthesis(abstraction,integer)]))],R) ,
R == [].
test(integer_abstractions2) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:get_integer_interval_size(-256,255,IntervalSize) ,
b_synthesis_afta:split_and_assert_abstractions(integer,-256,255,IntervalSize) ,
findall(A,(b_synthesis_afta:abstraction(integer,b(integer(1),integer,[]),Abstr) , A = abstraction(integer,b(integer(1),integer,[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-256,-233),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-232,-209),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-208,-185),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-184,-161),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-160,-137),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-136,-113),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-112,-89),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-88,-65),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-64,-41),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-40,-17),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(-16,7),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(8,31),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(32,55),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(56,79),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(80,103),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(104,127),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(128,151),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(152,175),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(176,199),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(200,223),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(224,247),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(1),integer,[]),b(member(b(integer(1),integer,[]),b(interval(248,255),set(integer),[])),pred,[synthesis(abstraction,integer)]))],R) ,
R == [].
test(integer_abstractions3) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:get_integer_interval_size(24,123,IntervalSize) ,
b_synthesis_afta:split_and_assert_abstractions(integer,24,123,IntervalSize) ,
findall(A,(b_synthesis_afta:abstraction(integer,b(integer(-2),integer,[]),Abstr) , A = abstraction(integer,b(integer(-2),integer,[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(24,34),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(35,45),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(46,56),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(57,67),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(68,78),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(79,89),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(90,100),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(101,111),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(112,122),set(integer),[])),pred,[synthesis(abstraction,integer)])),abstraction(integer,b(integer(-2),integer,[]),b(member(b(integer(-2),integer,[]),b(interval(123,123),set(integer),[])),pred,[synthesis(abstraction,integer)]))],R) ,
R == [].
test(integer_abstractions4) :-
findall(X,b_synthesis_afta:get_integer_interval_size(0,144,X),S) ,
S == [12].
test(integer_abstractions5) :-
findall(X,b_synthesis_afta:get_integer_interval_size(0,145,X),S) ,
S == [12].
test(integer_abstractions6) :-
findall(X,b_synthesis_afta:get_integer_interval_size(-2,18,X),S) ,
S == [4].
test(set_abstractions1) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:split_and_assert_abstractions(set,0,10,4) ,
findall(A,(b_synthesis_afta:abstraction(set,b(set_extension([]),set(integer),[]),Abstr) , A = abstraction(set,b(set_extension([]),set(integer),[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(0,4),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(5,9),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(10,10),set(integer),[])),pred,[synthesis(abstraction,set)]))],R) ,
R == [].
test(set_abstractions2) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:split_and_assert_abstractions(set,0,22,4) ,
findall(A,(b_synthesis_afta:abstraction(set,b(set_extension([]),set(integer),[]),Abstr) , A = abstraction(set,b(set_extension([]),set(integer),[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(0,4),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(5,9),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(10,14),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(15,19),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(20,22),set(integer),[])),pred,[synthesis(abstraction,set)]))],R) ,
R == [].
test(set_abstractions3) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:split_and_assert_abstractions(set,0,22,7) ,
findall(A,(b_synthesis_afta:abstraction(set,b(set_extension([]),set(integer),[]),Abstr) , A = abstraction(set,b(set_extension([]),set(integer),[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(0,7),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(8,15),set(integer),[])),pred,[synthesis(abstraction,set)])),abstraction(set,b(set_extension([]),set(integer),[]),b(member(b(card(b(set_extension([]),set(integer),[])),integer,[]),b(interval(16,22),set(integer),[])),pred,[synthesis(abstraction,set)]))],R) ,
R == [].
test(set_abstractions4) :-
retractall(b_synthesis_afta:abstraction(_,_,_)) ,
b_synthesis_afta:split_and_assert_abstractions(set,0,5,17) ,
findall(A,(b_synthesis_afta:abstraction(set,b(set_extension([b(integer(7),integer,[])]),set(integer),[]),Abstr) , A = abstraction(set,b(set_extension([b(integer(7),integer,[])]),set(integer),[]),Abstr)),Assertions) ,
subtract(Assertions,[abstraction(set,b(set_extension([b(integer(7),integer,[])]),set(integer),[]),b(member(b(card(b(set_extension([b(integer(7),integer,[])]),set(integer),[])),integer,[]),b(interval(0,5),set(integer),[])),pred,[synthesis(abstraction,set)]))],R) ,
R == [].