1 % minimize ProB AST sequence expressions for shrinking stage
2
3 minimize_seq_expr(b(sequence_extension(Seq),seq(Type),Info),b(sequence_extension(ShrunkenSeq),seq(Type),Info)) :-
4 is_list(Seq) ,
5 shrink(list(_),Seq,ShrunkenSeq).
6
7 minimize_seq_expr(b(value(Seq),seq(Type),Info),Shrunken) :-
8 shrink(prob_value_seq,Seq,ShrunkenSeq) ,
9 Shrunken = b(value(ShrunkenSeq),seq(Type),Info).
10
11 minimize_seq_expr(b(sequence_extension([]),seq(Inner),Info),b(sequence_extension([]),seq(Inner),Info)).
12
13 minimize_seq_expr(b(general_concat(SeqOfSeq),seq(Type),Info),Shrunken) :-
14 (prob_is_ground(SeqOfSeq,true)
15 -> seqint_avl(b(general_concat(SeqOfSeq),seq(Type),Info),ValueAvl) ,
16 Shrunken = b(value(ValueAvl),seq(Type),Info)
17 ; SeqOfSeq = b(sequence_extension(Seq),seq(OutterType),OutterInfo) ,
18 maplist(minimize_seq_expr,Seq,ShrunkenSeq) ,
19 Shrunken = b(general_concat(b(sequence_extension(ShrunkenSeq),seq(OutterType),OutterInfo)),seq(Type),Info)).
20
21 minimize_seq_expr(b(Expression,seq(Type),Info),Shrunken) :-
22 Expression =.. [Expr,Arg] ,
23 member(Expr,[front,tail,rev]) ,
24 (prob_is_ground(Arg,true)
25 -> seqint_avl(b(Expression,seq(Type),Info),ValueAvl) ,
26 (ValueAvl = avl_set(empty) ->
27 % no empty set for well-definedness
28 Shrunken = b(Expression,seq(Type),Info)
29 ; Shrunken = b(value(ValueAvl),seq(Type),Info))
30 ; minimize_seq_expr(Arg,NewArg) ,
31 NewExpr =.. [Expr,NewArg] ,
32 Shrunken = b(NewExpr,seq(Type),Info)).
33
34 minimize_seq_expr(b(Expression,seq(Type),Info),Shrunken) :-
35 Expression =.. [Expr,Seq,Value] ,
36 member(Expr,[restrict_front,restrict_tail]) ,
37 (prob_is_ground(Seq,true)
38 -> seqint_avl(b(Expression,seq(Type),Info),ValueAvl) ,
39 Shrunken = b(value(ValueAvl),seq(Type),Info)
40 ; minimize_seq_expr(Seq,NewArg) ,
41 % decrease restriction value by one after every shrinking call
42 % to keep well-definedness
43 Value = b(integer(Val),integer,IntInfo) ,
44 (Val = 0 -> NVal = Val ; NVal is Val - 1) ,
45 NewValue = b(integer(NVal),integer,IntInfo) ,
46 NewExpr =.. [Expr,NewArg,NewValue] ,
47 Shrunken = b(NewExpr,seq(Type),Info)).
48
49 minimize_seq_expr(b(concat(Seq1,Seq2),seq(Type),Info),b(value(ValueSeq),seq(Type),Info)) :-
50 prob_is_ground(Seq1,true) ,
51 prob_is_ground(Seq2,true) ,
52 seqint_avl(b(concat(Seq1,Seq2),seq(Type),Info),ValueSeq).
53 minimize_seq_expr(b(concat(Seq1,Seq2),seq(Type),Info),b(concat(NewSeq1,NewSeq2),seq(Type),Info)) :-
54 prob_is_ground(Seq1,Res1) ,
55 prob_is_ground(Seq2,Res2) ,
56 ( Res1 = true , Res2 = false
57 -> minimize_seq_expr(Seq2,NewSeq2) ,
58 NewSeq1 = Seq1
59 ; Res1 = false , Res2 = true
60 -> minimize_seq_expr(Seq1,NewSeq1) ,
61 NewSeq2 = Seq2
62 ; minimize_seq_expr(Seq1,NewSeq1) ,
63 minimize_seq_expr(Seq2,NewSeq2)).
64
65 minimize_seq_expr(b(insert_front(Value,Seq),seq(Type),Info),Shrunken) :-
66 (prob_is_ground(Seq,true)
67 -> seqint_avl(b(insert_front(Value,Seq),seq(Type),Info),ValueAvl) ,
68 Shrunken = b(value(ValueAvl),seq(Type),Info)
69 ; minimize_seq_expr(Seq,NewSeq) ,
70 NewExpr =.. [insert_front,Value,NewSeq] ,
71 Shrunken = b(NewExpr,seq(Type),Info)).
72
73 minimize_seq_expr(b(insert_tail(Seq,Value),seq(Type),Info),Shrunken) :-
74 (prob_is_ground(Seq,true)
75 -> seqint_avl(b(insert_tail(Value,Seq),seq(Type),Info),ValueAvl) ,
76 Shrunken = b(value(ValueAvl),seq(Type),Info)
77 ; minimize_seq_expr(Seq,NewSeq) ,
78 NewExpr =.. [insert_tail,NewSeq,Value] ,
79 Shrunken = b(NewExpr,seq(Type),Info)).
80
81 % skip identifier
82 minimize_seq_expr(b(identifier(Name),Type,Info),b(identifier(Name),Type,Info)).