| Imports | Exports |
|---|---|
Name: startup_prob/0 Module: prob_startup Name: b_load_machine_from_file/1 Module: bmachine Name: b_machine_precompile/0 Module: bmachine | Name: tests/0 Name: run_tests/0 Name: run_tests/1 |
b_test_boolean_expression_wf(E,LS,S) :-
b_test_boolean_expression_cs(E,LS,S,'Synthesis Tests',0).
Calls:
Name: b_test_boolean_expression_cs/5 |
Module: foo_error |
Called:
Name: test/2 |
Module: synthesis_tests |
test(lVar2Prog_Guard1) :-
b_synthesis:location_vars_to_program(([card-set(integer),constant-set(integer),constant-integer,greater],[]),guard,
[b(identifier(var),set(integer),[])],
[b(identifier(l0),set(integer),[synthesis(input(0)),synthesis(machinevar,var)]),b(identifier(li68),integer,[synthesis(card1,input),synthesis(type,set(integer))]),b(identifier(li74),integer,[synthesis(greater1,left_input),synthesis(type,integer)]),b(identifier(li75),integer,[synthesis(greater1,right_input),synthesis(type,integer)]),b(identifier(lo69),integer,[synthesis(card1,output),synthesis(type,integer)]),b(identifier(lo70),integer,[synthesis(constant71,output),synthesis(type,set(integer))]),b(identifier(lo72),integer,[synthesis(constant73,output),synthesis(type,integer)]),b(identifier(lo76),integer,[synthesis(greater1,output),synthesis(type,boolean)])],
4,1,
solution([binding(constant71,[],{}),binding(constant73,int(1),'1'),binding(l0set,int(0),'0'),binding(li68,int(0),'0'),binding(li74,int(3),'3'),binding(li75,int(2),'2'),binding(lo0boolean_false,int(4),'4'),binding(lo0boolean_true,int(4),'4'),binding(lo69,int(3),'3'),binding(lo70,int(1),'1'),binding(lo72,int(2),'2'),binding(lo76,int(4),'4'),binding(o72,int(-10),'-10')]),
[b(identifier(lo76),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo69),integer,[synthesis(card1,output),synthesis(type,integer)]),b(identifier(lo72),integer,[synthesis(constant73,output),synthesis(type,integer)])],
ProgramAST) ,
ProgramAST = b(greater(b(card(b(identifier(var),set(integer),_)),integer,_),b(value(int(1)),integer,_)),boolean,_).
test(lVar2Prog_Guard2) :-
b_synthesis:location_vars_to_program(([greater,equal-integer,constant-integer],[]),guard,
[b(identifier(var),integer,[])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,var)]),b(identifier(li86),integer,[synthesis(greater1,left_input),synthesis(type,integer)]),b(identifier(li87),integer,[synthesis(greater1,right_input),synthesis(type,integer)]),b(identifier(li89),integer,[synthesis(equal1,left_input),synthesis(type,integer)]),b(identifier(li90),integer,[synthesis(equal1,right_input),synthesis(type,integer)]),b(identifier(lo88),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo91),integer,[synthesis(equal1,output),synthesis(type,boolean)]),b(identifier(lo92),integer,[synthesis(constant93,output),synthesis(type,integer)])],
3,1,
solution([binding(constant93,int(0),'0'),binding(l00,int(0),'0'),binding(l01,int(0),'0'),binding(li86,int(0),'0'),binding(li87,int(1),'1'),binding(li89,int(0),'0'),binding(li90,int(0),'0'),binding(lo0boolean_false,int(3),'3'),binding(lo0boolean_true,int(3),'3'),binding(lo88,int(3),'3'),binding(lo91,int(2),'2'),binding(lo92,int(1),'1'),binding(o92,int(-10),'-10')]),
[b(identifier(lo88),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo92),integer,[synthesis(constant93,output),synthesis(type,integer)])],
ProgramAST) ,
ProgramAST = b(greater(b(identifier(var),integer,_),b(value(int(0)),integer,_)),boolean,_).
test(lVar2Prog_Guard3) :-
b_synthesis:location_vars_to_program(([greater,equal-integer,constant-integer],[add,minus]),guard,
[b(identifier(var1),integer,[]),b(identifier(var2),integer,[])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,var1)]),b(identifier(l1),integer,[synthesis(input(1)),synthesis(machinevar,var2)]),b(identifier(li448),integer,[synthesis(greater1,left_input),synthesis(type,integer)]),b(identifier(li449),integer,[synthesis(greater1,right_input),synthesis(type,integer)]),b(identifier(li451),integer,[synthesis(equal1,left_input),synthesis(type,integer)]),b(identifier(li452),integer,[synthesis(equal1,right_input),synthesis(type,integer)]),b(identifier(li456),integer,[synthesis(add1,left_input),synthesis(type,integer)]),b(identifier(li457),integer,[synthesis(add1,right_input),synthesis(type,integer)]),b(identifier(li459),integer,[synthesis(minus1,left_input),synthesis(type,integer)]),b(identifier(li460),integer,[synthesis(minus1,right_input),synthesis(type,integer)]),b(identifier(lo450),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo453),integer,[synthesis(equal1,output),synthesis(type,boolean)]),b(identifier(lo454),integer,[synthesis(constant455,output),synthesis(type,integer)]),b(identifier(lo458),integer,[synthesis(add1,output),synthesis(type,integer)]),b(identifier(lo461),integer,[synthesis(minus1,output),synthesis(type,integer)])],
6,2,
solution([binding(constant455,int(1),'1'),binding('l0-1',int(0),'0'),binding(l00,int(0),'0'),binding(l01,int(0),'0'),binding(l02,int(0),'0'),binding(l10,int(1),'1'),binding(l11,int(1),'1'),binding(l12,int(1),'1'),binding(li448,int(3),'3'),binding(li449,int(4),'4'),binding(li451,int(0),'0'),binding(li452,int(0),'0'),binding(li456,int(1),'1'),binding(li457,int(0),'0'),binding(li459,int(0),'0'),binding(li460,int(0),'0'),binding(lo0boolean_false,int(6),'6'),binding(lo0boolean_true,int(6),'6'),binding(lo450,int(6),'6'),binding(lo453,int(5),'5'),binding(lo454,int(4),'4'),binding(lo458,int(3),'3'),binding(lo461,int(2),'2'),binding(o454,int(-10),'-10')]),
[b(identifier(lo450),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo458),integer,[synthesis(add1,output),synthesis(type,integer)]),b(identifier(lo454),integer,[synthesis(constant455,output),synthesis(type,integer)])],
ProgramAST) ,
ProgramAST = b(greater(b(add(b(identifier(var2),integer,_),b(identifier(var1),integer,_)),integer,_),b(value(int(1)),integer,_)),boolean,_).
test(lVar2Prog_Guard4) :-
b_synthesis:location_vars_to_program(([greater,equal-integer,constant-integer,greater,equal-integer,constant-integer],[add,minus]),guard,
[b(identifier(coins),integer,[nodeid(pos(5,1,2,11,2,15))]),b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,coins)]),b(identifier(l1),integer,[synthesis(input(1)),synthesis(machinevar,soda)]),b(identifier(li100),integer,[synthesis(type,integer),synthesis(greater2,right_input)]),b(identifier(li102),integer,[synthesis(type,integer),synthesis(equal2,left_input)]),b(identifier(li103),integer,[synthesis(type,integer),synthesis(equal2,right_input)]),b(identifier(li107),integer,[synthesis(type,integer),synthesis(add1,left_input)]),b(identifier(li108),integer,[synthesis(type,integer),synthesis(add1,right_input)]),b(identifier(li110),integer,[synthesis(type,integer),synthesis(minus1,left_input)]),b(identifier(li111),integer,[synthesis(type,integer),synthesis(minus1,right_input)]),b(identifier(li91),integer,[synthesis(type,integer),synthesis(greater1,left_input)]),b(identifier(li92),integer,[synthesis(type,integer),synthesis(greater1,right_input)]),b(identifier(li94),integer,[synthesis(type,integer),synthesis(equal1,left_input)]),b(identifier(li95),integer,[synthesis(type,integer),synthesis(equal1,right_input)]),b(identifier(li99),integer,[synthesis(type,integer),synthesis(greater2,left_input)]),b(identifier(lo101),integer,[synthesis(type,boolean),synthesis(greater2,output)]),b(identifier(lo104),integer,[synthesis(type,boolean),synthesis(equal2,output)]),b(identifier(lo106),integer,[synthesis(type,integer),synthesis(constant105,output),synthesis(type,constant-integer)]),b(identifier(lo109),integer,[synthesis(type,integer),synthesis(add1,output)]),b(identifier(lo112),integer,[synthesis(type,integer),synthesis(minus1,output)]),b(identifier(lo93),integer,[synthesis(type,boolean),synthesis(greater1,output)]),b(identifier(lo96),integer,[synthesis(type,boolean),synthesis(equal1,output)]),b(identifier(lo98),integer,[synthesis(type,integer),synthesis(constant97,output),synthesis(type,constant-integer)])],
9,2,
solution([binding(constant105,int(0),'0'),binding(constant97,int(2),'2'),binding(l02,int(0),'0'),binding(l03,int(0),'0'),binding(l10,int(1),'1'),binding(l13,int(1),'1'),binding(li100,int(0),'0'),binding(li102,int(5),'5'),binding(li103,int(0),'0'),binding(li107,int(0),'0'),binding(li108,int(0),'0'),binding(li110,int(0),'0'),binding(li111,int(0),'0'),binding(li91,int(0),'0'),binding(li92,int(0),'0'),binding(li94,int(0),'0'),binding(li95,int(0),'0'),binding(li99,int(0),'0'),binding(lo0boolean_false,int(9),'9'),binding(lo0boolean_true,int(9),'9'),binding(lo101,int(4),'4'),binding(lo104,int(9),'9'),binding(lo106,int(6),'6'),binding(lo109,int(3),'3'),binding(lo112,int(2),'2'),binding(lo93,int(8),'8'),binding(lo96,int(7),'7'),binding(lo98,int(5),'5')]),
[b(identifier(lo104),integer,[synthesis(type,boolean),synthesis(equal2,output)]),b(identifier(lo98),integer,[synthesis(type,integer),synthesis(constant97,output),synthesis(type,constant-integer)])],
ProgramAST) ,
ProgramAST = b(equal(b(value(int(2)),integer,_),b(identifier(coins),integer,_)),boolean,_).
test(lVar2Prog_Invariant1) :-
b_synthesis:location_vars_to_program(([greater,equal-integer,constant-integer],[]),invariant,
[b(identifier(var),integer,[])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,var)]),b(identifier(li102),integer,[synthesis(greater1,left_input),synthesis(type,integer)]),b(identifier(li103),integer,[synthesis(greater1,right_input),synthesis(type,integer)]),b(identifier(li105),integer,[synthesis(equal1,left_input),synthesis(type,integer)]),b(identifier(li106),integer,[synthesis(equal1,right_input),synthesis(type,integer)]),b(identifier(lo104),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo107),integer,[synthesis(equal1,output),synthesis(type,boolean)]),b(identifier(lo108),integer,[synthesis(constant109,output),synthesis(type,integer)])],
3,1,
solution([binding(constant109,int(-1),'-1'),binding('l0-1',int(0),'0'),binding('l0-2',int(0),'0'),binding(l00,int(0),'0'),binding(l01,int(0),'0'),binding(l02,int(0),'0'),binding(l03,int(0),'0'),binding(l04,int(0),'0'),binding(l05,int(0),'0'),binding(li102,int(0),'0'),binding(li103,int(1),'1'),binding(li105,int(0),'0'),binding(li106,int(0),'0'),binding(lo0boolean_false,int(3),'3'),binding(lo0boolean_true,int(3),'3'),binding(lo104,int(3),'3'),binding(lo107,int(2),'2'),binding(lo108,int(1),'1'),binding(o108,int(-10),'-10')]),
[b(identifier(lo104),integer,[synthesis(greater1,output),synthesis(type,boolean)]),b(identifier(lo108),integer,[synthesis(constant109,output),synthesis(type,integer)])],
ProgramAST) ,
ProgramAST = b(greater(b(identifier(var),integer,_),b(value(int(-1)),integer,_)),boolean,_).
test(lVar2Prog_Action1) :-
b_synthesis:location_vars_to_program(([equal-integer,constant-integer,equal-integer,constant-integer],[add,minus,multiplication,div,add,minus,multiplication,div]),action,
[b(identifier(coins),integer,[]),b(identifier(soda),integer,[])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,coins)]),b(identifier(l1),integer,[synthesis(input(1)),synthesis(machinevar,soda)]),b(identifier(li183),integer,[synthesis(type,integer),synthesis(equal1,left_input)]),b(identifier(li184),integer,[synthesis(type,integer),synthesis(equal1,right_input)]),b(identifier(li188),integer,[synthesis(type,integer),synthesis(equal2,left_input)]),b(identifier(li189),integer,[synthesis(type,integer),synthesis(equal2,right_input)]),b(identifier(li193),integer,[synthesis(type,integer),synthesis(add1,left_input)]),b(identifier(li194),integer,[synthesis(type,integer),synthesis(add1,right_input)]),b(identifier(li196),integer,[synthesis(type,integer),synthesis(minus1,left_input)]),b(identifier(li197),integer,[synthesis(type,integer),synthesis(minus1,right_input)]),b(identifier(li199),integer,[synthesis(type,integer),synthesis(multiplication1,left_input)]),b(identifier(li200),integer,[synthesis(type,integer),synthesis(multiplication1,right_input)]),b(identifier(li202),integer,[synthesis(type,integer),synthesis(div1,left_input)]),b(identifier(li203),integer,[synthesis(type,integer),synthesis(div1,right_input)]),b(identifier(li205),integer,[synthesis(type,integer),synthesis(add2,left_input)]),b(identifier(li206),integer,[synthesis(type,integer),synthesis(add2,right_input)]),b(identifier(li208),integer,[synthesis(type,integer),synthesis(minus2,left_input)]),b(identifier(li209),integer,[synthesis(type,integer),synthesis(minus2,right_input)]),b(identifier(li211),integer,[synthesis(type,integer),synthesis(multiplication2,left_input)]),b(identifier(li212),integer,[synthesis(type,integer),synthesis(multiplication2,right_input)]),b(identifier(li214),integer,[synthesis(type,integer),synthesis(div2,left_input)]),b(identifier(li215),integer,[synthesis(type,integer),synthesis(div2,right_input)]),b(identifier(lo185),integer,[synthesis(type,boolean),synthesis(equal1,output)]),b(identifier(lo187),integer,[synthesis(type,integer),synthesis(constant186,output),synthesis(type,constant-integer)]),b(identifier(lo190),integer,[synthesis(type,boolean),synthesis(equal2,output)]),b(identifier(lo192),integer,[synthesis(type,integer),synthesis(constant191,output),synthesis(type,constant-integer)]),b(identifier(lo195),integer,[synthesis(type,integer),synthesis(add1,output)]),b(identifier(lo198),integer,[synthesis(type,integer),synthesis(minus1,output)]),b(identifier(lo201),integer,[synthesis(type,integer),synthesis(multiplication1,output)]),b(identifier(lo204),integer,[synthesis(type,integer),synthesis(div1,output)]),b(identifier(lo207),integer,[synthesis(type,integer),synthesis(add2,output)]),b(identifier(lo210),integer,[synthesis(type,integer),synthesis(minus2,output)]),b(identifier(lo213),integer,[synthesis(type,integer),synthesis(multiplication2,output)]),b(identifier(lo216),integer,[synthesis(type,integer),synthesis(div2,output)])],
13,2,
solution([binding(constant186,int(2),'2'),binding(constant191,int(3),'3'),binding(l02,int(0),'0'),binding(l04,int(0),'0'),binding(l05,int(0),'0'),binding(l06,int(0),'0'),binding(l13,int(1),'1'),binding(l14,int(1),'1'),binding(l15,int(1),'1'),binding(l19,int(1),'1'),binding(li183,int(5),'5'),binding(li184,int(0),'0'),binding(li188,int(0),'0'),binding(li189,int(0),'0'),binding(li193,int(0),'0'),binding(li194,int(0),'0'),binding(li196,int(1),'1'),binding(li197,int(9),'9'),binding(li199,int(0),'0'),binding(li200,int(0),'0'),binding(li202,int(0),'0'),binding(li203,int(0),'0'),binding(li205,int(0),'0'),binding(li206,int(0),'0'),binding(li208,int(0),'0'),binding(li209,int(10),'10'),binding(li211,int(0),'0'),binding(li212,int(0),'0'),binding(li214,int(0),'0'),binding(li215,int(0),'0'),binding(lo00,int(13),'13'),binding(lo02,int(13),'13'),binding(lo03,int(13),'13'),binding(lo04,int(13),'13'),binding(lo10,int(12),'12'),binding(lo11,int(12),'12'),binding(lo12,int(12),'12'),binding(lo16,int(12),'12'),binding(lo185,int(6),'6'),binding(lo187,int(10),'10'),binding(lo190,int(2),'2'),binding(lo192,int(9),'9'),binding(lo195,int(5),'5'),binding(lo198,int(12),'12'),binding(lo201,int(11),'11'),binding(lo204,int(4),'4'),binding(lo207,int(8),'8'),binding(lo210,int(13),'13'),binding(lo213,int(7),'7'),binding(lo216,int(3),'3')]),
[b(identifier(lo187),integer,[synthesis(type,integer),synthesis(constant186,output),synthesis(type,constant-integer)]),b(identifier(lo192),integer,[synthesis(type,integer),synthesis(constant191,output),synthesis(type,constant-integer)]),b(identifier(lo198),integer,[synthesis(type,integer),synthesis(minus1,output)]),b(identifier(lo210),integer,[synthesis(type,integer),synthesis(minus2,output)])],
ProgramAST) ,
ProgramAST = b(conjunct(b(equal(b(identifier('coins\''),integer,_),b(minus(b(identifier(coins),integer,_),b(value(int(2)),integer,_)),integer,_)),pred,_),b(equal(b(identifier('soda\''),integer,_),b(minus(b(identifier(soda),integer,_),b(value(int(3)),integer,_)),integer,_)),pred,_)),pred,_).
test(lVar2Prog_Action2) :-
b_synthesis:location_vars_to_program(([equal-integer,constant-integer,equal-integer,constant-integer],[add,minus,multiplication,div,add,minus,multiplication,div]),action,
[b(identifier(coins),integer,[]),b(identifier(soda),integer,[])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,coins)]),b(identifier(l1),integer,[synthesis(input(1)),synthesis(machinevar,soda)]),b(identifier(li273),integer,[synthesis(type,integer),synthesis(equal1,left_input)]),b(identifier(li274),integer,[synthesis(type,integer),synthesis(equal1,right_input)]),b(identifier(li278),integer,[synthesis(type,integer),synthesis(equal2,left_input)]),b(identifier(li279),integer,[synthesis(type,integer),synthesis(equal2,right_input)]),b(identifier(li283),integer,[synthesis(type,integer),synthesis(add1,left_input)]),b(identifier(li284),integer,[synthesis(type,integer),synthesis(add1,right_input)]),b(identifier(li286),integer,[synthesis(type,integer),synthesis(minus1,left_input)]),b(identifier(li287),integer,[synthesis(type,integer),synthesis(minus1,right_input)]),b(identifier(li289),integer,[synthesis(type,integer),synthesis(multiplication1,left_input)]),b(identifier(li290),integer,[synthesis(type,integer),synthesis(multiplication1,right_input)]),b(identifier(li292),integer,[synthesis(type,integer),synthesis(div1,left_input)]),b(identifier(li293),integer,[synthesis(type,integer),synthesis(div1,right_input)]),b(identifier(li295),integer,[synthesis(type,integer),synthesis(add2,left_input)]),b(identifier(li296),integer,[synthesis(type,integer),synthesis(add2,right_input)]),b(identifier(li298),integer,[synthesis(type,integer),synthesis(minus2,left_input)]),b(identifier(li299),integer,[synthesis(type,integer),synthesis(minus2,right_input)]),b(identifier(li301),integer,[synthesis(type,integer),synthesis(multiplication2,left_input)]),b(identifier(li302),integer,[synthesis(type,integer),synthesis(multiplication2,right_input)]),b(identifier(li304),integer,[synthesis(type,integer),synthesis(div2,left_input)]),b(identifier(li305),integer,[synthesis(type,integer),synthesis(div2,right_input)]),b(identifier(lo275),integer,[synthesis(type,boolean),synthesis(equal1,output)]),b(identifier(lo277),integer,[synthesis(type,integer),synthesis(constant276,output),synthesis(type,constant-integer)]),b(identifier(lo280),integer,[synthesis(type,boolean),synthesis(equal2,output)]),b(identifier(lo282),integer,[synthesis(type,integer),synthesis(constant281,output),synthesis(type,constant-integer)]),b(identifier(lo285),integer,[synthesis(type,integer),synthesis(add1,output)]),b(identifier(lo288),integer,[synthesis(type,integer),synthesis(minus1,output)]),b(identifier(lo291),integer,[synthesis(type,integer),synthesis(multiplication1,output)]),b(identifier(lo294),integer,[synthesis(type,integer),synthesis(div1,output)]),b(identifier(lo297),integer,[synthesis(type,integer),synthesis(add2,output)]),b(identifier(lo300),integer,[synthesis(type,integer),synthesis(minus2,output)]),b(identifier(lo303),integer,[synthesis(type,integer),synthesis(multiplication2,output)]),b(identifier(lo306),integer,[synthesis(type,integer),synthesis(div2,output)])],
13,2,
solution([binding(constant276,int(-2),'-2'),binding(constant281,int(3),'3'),binding(l02,int(0),'0'),binding(l04,int(0),'0'),binding(l13,int(1),'1'),binding(l14,int(1),'1'),binding(li273,int(0),'0'),binding(li274,int(0),'0'),binding(li278,int(0),'0'),binding(li279,int(0),'0'),binding(li283,int(11),'11'),binding(li284,int(0),'0'),binding(li286,int(1),'1'),binding(li287,int(10),'10'),binding(li289,int(0),'0'),binding(li290,int(0),'0'),binding(li292,int(0),'0'),binding(li293,int(0),'0'),binding(li295,int(0),'0'),binding(li296,int(0),'0'),binding(li298,int(0),'0'),binding(li299,int(0),'0'),binding(li301,int(0),'0'),binding(li302,int(0),'0'),binding(li304,int(0),'0'),binding(li305,int(0),'0'),binding(lo00,int(13),'13'),binding(lo02,int(13),'13'),binding(lo10,int(12),'12'),binding(lo11,int(12),'12'),binding(lo275,int(5),'5'),binding(lo277,int(11),'11'),binding(lo280,int(4),'4'),binding(lo282,int(10),'10'),binding(lo285,int(13),'13'),binding(lo288,int(12),'12'),binding(lo291,int(9),'9'),binding(lo294,int(3),'3'),binding(lo297,int(8),'8'),binding(lo300,int(7),'7'),binding(lo303,int(6),'6'),binding(lo306,int(2),'2')]),
[b(identifier(lo277),integer,[synthesis(type,integer),synthesis(constant276,output),synthesis(type,constant-integer)]),b(identifier(lo282),integer,[synthesis(type,integer),synthesis(constant281,output),synthesis(type,constant-integer)]),b(identifier(lo285),integer,[synthesis(type,integer),synthesis(add1,output)]),b(identifier(lo288),integer,[synthesis(type,integer),synthesis(minus1,output)])],
ProgramAST) ,
ProgramAST = b(conjunct(b(equal(b(identifier('coins\''),integer,_),b(add(b(value(int(-2)),integer,_),b(identifier(coins),integer,_)),integer,_)),pred,_),b(equal(b(identifier('soda\''),integer,_),b(minus(b(identifier(soda),integer,_),b(value(int(3)),integer,_)),integer,_)),pred,_)),pred,_).
test(lVar2Prog_Action3) :-
b_synthesis:location_vars_to_program(([equal-integer,constant-integer,equal-integer,constant-integer],[add,minus,multiplication,div,add,minus,multiplication,div]),action,
[b(identifier(coins),integer,[nodeid(pos(5,1,2,11,2,15))]),b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))])],
[b(identifier(l0),integer,[synthesis(input(0)),synthesis(machinevar,coins)]),b(identifier(l1),integer,[synthesis(input(1)),synthesis(machinevar,soda)]),b(identifier(li397),integer,[synthesis(type,integer),synthesis(equal1,left_input)]),b(identifier(li398),integer,[synthesis(type,integer),synthesis(equal1,right_input)]),b(identifier(li402),integer,[synthesis(type,integer),synthesis(equal2,left_input)]),b(identifier(li403),integer,[synthesis(type,integer),synthesis(equal2,right_input)]),b(identifier(li407),integer,[synthesis(type,integer),synthesis(add1,left_input)]),b(identifier(li408),integer,[synthesis(type,integer),synthesis(add1,right_input)]),b(identifier(li410),integer,[synthesis(type,integer),synthesis(minus1,left_input)]),b(identifier(li411),integer,[synthesis(type,integer),synthesis(minus1,right_input)]),b(identifier(li413),integer,[synthesis(type,integer),synthesis(multiplication1,left_input)]),b(identifier(li414),integer,[synthesis(type,integer),synthesis(multiplication1,right_input)]),b(identifier(li416),integer,[synthesis(type,integer),synthesis(div1,left_input)]),b(identifier(li417),integer,[synthesis(type,integer),synthesis(div1,right_input)]),b(identifier(li419),integer,[synthesis(type,integer),synthesis(add2,left_input)]),b(identifier(li420),integer,[synthesis(type,integer),synthesis(add2,right_input)]),b(identifier(li422),integer,[synthesis(type,integer),synthesis(minus2,left_input)]),b(identifier(li423),integer,[synthesis(type,integer),synthesis(minus2,right_input)]),b(identifier(li425),integer,[synthesis(type,integer),synthesis(multiplication2,left_input)]),b(identifier(li426),integer,[synthesis(type,integer),synthesis(multiplication2,right_input)]),b(identifier(li428),integer,[synthesis(type,integer),synthesis(div2,left_input)]),b(identifier(li429),integer,[synthesis(type,integer),synthesis(div2,right_input)]),b(identifier(lo399),integer,[synthesis(type,boolean),synthesis(equal1,output)]),b(identifier(lo401),integer,[synthesis(type,integer),synthesis(constant400,output),synthesis(type,constant-integer)]),b(identifier(lo404),integer,[synthesis(type,boolean),synthesis(equal2,output)]),b(identifier(lo406),integer,[synthesis(type,integer),synthesis(constant405,output),synthesis(type,constant-integer)]),b(identifier(lo409),integer,[synthesis(type,integer),synthesis(add1,output)]),b(identifier(lo412),integer,[synthesis(type,integer),synthesis(minus1,output)]),b(identifier(lo415),integer,[synthesis(type,integer),synthesis(multiplication1,output)]),b(identifier(lo418),integer,[synthesis(type,integer),synthesis(div1,output)]),b(identifier(lo421),integer,[synthesis(type,integer),synthesis(add2,output)]),b(identifier(lo424),integer,[synthesis(type,integer),synthesis(minus2,output)]),b(identifier(lo427),integer,[synthesis(type,integer),synthesis(multiplication2,output)]),b(identifier(lo430),integer,[synthesis(type,integer),synthesis(div2,output)])],
13,2,
solution([binding(constant400,int(3),'3'),binding(constant405,int(0),'0'),binding(l02,int(0),'0'),binding(l13,int(1),'1'),binding(l14,int(1),'1'),binding(li397,int(5),'5'),binding(li398,int(0),'0'),binding(li402,int(0),'0'),binding(li403,int(0),'0'),binding(li407,int(0),'0'),binding(li408,int(0),'0'),binding(li410,int(1),'1'),binding(li411,int(7),'7'),binding(li413,int(0),'0'),binding(li414,int(0),'0'),binding(li416,int(0),'0'),binding(li417,int(0),'0'),binding(li419,int(0),'0'),binding(li420,int(0),'0'),binding(li422,int(0),'0'),binding(li423,int(0),'0'),binding(li425,int(0),'0'),binding(li426,int(0),'0'),binding(li428,int(0),'0'),binding(li429,int(0),'0'),binding(lo00,int(13),'13'),binding(lo10,int(12),'12'),binding(lo11,int(12),'12'),binding(lo399,int(6),'6'),binding(lo401,int(7),'7'),binding(lo404,int(2),'2'),binding(lo406,int(13),'13'),binding(lo409,int(5),'5'),binding(lo412,int(12),'12'),binding(lo415,int(11),'11'),binding(lo418,int(4),'4'),binding(lo421,int(10),'10'),binding(lo424,int(9),'9'),binding(lo427,int(8),'8'),binding(lo430,int(3),'3')]),
[b(identifier(lo401),integer,[synthesis(type,integer),synthesis(constant400,output),synthesis(type,constant-integer)]),b(identifier(lo406),integer,[synthesis(type,integer),synthesis(constant405,output),synthesis(type,constant-integer)]),b(identifier(lo412),integer,[synthesis(type,integer),synthesis(minus1,output)])],
ProgramAST) ,
ProgramAST = b(conjunct(b(equal(b(identifier('coins\''),integer,_),b(value(int(0)),integer,_)),pred,_),b(equal(b(identifier('soda\''),integer,[nodeid(pos(6,1,2,18,2,21))]),b(minus(b(identifier(soda),integer,_),b(value(int(3)),integer,_)),integer,_)),pred,_)),pred,_).
test(lVar2Prog_Guard_EnumeratedSets) :-
b_synthesis:location_vars_to_program([equal-global('GROUPS'),not_equal-global('GROUPS'),constant-global('GROUPS')],guard,[b(identifier(group),global('GROUPS'),[nodeid(pos(13,1,10,3,10,7))])],[b(identifier(li51),integer,[synthesis(equal1,left_input),synthesis(type,global('GROUPS'))]),b(identifier(li52),integer,[synthesis(equal1,right_input),synthesis(type,global('GROUPS'))]),b(identifier(li54),integer,[synthesis(not_equal2,left_input),synthesis(type,global('GROUPS'))]),b(identifier(li55),integer,[synthesis(not_equal2,right_input),synthesis(type,global('GROUPS'))]),b(identifier(lo53),integer,[synthesis(equal1,output),synthesis(type,pred)]),b(identifier(lo56),integer,[synthesis(not_equal2,output),synthesis(type,pred)]),b(identifier(lo58),integer,[synthesis(constant57,output),synthesis(type,global('GROUPS')),synthesis(type,global('GROUPS'))]),b(identifier(lo59),integer,[synthesis(max_floor,output),synthesis(type,integer),synthesis(machineconstant,b(identifier(max_floor),integer,[nodeid(pos(9,1,6,3,6,11))]))]),b(identifier(lo60),integer,[synthesis(min_floor,output),synthesis(type,integer),synthesis(machineconstant,b(identifier(min_floor),integer,[nodeid(pos(10,1,7,3,7,11))]))]),b(identifier(lvisitor),integer,[synthesis(input(0)),synthesis(example(0)),synthesis(type,global('GROUPS')),synthesis(initial_example),synthesis(type,global('GROUPS')),synthesis(machinevar,group),nodeid(none)]),b(identifier(lovalue00boolean),integer,[synthesis(output(0)),synthesis(example(0)),synthesis(type,boolean),synthesis(type,pred)]),b(identifier(lo60),integer,[synthesis(min_floor,output),synthesis(type,integer),synthesis(machineconstant,b(identifier(min_floor),integer,[nodeid(pos(10,1,7,3,7,11))]))]),b(identifier(lo59),integer,[synthesis(max_floor,output),synthesis(type,integer),synthesis(machineconstant,b(identifier(max_floor),integer,[nodeid(pos(9,1,6,3,6,11))]))]),b(identifier(lo58),integer,[synthesis(constant57,output),synthesis(type,global('GROUPS')),synthesis(type,global('GROUPS'))]),b(identifier(lo56),integer,[synthesis(not_equal2,output),synthesis(type,pred)]),b(identifier(lo53),integer,[synthesis(equal1,output),synthesis(type,pred)]),b(identifier(li55),integer,[synthesis(not_equal2,right_input),synthesis(type,global('GROUPS'))]),b(identifier(li54),integer,[synthesis(not_equal2,left_input),synthesis(type,global('GROUPS'))]),b(identifier(li52),integer,[synthesis(equal1,right_input),synthesis(type,global('GROUPS'))]),b(identifier(li51),integer,[synthesis(equal1,left_input),synthesis(type,global('GROUPS'))]),b(identifier(lovalue00boolean),integer,[synthesis(program_line(5)),synthesis(output(0)),synthesis(example(0)),synthesis(type,boolean),synthesis(type,pred)])],5,1,solution([binding(constant57,fd(1,'GROUPS'),staff),binding(li51,int(0),'0'),binding(li52,int(1),'1'),binding(li54,int(0),'0'),binding(li55,int(0),'0'),binding(lo53,int(5),'5'),binding(lo56,int(4),'4'),binding(lo58,int(1),'1'),binding(lo59,int(3),'3'),binding(lo60,int(2),'2'),binding(lovalue00boolean,int(5),'5'),binding(lvisitor,int(0),'0')]),
[b(identifier(lo53),integer,[synthesis(equal1,output),synthesis(type,pred)]),b(identifier(lo58),integer,[synthesis(constant57,output),synthesis(type,global('GROUPS')),synthesis(type,global('GROUPS'))])],
ProgramAst) ,
ProgramAst = b(equal(b(identifier(group),global('GROUPS'),[nodeid(pos(13,1,10,3,10,7))]),b(value(fd(1,'GROUPS')),global('GROUPS'),[synthesis(constant57,output),synthesis(type,global('GROUPS')),synthesis(type,global('GROUPS'))])),pred,[synthesis(equal1,output),synthesis(type,pred)]).
Calls:
Name: =/2 |
|
| Module: b_synthesis |
test(simple_set,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_test_machine.mch')) , b_machine_precompile ,
b_synthesis:prepare_synthesis_of_action_by_examples(simple_set,[[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])]],[[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])]],Library,ParameterAmount,M1,CurrentVars,BehavioralConstraint,LocationVars,Solution) ,
b_synthesis:synthesis_from_examples(simple_set,b(truth,pred,[]),([],[]),Library,1,CurrentVars,CurrentVars,any,action,[[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])]],[[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),nodeid(none)])]],BehavioralConstraint,LocationVars,M1,ParameterAmount,Solution,Synthesized,_) , ! ,
b_synthesis:reset_synthesis_context ,
synthesis_util:parallel_to_conjunction(Synthesized,SynthesizedPred) ,
b_test_boolean_expression_wf(b(equivalence(SynthesizedPred,b(conjunct(b(conjunct(b(equal(b(identifier('b\''),boolean,[nodeid(pos(5,1,2,11,2,11))]),b(value(pred_true),integer,[synthesis(type,boolean),synthesis(constant6,output),synthesis(type,constant-boolean)])),pred,[]),b(equal(b(identifier('s\''),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(union(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(value([int(2)]),integer,[synthesis(type,set(integer)),synthesis(constant1,output),synthesis(type,constant-set(integer))])),set(integer),[synthesis(type,set(integer)),synthesis(union1,output)])),pred,[])),pred,[]),b(equal(b(identifier('i\''),integer,[nodeid(pos(6,1,2,13,2,13))]),b(add(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(value(int(0)),integer,[synthesis(type,integer),synthesis(constant8,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add1,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(simple_bool,[nondet]) :-
b_synthesis:start_specific_synthesis(bool_test,action,[[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(empty_set,set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,i),nodeid(none)])]],[],[[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(empty_set,set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,i),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,SubstitutionPred) ,
b_test_boolean_expression_wf(b(equivalence(SubstitutionPred,b(conjunct(b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(5,1,2,11,2,11))]),b(value(pred_false),integer,[synthesis(type,boolean),synthesis(type,boolean),synthesis(constant18,output),synthesis(type,constant-boolean)])),pred,[]),b(equal(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(union(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(value([]),integer,[synthesis(type,set(integer)),synthesis(constant13,output),synthesis(type,constant-set(integer))])),set(integer),[synthesis(type,set(integer)),synthesis(union1,output)])),pred,[])),pred,[]),b(equal(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(add(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(value(int(1)),integer,[synthesis(type,integer),synthesis(constant20,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add1,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(simple_bool_skip_variable,[nondet]) :-
b_synthesis:start_specific_synthesis(bool_test,action,[[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(empty_set,set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,i),nodeid(none)])]],[],[[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(empty_set,set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,i),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,SubstitutionPred) ,
b_test_boolean_expression_wf(b(equivalence(SubstitutionPred,b(conjunct(b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(5,1,2,11,2,11))]),b(identifier(b),boolean,[nodeid(pos(5,1,2,11,2,11))])),pred,[]),b(equal(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(union(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(value([]),integer,[synthesis(type,set(integer)),synthesis(constant13,output),synthesis(type,constant-set(integer))])),set(integer),[synthesis(type,set(integer)),synthesis(union1,output)])),pred,[])),pred,[]),b(equal(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(add(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(value(int(0)),integer,[synthesis(type,integer),synthesis(constant20,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add1,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(simple_test_union_multiplication,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_test_machine.mch')) , b_machine_precompile ,
preferences:set_preference(time_out,60000) ,
b_synthesis:start_specific_synthesis(test_all,action,[[b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(empty_set,set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,i),nodeid(none)])]],[],[[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(9),integer,[synthesis(machinevar,i),nodeid(none)])],[b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(1),true,1,empty,node(int(4),true,0,empty,empty)),node(int(6),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(machinevar,s),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,i),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,SubstitutionPred) ,
b_test_boolean_expression_wf(b(equivalence(SubstitutionPred,b(conjunct(b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(5,1,2,11,2,11))]),b(value(pred_false),integer,[synthesis(type,boolean),synthesis(type,boolean),synthesis(constant245,output),synthesis(type,constant-boolean)])),pred,[]),b(equal(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(union(b(identifier(s),set(integer),[nodeid(pos(7,1,2,15,2,15))]),b(value(avl_set(node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty)))),integer,[synthesis(type,set(integer)),synthesis(constant240,output),synthesis(type,constant-set(integer))])),set(integer),[synthesis(type,set(integer)),synthesis(union1,output)])),pred,[])),pred,[]),b(equal(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(multiplication(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(minus(b(identifier(i),integer,[nodeid(pos(6,1,2,13,2,13))]),b(value(int(0)),integer,[synthesis(type,integer),synthesis(constant249,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(minus1,output)])),integer,[synthesis(type,integer),synthesis(multiplication1,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(beverage_vending_machine_strengthen_guard,[nondet]) :-
preferences:set_preference(time_out,5000) ,
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_vending_machine.mch')) , b_machine_precompile ,
b_synthesis:start_specific_synthesis(get_soda,guard,[[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(8),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(7),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(6),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])]],[[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])]],[[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(7),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(6),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])]],[[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])]],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
b_test_boolean_expression_wf(b(equivalence(Synthesized,b(conjunct(b(greater(b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))]),b(value(int(0)),integer,[synthesis(type,integer),synthesis(constant9,output),synthesis(type,constant-integer)])),boolean,[synthesis(type,boolean),synthesis(greater1,output)]),b(greater(b(identifier(coins),integer,[nodeid(pos(31,1,8,29,8,33)),loc(local,simple_vending_machine,abstract_variables)]),b(integer(0),integer,[nodeid(pos(32,1,8,37,8,37))])),pred,[nodeid(pos(30,1,8,29,8,37))])),pred,[])),pred,[]),[],_).
test(beverage_vending_machine_relax_invariant,[nondet]) :-
b_synthesis:start_specific_synthesis(get_soda,invariant,[[b(integer(7),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(6),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(8),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],[[b(integer(6),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(7),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
b_test_boolean_expression_wf(b(equivalence(Synthesized,b(greater_equal(b(identifier(coins),integer,[nodeid(pos(10,1,4,2,4,6)),loc(local,simple_vending_machine,abstract_variables)]),b(integer(0),integer,[nodeid(pos(11,1,4,11,4,11))])),pred,[section(invariant),nodeid(pos(9,1,4,2,4,11))])),pred,[]),[],_).
test(beverage_vending_machine_get_soda_action,[nondet]) :-
b_synthesis:start_specific_synthesis(get_soda,action,[[b(integer(5),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],[[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(1),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,SubstitutionPred) ,
b_test_boolean_expression_wf(b(equivalence(SubstitutionPred,b(conjunct(b(equal(b(identifier(coins),integer,[nodeid(pos(5,1,2,11,2,15))]),b(add(b(identifier(coins),integer,[nodeid(pos(5,1,2,11,2,15))]),b(value(int(-1)),integer,[synthesis(type,integer),synthesis(constant11,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add2,output)])),pred,[]),b(equal(b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))]),b(add(b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))]),b(value(int(-1)),integer,[synthesis(type,integer),synthesis(constant11,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add1,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(beverage_vending_machine_three_for_two_action,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_vending_machine.mch')) , b_machine_precompile ,
b_synthesis:start_specific_synthesis(three_for_two,action,[[b(integer(4),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],[[b(integer(2),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,SubstitutionPred) ,
b_test_boolean_expression_wf(b(equivalence(SubstitutionPred,b(conjunct(b(equal(b(identifier('coins\''),integer,[nodeid(pos(5,1,2,11,2,15))]),b(add(b(identifier(coins),integer,[nodeid(pos(5,1,2,11,2,15))]),b(value(int(-2)),integer,[synthesis(type,integer),synthesis(constant3,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add1,output)])),pred,[]),b(equal(b(identifier('soda\''),integer,[nodeid(pos(6,1,2,18,2,21))]),b(add(b(identifier(soda),integer,[nodeid(pos(6,1,2,18,2,21))]),b(value(int(-3)),integer,[synthesis(type,integer),synthesis(constant1,output),synthesis(type,constant-integer)])),integer,[synthesis(type,integer),synthesis(add2,output)])),pred,[])),pred,[])),pred,[]),[],_).
test(access_control_lift_repair_considering_enumerated_set,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_lift.mch')) , b_machine_precompile ,
b_synthesis:start_specific_synthesis(protected_up,guard,[[b(identifier(staff),global('GROUPS'),[synthesis(type,global('GROUPS')),synthesis(machinevar,group),nodeid(none)])]],[[b(identifier(visitor),global('GROUPS'),[synthesis(type,global('GROUPS')),synthesis(machinevar,group),nodeid(none)])]],[],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
Synthesized \= none ,
b_test_boolean_expression_wf(b(equivalence(Synthesized,b(conjunct(b(equal(b(identifier(group),global('GROUPS'),[nodeid(pos(13,1,10,3,10,7))]),b(identifier(staff),global('GROUPS'),[synthesis(constant37,output),synthesis(type,global('GROUPS')),synthesis(type,global('GROUPS'))])),pred,[synthesis(equal1,output),synthesis(type,pred)]),b(equal(b(identifier(floor),integer,[nodeid(pos(90,1,55,9,55,13)),loc(local,sample_lift,abstract_variables)]),b(minus(b(identifier(max_floor),integer,[nodeid(pos(92,1,55,17,55,25)),loc(local,sample_lift,concrete_constants),readonly]),b(integer(1),integer,[nodeid(pos(93,1,55,29,55,29))])),integer,[nodeid(pos(91,1,55,17,55,29))])),pred,[nodeid(pos(89,1,55,9,55,29))])),pred,[])),pred,[]),[],_).
test(scheduler_inv1,[nondet]) :-
% exact lib: [0.06,0.08,0.07,0.09,0.06,0.08,0.08,0.07,0.08,0.08] -> [0.06,0.07,0.08,0.09] -> Median: 0.07
% default lib: [10.9,11.01,10.91,10.87,10.84,10.94,10.56,11.13,10.98,10.91] -> [10.56,10.84,10.87,10.9,10.91,10.94,10.98,11.01,11.13] -> Median: 10.91
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([intersection,equal,constant]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(null,invariant,[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],Synthesized) ,
translate:print_bexpr(Synthesized) , nl , nl ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_inv2,[nondet]) :-
% exact lib: [1.54,1.65,1.63,1.72,1.65,1.62,1.65,1.64,1.64,1.64] -> [1.54,1.62,1.63,1.64,1.65,1.72] -> Median: 1.63
% default lib: Median: 229.340
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([intersection,union,equal,constant]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(null,invariant,
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],Synthesized) ,
translate:print_bexpr(Synthesized) , nl , nl ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_inv3,[nondet]) :-
% exact lib: [0.07,0.03,0.06,0.07,0.06,0.04,0.03,0.03,0.06,0.05] -> [0.03,0.04,0.05,0.06,0.07] -> Median: 0.05
% default lib: [1.55,1.56,1.6,1.6,1.62,1.61,1.51,1.6,1.54,1.63] -> [1.51,1.54,1.55,1.56,1.6,1.61,1.62,1.63] -> Median: 1.56
%assertz(b_synthesis:library_from_ui([predicates([constant-integer]),numbers([less_equal]),relations([]),sequences([]),sets([card]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(null,invariant,
[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],Synthesized) ,
translate:print_bexpr(Synthesized) , nl , nl ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_inv4,[nondet]) :-
% exact lib: [0.17,0.18,0.15,0.17,0.18,0.17,0.19,0.16,0.17,0.17] -> [0.15,0.16,0.17,0.18,0.19] -> Median: 0.17
% default lib: [1.42,1.25,1.66,1.47,1.43,1.46,1.5,1.42,1.68,1.36] -> [1.25,1.36,1.42,1.43,1.46,1.47,1.5,1.66,1.68] -> Median: 1.46
%assertz(b_synthesis:library_from_ui([predicates([disjunct]),numbers([]),relations([]),sequences([]),sets([equal,not_equal,constant]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(null,invariant,[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],Synthesized) ,
translate:print_bexpr(Synthesized) , nl , nl ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_repair_new,[nondet]) :-
% adapt loaded machine in public_examples
assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([not_member]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(new,guard,
[[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p2),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],
[[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p1))]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p2),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_delete_process,[nondet]) :-
% exact lib: [0.25,0.25,0.23,0.24,0.25,0.24,0.24,0.2,0.22,0.22] -> [0.2,0.22,0.23,0.24,0.25] -> Median: 0.23
% default lib: [0.86,0.94,0.93,0.97,0.93,0.89,0.86,0.97,0.88,0.92] -> [0.86,0.88,0.89,0.92,0.93,0.94,0.97] -> Median: 0.92
% guard: member
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([set_subtraction]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(del,action,
[[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])]],
[[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])]],
[[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_new_process,[nondet]) :-
% exact lib: [0.17,0.21,0.17,0.18,0.18,0.19,0.18,0.14,0.19,0.18] -> [0.14,0.17,0.18,0.19,0.21] -> Median: 0.18
% default lib: [0.79,0.85,0.82,0.97,0.80,0.94,1.27,0.78,1.4,0.94] -> [0.78,0.79,0.8,0.82,0.85,0.94,0.97,1.27,1.4] -> Median: 0.85
% guard: not_member
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([union]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(new,action,
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_set_active,[nondet]) :-
% exact lib: [0.77,0.91,0.78,0.78,1.47,0.81,0.74,1.06,0.88,0.92] -> [0.74,0.77,0.78,0.81,0.88,0.91,0.92,1.06,1.47] -> Median: 0.88
% default lib: [2,65,2.54,2.95,2.85,2.65,4.76,4.64,2.62,3.03,2.65] -> [2.54,2.62,2.65,2.85,2.95,3.03,4.64,4.76,2,65] -> Median: 2.95
% preds for guard: equal,member,conjunct
%preferences:set_preference(time_out,500) ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([set_subtraction]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(set_active,action,
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_set_ready,[nondet]) :-
% exact lib: [1.13,0.78,0.74,1.37,1.0,0.75,1.03,0.99,1.19,1.08] -> [0.74,0.75,0.78,0.99,1.01,1.03,1.08,1.13,1.19,1.37] -> Median: 1.01
% default lib: [5.14,5.26,4.66,4.83,4.96,4.84,4.76,4.77,5.01,4.77] -> [4.66,4.76,4.77,4.83,4.84,4.96,5.01,5.14,5.26] -> Median: 4.84
% preds for guard: member,not_equal,conjunct,constant
%preferences:set_preference(time_out,1000) ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([set_subtraction,union]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(ready,action,
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_active_to_waiting,[nondet]) :-
% exact lib: [0.56,0.48,0.64,0.62,0.59,0.51,0.74,0.76,0.5,0.77] -> [0.48,0.5,0.51,0.56,0.59,0.62,0.64,0.74,0.76,0.77] -> Median: 0.59
% default lib: [4.98,2.62,4.91,4.68,4.40,5.44,4.5,4.96,5.64,5.21] -> [2.62,4.4,4.5,4.68,4.91,4.96,4.98,5.21,5.44,5.64] -> Median: 4.91
% preds for guard: equal,not_equal,conjunct,constant
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([union]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(active_to_waiting,action,
[[b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[]),b(identifier(p2),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[]),b(identifier(p2),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p1),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([]),set(global('PID')),[synthesis(machinevar,active)]),b(set_extension([]),set(global('PID')),[synthesis(machinevar,ready)]),b(set_extension([b(identifier(p1),global('PID'),[]),b(identifier(p3),global('PID'),[])]),set(global('PID')),[synthesis(machinevar,waiting)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)]),b(identifier(p3),global('PID'),[nodeid(5)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(scheduler_ready_to_active,[nondet]) :-
% exact lib: [1.56,1.93,1.76,1.73,1.55,1.93,2.27,1.66,2.48,1.67] -> [1.55,1.56,1.66,1.67,1.73,1.76,1.93,2.27,2.48] -> Median: 1.73
% default lib: [6.24,6.74,5.74,8.28,6.3,6.29,8.11,5.84,6.58,5.73] -> [5.73,5.74,5.84,6.24,6.29,6.3,6.58,6.74,8.11,8.28] -> Median: 6.29
% preds for guard: member,not_equal,conjunct,constant
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([union,set_subtraction]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(ready_to_active,action,
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p3),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p2),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],
[[b(empty_set,set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])],[b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)]),b(identifier(p2),global('PID'),[nodeid(4)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,waiting),nodeid(2)]),b(set_extension([b(identifier(p3),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,ready),nodeid(2)]),b(set_extension([b(identifier(p1),global('PID'),[nodeid(3)])]),set(global('PID')),[synthesis(type,set(global('PID'))),synthesis(machinevar,active),nodeid(2)])]],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) , !.
test(eval_1,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_vending_machine.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,constant-integer,skip-integer]),relations([]),sequences([]),sets([]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_1,action,[[b(integer(5),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[],[[b(integer(6),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(3),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,_SubstitutionPred).
test(eval_2,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_vending_machine.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([conjunct]),numbers([minus,minus,constant-integer,constant-integer,greater,greater]),relations([]),sequences([]),sets([]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_2,action,[[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(6),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(6),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(5),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[[b(integer(6),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_3,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_vending_machine.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([conjunct]),numbers([minus,minus,constant-integer,constant-integer,greater,greater]),relations([]),sequences([]),sets([]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_3,action,[[b(integer(3),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(4),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(4),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[[b(value(int(1)),integer,[synthesis(machinevar,coins)]),b(value(int(1)),integer,[synthesis(machinevar,soda)])],[b(value(int(0)),integer,[synthesis(machinevar,coins)]),b(value(int(1)),integer,[synthesis(machinevar,soda)])],[b(value(int(0)),integer,[synthesis(machinevar,coins)]),b(value(int(6)),integer,[synthesis(machinevar,soda)])],[b(value(int(6)),integer,[synthesis(machinevar,coins)]),b(value(int(0)),integer,[synthesis(machinevar,soda)])],[b(value(int(0)),integer,[synthesis(machinevar,coins)]),b(value(int(0)),integer,[synthesis(machinevar,soda)])],[b(value(int(3)),integer,[synthesis(machinevar,coins)]),b(value(int(2)),integer,[synthesis(machinevar,soda)])],[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(3),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(2),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])]],[[b(integer(1),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(0),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(0),integer,[synthesis(machinevar,soda),synthesis(type,integer),nodeid(none)])],[b(integer(2),integer,[synthesis(machinevar,coins),synthesis(type,integer),nodeid(none)]),b(integer(1),integer,[synthesis(machinevar,soda),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_4,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/simple_test_machine.mch')) , b_machine_precompile ,
Input = [[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(type,set(integer)),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_false,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(2),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(5),integer,[nodeid(none)]),b(integer(8),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(3),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_false,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(6),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])]] ,
Output = [[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(0),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_false,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(8),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_true,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(set_extension([b(integer(5),integer,[nodeid(none)]),b(integer(8),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)])]),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(12),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])],
[b(boolean_false,boolean,[synthesis(initial_example),synthesis(type,boolean),synthesis(machinevar,b),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(initial_example),synthesis(machinevar,s),synthesis(type,set(integer)),nodeid(none)]),b(integer(24),integer,[synthesis(initial_example),synthesis(machinevar,i),synthesis(type,integer),nodeid(none)])]] ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([multiplication,constant-integer]),relations([]),sequences([]),sets([union,constant]),substitutions([skip-boolean])])) ,
b_synthesis:start_specific_synthesis(eval_4,action,Input,[],Output,[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_5,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([multiplication,power_of]),relations([]),sequences([]),sets([set_subtraction,union]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_5,action,
[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(12),true,0,node(int(3),true,0,empty,empty),node(int(34),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(9),true,0,node(int(1),true,0,empty,empty),node(int(12),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(19),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))),node(int(7),true,1,node(int(6),true,0,empty,empty),node(int(8),true,1,empty,node(int(13),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],
[],
[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(65536),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(32),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(9),true,0,node(int(1),true,1,empty,node(int(3),true,0,empty,empty)),node(int(12),true,1,empty,node(int(34),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,1,empty,node(int(34),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(256),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(16),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],
[b(value(avl_set(node(int(5),true,0,node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))),node(int(8),true,0,node(int(6),true,1,empty,node(int(7),true,0,empty,empty)),node(int(13),true,1,empty,node(int(19),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(19),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(25),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(10),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],
[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_6,[nondet]) :-
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([union,union,skip,intersection]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_6,action,[[b(value(avl_set(node(int(7),true,0,node(int(3),true,0,empty,empty),node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(5),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(7),true,1,empty,node(int(12),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(4),true,1,node(int(2),true,0,empty,empty),node(int(8),true,1,empty,node(int(9),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(9),true,0,node(int(3),true,1,empty,node(int(5),true,0,empty,empty)),node(int(12),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(8),true,1,node(int(2),true,0,empty,empty),node(int(12),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(5),true,1,node(int(3),true,0,empty,empty),node(int(6),true,1,empty,node(int(12),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[],[[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(5),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(7),true,0,node(int(5),true,0,empty,empty),node(int(12),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(8),true,0,node(int(2),true,1,empty,node(int(4),true,0,empty,empty)),node(int(12),true,0,node(int(9),true,0,empty,empty),node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(9),true,0,node(int(3),true,1,empty,node(int(5),true,0,empty,empty)),node(int(12),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(8),true,0,node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(5),true,0,empty,empty)),node(int(12),true,0,node(int(9),true,0,empty,empty),node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(3),true,1,empty,node(int(4),true,0,empty,empty)),node(int(6),true,1,empty,node(int(12),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,_SubstitutionPred).
test(eval_7,[nondet]) :-
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([multiplication]),relations([]),sequences([first,skip]),sets([intersection,subset,skip]),substitutions([convert_bool])])) ,
b_synthesis:start_specific_synthesis(eval_7,action,[[b(value(avl_set(node(int(8),true,0,node(int(2),true,1,empty,node(int(5),true,0,empty,empty)),node(int(9),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(25),integer,[nodeid(none)]),b(integer(24),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(13),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(6),true,1,empty,node(int(13),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(12),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,0,empty,empty),node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(12),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(9),integer,[nodeid(none)]),b(integer(13),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(8),true,1,node(int(3),true,0,empty,empty),node(int(9),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(8),true,0,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)),node(int(13),true,0,node(int(9),true,0,empty,empty),node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(2),integer,[nodeid(none)]),b(integer(13),integer,[nodeid(none)]),b(integer(14),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(value(avl_set(node(int(8),true,0,node(int(2),true,1,empty,node(int(5),true,0,empty,empty)),node(int(9),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(2),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(25),integer,[nodeid(none)]),b(integer(24),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(60),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(13),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(13),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(12),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(15),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,0,empty,empty),node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(4),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(9),integer,[nodeid(none)]),b(integer(13),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(54),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(8),true,1,node(int(3),true,0,empty,empty),node(int(9),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(8),true,1,node(int(3),true,0,empty,empty),node(int(9),true,1,empty,node(int(14),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(2),integer,[nodeid(none)]),b(integer(13),integer,[nodeid(none)]),b(integer(14),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(16),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,_SubstitutionPred).
test(eval_8,[nondet]) :-
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([concat,skip]),sets([set_subtraction,intersection,subset,union,union]),substitutions([convert_bool])])) ,
b_synthesis:start_specific_synthesis(eval_8,action,[[b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(12),true,1,empty,node(int(33),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(12),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(6),true,1,node(int(5),true,0,empty,empty),node(int(14),true,1,empty,node(int(21),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(9),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(12),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(value(avl_set(node(int(22),true,0,node(int(13),true,0,empty,empty),node(int(24),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(13),true,0,node(int(10),true,1,empty,node(int(12),true,0,empty,empty)),node(int(22),true,0,node(int(14),true,0,empty,empty),node(int(24),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(6),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(8),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(value(avl_set(node((int(1),int(12)),true,1,empty,node((int(2),int(14)),true,0,empty,empty)))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,seq_2),nodeid(none)])],[b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(4),true,1,empty,node(int(13),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(13),true,0,node(int(6),true,0,empty,empty),node(int(15),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(4),true,0,node(int(3),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(12),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(10),integer,[nodeid(none)]),b(integer(11),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(value(avl_set(node(int(12),true,0,node(int(2),true,0,empty,empty),node(int(14),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(13),true,0,node(int(2),true,1,empty,node(int(12),true,0,empty,empty)),node(int(14),true,1,empty,node(int(15),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(4),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(8),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(10),integer,[nodeid(none)]),b(integer(12),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(value([int(0)]),set(integer),[synthesis(machinevar,set_1)]),b(value([]),set(integer),[synthesis(machinevar,set_2)]),b(value([int(0)]),set(integer),[synthesis(machinevar,set_3)]),b(sequence_extension([b(integer(0),integer,[])]),seq(integer),[synthesis(machinevar,seq_1)]),b(value(pred_false),boolean,[synthesis(machinevar,b_1)]),b(sequence_extension([]),seq(integer),[synthesis(machinevar,seq_2)])]],[],[[b(value(avl_set(node(int(1),true,1,empty,node(int(33),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(12),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(6),true,1,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(5),true,0,empty,empty)),node(int(14),true,1,node(int(12),true,0,empty,empty),node(int(21),true,1,empty,node(int(33),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(9),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(12),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(9),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(22),true,0,node(int(13),true,0,empty,empty),node(int(24),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(13),true,0,node(int(10),true,0,node(int(3),true,0,empty,empty),node(int(12),true,0,empty,empty)),node(int(22),true,0,node(int(14),true,0,empty,empty),node(int(24),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(6),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(8),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(12),integer,[nodeid(none)]),b(integer(14),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(8),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(4),true,1,empty,node(int(13),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)),node(int(6),true,1,node(int(5),true,0,empty,empty),node(int(13),true,1,empty,node(int(15),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(12),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(10),integer,[nodeid(none)]),b(integer(11),integer,[nodeid(none)]),b(integer(12),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(12),true,0,node(int(2),true,0,empty,empty),node(int(14),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(7),true,1,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(4),true,0,empty,empty)),node(int(13),true,1,node(int(12),true,0,empty,empty),node(int(14),true,1,empty,node(int(15),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)]),b(sequence_extension([b(integer(8),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(10),integer,[nodeid(none)]),b(integer(12),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)])],[b(value([int(0)]),set(integer),[synthesis(machinevar,set_1)]),b(value([]),set(integer),[synthesis(machinevar,set_2)]),b(value([int(0)]),set(integer),[synthesis(machinevar,set_3)]),b(sequence_extension([b(integer(0),integer,[])]),seq(integer),[synthesis(machinevar,seq_1)]),b(value(pred_false),boolean,[synthesis(machinevar,b_1)]),b(sequence_extension([b(integer(0),integer,[])]),seq(integer),[synthesis(machinevar,seq_2)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,Substitution),_,_) ,
synthesis_util:parallel_to_conjunction(Substitution,_SubstitutionPred).
test(eval_9,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/euclid.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([greater,add,minus,constant-integer,constant-integer,if_then_else-integer]),relations([]),sequences([]),sets([]),substitutions([])])) ,
assertz(b_synthesis:consider_if_var_names([a])) ,
%assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_9,action,[[b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(21),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(10),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])]],[],[[b(integer(17),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(24),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])],[b(integer(15),integer,[synthesis(type,integer),synthesis(machinevar,a),nodeid(none)])]],[],Synthesized) , ! ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
retractall(b_synthesis:consider_if_var_names(_)) ,
retractall(b_synthesis:not_consider_constants(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_10,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%preferences:set_preference(time_out,240000) ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,constant-integer,greater,constant-integer,if_then_else-integer,if_then_else-set(integer),union-set(integer),constant-set(integer),skip-integer,skip-set(integer)]),relations([]),sequences([]),sets([]),substitutions([])])) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_10,action,[[b(value(avl_set(node(int(1),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(10),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(1),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(value(avl_set(node(int(1),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(2),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(integer(15),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
retractall(b_synthesis:not_consider_constants(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_12,[nondet]) :-
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([union-set(integer),union-set(integer),union-set(integer),general_union-set(set(integer)),skip-set(set(integer)),subset-set(integer),member-set(set(integer))]),relations([]),sequences([]),sets([]),substitutions([convert_bool])])) ,
b_synthesis:start_specific_synthesis(eval_12,action,[[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(6),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(5),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(set_extension([b(integer(6),integer,[nodeid(none)])]),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(6),true,1,node(int(4),true,0,empty,empty),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(12),true,1,empty,node(int(13),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(6),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(4),true,0,node(int(1),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(6),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(4),true,0,node(int(3),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(8),true,0,node(int(4),true,0,empty,empty),node(int(9),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(7),true,1,empty,node(int(8),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(12),true,1,empty,node(int(14),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])]],[],[[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(5),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(set_extension([b(integer(6),integer,[nodeid(none)])]),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(6),true,1,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(4),true,0,empty,empty)),node(int(8),true,1,node(int(7),true,0,empty,empty),node(int(12),true,1,empty,node(int(13),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(7),true,0,node(int(4),true,1,empty,node(int(6),true,0,empty,empty)),node(int(12),true,0,node(int(8),true,0,empty,empty),node(int(13),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(4),true,0,node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)),node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(6),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(4),true,0,node(int(1),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(6),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_true,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])],[b(value(avl_set(node(int(7),true,1,node(int(4),true,0,node(int(3),true,0,empty,empty),node(int(5),true,0,empty,empty)),node(int(9),true,1,node(int(8),true,0,empty,empty),node(int(12),true,1,empty,node(int(14),true,0,empty,empty)))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(3),true,1,empty,node(int(4),true,0,empty,empty)),node(int(8),true,1,empty,node(int(9),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(value(avl_set(node(int(7),true,1,empty,node(int(8),true,0,empty,empty)))),set(integer),[nodeid(none)]),b(value(avl_set(node(int(12),true,1,empty,node(int(14),true,0,empty,empty)))),set(integer),[nodeid(none)])]),set(set(integer)),[synthesis(type,set(set(integer))),synthesis(machinevar,set_4),nodeid(none)]),b(boolean_false,boolean,[synthesis(type,boolean),synthesis(machinevar,b_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_13,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/mixed_typed.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,div,multiplication,constant-integer,constant-integer]),relations([]),sequences([]),sets([intersection,union,constant]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_13,action,[[b(set_extension([b(string(b),string,[nodeid(none)]),b(string(d),string,[nodeid(none)]),b(string(f),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(b),string,[nodeid(none)]),b(string(f),string,[nodeid(none)]),b(string(k),string,[nodeid(none)]),b(string(l),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(36),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(ds),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(dss),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(44),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)]),b(string(c),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(set_extension([b(string(b),string,[nodeid(none)]),b(string(d),string,[nodeid(none)]),b(string(f),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(b),string,[nodeid(none)]),b(string(f),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(26),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(dss),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(18),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_14,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/mixed_typed.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,div,multiplication,constant-integer,constant-integer]),relations([]),sequences([]),sets([intersection,union,constant]),substitutions([])])) ,
b_synthesis:start_specific_synthesis(eval_14,action,[[b(set_extension([b(string(b),string,[nodeid(none)]),b(string(d),string,[nodeid(none)]),b(string(f),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(b),string,[nodeid(none)]),b(string(f),string,[nodeid(none)]),b(string(k),string,[nodeid(none)]),b(string(l),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(36),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(ds),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(dss),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(44),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)]),b(string(c),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(b),string,[nodeid(none)]),b(string(d),string,[nodeid(none)]),b(string(f),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(36),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(dss),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(44),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(set_extension([b(string(b),string,[nodeid(none)]),b(string(d),string,[nodeid(none)]),b(string(f),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(b),string,[nodeid(none)]),b(string(f),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(26),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(ba),string,[nodeid(none)]),b(string(dss),string,[nodeid(none)]),b(string(fa),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(18),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(string(a),string,[nodeid(none)]),b(string(b),string,[nodeid(none)]),b(string(test),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(string(a),string,[nodeid(none)])]),set(string),[synthesis(type,set(string)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_15,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([max,union-set(integer),set_subtraction-set(integer),multiplication]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_15,action,[[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(1),true,0,empty,empty),node(int(5),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(6),true,0,node(int(2),true,0,empty,empty),node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(9),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,1,node(int(1),true,0,empty,empty),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(2),true,0,empty,empty),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(42),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(6),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(6),true,1,empty,node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(56),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(7),true,0,node(int(6),true,0,empty,empty),node(int(9),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(9),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(117),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(7),true,0,node(int(4),true,0,empty,empty),node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(40),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(4),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(24),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_16,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
% assertz components for the guard when running with explicit library
assertz(b_synthesis:library_from_ui([predicates([]),numbers([max,union-set(integer),set_subtraction-set(integer),multiplication]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_16,action,[[b(value(avl_set(node(int(7),true,0,node(int(3),true,0,empty,empty),node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(2),true,0,empty,empty),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(6),true,0,node(int(2),true,0,empty,empty),node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(1),true,0,empty,empty),node(int(5),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(6),true,0,node(int(5),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(9),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(2),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(4),true,1,node(int(2),true,0,empty,empty),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(5),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(value(avl_set(node(int(2),true,0,node(int(1),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(1),true,0,empty,empty),node(int(5),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(1),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(1),true,0,empty,empty),node(int(5),true,1,empty,node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,1,empty,node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,0,node(int(1),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(value(avl_set(node(int(4),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(40),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(6),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(6),true,1,empty,node(int(8),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(56),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(7),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(7),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(42),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(7),true,0,node(int(6),true,0,empty,empty),node(int(9),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(2),true,0,empty,empty),node(int(9),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(117),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(3),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(5),true,1,empty,node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(4),true,0,node(int(1),true,1,empty,node(int(2),true,0,empty,empty)),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(integer(24),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_17,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_int.mch')) , b_machine_precompile ,
% assertz components for the guard when running with explicit library
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,power_of,multiplication,skip-integer,add,minus]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_17,action,[[b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(10),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])]],[],[[b(integer(4096),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(130),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(1000),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(156),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(70),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(unary_minus(b(integer(3),integer,[nodeid(none)])),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(36),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(72),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_18,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_int.mch')) , b_machine_precompile ,
% assertz components for the guard when running with explicit library
%preferences:set_preference(time_out,15000) ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([add,power_of,multiplication,skip-integer,add,minus,minus,modulo]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(eval_18,action,[[b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(24),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(10),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(16),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(integer(16),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(14),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(15),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])]],[],[[b(integer(36),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(72),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(unary_minus(b(integer(6),integer,[nodeid(none)])),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(1000),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(156),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(12),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(70),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(unary_minus(b(integer(1),integer,[nodeid(none)])),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(unary_minus(b(integer(3),integer,[nodeid(none)])),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])],[b(integer(4096),integer,[synthesis(type,integer),synthesis(machinevar,int_3),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_2),nodeid(none)]),b(integer(130),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_6),nodeid(none)]),b(unary_minus(b(integer(4),integer,[nodeid(none)])),integer,[synthesis(type,integer),synthesis(machinevar,int_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_4),nodeid(none)])]],[],Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)) ,
Synthesized = b(operation(_,_,_,_Substitution),_,_).
test(eval_19,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([greater,constant-integer]),relations([]),sequences([]),sets([card,union]),substitutions([])])) ,
%preferences:set_preference(time_out,2500) ,
%retractall(b_synthesis:not_consider_constants(_)) ,
%assertz(b_synthesis:not_consider_constants(yes)),
b_synthesis:start_specific_synthesis(eval_19,guard,[[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[[b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(0),true,0,empty,empty),node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,0,node(int(2),true,1,empty,node(int(3),true,0,empty,empty)),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[],_Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(eval_20,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([constant-integer,disjunct]),relations([]),sequences([]),sets([member,constant,equal]),substitutions([])])) ,
%retractall(b_synthesis:not_consider_constants(_)) ,
%assertz(b_synthesis:not_consider_constants(yes)) ,
%preferences:set_preference(time_out,2500) ,
b_synthesis:start_specific_synthesis(eval_20,guard,[[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[[b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,0,node(int(0),true,0,empty,empty),node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[],_Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(eval_21,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([implication]),numbers([]),relations([]),sequences([]),sets([equal,constant,constant,subset_strict]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
%preferences:set_preference(time_out,2500) ,
b_synthesis:start_specific_synthesis(null,invariant,[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[],[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(6),true,1,node(int(3),true,0,empty,empty),node(int(7),true,1,empty,node(int(8),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(8),true,0,node(int(7),true,0,empty,empty),node(int(10),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_3),nodeid(none)])]],Synthesized) ,
translate:print_bexpr_or_subst(Synthesized) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(eval_22,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([]),sets([cartesian_product,union,union]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
%preferences:set_preference(time_out,2500) ,
b_synthesis:start_specific_synthesis(eval_22,action,[[b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(3),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(empty_set,set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(3)),true,0,empty,empty)))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(3),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node((int(2),int(1)),true,1,empty,node((int(3),int(2)),true,0,empty,empty)))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(4),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(set_extension([b(integer(2),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(set_extension([b(couple(b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)])),couple(integer,integer),[nodeid(none)])]),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,node(int(1),true,0,empty,empty),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node((int(1),int(4)),true,1,node((int(1),int(3)),true,0,empty,empty),node((int(2),int(3)),true,1,empty,node((int(2),int(4)),true,0,empty,empty))))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(1),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(2),true,1,empty,node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(empty_set,set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(1),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(3),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node((int(0),int(3)),true,1,empty,node((int(1),int(3)),true,0,empty,empty)))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,1,node(int(4),true,0,empty,empty),node(int(6),true,1,empty,node(int(9),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node(int(4),true,1,node(int(2),true,0,empty,empty),node(int(5),true,1,empty,node(int(6),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_2),nodeid(none)]),b(value(avl_set(node((int(5),int(2)),true,0,node((int(4),int(2)),true,0,empty,empty),node((int(6),int(2)),true,0,empty,empty)))),set(couple(integer,integer)),[synthesis(type,set(couple(integer,integer))),synthesis(machinevar,set_5),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],_) ,
retractall(b_synthesis:not_consider_constants(_)) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(eval_23,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([interval,add,max,constant-integer]),relations([]),sequences([domain_restriction]),sets([union]),substitutions([])])) ,
%retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
%preferences:set_preference(time_out,2500) ,
b_synthesis:start_specific_synthesis(eval_23,action,[[b(value(avl_set(node(int(1),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(0),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(integer(0),integer,[nodeid(none)])]),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,1,empty,node(int(1),true,0,empty,empty)),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,1,empty,node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(2)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(2)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[[b(value(avl_set(node(int(1),true,0,node(int(0),true,0,empty,empty),node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(0),true,1,empty,node(int(2),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(2)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,0,node(int(0),true,1,empty,node(int(1),true,0,empty,empty)),node(int(3),true,1,empty,node(int(4),true,0,empty,empty))))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(2),true,1,empty,node(int(4),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(6),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node(int(5),true,0,node(int(3),true,0,empty,empty),node(int(6),true,0,empty,empty)))),set(integer),[synthesis(type,set(integer)),synthesis(machinevar,set_1),nodeid(none)]),b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(2)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],_62965) ,
retractall(b_synthesis:not_consider_constants(_)) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(eval_25,[nondet]) :-
%b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
%assertz(b_synthesis:library_from_ui([predicates([]),numbers([]),relations([]),sequences([insert_tail,domain,domain_restriction]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
%preferences:set_preference(time_out,2500) ,
b_synthesis:start_specific_synthesis(eval_25,action,[[b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(sequence_extension([b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(value(avl_set(node((int(1),int(1)),true,1,empty,node((int(2),int(2)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(5),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(2),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],[[b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)]),b(integer(9),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(9),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(sequence_extension([b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(6),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(3),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(1),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(4),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(value(avl_set(node((int(1),int(5)),true,1,empty,node((int(2),int(3)),true,0,empty,empty)))),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(4),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(set_extension([b(couple(b(integer(1),integer,[nodeid(none)]),b(integer(7),integer,[nodeid(none)])),couple(integer,integer),[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(empty_set,seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])],[b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)]),b(integer(5),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_1),nodeid(none)]),b(sequence_extension([b(integer(1),integer,[nodeid(none)]),b(integer(2),integer,[nodeid(none)]),b(integer(3),integer,[nodeid(none)])]),seq(integer),[synthesis(type,seq(integer)),synthesis(machinevar,seq_2),nodeid(none)]),b(integer(5),integer,[synthesis(type,integer),synthesis(machinevar,int_1),nodeid(none)])]],[],_41195) ,
retractall(b_synthesis:not_consider_constants(_)) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(x_mal_x_plus_x_plus_1,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([multiplication,add,add,constant-integer]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(x_mal_x_plus_x_plus_1,action,
[[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],
[[b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(7),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(13),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(x_hoch_3,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([power_of,constant-integer]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(x_mal_x_mal_x,action,
[[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],
[[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(27),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(x_mal_x_mal_x,[nondet]) :-
b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/sample_all.mch')) , b_machine_precompile ,
assertz(b_synthesis:library_from_ui([predicates([]),numbers([multiplication,multiplication]),relations([]),sequences([]),sets([]),substitutions([])])) ,
retractall(b_synthesis:not_consider_constants(_)) ,
assertz(b_synthesis:not_consider_constants(yes)) ,
b_synthesis:start_specific_synthesis(x_mal_x_mal_x,action,
[[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(2),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(3),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],
[[b(integer(1),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(8),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])],[b(integer(27),integer,[synthesis(type,integer),synthesis(machinevar,int_1)])]],
[],_) ,
b_synthesis:reset_synthesis_context ,
retractall(b_synthesis:library_from_ui(_)).
test(get_single_constant_or_set_operator_id,[]) :-
synthesis_util:get_single_constant_or_set_operator_id(seq-integer_set,OutputId1,ValueId1) ,
OutputId1 = b(identifier(_),set(seq(integer)),[synthesis(type,seq-integer_set)]) ,
ValueId1 = b(seq(b(integer_set('INTEGER'),set(integer),[])),set(seq(integer)),[]) ,
synthesis_util:get_single_constant_or_set_operator_id(seq-integer_set_natural1,OutputId2,ValueId2) ,
OutputId2 = b(identifier(_),set(seq(integer)),[synthesis(type,seq-integer_set_natural1)]) ,
ValueId2 = b(seq(b(integer_set('NATURAL1'),set(integer),[])),set(seq(integer)),[]) ,
synthesis_util:get_single_constant_or_set_operator_id(seq-string_set,OutputId3,ValueId3) ,
OutputId3 = b(identifier(_),set(seq(string)),[synthesis(type,seq-string_set)]) ,
ValueId3 = b(seq(b(string_set,set(string),[])),set(seq(string)),[]) ,
synthesis_util:get_single_constant_or_set_operator_id(constant-set(seq(integer)),OutputId4,ValueId4) ,
OutputId4 = b(identifier(_),set(seq(integer)),[synthesis(type,constant-set(seq(integer)))]) ,
ValueId4 = b(identifier(ConstantName4),set(seq(integer)),[]) ,
synthesis_util:delete_numbers_from_atom(ConstantName4,RawConstantName4) ,
RawConstantName4 = constant ,
synthesis_util:get_single_constant_or_set_operator_id(constant-string,OutputId5,ValueId5) ,
OutputId5 = b(identifier(_),string,[synthesis(type,constant-string)]) ,
ValueId5 = b(identifier(ConstantName5),string,[]) ,
synthesis_util:delete_numbers_from_atom(ConstantName5,RawConstantName5) ,
RawConstantName5 = constant ,
synthesis_util:get_single_constant_or_set_operator_id(constant-set(boolean),OutputId6,ValueId6) ,
OutputId6 = b(identifier(_),set(boolean),[synthesis(type,constant-set(boolean))]) ,
ValueId6 = b(identifier(ConstantName6),set(boolean),[]) ,
synthesis_util:delete_numbers_from_atom(ConstantName6,RawConstantName6) ,
RawConstantName6 = constant.
test(fuzzing,[]) :-
fuzz(synthesis_util:find_typed_identifier_uses_with_info/2,100000,prob_ast_pred([]):var) ,
fuzz(synthesis_util:prime_or_unprime_variables_in_ast/4,100000,fixed(prime):fixed([]):prob_ast_pred([]):var) ,
fuzz(synthesis_util:prime_or_unprime_variables_in_ast/4,100000,fixed(unprime):fixed([]):prob_ast_pred([]):var).
Calls:
Name: fuzz/3 |
Module: foo_error |
Name: =/2 |
|
| Module: synthesis_util | |
| Module: synthesis_util | |
Name: retractall/1 |
|
| Module: b_synthesis | |
| Module: b_synthesis | |
Name: assertz/1 |
|
Name: b_machine_precompile/0 |
Module: bmachine |
| Module: bmachine | |
Name: print_bexpr_or_subst/1 |
Module: translate |
Name: ! |
|
| Module: synthesis_util | |
Name: nl |
|
Name: print_bexpr/1 |
Module: translate |
| Module: synthesis_tests | |
Name: \=/2 |
|
Name: set_preference/2 |
Module: preferences |
| Module: b_synthesis | |
| Module: b_synthesis |
tests :-
startup_prob,
external_functions:reset_argv,
prob_cli:set_prefs ,
logging:disable_logging ,
preferences:set_preference(randomise_enumeration_order,true).
Calls:
Name: set_preference/2 |
Module: preferences |
Name: disable_logging/0 |
Module: logging |
Name: set_prefs/0 |
Module: prob_cli |
Name: reset_argv/0 |
Module: external_functions |
Name: startup_prob/0 |
Module: prob_startup |