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)). |