| 1 | :- module(library_setup,[library_setup/8]). | |
| 2 | ||
| 3 | :- use_module(synthesis(synthesis_util),[get_machinevars_by_name/2]). | |
| 4 | ||
| 5 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 6 | ||
| 7 | :- use_module(library(lists),[append/2,is_list/1,remove_dups/2]). | |
| 8 | :- use_module(library(sets),[subtract/3]). | |
| 9 | :- use_module(library(random),[random_subseq/3]). | |
| 10 | :- use_module(probsrc(bsyntaxtree),[get_texpr_type/2]). | |
| 11 | ||
| 12 | :- module_info(group,synthesis). | |
| 13 | :- module_info(description,'This module defines the default library configuration and sets up the selected library from the user used for synthesis.'). | |
| 14 | ||
| 15 | library_setup(UseOperationParameters,MachineSets,ConsiderIfVarNames,NotConsiderConstants,default:LibExpansion,SynthesisType,Example,ExtendedComponents) :- | |
| 16 | count_var_types(Example,Int,Bool,(_,SetTypes),(_,SeqTypes),(Ind,IndependentTypes)) , | |
| 17 | try_minimized_types_first(LibExpansion,Int,Bool,SetTypes,SeqTypes,NewInt,NewBool,NewSetTypes,NewSeqTypes) , | |
| 18 | findall(set(IT),member(IT,IndependentTypes),IndependentSetTypes) , | |
| 19 | length(SetTypes,Set) , | |
| 20 | length(SeqTypes,Seq) , | |
| 21 | append([NewSetTypes,IndependentSetTypes],NewSetTypes2), | |
| 22 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,intOp,NewInt,[],TLib1) , | |
| 23 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,boolOp,NewBool,TLib1,TLib2) , | |
| 24 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,setOp-NewSetTypes2,Set,TLib2,TLib3) , | |
| 25 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,seqOp-NewSeqTypes,Seq,TLib3,TLib4) , | |
| 26 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,independent-IndependentTypes,Ind,TLib4,TOperators) , | |
| 27 | library_add_conn(SynthesisType,LibExpansion,Example,Or,And) , | |
| 28 | append([Or,And,TOperators],Operators) , | |
| 29 | library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,arithmetic,Int,[],Arithmetic) , | |
| 30 | append(Operators,Arithmetic,TempComponents) , | |
| 31 | randomize_library_configuration(TempComponents,RandomComponents) , | |
| 32 | (UseOperationParameters = yes | |
| 33 | -> add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) , | |
| 34 | append(RandomComponents,SetConstants,Components) | |
| 35 | ; RandomComponents = Components) , | |
| 36 | extend_components_to_consider_if_statements(ConsiderIfVarNames,NotConsiderConstants,LibExpansion,Components,ExtendedComponents). | |
| 37 | ||
| 38 | library_setup(UseOperationParameters,MachineSets,ConsiderIfVarNames,NotConsiderConstants,UserLibrary,SynthesisType,Example,ExtendedComponents) :- | |
| 39 | UserLibrary \= default:_ , | |
| 40 | setup_user_library(UserLibrary,NotConsiderConstants,SynthesisType,Example,TempComponents) , | |
| 41 | (UseOperationParameters == yes | |
| 42 | -> add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) , | |
| 43 | append(TempComponents,SetConstants,Components) | |
| 44 | ; TempComponents = Components) , | |
| 45 | extend_components_to_consider_if_statements(ConsiderIfVarNames,NotConsiderConstants,SynthesisType,Components,ExtendedComponents). | |
| 46 | ||
| 47 | % Try to use the sub libraries for each type only once at first. | |
| 48 | try_minimized_types_first(LibExpansion,Int,Bool,SetTypes,SeqTypes,NewInt,NewBool,NewSetTypes,NewSeqTypes) :- | |
| 49 | LibExpansion mod 2 =\= 0 , ! , % odd lib expansion | |
| 50 | try_minimized_types_first_aux(Int,NewInt) , | |
| 51 | try_minimized_types_first_aux(Bool,NewBool) , | |
| 52 | try_minimized_types_first_aux(SetTypes,NewSetTypes) , | |
| 53 | try_minimized_types_first_aux(SeqTypes,NewSeqTypes). | |
| 54 | % Otherwise, use the full library. | |
| 55 | try_minimized_types_first(_,Int,Bool,SetTypes,SeqTypes,Int,Bool,SetTypes,SeqTypes). | |
| 56 | ||
| 57 | try_minimized_types_first_aux(IntOrBoolTypes,1) :- | |
| 58 | integer(IntOrBoolTypes) , | |
| 59 | IntOrBoolTypes > 0. | |
| 60 | try_minimized_types_first_aux(0,0). | |
| 61 | try_minimized_types_first_aux(SetOrSeqTypes,NewTypes) :- | |
| 62 | is_list(SetOrSeqTypes) , | |
| 63 | remove_dups(SetOrSeqTypes,NewTypes). | |
| 64 | ||
| 65 | % TODO: we may need more than one operation parameter for a enumerated/deferred set | |
| 66 | add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) :- | |
| 67 | add_set_constants_as_op_params_for_independent_types(MachineSets,[],SetConstants). | |
| 68 | ||
| 69 | add_set_constants_as_op_params_for_independent_types([],Acc,Acc). | |
| 70 | add_set_constants_as_op_params_for_independent_types([MachineSet|T],Acc,SetConstants) :- | |
| 71 | MachineSet = b(_,set(global(IndependentType)),_) , | |
| 72 | add_set_constants_as_op_params_for_independent_types(T,[param_constant-set(global(IndependentType)),param_constant-global(IndependentType)|Acc],SetConstants). | |
| 73 | ||
| 74 | % Given a list of machine variable names that we want to consider if-statements for. | |
| 75 | extend_components_to_consider_if_statements([],_,_,Components,Components). | |
| 76 | extend_components_to_consider_if_statements([ConsiderIfVarName|T],NotConsiderConstants,LibExpansion,Components,ExtendedComponents) :- | |
| 77 | get_machinevars_by_name([ConsiderIfVarName],[MachineVar]) , | |
| 78 | get_texpr_type(MachineVar,MachineVarType) , | |
| 79 | encode_component_type(MachineVarType,ComponentType) , | |
| 80 | % besides adding the if_then_else component itself we need to consider appropriate operators for the condition | |
| 81 | % TODO: assume that initially all if-statements have the same condition to reduce the overhead of considering too much preciates in addition to expressions needed for synthesizing the substitution | |
| 82 | % therefore, implement an own library expansion for the condition of if-statements relaxing this assumption successively | |
| 83 | library_add_component_aux(guard,NotConsiderConstants,LibExpansion,ComponentType,[],ConditionComponents) , | |
| 84 | append(Components,[if_then_else-MachineVarType|ConditionComponents],NewComponents) , | |
| 85 | extend_components_to_consider_if_statements(T,NotConsiderConstants,LibExpansion,NewComponents,ExtendedComponents). | |
| 86 | ||
| 87 | encode_component_type(integer,intOp). | |
| 88 | encode_component_type(bool,boolOp). | |
| 89 | encode_component_type(set(Type),setOp-set(Type)). | |
| 90 | encode_component_type(seq(Type),seqOp-seq(Type)). | |
| 91 | ||
| 92 | % If the library consists of more than 20 components choose a random subset. | |
| 93 | randomize_library_configuration(Components,Components) :- | |
| 94 | length(Components,L) , | |
| 95 | L =< 20. | |
| 96 | randomize_library_configuration(Components,RandomComponents) :- | |
| 97 | random_subseq(Components,Sub1,Sub2) , | |
| 98 | get_larger_sublist(Sub1,Sub2,RandomComponents). | |
| 99 | ||
| 100 | get_larger_sublist(Sub1,Sub2,Sub1) :- | |
| 101 | length(Sub1,L1) , length(Sub2,L2) , | |
| 102 | L1 > L2. | |
| 103 | get_larger_sublist(_,Sub2,Sub2). | |
| 104 | ||
| 105 | setup_user_library(UserLibrary,NotConsiderConstants,SynthesisType,Example,Components) :- | |
| 106 | % TODO: consider independent types | |
| 107 | count_var_types(Example,Int,Bool,(Set,SetTypes),(Seq,SeqTypes),(IndT,IndependentTypes)) , | |
| 108 | setup_user_library_aux(UserLibrary,Int,Bool,(Set,SetTypes),(Seq,SeqTypes),(IndT,IndependentTypes),SelectedComponents) , | |
| 109 | (NotConsiderConstants == no | |
| 110 | -> add_constants(UserLibrary,Int,Bool,SetTypes,SeqTypes,IndependentTypes,ConstantComponents) | |
| 111 | ; ConstantComponents = []) , | |
| 112 | append(SelectedComponents,ConstantComponents,TComponents) , | |
| 113 | add_skip_components(SynthesisType,TComponents,Int,Bool,SetTypes,SeqTypes,IndependentTypes,Components). | |
| 114 | ||
| 115 | setup_user_library_aux(UserLibrary,Int,Bool,(SetAmount,SetTypes),(SeqAmount,SeqTypes),(IndT,IndependentTypes),Components) :- | |
| 116 | member(predicates(Predicates),UserLibrary) , | |
| 117 | split_typed_and_untyped_predicates(Predicates,PredicatesToBeTyped,UntypedPredicates) , | |
| 118 | setup_typed_predicates(PredicatesToBeTyped,Int,Bool,(SetAmount,SetTypes),(SeqAmount,SeqTypes),(IndT,IndependentTypes),TypedPredicates) , | |
| 119 | member(numbers(Numbers),UserLibrary) , | |
| 120 | member(relations(Relations),UserLibrary) , | |
| 121 | member(sequences(Sequences),UserLibrary) , | |
| 122 | append(Sequences,Relations,SequencesAndRelations) , % components in Relations refer to sequences | |
| 123 | setup_typed_expressions(SequencesAndRelations,SeqTypes,[],TypedSequences) , | |
| 124 | member(sets(Sets),UserLibrary) , | |
| 125 | findall(set(IT),member(IT,IndependentTypes),IndependentTypes2) , | |
| 126 | append([SetTypes,IndependentTypes2],SetTypes2) , | |
| 127 | setup_typed_expressions(Sets,SetTypes2,[],TypedSets) , | |
| 128 | member(substitutions(Substitutions),UserLibrary) , | |
| 129 | append([UntypedPredicates,TypedPredicates,Numbers,TypedSequences,TypedSets,Substitutions],Components). | |
| 130 | ||
| 131 | % By now 'equal'/'not_equal' are the only predicates that can use different (top-level) types since we need to consider e.g. equality of booleans, integers, sets etc. | |
| 132 | split_typed_and_untyped_predicates(Predicates,TypedPredicates,UntypedPredicates) :- | |
| 133 | findall(UntypedPredicate,(member(UntypedPredicate,Predicates) , UntypedPredicate \= equal , UntypedPredicate \= not_equal),UntypedPredicates) , | |
| 134 | subtract(Predicates,UntypedPredicates,TypedPredicates). | |
| 135 | ||
| 136 | add_skip_components(action,TComponents,Int,Bool,SetTypes,SeqTypes,IndependentTypes,Components) :- | |
| 137 | length(IntDummies,Int) , | |
| 138 | findall(Skip,(member(Skip,IntDummies) , Skip = skip-integer),SkipInts) , | |
| 139 | length(BoolDummies,Bool) , | |
| 140 | findall(Skip,(member(Skip,BoolDummies) , Skip = skip-boolean),SkipBools) , | |
| 141 | findall(Skip,(member(SetType,SetTypes) , Skip = skip-SetType),SkipSets) , | |
| 142 | findall(Skip,(member(SeqType,SeqTypes) , Skip = skip-SeqType),SkipSeqs) , | |
| 143 | findall(Skip,(member(IndependentType,IndependentTypes) , Skip = skip-IndependentType),SkipInd) , | |
| 144 | append([TComponents,SkipInts,SkipBools,SkipSets,SkipSeqs,SkipInd],Components). | |
| 145 | add_skip_components(SynthesisType,Components,_,_,_,_,_,Components) :- | |
| 146 | SynthesisType \= action. | |
| 147 | ||
| 148 | % Create typed equal components like 'equal-integer' for each used type with duplicates. | |
| 149 | % For instance, the user chooses to use two equality components. Then, we provide two equality components for each | |
| 150 | % considered type from the current examples. | |
| 151 | setup_typed_predicates([],_,_,_,_,_,[]). | |
| 152 | setup_typed_predicates(Predicates,Int,Bool,(Sets,SetTypes),(Seqs,SeqTypes),(IndT,IndependentTypes),TypedPredicates) :- | |
| 153 | setup_typed_predicates_aux(Predicates,Int,integer,IntPredicates) , | |
| 154 | setup_typed_predicates_aux(Predicates,Bool,boolean,BoolPredicates) , | |
| 155 | setup_typed_predicates_aux(Predicates,Sets,SetTypes,SetPredicates) , | |
| 156 | setup_typed_predicates_aux(Predicates,Seqs,SeqTypes,SeqPredicates) , | |
| 157 | setup_typed_predicates_aux(Predicates,IndT,IndependentTypes,IndPredicates) , | |
| 158 | append([IntPredicates,BoolPredicates,SetPredicates,SeqPredicates,IndPredicates],TypedPredicates). | |
| 159 | ||
| 160 | setup_typed_predicates_aux(_,0,_,[]). | |
| 161 | setup_typed_predicates_aux(Predicates,Amount,Type,TypedPredicates) :- | |
| 162 | % single type | |
| 163 | Amount \= 0 , \+ is_list(Type) , | |
| 164 | findall(Equal,(member(Op,[equal,not_equal]) , member(Op,Predicates) , Equal = Op-Type),TypedPredicates). | |
| 165 | setup_typed_predicates_aux(_,_,[],[]). | |
| 166 | setup_typed_predicates_aux(Predicates,Amount,Types,TypedPredicates) :- | |
| 167 | % list of types, e.g., different types of sets | |
| 168 | Amount \= 0 , is_list(Types) , Types \= [] , | |
| 169 | findall(Equal,(member(Op,[equal,not_equal]) , member(Op,Predicates) , member(Type,Types) , Equal = Op-Type),TypedPredicates). | |
| 170 | ||
| 171 | add_constants(UserLibrary,Int,Bool,SetTypes,SeqTypes,IndependentTypes,ConstantComponents) :- | |
| 172 | length(IntConstants,Int) , | |
| 173 | findall(IntConstant,(member(IntConstant,IntConstants) , IntConstant = constant-integer),IntConstants) , | |
| 174 | length(BoolConstants,Bool) , | |
| 175 | findall(BoolConstant = constant-boolean,(member(BoolConstant,BoolConstants)),BoolConstants) , | |
| 176 | findall(constant-SetType,member(SetType,SetTypes),SetConstants) , | |
| 177 | findall(constant-SeqType,member(SeqType,SeqTypes),SeqConstants) , | |
| 178 | findall(constant-IndependentType,member(IndependentType,IndependentTypes),IndConstants) , | |
| 179 | findall(constant-set(IndependentType),member(IndependentType,IndependentTypes),SetIndConstants) , | |
| 180 | append([IntConstants,BoolConstants,SetConstants,SeqConstants,IndConstants,SetIndConstants],TempConstantComponents) , | |
| 181 | add_set_constants_for_seq_relations(UserLibrary,SeqTypes,TempConstantComponents,ConstantComponents). | |
| 182 | ||
| 183 | add_set_constants_for_seq_relations(UserLibrary,SeqTypes,TempConstantComponents,ConstantComponents) :- | |
| 184 | member(relations(Relations),UserLibrary) , | |
| 185 | length(Relations,RelationAmount) , | |
| 186 | add_set_constants_for_seq_relations_aux(RelationAmount,SeqTypes,[],SetConstants) , | |
| 187 | append(TempConstantComponents,SetConstants,ConstantComponents). | |
| 188 | add_set_constants_for_seq_relations(_,_,ConstantComponents,ConstantComponents). | |
| 189 | ||
| 190 | add_set_constants_for_seq_relations_aux(_,[],Acc,Acc). | |
| 191 | add_set_constants_for_seq_relations_aux(RelationAmount,[SeqType|T],Acc,SetConstants) :- | |
| 192 | length(Constants,RelationAmount) , | |
| 193 | SeqType = seq(InnerType) , | |
| 194 | findall(Constant,(member(Constant,Constants) , Constant = constant-set(InnerType)),Constants) , | |
| 195 | append(Constants,Acc,NewAcc) , | |
| 196 | add_set_constants_for_seq_relations_aux(RelationAmount,T,NewAcc,SetConstants). | |
| 197 | ||
| 198 | % Set and Sequence expressions are type like 'union-set(integer)'. | |
| 199 | % Therefore, we add the selected set or sequence components from the user for each set or sequence type | |
| 200 | % that is considered in the current examples. | |
| 201 | setup_typed_expressions(Components,Types,Acc,FinalComponents) :- | |
| 202 | remove_dups(Types,NTypes) , | |
| 203 | setup_typed_expressions_aux(Components,NTypes,Acc,FinalComponents). | |
| 204 | setup_typed_expressions_aux([],_,Acc,Acc). | |
| 205 | setup_typed_expressions_aux([Component|T],Types,Acc,FinalComponents) :- | |
| 206 | findall(TypedComponent,(member(Type,Types) , TypedComponent = Component-Type),TypedComponents) , | |
| 207 | append(TypedComponents,Acc,NAcc) , | |
| 208 | setup_typed_expressions_aux(T,Types,NAcc,FinalComponents). | |
| 209 | ||
| 210 | % Determine the variable types to provide an appropriate library configuration. | |
| 211 | count_var_types(Example,LInt,LBool,(LSet,SetTypes),(LSeq,SeqTypes),(LIndependent,IndependentTypes)) :- | |
| 212 | findall(Val,member(b(Val,integer,_),Example),Int) , | |
| 213 | findall(Val,member(b(Val,boolean,_),Example),Bool) , | |
| 214 | findall(Type,(member(b(Node,Type,_),Example) , Type = seq(_)),SeqTypes) , | |
| 215 | findall(Type,(member(b(Node,Type,_),Example) , Type = set(_)),SetTypes) , | |
| 216 | findall(Type,(member(b(Node,Type,_),Example) , Type = global(_)),IndependentTypes) , | |
| 217 | length(Int,LInt) , length(Bool,LBool) , length(SetTypes,LSet) , length(SeqTypes,LSeq) , length(IndependentTypes,LIndependent). | |
| 218 | ||
| 219 | % Add conjunct/disjunct to the library. | |
| 220 | library_add_conn(action,_,_,[],[]). | |
| 221 | library_add_conn(_,LibExpansion,Example,Or,And) :- | |
| 222 | length(Example,VarAmount) , | |
| 223 | (LibExpansion mod 2 =\= 0 , VarAmount > 2 -> Div = 3 ; Div = 2) , | |
| 224 | %C is round(VarAmount/2) , | |
| 225 | TempC is VarAmount / Div , | |
| 226 | (TempC = 0.5 -> C = 0 ; C is floor(TempC)) , | |
| 227 | library_add_conn_aux(C,Or,And). | |
| 228 | library_add_conn_aux(C,Or,And) :- | |
| 229 | length(And,C) , length(Or,C) , | |
| 230 | findall(A,(member(A,And), A = conjunct),And) , | |
| 231 | findall(O,(member(O,Or), O = disjunct),Or). | |
| 232 | ||
| 233 | % Limited arithmetic library for guards and invariants: no arithmetic in the first expansion step. | |
| 234 | library_add_components(Type,_,0,arithmetic,_,Acc,Acc) :- | |
| 235 | (Type = guard ; Type = invariant) , !. | |
| 236 | %library_add_components(Type,_,arithmetic,0,Acc,Acc) :- | |
| 237 | % (Type = guard ; Type = invariant) , !. | |
| 238 | %library_add_components(action,1,arithmetic,1,Acc,Acc). | |
| 239 | library_add_components(_,_,_,_,0,Acc,Acc). | |
| 240 | library_add_components(Type,NotConsiderConstants,LibExpansion,OpType,VarAmount,Acc,Library) :- | |
| 241 | NVarAmount is VarAmount - 1 , | |
| 242 | (OpType = TOp-[ExactType|RTypes] | |
| 243 | % get the type from the list of set/seq/independent types | |
| 244 | -> Op = TOp-ExactType , | |
| 245 | NOpType = TOp-RTypes | |
| 246 | ; Op = OpType , | |
| 247 | NOpType = OpType) , | |
| 248 | library_add_component_aux(Type,NotConsiderConstants,LibExpansion,Op,Acc,Operators) , | |
| 249 | library_add_components(Type,NotConsiderConstants,LibExpansion,NOpType,NVarAmount,Operators,Library). | |
| 250 | ||
| 251 | % We define several library steps for each synthesis type to improve the performance. | |
| 252 | % Start with a small library and expand successively. | |
| 253 | ||
| 254 | library_add_component_aux(_,_,_,_-[],Acc,Acc). | |
| 255 | % independent types | |
| 256 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,independent-Type,Acc,NewAcc) :- | |
| 257 | library_add_indepentend_type_components(SynthesisType,LibExpansion,Type,Acc,TempAcc) , | |
| 258 | (NotConsiderConstants = no -> NewAcc = [constant-Type|TempAcc] ; NewAcc = TempAcc). | |
| 259 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,intOp,Acc,NewAcc) :- | |
| 260 | library_add_integer_components(SynthesisType,LibExpansion,Acc,TempAcc), | |
| 261 | (NotConsiderConstants = no -> NewAcc = [constant-integer|TempAcc] ; NewAcc = TempAcc). | |
| 262 | % integer, arithmetic components are added separately | |
| 263 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,boolOp,Acc,NewAcc) :- | |
| 264 | library_add_boolean_components(SynthesisType,LibExpansion,Acc,TempAcc) , | |
| 265 | ((NotConsiderConstants = no) , (SynthesisType \= action) -> NewAcc = [constant-boolean|TempAcc] ; NewAcc = TempAcc). | |
| 266 | % arithmetic | |
| 267 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,arithmetic,Acc,NewAcc) :- | |
| 268 | library_add_arithmetic_components(SynthesisType,LibExpansion,Acc,TempAcc) , | |
| 269 | (NotConsiderConstants = no -> NewAcc = [constant-integer|TempAcc] ; NewAcc = TempAcc). | |
| 270 | % set | |
| 271 | % use min/max only if we have set(integer), general_union/intersection only if we have set(set(_)) | |
| 272 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,setOp-SetType,Acc,NewAcc) :- | |
| 273 | library_add_set_components(SynthesisType,LibExpansion,SetType,Acc,TempAcc) , | |
| 274 | (NotConsiderConstants = no | |
| 275 | -> (SynthesisType = action -> NewAcc = [constant-SetType|TempAcc] ; NewAcc = [constant-SetType,constant-integer|TempAcc]) % integer constant for card(_) > _ | |
| 276 | ; NewAcc = TempAcc). | |
| 277 | % sequence | |
| 278 | library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,seqOp-SeqType,Acc,NewAcc) :- | |
| 279 | (SeqType = seq(_) ; SeqType = set(couple(integer,_))) , | |
| 280 | library_add_seq_components(SynthesisType,LibExpansion,SeqType,TLibrary) , | |
| 281 | % use constant of type seq(_) | |
| 282 | append([TLibrary,Acc],TempAcc) , | |
| 283 | SeqType = seq(InnerType) , % add set constant for components like domain_restriction | |
| 284 | (NotConsiderConstants = no | |
| 285 | -> (SynthesisType = action -> NewAcc = [constant-SeqType,constant-set(InnerType)|TempAcc] ; NewAcc = [constant-SeqType,constant-integer|TempAcc]) | |
| 286 | ; NewAcc = TempAcc). | |
| 287 | ||
| 288 | % boolean | |
| 289 | library_add_boolean_components(action,1,Acc,[convert_bool,subset-set(integer),skip-boolean|Acc]). | |
| 290 | library_add_boolean_components(_,1,Acc,[equal-boolean|Acc]). | |
| 291 | % TODO: use member, subset, etc. to be used within convert_bool but consider the current machine variables | |
| 292 | library_add_boolean_components(_,_,Acc,[equal-boolean,convert_bool,subset-set(integer)|Acc]). | |
| 293 | ||
| 294 | library_add_indepentend_type_components(action,_,Type,Acc,[skip-Type|Acc]). | |
| 295 | library_add_indepentend_type_components(SynthesisType,_,Type,Acc,[equal-Type,not_equal-Type|Acc]) :- | |
| 296 | SynthesisType \= action. | |
| 297 | ||
| 298 | library_add_integer_components(action,_,Acc,[skip-integer|Acc]). | |
| 299 | library_add_integer_components(_,C,Acc,[greater|Acc]) :- C = 1 ; C = 2. | |
| 300 | library_add_integer_components(_,_,Acc,[greater,equal-integer|Acc]). | |
| 301 | % member,integer_set-natural,integer_set-natural1,integer_set | |
| 302 | ||
| 303 | library_add_arithmetic_components(action,C,Acc,[add,minus|Acc]) :- C = 1 ; C = 2. | |
| 304 | library_add_arithmetic_components(action,C,Acc,[multiplication,power_of|Acc]) :- C = 3 ; C = 4. | |
| 305 | library_add_arithmetic_components(action,C,Acc,[multiplication,div|Acc]) :- C = 5 ; C = 6. | |
| 306 | library_add_arithmetic_components(action,C,Acc,[multiplication,div,add|Acc]) :- C = 7 ; C = 8. | |
| 307 | library_add_arithmetic_components(action,C,Acc,[div,modulo|Acc]) :- C = 9 ; C = 10. | |
| 308 | library_add_arithmetic_components(action,C,Acc,[multiplication,div,modulo|Acc]) :- C = 11 ; C = 12. | |
| 309 | library_add_arithmetic_components(action,C,Acc,[multiplication,div|Acc]) :- C = 13 ; C = 14. | |
| 310 | library_add_arithmetic_components(action,_,Acc,[add,minus,multiplication,div,modulo,power_of|Acc]). | |
| 311 | library_add_arithmetic_components(_,C,Acc,Acc) :- C = 1 ; C = 2. | |
| 312 | library_add_arithmetic_components(_,C,Acc,[add,minus|Acc]) :- C = 3 ; C = 4. | |
| 313 | library_add_arithmetic_components(_,C,Acc,[multiplication,power_of|Acc]) :- C = 5 ; C = 6. | |
| 314 | library_add_arithmetic_components(_,C,Acc,[multiplication,div|Acc]) :- C = 7 ; C = 8. | |
| 315 | library_add_arithmetic_components(_,C,Acc,[multiplication,div,add|Acc]) :- C = 9 ; C = 10. | |
| 316 | library_add_arithmetic_components(_,C,Acc,[div,modulo|Acc]) :- C = 11 ; C = 12. | |
| 317 | library_add_arithmetic_components(_,C,Acc,[multiplication,div,modulo|Acc]) :- C = 13 ; C = 14. | |
| 318 | library_add_arithmetic_components(_,C,Acc,[multiplication,div|Acc]) :- C = 15 ; C = 16. | |
| 319 | library_add_arithmetic_components(_,_,Acc,[add,minus,multiplication,div,modulo,power_of|Acc]). | |
| 320 | ||
| 321 | %% nested sets | |
| 322 | library_add_set_components(action,C,SetType,Acc,[union-SetType,skip-SetType|Acc]) :- | |
| 323 | SetType = set(set(_)) , C = 1 ; C = 2. | |
| 324 | library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,skip-SetType|Acc]) :- | |
| 325 | SetType = set(set(_)) , C = 3 ; C = 4. | |
| 326 | library_add_set_components(action,C,SetType,Acc,[intersection-SetType,skip-SetType|Acc]) :- | |
| 327 | SetType = set(set(_)) , C = 5 ; C = 6. | |
| 328 | library_add_set_components(action,C,SetType,Acc,[general_union-SetType,skip-SetType|Acc]) :- | |
| 329 | SetType = set(set(_)) , C = 7 ; C = 8. | |
| 330 | library_add_set_components(action,C,SetType,Acc,[general_intersection-SetType,skip-SetType|Acc]) :- | |
| 331 | SetType = set(set(_)) , C = 9 ; C = 10. | |
| 332 | library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,general_union-SetType,general_intersection-SetType,skip-SetType|Acc]) :- | |
| 333 | SetType = set(set(_)) , C = 11 ; C = 12. | |
| 334 | library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,set_subtraction-SetType,skip-SetType|Acc]) :- | |
| 335 | SetType = set(set(_)) , C = 13 ; C = 14. | |
| 336 | library_add_set_components(action,_,SetType,Acc,[cartesian_product-SetType,union-SetType,set_subtraction-SetType,intersection-SetType,general_union-SetType,general_intersection-SetType,skip-SetType|Acc]) :- | |
| 337 | SetType = set(set(_)). | |
| 338 | % flat sets | |
| 339 | library_add_set_components(action,C,SetType,Acc,[union-SetType,skip-SetType|Acc]) :- | |
| 340 | SetType \= set(set(_)) , C = 1 ; C = 2. | |
| 341 | library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,skip-SetType|Acc]) :- | |
| 342 | SetType \= set(set(_)) , C = 3 ; C = 4. | |
| 343 | library_add_set_components(action,C,SetType,Acc,[intersection-SetType,skip-SetType|Acc]) :- | |
| 344 | SetType \= set(set(_)) , C = 5 ; C = 6. | |
| 345 | library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,skip-SetType|Acc]) :- | |
| 346 | SetType \= set(set(_)) , C = 7 ; C = 8. | |
| 347 | library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,skip-SetType|Acc]) :- | |
| 348 | SetType \= set(set(_)) , C = 9 ; C = 10. | |
| 349 | library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,intersection-SetType,skip-SetType|Acc]) :- | |
| 350 | SetType \= set(set(_)) , C = 11 ; C = 12. | |
| 351 | library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,skip-SetType,max,min|Acc]) :- | |
| 352 | SetType = set(integer) , C = 13 ; C = 14. | |
| 353 | library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,skip-SetType|Acc]) :- | |
| 354 | SetType \= set(set(_)) , C = 13 ; C = 14. | |
| 355 | library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,cartesian_product-SetType,skip-SetType|Acc]) :- | |
| 356 | SetType \= set(set(_)) , C = 15 ; C = 16. | |
| 357 | library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,cartesian_product-SetType,skip-SetType|Acc]) :- | |
| 358 | SetType \= set(set(_)) , C = 17 ; C = 18. | |
| 359 | library_add_set_components(action,_,SetType,Acc,[union-SetType,set_subtraction-SetType,cartesian_product-SetType,intersection-SetType,skip-SetType,max,min|Acc]) :- | |
| 360 | SetType = set(integer). | |
| 361 | % guard or invariant for sets | |
| 362 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType|Acc]) :- C = 1 ; C = 2. | |
| 363 | library_add_set_components(_,C,SetType,Acc,[not_equal-SetType,equal-SetType|Acc]) :- C = 3 ; C = 4. | |
| 364 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_equal-SetType|Acc]) :- C = 5 ; C = 6. | |
| 365 | library_add_set_components(_,C,SetType,Acc,[member-SetType,equal-SetType|Acc]) :- C = 7 ; C = 8. | |
| 366 | library_add_set_components(_,C,SetType,Acc,[not_member-SetType,not_equal-SetType|Acc]) :- C = 9 ; C = 10. | |
| 367 | library_add_set_components(_,C,SetType,Acc,[not_member-SetType,equal-SetType|Acc]) :- C = 11 ; C = 12. | |
| 368 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 13 ; C = 14. | |
| 369 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,equal-SetType,not_equal-SetType,union-SetType,intersection-SetType,set_subtraction-SetType|Acc]) :- C = 15 ; C = 16. | |
| 370 | library_add_set_components(_,C,SetType,Acc,[card-SetType,greater,equal-integer|Acc]) :- C = 17 ; C = 18. | |
| 371 | library_add_set_components(_,C,SetType,Acc,[union-SetType,intersection-SetType,equal-SetType|Acc]) :- C = 19 ; C = 20. | |
| 372 | library_add_set_components(_,C,SetType,Acc,[union-SetType,intersection-SetType,not_equal-SetType|Acc]) :- C = 21 ; C = 22. | |
| 373 | library_add_set_components(_,C,SetType,Acc,[intersection-SetType,union-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 23 ; C = 24. | |
| 374 | library_add_set_components(_,C,SetType,Acc,[intersection-SetType,union-SetType,set_subtraction-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 25 ; C = 26. | |
| 375 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,card-SetType,greater,equal-integer,union-SetType|Acc]) :- C = 27 ; C = 28. | |
| 376 | library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,card-SetType,greater,equal-integer,union-SetType,intersection-SetType,set_subtraction-SetType|Acc]) :- C = 29 ; C = 30. | |
| 377 | library_add_set_components(_,C,SetType,Acc,[equal-SetType,member-SetType,subset-SetType,subset_strict-SetType,negation|Acc]) :- C = 31 ; C = 32. | |
| 378 | library_add_set_components(_,C,SetType,Acc,[card-SetType,greater,equal-integer,member-SetType,subset_strict-SetType,subset-SetType,negation|Acc]) :- | |
| 379 | SetType \= set(integer) , C = 33 ; C = 34. | |
| 380 | library_add_set_components(_,C,SetType,Acc,[card-SetType,max,min,greater,equal-integer,member-SetType,subset_strict-SetType,subset-SetType,negation|Acc]) :- | |
| 381 | SetType = set(integer) , C = 33 ; C = 34. | |
| 382 | library_add_set_components(_,_,SetType,Acc,[max,min,card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,general_union-SetType,general_intersection-SetType,set_subtraction-SetType,member-SetType,negation,not_member-SetType|Acc]) :- | |
| 383 | SetType = set(integer). | |
| 384 | library_add_set_components(_,_,SetType,Acc,[card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,general_union-SetType,general_intersection-SetType,set_subtraction-SetType,member-SetType,negation,not_member-SetType|Acc]) :- | |
| 385 | SetType = set(set(_)). | |
| 386 | library_add_set_components(_,_,SetType,Acc,[card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,union-SetType,intersection-SetType,set_subtraction-SetType,member-SetType,negation|Acc]) :- | |
| 387 | SetType \= set(set(_)). | |
| 388 | ||
| 389 | library_add_seq_components(action,C,SeqType,[concat-SeqType,skip-SeqType]) :- C = 1 ; C = 2. | |
| 390 | library_add_seq_components(action,C,SeqType,[overwrite-SeqType,concat-SeqType,skip-SeqType]) :- C = 3 ; C = 4. | |
| 391 | library_add_seq_components(action,C,SeqType,[insert_tail-SeqType,domain-SeqType,domain_restriction-SeqType,skip-SeqType]) :- C = 5 ; C = 6. | |
| 392 | library_add_seq_components(action,C,SeqType,[insert_front-SeqType,insert_tail-SeqType,domain-SeqType,domain_restriction-SeqType,range_restriction-SeqType,skip-SeqType]) :- C = 7 ; C = 8. | |
| 393 | library_add_seq_components(action,C,SeqType,[concat-SeqType,first-SeqType,last-SeqType,skip-SeqType]) :- C = 9 ; C = 10. | |
| 394 | library_add_seq_components(action,C,SeqType,[concat-SeqType,domain_restriction-SeqType,range_restriction-SeqType,domain_subtraction-SeqType,domain_restriction-SeqType,skip-SeqType]) :- C = 11 ; C = 12. | |
| 395 | library_add_seq_components(action,_,SeqType,[overwrite-SeqType,concat-SeqType,insert_tail-SeqType,insert_front-SeqType,first-SeqType,last-SeqType,domain_restriction-SeqType,range_restriction-SeqType,domain_subtraction-SeqType,domain_restriction-SeqType,skip-SeqType]). | |
| 396 | ||
| 397 | library_add_seq_components(_,C,SeqType,[card-SeqType,greater,equal-integer]) :- C = 1 ; C = 2. % member-set(seq(integer)),seq-integer_set | |
| 398 | library_add_seq_components(_,C,SeqType,[card-SeqType,greater,equal-integer,range-SeqType,domain-SeqType,equal-SeqType]) :- C = 3 ; C = 4. | |
| 399 | library_add_seq_components(_,C,SeqType,[range-SeqType,domain-SeqType,image-SeqType,reverse-SeqType,equal-SeqType]) :- C = 5 ; C = 6. | |
| 400 | library_add_seq_components(_,C,SeqType,[range_restriction-SeqType,range_subtraction-SeqType,domain_restriction-SeqType,domain_subtraction-SeqType, | |
| 401 | equal-SeqType]) :- C = 7 ; C = 8. | |
| 402 | library_add_seq_components(_,_,SeqType,[restrict_front-SeqType,restrict_tail-SeqType,range_restriction-SeqType,range_subtraction-SeqType, | |
| 403 | domain_restriction-SeqType,domain_subtraction-SeqType,range-SeqType,domain-SeqType,image-SeqType,equal-SeqType, | |
| 404 | first-SeqType,last-SeqType,union-SeqType,equal-SeqType]). |