1 % collection of code snippets
2
3 set_wd_option(Options, WD) :-
4 member(not-well-defined, Options),
5 !,
6 WD = no.
7 set_wd_option(_, yes).
8
9 %% insert_identifier_to_ast(+WD, +AST, +Amount, -NewAst).
10 % Try to insert a given amount of identifier nodes to an ast, the actual amount can be less.
11 % WD is 'yes' or 'no' for considering well-definedness.
12 insert_identifier_to_ast(_,AST,0,AST) :- !.
13 insert_identifier_to_ast(_,b(Node,Type,_),_,NewAST) :-
14 (Node = min_int ; Node = max_int ; Type = boolean ; Node = integer(_) ; Node = string(_)) ,
15 generate(prob_ast_identifier(Type),NewAST).
16 insert_identifier_to_ast(_,b(Node,Type,_),_,NewAST) :-
17 Node =.. [_,Temp] , Type \= pred , Type \= record(_) , (Temp =.. [_] ; is_list(Temp)) ,
18 generate(prob_ast_identifier(Type),NewAST).
19 insert_identifier_to_ast(_,b(rec(_),record(Type),_),_,NewAST) :-
20 generate(prob_ast_identifier(record(Type)),NewAST).
21 insert_identifier_to_ast(WD,b(Node,Type,Info),Amount,NewAST) :-
22 Node =.. [Inner,Arg] ,
23 insert_identifier_to_ast(WD,Arg,Amount,NewArg) ,
24 NewNode =.. [Inner,NewArg] ,
25 NewAST = b(NewNode,Type,Info).
26 % no identifier for power_of
27 insert_identifier_to_ast(_,b(Node,Type,Info),_,NewAst) :-
28 Node = power_of(_,_),
29 !,
30 NewAst = b(Node,Type,Info).
31 insert_identifier_to_ast(yes,b(Node,Type,Info),Amount,NewAst) :-
32 Node = div(Lhs,Rhs),
33 !,
34 insert_identifier_to_ast(yes,Lhs,Amount,NewLhs) ,
35 NewAst = b(div(NewLhs,Rhs),Type,Info).
36 insert_identifier_to_ast(WD,b(Node,Type,Info),Amount,NewAST) :-
37 Node =.. [Inner,LArg,RArg] ,
38 LAmount is Amount div 2 ,
39 RAmount is Amount - LAmount ,
40 insert_identifier_to_ast(WD,LArg,LAmount,NLArg) ,
41 insert_identifier_to_ast(WD,RArg,RAmount,NRArg) ,
42 NewNode =.. [Inner,NLArg,NRArg] ,
43 NewAST = b(NewNode,Type,Info).
44 insert_identifier_to_ast(_,AST,_,AST).
45
46 % creates the type to use in generate/2 with prefix 'prob_ast_' or 'prob_value'
47 % only atom_concat wouldn't succeed if type is a term like set(integer([]))
48 % ASTType is either 'ast' or 'value'
49
50 % don't expand fixed values
51 gen_type(TypeIn,_,TypeIn) :-
52 TypeIn =.. [fixed,_].
53 gen_type(TypeIn,ASTType,NType) :-
54 TypeIn =.. [set,In] ,
55 atom_concat(prob_,ASTType,Temp) ,
56 atom_concat(Temp,'_',ProBType) ,
57 atom_concat(ProBType,set,NewPre) ,
58 NType =.. [NewPre,In,[]]. % no options for ast or value sets
59 gen_type(TypeIn,ASTType,NType) :-
60 TypeIn =.. [Type,In1,In2] ,
61 atom_concat(prob_,ASTType,Temp) ,
62 atom_concat(Temp,'_',ProBType) ,
63 atom_concat(ProBType,Type,NewPre) ,
64 NType =.. [NewPre,In1,In2].
65 gen_type(TypeIn,ASTType,NType) :-
66 TypeIn =.. [Type,In] , ! ,
67 atom_concat(prob_,ASTType,Temp) ,
68 atom_concat(Temp,'_',ProBType) ,
69 atom_concat(ProBType,Type,NewPre) ,
70 NType =.. [NewPre,In].
71 gen_type(Type,ASTType,NType) :-
72 Type =.. [_] ,
73 atom_concat(prob_,ASTType,Temp) ,
74 atom_concat(Temp,'_',ProBType) ,
75 atom_concat(ProBType,Type,NType).
76
77 % detype an ast like the parsers output
78 :- multifile generate/2.
79 generate(detype(AST),DetypedAST) :-
80 detype_ast(AST,1,DetypedAST,_NodeAmount).
81
82 detype_ast(AST,DetypedAST) :-
83 detype_ast(AST,1,DetypedAST,_NodeAmount).
84 % remove index of sequence elements
85 detype_ast((_,Node),C,DetypedAST,NC) :-
86 detype_ast(Node,C,DetypedAST,NC).
87 % ProB-Values
88 detype_ast(int(Value),C,integer(C,Value),C).
89 detype_ast(string(Value),C,string(C,Value),C).
90 detype_ast(Bool,C,DetypedBool,C) :-
91 ( Bool = pred_true ->
92 DetypedBool = boolean_true(C)
93 ; Bool = pred_false ->
94 DetypedBool = boolean_false(C)).
95 % ProB-AST-Nodes
96 detype_ast(b(integer(Value),_,_),C,integer(C,Value),C).
97 detype_ast(b(string(Value),_,_),C,string(C,Value),C).
98 detype_ast(b(Node,_,_),C,DetypedAST,C) :-
99 Node =.. [_] ,
100 DetypedAST =.. [Node,C].
101 detype_ast(field(Name,ValueNode),C,rec_entry(C,identifier(C1,Name),DetypedValueNode),NC) :-
102 C1 is C + 1 ,
103 C2 is C1 + 1 ,
104 detype_ast(ValueNode,C2,DetypedValueNode,NC).
105 detype_ast(b(identifier(Name),_,_),C,identifier(C,Name),C).
106 % sequence_extension or value sequence
107 detype_ast(b(Node,_,_),C,DetypedAST,NC) :-
108 Node =.. [NodeType,Arg] ,
109 avl_to_list_set(Arg,NArg) ,
110 (NodeType = sequence_extension ; (NodeType = value , NArg = [(_,_)|_])) ,
111 C1 is C + 1 ,
112 detype_set(NArg,C1,DetypedArg,NC) ,
113 % use 'sequence_extension' instead of 'value' for detyped ASTs
114 DetypedAST =.. [sequence_extension,C,DetypedArg].
115 % set_extension or value set
116 detype_ast(b(Node,_,_),C,DetypedAST,NC) :-
117 Node =.. [NodeType,Arg] ,
118 (NodeType = set_extension ; NodeType = value) ,
119 avl_to_list_set(Arg,NArg) ,
120 C1 is C + 1 ,
121 detype_set(NArg,C1,DetypedArg,NC) ,
122 % use 'set_extension' instead of 'value' for detyped ASTs
123 DetypedAST =.. [set_extension,C,DetypedArg].
124 detype_ast(b(rec(FieldList),_,_),C,rec(C,DetypedFieldList),NC) :-
125 C1 is C + 1 ,
126 detype_set(FieldList,C1,DetypedFieldList,NC).
127 % quantifier
128 detype_ast(b(exists(IDList,Predicate),_,_),C,exists(C,DetypedIDList,DetypedPredicate),NC) :-
129 C1 is C + 1 ,
130 detype_set(IDList,C1,DetypedIDList,TempC) ,
131 C2 is TempC + 1 ,
132 detype_ast(Predicate,C2,DetypedPredicate,NC).
133 detype_ast(b(forall(IDList,LHS,RHS),_,_),C,forall(C,DetypedIDList,implication(ImpC,DetypedLHS,DetypedRHS)),NC) :-
134 C1 is C + 1 ,
135 detype_set(IDList,C1,DetypedIDList,TempC) ,
136 ImpC is TempC + 1 ,
137 C2 is ImpC + 1 ,
138 detype_ast(LHS,C2,DetypedLHS,TempC2) ,
139 C3 is TempC2 + 1 ,
140 detype_ast(RHS,C3,DetypedRHS,NC).
141 % one argument nodes
142 detype_ast(b(Node,_,_),C,DetypedAST,NC) :-
143 Node =.. [NodeType,Arg] ,
144 C1 is C + 1 ,
145 detype_ast(Arg,C1,DetypedArg,NC) ,
146 DetypedAST =.. [NodeType,C,DetypedArg].
147 % two argument nodes
148 detype_ast(b(Node,_,_),C,DetypedAST,NC) :-
149 Node =.. [NodeType,Arg1,Arg2] ,
150 C1 is C + 1 ,
151 detype_ast(Arg1,C1,DetypedArg1,TempC) ,
152 C2 is TempC + 1 ,
153 detype_ast(Arg2,C2,DetypedArg2,NC) ,
154 DetypedAST =.. [NodeType,C,DetypedArg1,DetypedArg2].
155
156 % detype a set of ast or value nodes
157 detype_set([],C,[],NC) :-
158 NC is C - 1.
159 detype_set([Node|R],C,[NewNode|NewR],NC) :-
160 detype_ast(Node,C,NewNode,TempC) ,
161 C1 is TempC + 1 ,
162 detype_set(R,C1,NewR,NC).
163
164 % convert avl set to list set, otherwise just return the list set
165 avl_to_list_set(avl_set(AVL),Set) :-
166 avl_to_list(AVL,TempSet) ,
167 findall(Elm,member(Elm-_,TempSet),Set).
168 avl_to_list_set(Set,Set).
169
170 % get inner type and a list of the surrounding terms of an ast type
171 % for input like set(set(integer([]))) inner_type/3 will return
172 % [] and [set,set,integer] in its second and third argument
173 inner_type(Type,Inner,[H|Outter]) :-
174 Type =.. [H,Temp] , ! ,
175 inner_type(Temp,Inner,Outter).
176 inner_type(Inner,Inner,[]).
177
178 % surround type with terms from a list
179 surround_type(Inner,[],Inner).
180 surround_type(Inner,[Outter],New) :-
181 New =.. [Outter,Inner].
182 surround_type(Inner,[Outter|T],New) :-
183 surround_type(Inner,T,Temp) ,
184 New =.. [Outter,Temp].
185 surround_type(Inner,_,Inner).
186
187 get_type_from_value(field(_,Value),Type) :-
188 get_type_from_value(Value,Type).
189 get_type_from_value(int(_),integer).
190 get_type_from_value(string(_),string).
191 get_type_from_value(Bool,boolean) :-
192 Bool = pred_true ; Bool = pred_false.
193 get_type_from_value(Seq,seq(Type)) :-
194 is_list(Seq) , Seq = [Value|_] ,
195 Value = (_,_) ,
196 get_type_from_value(Value,Type).
197 get_type_from_value(Set,set(Type)) :-
198 is_list(Set) , Set = [Value|_] ,
199 get_type_from_value(Value,Type).
200 get_type_from_value(rec(FieldList),record(Type)) :-
201 FieldList = [Value|_] ,
202 get_type_from_value(Value,Type).
203
204 value_to_ast(int(Value),b(integer(Value),integer,[])).
205 value_to_ast(string(Value),b(string(Value),string,[])).
206 value_to_ast(pred_true,b(boolean_true,boolean,[])).
207 value_to_ast(pred_false,b(boolean_false,boolean,[])).
208 value_to_ast(Seq,b(value(Seq),seq(Type),[])) :-
209 is_list(Seq) , Seq = [Value|_] ,
210 Value = (_,_) ,
211 get_type_from_value(Value,Type).
212 value_to_ast(Set,b(value(Set),set(Type),[])) :-
213 is_list(Set) , Set = [Value|_] ,
214 get_type_from_value(Value,Type).
215 value_to_ast(Record,b(Record,record(FieldTypes),[])) :-
216 Record = rec(FieldList) ,
217 findall(field(Name,Type),(member(field(Name,Value),FieldList) ,
218 get_type_from_value(Value,Type)),FieldTypes).
219
220 % add solutions given as a list of bindings to an ast (smt-solver)
221 add_solution_to_ast(AST,Bindings,NewAST) :-
222 add_solution_to_ast(AST,Bindings,empty_ast,NewAST).
223
224 add_solution_to_ast(AST,[],Acc,NewAcc) :-
225 NewAcc = b(conjunct(AST,Acc),pred,[]).
226 add_solution_to_ast(AST,[binding(Name,Value,_RawValue)|Bindings],Acc,NewAST) :-
227 value_to_ast(Value,ASTValue) ,
228 ASTValue = b(_,Type,_) ,
229 Node = b(equal(b(identifier(Name),Type,[]),ASTValue),pred,[]) ,
230 (Acc = empty_ast ->
231 NewAcc = Node
232 ; NewAcc = b(conjunct(Acc,Node),pred,[])) ,
233 add_solution_to_ast(AST,Bindings,NewAcc,NewAST).
234
235 % check if prob ast node has "ground" value
236 % here ground means ast leave, one-element (or empty) set/seq or quantifier
237 prob_is_ground(b(Bool,pred,_),true) :-
238 Bool = truth ; Bool = falsity.
239 prob_is_ground(b(Bool,boolean,_),true) :-
240 Bool = boolean_true ; Bool = boolean_false.
241 prob_is_ground(b(identifier(_),_,_),true).
242 prob_is_ground(b(Int,integer,_),true) :-
243 Int = max_int ; Int = min_int.
244 prob_is_ground(b(integer(_),integer,_),true).
245 prob_is_ground(b(unary_minus(b(integer(_),integer,[])),integer,_),true).
246 prob_is_ground(b(string(_),string,_),true).
247 prob_is_ground(b(rec([_]),_,_),true).
248 % one value or empty sets are ground
249 prob_is_ground(b(set_extension([]),set(_),_),true).
250 prob_is_ground(b(set_extension([_]),set(_),_),true).
251 prob_is_ground(b(sequence_extension([]),seq(_),_),true).
252 prob_is_ground(b(sequence_extension([_]),seq(_),_),true).
253 % handle exists and forall as "ground" to improve shrinking
254 % by allowing to evaluate those nodes
255 prob_is_ground(b(exists(_,_),_,_),true).
256 prob_is_ground(b(forall(_,_,_),_,_),true).
257 prob_is_ground(b(value([]),_,_),true).
258 prob_is_ground(b(value([_]),_,_),true).
259 prob_is_ground(b(value(avl_set(empty)),_,_),true).
260 prob_is_ground(b(value(avl_set(node(_,_,0,empty,empty))),_,_),true).
261 % true for small interval, used in shrinking
262 prob_is_ground(b(interval(b(integer(Value1),integer,_),b(integer(Value2),integer,_)),set(integer),_),true) :-
263 C1 is Value1 + 5 ,
264 C2 is Value2 - 5 ,
265 C1 >= C2.
266 prob_is_ground(_,false).