| 1 | % (c) 2017 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(constraints,[get_behavioral_constraint_from_input/6, | |
| 6 | get_behavioral_constraint/6, | |
| 7 | get_behavioral_constraint_aux/7, | |
| 8 | get_new_behavioral_constraint/5, | |
| 9 | get_prevent_component_swap_constraint/4, | |
| 10 | get_line_amount/4]). | |
| 11 | ||
| 12 | :- use_module(synthesis(synthesis_util)). | |
| 13 | :- use_module(synthesis(symmetry_reduction)). | |
| 14 | ||
| 15 | :- use_module(probsrc(bsyntaxtree)). | |
| 16 | :- use_module(probsrc(bmachine_structure),[get_section/3]). | |
| 17 | :- use_module(probsrc(tools),[flatten/2]). | |
| 18 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 19 | :- use_module(probsrc(bmachine),[full_b_machine/1, | |
| 20 | b_get_machine_constants/1, | |
| 21 | b_get_properties_from_machine/1, | |
| 22 | b_get_machine_operation/4, | |
| 23 | b_get_machine_variables/1, | |
| 24 | b_get_machine_set/1]). | |
| 25 | ||
| 26 | :- use_module(library(lists)). | |
| 27 | ||
| 28 | :- use_module(extension('plspec/plspec/plspec_core')). | |
| 29 | ||
| 30 | :- module_info(group,synthesis). | |
| 31 | :- module_info(description,'This module defines the constraint for synthesizing invariants, preconditions or complete operations using simple I/O examples.'). | |
| 32 | ||
| 33 | split_input_output_location_vars(LocationVars,LocationVarsIn,LocationVarsOut) :- | |
| 34 | split_input_output_location_vars(LocationVars,[],[],LocationVarsIn,LocationVarsOut). | |
| 35 | ||
| 36 | split_input_output_location_vars([],InAcc,OutAcc,InAcc,OutAcc). | |
| 37 | split_input_output_location_vars([LocationVar|T],InAcc,OutAcc,LocationVarsIn,LocationVarsOut) :- | |
| 38 | accumulate_location_var(LocationVar,InAcc,OutAcc,NewInAcc,NewOutAcc) , | |
| 39 | split_input_output_location_vars(T,NewInAcc,NewOutAcc,LocationVarsIn,LocationVarsOut). | |
| 40 | ||
| 41 | accumulate_location_var(b(identifier(LocationVarName),integer,Info),InAcc,OutAcc,[b(identifier(LocationVarName),integer,Info)|InAcc],OutAcc) :- | |
| 42 | atom_concat(li,_,LocationVarName). | |
| 43 | accumulate_location_var(b(identifier(LocationVarName),integer,Info),InAcc,OutAcc,InAcc,[b(identifier(LocationVarName),integer,Info)|OutAcc]) :- | |
| 44 | atom_concat(lo,_,LocationVarName). | |
| 45 | accumulate_location_var(_,InAcc,OutAcc,InAcc,OutAcc). | |
| 46 | ||
| 47 | % Exclude a solution and add this node to the behavioral constraint. We exclude only the solution given | |
| 48 | % by the program ast without involving generated deadcode. | |
| 49 | get_new_behavioral_constraint(ProgramAST,LocationVars,solution(SolutionBindings),BehavioralConstraint,NewBehavioralConstraint) :- | |
| 50 | % get the used operators output location variables to exclude from the further solution | |
| 51 | get_used_location_vars_and_op_names(ProgramAST,LocationVars,[],[],_,UsedOperatorNames) , | |
| 52 | exclude_solution_for_further_search(UsedOperatorNames,LocationVars,SolutionBindings,Exclusion) , | |
| 53 | split_input_output_location_vars(LocationVars,LocationVarsIn,LocationVarsOut) , | |
| 54 | used_library(Components) , | |
| 55 | %findall(Component,(member(Component,AllComponents) , Component = (_,Name) , member(Name,UsedOperatorNames)),UsedComponents) , | |
| 56 | get_post_symmetry_reduction_constraint(Components,SolutionBindings,LocationVarsIn,LocationVarsOut,SymmetryReduction) , | |
| 57 | conjunct_predicates([BehavioralConstraint,Exclusion,SymmetryReduction],NewBehavioralConstraint). | |
| 58 | ||
| 59 | get_behavioral_constraint_aux((ValidGuards,Operation),action,Library,PosInput,PosOutput,BehavioralConstraint,LocationVars) :- | |
| 60 | get_behavioral_constraint(Library,(ValidGuards,Operation),PosInput,PosOutput,BehavioralConstraint,LocationVars). | |
| 61 | get_behavioral_constraint_aux((ValidInvariantsOrGuards,Operation),_,Library,PosInput,PosOutput,BehavioralConstraint,LocationVars) :- | |
| 62 | get_behavioral_constraint_from_input(Library,(ValidInvariantsOrGuards,Operation),PosInput,PosOutput,BehavioralConstraint,LocationVars). | |
| 63 | ||
| 64 | % create outputs and get behavioral constraint | |
| 65 | get_behavioral_constraint_from_input(Library,(ValidGuards,Operation),PosInput,NegInput,BehavioralConstraint,LocationVars) :- | |
| 66 | % get output values | |
| 67 | length(PosInput,PosLength) , length(NegInput,NegLength) , | |
| 68 | % create empty lists | |
| 69 | length(TempPosOutput,PosLength) , length(TempNegOutput,NegLength) , | |
| 70 | % for our task to repair invariant violations output is either "true" or "false" (interpreted as pred_true/pred_false (synthesis(type,pred)) | |
| 71 | % but implemented as boolean_true/boolean_false, we set options each node's info representing the type which can differ from the ast node's type) | |
| 72 | findall(In,(member(In,TempPosOutput) , In = [b(boolean_true,boolean,[synthesis(type,pred)])]),PosOutput) , | |
| 73 | findall(In,(member(In,TempNegOutput) , In = [b(boolean_false,boolean,[synthesis(type,pred)])]),NegOutput) , | |
| 74 | append(PosInput,NegInput,Input) , | |
| 75 | append(PosOutput,NegOutput,Output) , | |
| 76 | get_behavioral_constraint(Library,(ValidGuards,Operation),Input,Output,BehavioralConstraint,LocationVars). | |
| 77 | ||
| 78 | :- dynamic used_library/1. | |
| 79 | :- volatile used_library/1. | |
| 80 | ||
| 81 | % Get the functional constraint for each Input-Output Example | |
| 82 | % It is sufficient to create one well-definedness constraint surrounding the behavioral constraint | |
| 83 | % but the library constraint needs to be defined for every examples functional constraint. | |
| 84 | get_behavioral_constraint(Library,(ValidGuards,Operation),InputExamples,OutputExamples,BehavioralConstraint,LocationVars) :- | |
| 85 | % lists of currently used components, necessary if a library is used several times | |
| 86 | retractall(used_library(_)) , | |
| 87 | asserta(used_library([])) , | |
| 88 | InputExamples = [InputValues|_] , | |
| 89 | % create library constraint separated from the funtional constraint | |
| 90 | % to make sure to just obtain one set of location variables | |
| 91 | get_library_constraint(InputValues,Library,(ValidGuards,Operation),LibConstraint,InputVars,OutputVars,EnumeratedConstants) , | |
| 92 | % set the temporary location variables with prefix "l" | |
| 93 | maplist(get_location_var_from_ast_node,InputVars,LocationVarsIn) , | |
| 94 | maplist(get_location_var_from_ast_node,OutputVars,LocationVarsOut) , | |
| 95 | % tuples of raw component name and internal component name like (add,add1) | |
| 96 | used_library(Components) , | |
| 97 | get_preliminary_symmetry_reduction_constraint(Components,LocationVarsIn,LocationVarsOut,SymmetryReductionPred) , | |
| 98 | conjunct_predicates([LibConstraint,SymmetryReductionPred],ExtendedLibConstraint) , | |
| 99 | ||
| 100 | % get some information needed for well-definedness constraint | |
| 101 | get_line_amount(Operation,Library,InputValues,M) , | |
| 102 | length(InputValues,VarAmount) , | |
| 103 | % create well-definedness constraint separated from function constraints | |
| 104 | get_well_definedness_constraint(VarAmount,LocationVarsIn,LocationVarsOut,M,WellDefinednessConstraint) , | |
| 105 | get_max_cardinality_from_examples(InputExamples,MaxCard) , | |
| 106 | get_range_of_integer_nodes_from_examples(MaxCard,InputExamples,InMin,InMax) , | |
| 107 | % create upper and lower bound for input values (kodkod warning) and constants | |
| 108 | create_texpr(integer(InMin),integer,[],IntLowerBound) , | |
| 109 | create_texpr(integer(InMax),integer,[],IntUpperBound) , | |
| 110 | create_texpr(integer(MaxCard),integer,[],CardUpperBound) , ! , | |
| 111 | map_get_function_constraint(Operation,0,Library,ExtendedLibConstraint,InputVars,OutputVars,InputExamples,OutputExamples,FunctionConstraints,ProgramInLocationVars) , | |
| 112 | enumerated_sets_constraint(EnumeratedSetsConstraint) , | |
| 113 | append(OutputVars,EnumeratedConstants,ConstantsAndOutputs) , | |
| 114 | % restrict domains outside of the existential quantifiers | |
| 115 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,ConstantsAndOutputs,ConstantRestrictionList) , | |
| 116 | % and create typing predicates for constants and input output values of components | |
| 117 | create_typing_predicates_from_info(ConstantsAndOutputs,TypingPredicatesConj) , | |
| 118 | conjunct_predicates(ConstantRestrictionList,ConstantRestrictions) , | |
| 119 | findall(InputRestriction,(member(In,InputVars) , get_bounds_for_node(In,IntLowerBound,IntUpperBound,CardUpperBound,InputRestriction)),TempInputRestrictions) , | |
| 120 | conjunct_predicates(TempInputRestrictions,InputRestrictions) , | |
| 121 | conjunct_predicates([EnumeratedSetsConstraint,WellDefinednessConstraint,TypingPredicatesConj,ConstantRestrictions,InputRestrictions|FunctionConstraints],BehavioralConstraint) , | |
| 122 | append([LocationVarsIn,LocationVarsOut,ProgramInLocationVars],LocationVars). | |
| 123 | ||
| 124 | enumerated_sets_constraint(EnumeratedSetsConstraint) :- | |
| 125 | findall(SetName,b_get_machine_set(SetName),EnumeratedSets) , | |
| 126 | full_b_machine(BMachine) , | |
| 127 | get_section(enumerated_elements,BMachine,Elems), | |
| 128 | enumerated_sets_constraint_aux(Elems,EnumeratedSets,TEnumeratedSetsConstraint) , | |
| 129 | conjunct_predicates(TEnumeratedSetsConstraint,EnumeratedSetsConstraint). | |
| 130 | ||
| 131 | enumerated_sets_constraint_aux(_,[],[]). | |
| 132 | enumerated_sets_constraint_aux(Elems,[SetName|T],[b(conjunct(Equality,DistinctConstraint),pred,[])|NT]) :- | |
| 133 | findall(b(identifier(N),global(SetName),[]),member(b(identifier(N),global(SetName),_),Elems),EElems) , | |
| 134 | EElems \== [] , ! , | |
| 135 | Equality = b(equal(b(identifier(SetName),global(SetName),[]),b(set_extension(EElems),set(global(SetName)),[])),pred,[]) , | |
| 136 | get_consistency_constraint(EElems,DistinctConstraint) , | |
| 137 | enumerated_sets_constraint_aux(Elems,T,NT). | |
| 138 | enumerated_sets_constraint_aux(Elems,[_|T],NT) :- | |
| 139 | enumerated_sets_constraint_aux(Elems,T,NT). | |
| 140 | ||
| 141 | map_get_function_constraint(_,_,_,_,_,_,[],[],[],[]). | |
| 142 | map_get_function_constraint(Operation,ExampleCount,Library,LibConstraint,InputVars,OutputVars,[Input|TIn],[Output|TOut],[FunctionConstraint|NTFunction],LocationVars) :- | |
| 143 | get_function_constraint(Operation,ExampleCount,Library,LibConstraint,InputVars,OutputVars,Input,Output,FunctionConstraint,NewLocationVars) , | |
| 144 | NewExampleCount is ExampleCount + 1 , | |
| 145 | map_get_function_constraint(Operation,NewExampleCount,Library,LibConstraint,InputVars,OutputVars,TIn,TOut,NTFunction,NTLVars) , | |
| 146 | append(NewLocationVars,NTLVars,LocationVars). | |
| 147 | ||
| 148 | get_function_constraint(Operation,ExampleCount,Library,LibConstraint,InputVars,OutputVars,InputValues,OutputValues,FunctionConstraint,LocationVars) :- | |
| 149 | % add a predicate setting equalities to the machine variables for the current example, since we possibly consider additional set constants like c = {i}, where i is a machine variable | |
| 150 | synthesis_util:create_equality_nodes_from_example(InputValues,InputEqualityList) , | |
| 151 | % in this context, we have to add the invariants setting the types of the machine variables | |
| 152 | conjunct_predicates(InputEqualityList,InputEquality) , | |
| 153 | b_get_machine_variables(MachineVars) , | |
| 154 | findall(MachineVar,(member(InputValue,InputValues) , get_texpr_info(InputValue,Info) , member(synthesis(machinevar,CurrentVarName),Info) , | |
| 155 | member(MachineVar,MachineVars) , get_texpr_id(MachineVar,CurrentVarName)),CurrentVars) , | |
| 156 | b_get_typing_predicate_for_vars(CurrentVars,TypingMachineVarsPredicate) , | |
| 157 | get_line_amount(Operation,Library,InputValues,M) , | |
| 158 | % enumerate input/output values | |
| 159 | enumerate_inputs_and_outputs(ExampleCount,InputValues,input,InputValueNodes) , | |
| 160 | enumerate_inputs_and_outputs(ExampleCount,OutputValues,output,OutputValueNodes) , | |
| 161 | get_connectivity_constraint(InputValueNodes,OutputValueNodes,InputVars,OutputVars,ConnectivityConstraint) , | |
| 162 | set_input_location_vars(InputValueNodes,InputLocationConstraint) , | |
| 163 | set_output_location_vars(OutputValueNodes,M,OutputLocationConstraint,OutputLocationVars) , | |
| 164 | conjunct_predicates([TypingMachineVarsPredicate,InputEquality,OutputLocationConstraint,InputLocationConstraint,LibConstraint,ConnectivityConstraint],ExistsBody) , | |
| 165 | % get all used identifier as ast nodes | |
| 166 | find_typed_identifier_uses_with_info(ExistsBody,TListOfIDNodes) , | |
| 167 | remove_dup_id_nodes(TListOfIDNodes,ListOfIDNodes) , | |
| 168 | get_temporary_ids(ListOfIDNodes,TempTemporaryIDs) , | |
| 169 | append(TempTemporaryIDs,CurrentVars,TemporaryIDs) , % the machine variables are local to the exists quantifier which are used within the equalities to the machine variables | |
| 170 | findall(LocationVar,(member(LocationVar,ListOfIDNodes) , LocationVar = b(identifier(Name),integer,_) , atom_concat(l,_,Name)),TempListOfLVarNodes) , | |
| 171 | append(TempListOfLVarNodes,OutputLocationVars,LocationVars) , | |
| 172 | % and their corresponding identifier names | |
| 173 | maplist(get_texpr_id,ListOfIDNodes,UsedIDs) , | |
| 174 | % remove exists quantifier --> seems to be slower | |
| 175 | % set_unique_temporary_id_names(ExampleCount,TemporaryIDs,ExistsBody,FunctionConstraint). | |
| 176 | FunctionConstraint = b(exists(TemporaryIDs,ExistsBody),pred,[used_ids(UsedIDs)]). | |
| 177 | ||
| 178 | /*set_unique_temporary_id_names(ExampleCount,TemporaryIDs,b(identifier(Name),Type,Info),b(identifier(UniqueName),Type,Info)) :- | |
| 179 | member(b(identifier(Name),Type,_),TemporaryIDs) , ! , | |
| 180 | atom_codes(Name,NameCodes) , | |
| 181 | number_codes(ExampleCount,SuffixNumber) , | |
| 182 | append(NameCodes,[95|SuffixNumber],UniqueNameCodes) , | |
| 183 | atom_codes(UniqueName,UniqueNameCodes). | |
| 184 | set_unique_temporary_id_names(_,_,b(identifier(Name),Type,Info),b(identifier(Name),Type,Info)). | |
| 185 | set_unique_temporary_id_names(ExampleCount,TemporaryIDs,b(Node,Type,Info),b(NewNode,Type,Info)) :- | |
| 186 | Node =.. [Functor,Arg1,Arg2] , ! , | |
| 187 | set_unique_temporary_id_names(ExampleCount,TemporaryIDs,Arg1,NewArg1) , | |
| 188 | set_unique_temporary_id_names(ExampleCount,TemporaryIDs,Arg2,NewArg2) , | |
| 189 | NewNode =.. [Functor,NewArg1,NewArg2]. | |
| 190 | set_unique_temporary_id_names(ExampleCount,TemporaryIDs,b(Node,Type,Info),b(NewNode,Type,Info)) :- | |
| 191 | Node =.. [Functor,Arg] , ! , | |
| 192 | set_unique_temporary_id_names(ExampleCount,TemporaryIDs,Arg,NewArg) , | |
| 193 | NewNode =.. [Functor,NewArg]. | |
| 194 | set_unique_temporary_id_names(_,_,Ast,Ast).*/ | |
| 195 | ||
| 196 | create_typing_predicates_from_info([],b(truth,pred,[])). | |
| 197 | create_typing_predicates_from_info([Node|T],TypingPredicatesConj) :- | |
| 198 | create_typing_predicate_from_info(Node,TypingPredicate) , | |
| 199 | create_typing_predicates_from_info(T,TypingPredicate,TypingPredicatesConj). | |
| 200 | ||
| 201 | create_typing_predicates_from_info([],Acc,Acc). | |
| 202 | create_typing_predicates_from_info([Node|T],Acc,TypingPredicatesConj) :- | |
| 203 | create_typing_predicate_from_info(Node,TypingPredicate) , | |
| 204 | create_texpr(conjunct(Acc,TypingPredicate),pred,[],NewAcc) , | |
| 205 | create_typing_predicates_from_info(T,NewAcc,TypingPredicatesConj). | |
| 206 | ||
| 207 | create_typing_predicate_from_info(Node,b(member(Node,TypeAst),pred,[])) :- | |
| 208 | get_texpr_info(Node,Info) , | |
| 209 | member(synthesis(type,Type),Info) , | |
| 210 | Type \= pred , ! , | |
| 211 | get_type_ast(Type,TypeAst). | |
| 212 | create_typing_predicate_from_info(_,b(truth,pred,[])). | |
| 213 | ||
| 214 | get_type_ast(global(IndependentType),b(identifier(IndependentType),set(global(IndependentType)),[])). | |
| 215 | get_type_ast(set(global(IndependentType)),b(pow_subset(b(identifier(IndependentType),set(global(IndependentType)),[])),pred,[])) :- !. | |
| 216 | get_type_ast(Nested,b(pow_subset(TypeAst),pred,[])) :- | |
| 217 | Nested =.. [Functor,Type] , | |
| 218 | (Functor = set ; Functor = seq) , | |
| 219 | get_type_ast(Type,TypeAst). | |
| 220 | get_type_ast(couple(A,B),b(cartesian_product(TA,TB),set(couple(A,B)),[])) :- | |
| 221 | get_type_ast(A,TA) , | |
| 222 | get_type_ast(B,TB). | |
| 223 | get_type_ast(integer,b(integer_set('INTEGER'),set(integer),[])). | |
| 224 | get_type_ast(string,b(string_set,set(string),[])). | |
| 225 | get_type_ast(boolean,b(bool_set,set(boolean),[])). | |
| 226 | ||
| 227 | restrict_constant_domains(_,_,_,[],[]). | |
| 228 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,[Out|T],[ConstantRestriction|Restrictions]) :- | |
| 229 | is_integer_constant(Out) , | |
| 230 | ConstantRestriction = b(member(Out,b(interval(IntLowerBound,IntUpperBound),set(integer),[])),pred,[]) , | |
| 231 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,T,Restrictions). | |
| 232 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,[Out|T],[ConstantRestriction|Restrictions]) :- | |
| 233 | is_set_or_seq_constant(Out) , | |
| 234 | ConstantRestriction = b(less_equal(b(card(Out),integer,[]),CardUpperBound),pred,[]) , | |
| 235 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,T,Restrictions). | |
| 236 | % skip constants like boolean | |
| 237 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,[_|T],Restrictions) :- | |
| 238 | restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,T,Restrictions). | |
| 239 | ||
| 240 | get_max_cardinality_from_examples(InputExamples,MaxCard) :- | |
| 241 | flatten(InputExamples,InputSet) , | |
| 242 | findall(SetOrSeqNode,(member(SetOrSeqNode,InputSet) , get_texpr_type(SetOrSeqNode,Type) , (Type = set(_) ; Type = seq(_)) , | |
| 243 | get_texpr_info(SetOrSeqNode,Info) , member(synthesis(initial_example),Info)),SetOrSeqNodes) , | |
| 244 | SetOrSeqNodes \= [] , ! , | |
| 245 | findall(Card,(member(Node,SetOrSeqNodes) , b_compute_expression_nowf_no_bindings(b(card(Node),integer,[]),Card)),Cards) , | |
| 246 | (Cards = [] | |
| 247 | -> MaxCardExamples = 0 | |
| 248 | ; b_compute_expression_nowf_no_bindings(b(max(b(value(Cards),set(integer),[])),integer,[]),Res) , Res = int(MaxCardExamples)) , | |
| 249 | % subjectively add a limit of MaxCard + 3 | |
| 250 | MaxCard is MaxCardExamples + 3. | |
| 251 | % zero if no sets or seq are given | |
| 252 | get_max_cardinality_from_examples(_,0). | |
| 253 | ||
| 254 | % Get the range of integer nodes from the initial examples to restrict constant domains. | |
| 255 | get_range_of_integer_nodes_from_examples(_,InputExamples,InMin,InMax) :- | |
| 256 | flatten(InputExamples,InputSet) , | |
| 257 | get_values_of_integer_nodes(InputSet,[],IntegerValues) , | |
| 258 | IntegerValues \= [] , ! , | |
| 259 | min_member(TInMin,IntegerValues) , max_member(TInMax,IntegerValues) , | |
| 260 | InMin is TInMin - 10 , InMax is TInMax + 10. | |
| 261 | get_range_of_integer_nodes_from_examples(MaxCard,_,0,NMaxCard) :- % at least MaxCard + 5, e.g. card(x) > 5 but no integer is given | |
| 262 | NMaxCard is MaxCard + 5. | |
| 263 | ||
| 264 | % TODO: consider nested sets and seqs of integer for domain restrictions? | |
| 265 | get_values_of_integer_nodes([],Acc,Acc). | |
| 266 | get_values_of_integer_nodes([Input|T],Acc,IntegerValues) :- | |
| 267 | % type is integer, set(integer) or seq(integer) | |
| 268 | get_texpr_type(Input,Type) , | |
| 269 | get_values_of_integer_nodes_aux(Type,Input,Integer) , | |
| 270 | get_values_of_integer_nodes(T,[Integer|Acc],IntegerValues). | |
| 271 | get_values_of_integer_nodes([_|T],Acc,IntegerValues) :- | |
| 272 | % other type or empty set/seq | |
| 273 | get_values_of_integer_nodes(T,Acc,IntegerValues). | |
| 274 | get_values_of_integer_nodes_aux(integer,Input,Integer) :- | |
| 275 | b_compute_expression_nowf_no_bindings(Input,Value) , Value = int(Integer). | |
| 276 | get_values_of_integer_nodes_aux(set(integer),Input,Integer) :- | |
| 277 | not_empty_set_or_seq(Input) , % max([]) is not well-defined | |
| 278 | b_compute_expression_nowf_no_bindings(b(max(Input),integer,[]),Value) , Value = int(Integer). | |
| 279 | get_values_of_integer_nodes_aux(set(integer),Input,Integer) :- | |
| 280 | not_empty_set_or_seq(Input) , % same for empty sequences | |
| 281 | b_compute_expression_nowf_no_bindings(b(max(b(range(Input),set(integer),[])),integer,[]),Value) , Value = int(Integer). | |
| 282 | ||
| 283 | not_empty_set_or_seq(Input) :- | |
| 284 | b_compute_expression_nowf_no_bindings(Input,Value) , Value \= []. | |
| 285 | ||
| 286 | % TODO: same here, consider nested sets and seqs of integer? | |
| 287 | get_bounds_for_node(Node,LowerIntBound,UpperIntBound,_,Restriction) :- | |
| 288 | Node = b(_,integer,_) , | |
| 289 | Restriction = b(member(Node,b(interval(LowerIntBound,UpperIntBound),set(integer),[])),pred,[]). | |
| 290 | get_bounds_for_node(Node,LowerIntBound,UpperIntBound,CardUpperBound,Restriction) :- | |
| 291 | Node = b(_,Type,_) , | |
| 292 | Type = set(integer) , | |
| 293 | % we restrict the cardinality of sets of integers as well as the domain of their elements | |
| 294 | Restriction = b(conjunct(b(less_equal(b(card(Node),integer,[]),CardUpperBound),pred,[]), | |
| 295 | b(member(Node,b(pow_subset(b(interval(LowerIntBound,UpperIntBound),set(integer),[])),set(set(integer)),[])),pred,[])),pred,[]). | |
| 296 | get_bounds_for_node(Node,_LowerIntBound,_UpperIntBound,CardUpperBound,Restriction) :- | |
| 297 | Node = b(_,Type,_) , | |
| 298 | Type = seq(integer) , | |
| 299 | % we restrict the size of seqs of integers | |
| 300 | % TODO: restrict domain of elements of seq(integer) | |
| 301 | Restriction = b(less_equal(b(card(Node),integer,[]),CardUpperBound),pred,[]). | |
| 302 | get_bounds_for_node(Node,_,_,CardUpperBound,Restriction) :- | |
| 303 | Node = b(_,Type,_) , | |
| 304 | % either card or size for sets or sequences | |
| 305 | (Type = set(InnerType) , Functor = card ; Type = seq(InnerType) , Functor = size) , | |
| 306 | InnerType \= integer , | |
| 307 | RestrNode =.. [Functor,Node] , | |
| 308 | % we restrict cardinality/size of sets/seqs with an other type than integer | |
| 309 | Restriction = b(less_equal(b(RestrNode,integer,[]),CardUpperBound),pred,[]). | |
| 310 | ||
| 311 | is_integer_constant(b(Node,integer,Info)) :- | |
| 312 | is_constant(b(Node,integer,Info)). | |
| 313 | ||
| 314 | is_set_or_seq_constant(b(Node,Type,Info)) :- | |
| 315 | (Type = set(_) ; Type = seq(_)) , | |
| 316 | is_constant(b(Node,Type,Info)). | |
| 317 | ||
| 318 | % all temporary library variables like i0,i1,o1 in exists node except 'constant' | |
| 319 | get_temporary_ids([],[]). | |
| 320 | get_temporary_ids([ID|T],[ID|NT]) :- | |
| 321 | get_texpr_id(ID,Name) , | |
| 322 | % filter identifier nodes e.g. referring to enumerated sets or independent types | |
| 323 | get_texpr_info(ID,Info) , | |
| 324 | member(synthesis(_,_),Info) , | |
| 325 | atom_codes(Name,[Char|_]) , | |
| 326 | Char \= 108 , | |
| 327 | \+atom_concat(constant,_,Name) , ! , | |
| 328 | get_temporary_ids(T,NT). | |
| 329 | get_temporary_ids([_|T],NT) :- | |
| 330 | get_temporary_ids(T,NT). | |
| 331 | ||
| 332 | % we can have duplicate nodes because of undefined types of sets | |
| 333 | remove_dup_id_nodes(Nodes,Distinct) :- | |
| 334 | remove_dup_id_nodes(Nodes,[],Distinct). | |
| 335 | remove_dup_id_nodes([],Acc,Acc). | |
| 336 | remove_dup_id_nodes([Node|T],Acc,Distinct) :- | |
| 337 | Node = b(identifier(Name),_,_) , | |
| 338 | \+member(b(identifier(Name),_,_),Acc) , ! , | |
| 339 | remove_dup_id_nodes(T,[Node|Acc],Distinct). | |
| 340 | remove_dup_id_nodes([_|T],Acc,Distinct) :- | |
| 341 | remove_dup_id_nodes(T,Acc,Distinct). | |
| 342 | ||
| 343 | % define connections of temporary inputs and outputs | |
| 344 | get_connectivity_constraint(InputExampleNodes,OutputExampleNodes,InputVars,OutputVars,ConnectivityConstraint) :- | |
| 345 | append([InputVars,OutputVars,InputExampleNodes,OutputExampleNodes],SetOfVars) , | |
| 346 | findall((X,Y),(member(X,SetOfVars) , member(Y,SetOfVars) , X \= Y , nth0(I1,SetOfVars,X) , nth0(I2,SetOfVars,Y) , I1 < I2),ListOfVarPairs) , | |
| 347 | maplist(get_single_connectivity_constraint,ListOfVarPairs,ConstraintList) , | |
| 348 | conjunct_predicates(ConstraintList,ConnectivityConstraint). | |
| 349 | ||
| 350 | get_single_connectivity_constraint((Var1,Var2),ConnectivityConstraint) :- | |
| 351 | get_location_var_from_ast_node(Var1,LocationVar1) , | |
| 352 | get_location_var_from_ast_node(Var2,LocationVar2) , | |
| 353 | % only connect two variables if they have the same type | |
| 354 | (valid_connection(Var1,Var2) | |
| 355 | -> LHS = b(equal(LocationVar1,LocationVar2),pred,[]) , | |
| 356 | RHS = b(equal(Var1,Var2),pred,[]) , | |
| 357 | create_implication(LHS,RHS,ConnectivityConstraint) | |
| 358 | % prevent equality of such incompatible location variables | |
| 359 | ; ConnectivityConstraint = b(not_equal(LocationVar1,LocationVar2),pred,[])). | |
| 360 | ||
| 361 | valid_connection(Var1,Var2) :- | |
| 362 | get_texpr_info(Var1,Info1) , | |
| 363 | get_texpr_info(Var2,Info2) , | |
| 364 | % same type, we use the term synthesis(type,Type) from each node's info instead of the ast node's type | |
| 365 | % reason: we use the type boolean for predicates and real boolean values since one cannot define an identifier of type pred, and thus, | |
| 366 | % a boolean node representing a predicate contains the term synthesis(type,pred) whereat the node itself has the type boolean. | |
| 367 | valid_type_connection(Info1,Info2) , ! , | |
| 368 | valid_connection_aux(Info1,Info2). | |
| 369 | ||
| 370 | % Check if a location variable refers to an input location. | |
| 371 | refers_to_input(Info) :- | |
| 372 | member(synthesis(_,left_input),Info) ; member(synthesis(_,right_input),Info) ; member(synthesis(_,input),Info). | |
| 373 | ||
| 374 | % TODO: maybe rewrite this more pretty, but we definitely have to consider both cases like we do in here | |
| 375 | valid_connection_aux(Info1,Info2) :- | |
| 376 | % machineconstants have fixed values, and thus, are not mapped to program input parameters | |
| 377 | member(synthesis(machineconstant,_),Info1) , | |
| 378 | \+member(synthesis(input(_)),Info2). | |
| 379 | valid_connection_aux(Info2,Info1) :- | |
| 380 | member(synthesis(machineconstant,_),Info1) , | |
| 381 | \+member(synthesis(input(_)),Info2). | |
| 382 | valid_connection_aux(Info1,Info2) :- | |
| 383 | % if_then_else only on the top level of a program output | |
| 384 | member(synthesis(ComponentName,output),Info1) , | |
| 385 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 386 | RawName = if_then_else , | |
| 387 | member(synthesis(output(_)),Info2). | |
| 388 | valid_connection_aux(Info2,Info1) :- | |
| 389 | member(synthesis(ComponentName,output),Info1) , | |
| 390 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 391 | RawName = if_then_else , ! , | |
| 392 | member(synthesis(output(_)),Info2). | |
| 393 | % input of skip component only from program parameters, i.e., the first lines of the program, or the input of another component to not create a contradiction | |
| 394 | valid_connection_aux(Info1,Info2) :- | |
| 395 | member(synthesis(ComponentName,input),Info1) , | |
| 396 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 397 | RawName = skip , | |
| 398 | (member(synthesis(input(_)),Info2) ; refers_to_input(Info2)). | |
| 399 | valid_connection_aux(Info2,Info1) :- | |
| 400 | member(synthesis(ComponentName,input),Info1) , | |
| 401 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 402 | RawName = skip , ! , | |
| 403 | (member(synthesis(input(_)),Info2) ; refers_to_input(Info2)). | |
| 404 | % output of skip component only for program output parameters, i.e., the last lines of the program, or as an if-statement's output | |
| 405 | valid_connection_aux(Info1,Info2) :- | |
| 406 | member(synthesis(ComponentName,output),Info1) , | |
| 407 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 408 | RawName = skip , | |
| 409 | (member(synthesis(output(_)),Info2) ; is_if_statement_output(Info2)). | |
| 410 | valid_connection_aux(Info2,Info1) :- | |
| 411 | member(synthesis(ComponentName,output),Info1) , | |
| 412 | delete_numbers_from_atom(ComponentName,RawName) , | |
| 413 | RawName = skip ,! , | |
| 414 | (member(synthesis(output(_)),Info2) ; is_if_statement_output(Info2)). | |
| 415 | % constant_set only right input of member | |
| 416 | valid_connection_aux(Info1,Info2) :- | |
| 417 | member(synthesis(ConstantSet,output),Info1) , | |
| 418 | delete_numbers_from_atom(ConstantSet,constant_set) , ! , | |
| 419 | member(synthesis(Member,right_input),Info2) , | |
| 420 | delete_numbers_from_atom(Member,Op) , | |
| 421 | (Op = member ; Op = not_member). | |
| 422 | valid_connection_aux(Info2,Info1) :- | |
| 423 | member(synthesis(ConstantSet,output),Info1) , | |
| 424 | delete_numbers_from_atom(ConstantSet,constant_set) , ! , | |
| 425 | member(synthesis(Member,right_input),Info2) , | |
| 426 | delete_numbers_from_atom(Member,Op) , | |
| 427 | (Op = member ; Op = not_member). | |
| 428 | valid_connection_aux(Info1,Info2) :- | |
| 429 | member(synthesis(type,boolean),Info1) , | |
| 430 | (member(synthesis(input(_)),Info2) ; | |
| 431 | (member(synthesis(Comp2,_),Info2) , atom_concat(constant,_,Comp2))). | |
| 432 | valid_connection_aux(Info2,Info1) :- | |
| 433 | member(synthesis(type,boolean),Info1) , | |
| 434 | (member(synthesis(input(_)),Info2) ; | |
| 435 | (member(synthesis(Comp2,_),Info2) , atom_concat(constant,_,Comp2))). | |
| 436 | valid_connection_aux(Info1,Info2) :- | |
| 437 | % input to output mapping is not possible in the synthesis constraint anyway, but explicitly prevent this here to support the solver (we use skip components for that) | |
| 438 | member(synthesis(input(_)),Info1) , ! , | |
| 439 | \+member(synthesis(output(_)),Info2). | |
| 440 | valid_connection_aux(Info2,Info1) :- | |
| 441 | member(synthesis(input(_)),Info1) , ! , | |
| 442 | \+member(synthesis(output(_)),Info2). | |
| 443 | valid_connection_aux(_,_). | |
| 444 | ||
| 445 | valid_type_connection(Info1,Info2) :- | |
| 446 | member(synthesis(type,Type1),Info1) , | |
| 447 | member(synthesis(type,Type2),Info2) , | |
| 448 | valid_type_connection_aux(Type1,Type2). | |
| 449 | ||
| 450 | valid_type_connection_aux(Type,Type). | |
| 451 | % Sequences can also be mapped to set of couples with integer keys. Well definedness is ensured | |
| 452 | % by the well-definedness constraint, i.e., sequences have to be enumerated from 1..n | |
| 453 | valid_type_connection_aux(Type1,Type2) :- | |
| 454 | (Type1 = seq(InnerType) ; Type1 = set(couple(integer,InnerType))) , | |
| 455 | (Type2 = seq(InnerType) ; Type2 = set(couple(integer,InnerType))). | |
| 456 | ||
| 457 | is_if_statement_output(Info) :- | |
| 458 | (member(synthesis(Component,true_out),Info) ; member(synthesis(Component,false_out),Info)) , | |
| 459 | delete_numbers_from_atom(Component,RawComponent) , ! , | |
| 460 | RawComponent = if_then_else. | |
| 461 | ||
| 462 | get_well_definedness_constraint(VarAmount,LocationVarsIn,LocationVarsOut,M,WellDefinednessConstraint) :- | |
| 463 | get_consistency_constraint(LocationVarsOut,ConsistencyConstraint) , | |
| 464 | get_acyclic_constraint(LocationVarsIn,LocationVarsOut,AcyclicConstraint) , | |
| 465 | NewM is M - 1 , % minus one to use an interval | |
| 466 | NewMInput is NewM - 1 , % no input location can get its value from the last line of the internal program | |
| 467 | get_location_constraint(LocationVarsIn,0,NewMInput,InputRestriction) , | |
| 468 | get_location_constraint(LocationVarsOut,VarAmount,NewM,OutputRestriction) , | |
| 469 | restrict_if_statements_output_location(LocationVarsOut,VarAmount,NewM,IfOutputRestrictions) , | |
| 470 | conjunct_predicates([IfOutputRestrictions,InputRestriction,OutputRestriction,ConsistencyConstraint,AcyclicConstraint], | |
| 471 | WellDefinednessConstraint). | |
| 472 | ||
| 473 | % If-statements can only be used on the top level, that is, one of the program outputs. | |
| 474 | restrict_if_statements_output_location(LocationVarsOut,VarAmount,NewM,IfOutputRestrictions) :- | |
| 475 | LowerBound is NewM - VarAmount + 1 , % + 1 to use an interval | |
| 476 | findall(IfOutputRestriction,(member(IfOutputLocation,LocationVarsOut) , get_texpr_info(IfOutputLocation,Info) , member(synthesis(Component,output),Info) , | |
| 477 | delete_numbers_from_atom(Component,RawComponent) , RawComponent = if_then_else , | |
| 478 | IfOutputRestriction = b(member(IfOutputLocation,b(interval(b(integer(LowerBound),integer,[]),b(integer(NewM),integer,[])),set(integer),[])),pred,[])),IfOutputRestrictionList) , | |
| 479 | conjunct_predicates(IfOutputRestrictionList,IfOutputRestrictions). | |
| 480 | ||
| 481 | % create restriction nodes (membership to an interval) to the domain of each location variable | |
| 482 | get_location_constraint(LocationVars,A,B,RestrictionNode) :- | |
| 483 | maplist(get_single_location_constraint(A,B),LocationVars,RestrictionList) , | |
| 484 | conjunct_predicates(RestrictionList,RestrictionNode). | |
| 485 | get_single_location_constraint(A,B,LocationVar,RestrictionNode) :- | |
| 486 | RestrictionNode = b(member(LocationVar, | |
| 487 | b(interval(b(integer(A),integer,[]),b(integer(B),integer,[])),set(integer),[])),pred,[]). | |
| 488 | ||
| 489 | % consistency constraint guarantees that there is only one output in each line | |
| 490 | get_consistency_constraint(LocationVarsOut,Constraint) :- | |
| 491 | % find all pairs of location variables (not redundant) and create "not_equal"-Node for each pair | |
| 492 | get_consistency_constraint_aux(LocationVarsOut,TConstraint) , | |
| 493 | %findall(InequalityNode, | |
| 494 | % (member(L1,LocationVarsOut) , member(L2,LocationVarsOut) , | |
| 495 | % L1 \= L2 , nth0(I1,LocationVarsOut,L1) , nth0(I2,LocationVarsOut,L2) , | |
| 496 | % I1 < I2 , create_texpr(not_equal(L1,L2),pred,[],InequalityNode)),InequalityList) , | |
| 497 | conjunct_predicates(TConstraint,Constraint). | |
| 498 | ||
| 499 | get_consistency_constraint_aux([],[]). | |
| 500 | get_consistency_constraint_aux([LocationVarOut|T],[Inequality|NT]) :- | |
| 501 | findall(b(not_equal(LocationVarOut,LVar),pred,[]),member(LVar,T),InequalityList) , | |
| 502 | conjunct_predicates(InequalityList,Inequality) , | |
| 503 | get_consistency_constraint_aux(T,NT). | |
| 504 | ||
| 505 | % acyclic constraint guarantees that every operator's input is defined before its corresponding output | |
| 506 | get_acyclic_constraint(LocationVarsIn,LocationVarsOut,Constraint) :- | |
| 507 | get_acyclic_constraint_list(LocationVarsIn,LocationVarsOut,ConstraintList) , | |
| 508 | conjunct_predicates(ConstraintList,Constraint). | |
| 509 | get_acyclic_constraint_list(_,[],[]). | |
| 510 | get_acyclic_constraint_list(LocationVarsIn,[Out|ROut],[Constraint|ConstraintList]) :- | |
| 511 | get_texpr_info(Out,Info) , member(synthesis(ComponentID,output),Info) , | |
| 512 | get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,left_input),In1) , | |
| 513 | get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,right_input),In2) , | |
| 514 | create_texpr(less(In1,Out),pred,[],Node1) , | |
| 515 | create_texpr(less(In2,Out),pred,[],Node2) , | |
| 516 | conjunct_predicates([Node1,Node2],Constraint) , | |
| 517 | get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList). | |
| 518 | get_acyclic_constraint_list(LocationVarsIn,[Out|ROut],[Constraint|ConstraintList]) :- | |
| 519 | get_texpr_info(Out,Info) , member(synthesis(ComponentID,output),Info) , | |
| 520 | get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,input),In) , | |
| 521 | create_texpr(less(In,Out),pred,[],Constraint) , | |
| 522 | get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList). | |
| 523 | % skip constants | |
| 524 | get_acyclic_constraint_list(LocationVarsIn,[_|ROut],ConstraintList) :- | |
| 525 | get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList). | |
| 526 | ||
| 527 | % Construct the library constraint by encoding the given library components as logical formulas. | |
| 528 | get_library_constraint(InputValues,Components,(ValidGuards,Operation),Constraint,InputVars,OutputVars,EnumeratedConstants) :- | |
| 529 | create_fixed_constants_to_insert_to_sets(InputValues,FixedSetConstantsConstraint) , | |
| 530 | maplist(get_single_component_constraint,Components,ConstraintList) , | |
| 531 | get_machine_constants_constraint(MachineConstantsConstraint) , | |
| 532 | get_operation_parameters_constraint(ValidGuards,Operation,OperationParametersConstraint) , | |
| 533 | conjunct_predicates([OperationParametersConstraint,FixedSetConstantsConstraint,MachineConstantsConstraint|ConstraintList],TConstraint) , | |
| 534 | find_typed_identifier_uses_with_info(TConstraint,ListOfIDNodes) , | |
| 535 | % split used identifier by input and output | |
| 536 | findall(I,(member(I,ListOfIDNodes) , get_texpr_id(I,IName) , is_component_input(I) , atom_concat(i,_,IName)),InputVars) , | |
| 537 | findall(O,(member(O,ListOfIDNodes) , get_texpr_id(O,OName) , is_component_output(O) , atom_concat(o,_,OName)),OutputVars) , | |
| 538 | findall(C,(member(C,ListOfIDNodes) , is_enumerated_constant(C)),EnumeratedConstants) , | |
| 539 | get_library_wd_constraints(ListOfIDNodes,ListOfIDNodes,[],WDConstraintList) , | |
| 540 | conjunct_predicates([TConstraint|WDConstraintList],Constraint). | |
| 541 | ||
| 542 | is_component_input(Node) :- | |
| 543 | get_texpr_info(Node,Info) , | |
| 544 | (member(synthesis(_,left_input),Info) ; member(synthesis(_,right_input),Info) ; member(synthesis(_,input),Info) | |
| 545 | ; member(synthesis(_,condition),Info) ; member(synthesis(_,true_out),Info) ; member(synthesis(_,false_out),Info)) , !. | |
| 546 | ||
| 547 | is_component_output(Node) :- | |
| 548 | get_texpr_info(Node,Info) , | |
| 549 | member(synthesis(_,output),Info) , !. | |
| 550 | ||
| 551 | is_enumerated_constant(b(identifier(Name),_,Info)) :- | |
| 552 | atom_concat(constant,_,Name) , | |
| 553 | member(synthesis(enumerated_constant),Info) , !. | |
| 554 | ||
| 555 | :- dynamic additional_set_constants/1. | |
| 556 | :- volatile additional_set_constants/1. | |
| 557 | ||
| 558 | % We analyze the current machine variables and add additional set constants. | |
| 559 | % B does not provide an operator to directly insert an element in a set. We provide set constants that | |
| 560 | % are enumerated by the solver, but in this connection the solver is not able to consider machine variables, | |
| 561 | % like enumerating a set constant to be {1,2,i} where i is an integer valued machine variable. | |
| 562 | % To that effect, we add set constants containing a single machine variable, like c = {i} which then | |
| 563 | % can be unified with a set. This is only necessary if, for instance, a set of integers as well as at least one integer | |
| 564 | % valued machine variable is given. | |
| 565 | create_fixed_constants_to_insert_to_sets(InputValues,FixedSetConstantsConstraint) :- | |
| 566 | findall((MachineVarName,Type),(member(InputValue,InputValues) , get_texpr_info(InputValue,Info) , | |
| 567 | member(synthesis(type,Type),Info) , member(synthesis(machinevar,MachineVarName),Info)),MachineVarNameTypeTuples) , | |
| 568 | create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,FixedSetConstantsConstraint). | |
| 569 | % We do not need to add additional constants if no set is given. | |
| 570 | create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,b(truth,pred,[])) :- | |
| 571 | retractall(additional_set_constants(_)) , | |
| 572 | assert(additional_set_constants([])) , | |
| 573 | \+member((_,set(_)),MachineVarNameTypeTuples) , !. | |
| 574 | % Otherwise, create additional set constants. | |
| 575 | create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,FixedSetConstantsConstraint) :- | |
| 576 | get_set_types(MachineVarNameTypeTuples,TempSetTypes) , | |
| 577 | findall(NonSetTypeTuple,(member(NonSetTypeTuple,MachineVarNameTypeTuples) , NonSetTypeTuple = (_,Type) , \+member(Type,TempSetTypes)),NonSetTypeTupleTuples) , | |
| 578 | remove_dups(TempSetTypes,SetTypes) , % we only need one constant for an arbitrary amount of sets of this specific type, like one constant c = {i} for several sets of type integer | |
| 579 | maplist(create_fixed_constants_to_insert_to_sets_aux2(SetTypes,[]),NonSetTypeTupleTuples,TempFixedSetConstantsConstraintList) , | |
| 580 | findall(FixedConstraint,(member(FixedConstraint,TempFixedSetConstantsConstraintList) , FixedConstraint \= []),FixedSetConstantsConstraintList) , | |
| 581 | retractall(additional_set_constants(_)) , | |
| 582 | assert(additional_set_constants(FixedSetConstantsConstraintList)) , | |
| 583 | conjunct_predicates(FixedSetConstantsConstraintList,FixedSetConstantsConstraint). | |
| 584 | ||
| 585 | create_fixed_constants_to_insert_to_sets_aux2([],[],_,[]). % do not use conjunct_predicates if Acc is an empty list since this create b(truth,pred,[]) | |
| 586 | create_fixed_constants_to_insert_to_sets_aux2([],Acc,_,FixedSetConstantsConstraint) :- | |
| 587 | conjunct_predicates(Acc,FixedSetConstantsConstraint). | |
| 588 | create_fixed_constants_to_insert_to_sets_aux2([SetType|T],Acc,NonSetTypeTuple,FixedSetConstantsConstraint) :- | |
| 589 | create_fixed_constant_for_set_and_machine_var_type(SetType,NonSetTypeTuple,FixedConstantValue) , ! , | |
| 590 | unique_typed_id("o",SetType,TempOut) , | |
| 591 | get_texpr_id(TempOut,OutId) , | |
| 592 | add_texpr_infos(TempOut,[synthesis(OutId,output),synthesis(type,SetType),synthesis(machineconstant,FixedConstantValue)],Out) , | |
| 593 | create_texpr(equal(Out,FixedConstantValue),pred,[],FixedConstant) , | |
| 594 | create_fixed_constants_to_insert_to_sets_aux2(T,[FixedConstant|Acc],NonSetTypeTuple,FixedSetConstantsConstraint). | |
| 595 | create_fixed_constants_to_insert_to_sets_aux2([_|T],Acc,NonSetTypeTuple,FixedSetConstantsConstraint) :- | |
| 596 | % skip: the set type does not match the machine var type, that is, NonSetTypeTuple | |
| 597 | create_fixed_constants_to_insert_to_sets_aux2(T,Acc,NonSetTypeTuple,FixedSetConstantsConstraint). | |
| 598 | ||
| 599 | % Fails if the inner type of the set does not match the machine var type, that is, NonSetTypeTuple | |
| 600 | create_fixed_constant_for_set_and_machine_var_type(InnerType,(MachineVarName,InnerType),MachineVar) :- | |
| 601 | b_get_machine_variables(MachineVars) , | |
| 602 | member(MachineVar,MachineVars) , | |
| 603 | get_texpr_id(MachineVar,IdName) , IdName = MachineVarName. | |
| 604 | % We also consider nested sets of sets here. | |
| 605 | create_fixed_constant_for_set_and_machine_var_type(set(InnerType),NonSetTypeTuple,b(set_extension([PartialFixedConstant]),set(InnerType),[])) :- | |
| 606 | create_fixed_constant_for_set_and_machine_var_type(InnerType,NonSetTypeTuple,PartialFixedConstant). | |
| 607 | ||
| 608 | get_set_types(MachineVarNameTypeTuples,SetTypes) :- | |
| 609 | get_set_types_aux(MachineVarNameTypeTuples,[],SetTypes). | |
| 610 | get_set_types_aux([],Acc,Acc). | |
| 611 | get_set_types_aux([(_,set(InnerType))|T],Acc,SetTypes) :- ! , | |
| 612 | get_set_types_aux(T,[set(InnerType)|Acc],SetTypes). | |
| 613 | get_set_types_aux([_|T],Acc,SetTypes) :- | |
| 614 | get_set_types_aux(T,Acc,SetTypes). | |
| 615 | ||
| 616 | % Create synthesis constants for operation parameters and consider the valid guards of the operation which hold | |
| 617 | % the typing of each parameter (this assumption is a fact since otherwise the machine is not well-defined). | |
| 618 | get_operation_parameters_constraint(ValidGuards,Operation,OperationParametersConstraint) :- | |
| 619 | b_get_machine_operation(Operation,_,OperationParameters,_) , ValidGuards \= [] , ! , | |
| 620 | get_operation_parameters_constraint_aux(OperationParameters,[],ConstraintList) , | |
| 621 | get_operation_parameters_constraint_aux2(ValidGuards,ConstraintList,OperationParametersConstraint). | |
| 622 | % The operation does not exist yet, e.g., because we synthesize a new operation from scratch. | |
| 623 | get_operation_parameters_constraint(_,_,b(truth,pred,[])). | |
| 624 | ||
| 625 | get_operation_parameters_constraint_aux([],Acc,Acc). | |
| 626 | get_operation_parameters_constraint_aux([OperationParameter|T],Acc,ConstraintList) :- | |
| 627 | get_texpr_type(OperationParameter,ParameterType) , | |
| 628 | get_texpr_id(OperationParameter,ParameterName) , | |
| 629 | unique_typed_id("o",ParameterType,TempOut) , | |
| 630 | add_texpr_infos(TempOut,[synthesis(ParameterName,output),synthesis(type,ParameterType),synthesis(operationparameter,OperationParameter)],Out) , | |
| 631 | create_texpr(equal(Out,OperationParameter),pred,[],Constraint) , | |
| 632 | get_machine_constants_constraint_aux(T,[Constraint|Acc],ConstraintList). | |
| 633 | ||
| 634 | get_operation_parameters_constraint_aux2(_,[],b(truth,pred,[])). | |
| 635 | get_operation_parameters_constraint_aux2(ValidGuards,ConstraintList,OperationParametersConstraint) :- | |
| 636 | append(ValidGuards,ConstraintList,NewConstraintList) , | |
| 637 | conjunct_predicates(NewConstraintList,OperationParametersConstraint). | |
| 638 | ||
| 639 | % Create synthesis constants for machine constants and consider the machine properties defining the values of | |
| 640 | % machine constants. Therefore, these synthesis constants will not be enumerated by the solver. | |
| 641 | get_machine_constants_constraint(MachineConstantsConstraint) :- | |
| 642 | b_get_machine_constants(MachineConstants) , | |
| 643 | get_machine_constants_constraint_aux(MachineConstants,[],ConstraintList) , | |
| 644 | conjunct_predicates(ConstraintList,MachineConstantsConstraint). | |
| 645 | ||
| 646 | get_machine_constants_constraint_aux([],Acc,[MachineProperties|Acc]) :- | |
| 647 | % append the machine properties defining the machine constants | |
| 648 | b_get_properties_from_machine(MachineProperties). | |
| 649 | get_machine_constants_constraint_aux([MachineConstant|T],Acc,ConstraintList) :- | |
| 650 | get_texpr_type(MachineConstant,ConstantType) , | |
| 651 | get_texpr_id(MachineConstant,ConstantName) , | |
| 652 | unique_typed_id("o",ConstantType,TempOut) , | |
| 653 | add_texpr_infos(TempOut,[synthesis(ConstantName,output),synthesis(type,ConstantType),synthesis(machineconstant,MachineConstant)],Out) , | |
| 654 | create_texpr(equal(Out,MachineConstant),pred,[],Constraint) , | |
| 655 | get_machine_constants_constraint_aux(T,[Constraint|Acc],ConstraintList). | |
| 656 | ||
| 657 | % Create well-definedness constraints to prevent division by zero, max/min of empty sets or | |
| 658 | % front/tail/last/first/perm on empty sequences or power_of with a negative number. | |
| 659 | get_library_wd_constraints(_,[],Acc,Acc). | |
| 660 | get_library_wd_constraints(ListOfIDNodes,[b(Node,Type,Info)|T],Acc,WDConstraintList) :- | |
| 661 | \+member(synthesis(_,output),Info) , | |
| 662 | member(synthesis(OpName,_),Info) , | |
| 663 | get_library_wd_constraints_aux(ListOfIDNodes,OpName,b(Node,Type,Info),AccWDConstraint) , | |
| 664 | get_library_wd_constraints(ListOfIDNodes,T,[AccWDConstraint|Acc],WDConstraintList). | |
| 665 | get_library_wd_constraints(ListOfIDNodes,[_|T],Acc,WDConstraintList) :- | |
| 666 | get_library_wd_constraints(ListOfIDNodes,T,Acc,WDConstraintList). | |
| 667 | ||
| 668 | get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(less_equal(LeftInput,RightInput),pred,[])) :- | |
| 669 | % left input of interval is smaller or equal than the right input | |
| 670 | delete_numbers_from_atom(OpName,RawOpName) , | |
| 671 | RawOpName = interval , | |
| 672 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) , | |
| 673 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput). | |
| 674 | get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(conjunct(b(greater(LeftInput,b(integer(-1),integer,[])),pred,[]),b(greater(RightInput,b(integer(-1),integer,[])),pred,[])),pred,[])) :- | |
| 675 | % modulo only for positive numbers | |
| 676 | delete_numbers_from_atom(OpName,RawOpName) , | |
| 677 | RawOpName = modulo , | |
| 678 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) , | |
| 679 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput). | |
| 680 | get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(not_equal(LeftInput,RightInput),pred,[])) :- | |
| 681 | % prohibit the same inputs for subset/subset_strict like 's <<: s' | |
| 682 | delete_numbers_from_atom(OpName,RawOpName) , | |
| 683 | member(RawOpName,[subset]) , % subset_strict (union and intersection is too restrictive here) | |
| 684 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) , | |
| 685 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput). | |
| 686 | get_library_wd_constraints_aux(_,OpName,Node,b(not_equal(Node,b(integer(0),integer,[])),pred,[])) :- | |
| 687 | % to only check division by zero we would need to check that the variable is the right input, thus the denominator, | |
| 688 | % but we also want to prevent 0/c since this is just the constant value 0 | |
| 689 | delete_numbers_from_atom(OpName,div). | |
| 690 | get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(member(RightInput,b(interval(b(integer(0),integer,[]),b(integer(10),integer,[])),set(integer),[])),pred,[])) :- | |
| 691 | % the exponent of power_of has to be positive and we furthermore restrict the exponent to be less or equal to 10 | |
| 692 | delete_numbers_from_atom(OpName,RawOpName) , | |
| 693 | RawOpName = power_of , | |
| 694 | get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput). | |
| 695 | get_library_wd_constraints_aux(_,OpName,Node,b(greater(b(card(Node),integer,[]),b(integer(0),integer,[])),pred,[])) :- | |
| 696 | delete_numbers_from_atom(OpName,RawOpName) , | |
| 697 | member(RawOpName,[max,min,front,tail,first,last,perm,general_intersection]). | |
| 698 | ||
| 699 | % Library components represented as logical formulas. | |
| 700 | ||
| 701 | get_single_component_constraint(if_then_else-Type,Constraint) :- | |
| 702 | unique_typed_id("i",boolean,TempCondition) , | |
| 703 | unique_typed_id("i",Type,TempIn1) , | |
| 704 | unique_typed_id("i",Type,TempIn2) , | |
| 705 | unique_typed_id("o",Type,TempOut) , | |
| 706 | set_component_id(if_then_else,UniqueComponent) , | |
| 707 | % set information of identifier nodes | |
| 708 | add_texpr_infos(TempCondition,[synthesis(type,pred),synthesis(UniqueComponent,condition)],Condition) , | |
| 709 | add_texpr_infos(TempIn1,[synthesis(type,Type),synthesis(UniqueComponent,true_out)],In1) , | |
| 710 | add_texpr_infos(TempIn2,[synthesis(type,Type),synthesis(UniqueComponent,false_out)],In2) , | |
| 711 | add_texpr_infos(TempOut,[synthesis(type,Type),synthesis(UniqueComponent,output)],Out) , | |
| 712 | Node =.. [if_then_else,Condition,In1,In2] , | |
| 713 | Constraint = b(equal(b(Node,Type,[]),Out),pred,[]). | |
| 714 | % (INTEGER,INTEGER) :: INTEGER | |
| 715 | get_single_component_constraint(Component,Constraint) :- | |
| 716 | member(Component,[add,minus,multiplication,div,modulo,power_of]) , ! , | |
| 717 | unique_typed_id("i",integer,TempIn1) , | |
| 718 | unique_typed_id("i",integer,TempIn2) , | |
| 719 | unique_typed_id("o",integer,TempOut) , | |
| 720 | set_component_id(Component,UniqueComponent) , | |
| 721 | % set information of identifier nodes | |
| 722 | add_texpr_infos(TempIn1,[synthesis(type,integer),synthesis(UniqueComponent,left_input)],In1) , | |
| 723 | add_texpr_infos(TempIn2,[synthesis(type,integer),synthesis(UniqueComponent,right_input)],In2) , | |
| 724 | add_texpr_infos(TempOut,[synthesis(type,integer),synthesis(UniqueComponent,output)],Out) , | |
| 725 | Node =.. [Component,In1,In2] , | |
| 726 | Constraint = b(equal(b(Node,integer,[]),Out),pred,[]). | |
| 727 | % TYPE :: TYPE | |
| 728 | get_single_component_constraint(skip-Type,b(equal(In,Out),pred,[])) :- | |
| 729 | % We can't map inputs to outputs directly since input parameters are located in the first lines of the program | |
| 730 | % whereat output parameter are located in the last lines, and thus, their locations can't match. | |
| 731 | % Therefore, we use a simple wrapper allowing to connect input to output locations implicitly to skip values. | |
| 732 | unique_typed_id("i",Type,TempIn) , | |
| 733 | unique_typed_id("o",Type,TempOut) , | |
| 734 | set_component_id(skip,ComponentName) , | |
| 735 | add_texpr_infos(TempIn,[synthesis(ComponentName,input),synthesis(type,Type)],In) , | |
| 736 | add_texpr_infos(TempOut,[synthesis(ComponentName,output),synthesis(type,Type)],Out). | |
| 737 | % (BOOLEAN,BOOLEAN) :: BOOLEAN | |
| 738 | /*get_single_component_constraint(Operator,Constraint) :- | |
| 739 | member(Operator,[conjunct,disjunct,implication,equivalence]) , ! , | |
| 740 | unique_typed_id("i",boolean,TempIn1) , | |
| 741 | unique_typed_id("i",boolean,TempIn2) , | |
| 742 | unique_typed_id("o",boolean,TempOut) , | |
| 743 | set_component_id(Operator,ComponentName) , | |
| 744 | % set information of identifier nodes | |
| 745 | add_texpr_infos(TempIn1,[synthesis(ComponentName,left_input),synthesis(type,pred)],In1) , | |
| 746 | add_texpr_infos(TempIn2,[synthesis(ComponentName,right_input),synthesis(type,pred)],In2) , | |
| 747 | add_texpr_infos(TempOut,[synthesis(ComponentName,output),synthesis(type,pred)],Out) , | |
| 748 | Node =.. [Operator,In1,In2] , | |
| 749 | Constraint = b(equal(Out,b(convert_bool(b(Node,pred,[])),boolean,[])),pred,[]).*/ | |
| 750 | get_single_component_constraint(Operator,Constraint) :- | |
| 751 | member(Operator,[conjunct,disjunct,implication,equivalence]) , ! , | |
| 752 | unique_typed_id("i",boolean,TempIn1) , | |
| 753 | unique_typed_id("i",boolean,TempIn2) , | |
| 754 | unique_typed_id("o",boolean,TempOut) , | |
| 755 | set_component_id(Operator,ComponentName) , | |
| 756 | % set information of identifier nodes | |
| 757 | add_texpr_infos(TempIn1,[synthesis(ComponentName,left_input),synthesis(type,pred)],In1) , | |
| 758 | add_texpr_infos(TempIn2,[synthesis(ComponentName,right_input),synthesis(type,pred)],In2) , | |
| 759 | add_texpr_infos(TempOut,[synthesis(ComponentName,output),synthesis(type,pred)],Out) , | |
| 760 | get_logical_constraint(Operator,In1,In2,Out,Truth,Falsity) , | |
| 761 | disjunct_predicates([Truth,Falsity],Constraint). | |
| 762 | % (PRED) :: BOOLEAN | |
| 763 | get_single_component_constraint(convert_bool,Constraint) :- | |
| 764 | unique_typed_id("i",boolean,TempIn) , | |
| 765 | unique_typed_id("o",boolean,TempOut) , | |
| 766 | set_component_id(convert_bool,ComponentName) , | |
| 767 | % set information of identifier nodes | |
| 768 | add_texpr_infos(TempIn,[synthesis(ComponentName,input),synthesis(type,pred)],In) , | |
| 769 | add_texpr_infos(TempOut,[synthesis(ComponentName,output),synthesis(type,boolean)],Out) , | |
| 770 | Constraint = b(equal(Out,In),pred,[]). | |
| 771 | % (BOOLEAN :: BOOLEAN) | |
| 772 | get_single_component_constraint(negation,Constraint) :- ! , | |
| 773 | unique_typed_id("i",boolean,TempIn) , | |
| 774 | unique_typed_id("o",boolean,TempOut) , | |
| 775 | set_component_id(negation,Negation) , | |
| 776 | % set information of identifier nodes | |
| 777 | add_texpr_infos(TempIn,[synthesis(Negation,input),synthesis(type,pred)],In) , | |
| 778 | add_texpr_infos(TempOut,[synthesis(Negation,output),synthesis(type,pred)],Out) , | |
| 779 | Truth = b(conjunct(b(equal(In,b(boolean_false,boolean,[])),pred,[]), | |
| 780 | b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) , | |
| 781 | Falsity = b(conjunct(b(equal(In,b(boolean_true,boolean,[])),pred,[]), | |
| 782 | b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]) , | |
| 783 | disjunct_predicates([Truth,Falsity],Constraint). | |
| 784 | % explicit set constants referring to enumerated/deferred sets accessed via operation parameters | |
| 785 | % create two constants p and {p} for each operation parameter p | |
| 786 | % both constants are set up in one call to ensure that the shared identifier p is the same | |
| 787 | get_single_component_constraint(param_constant-global(_),b(truth,pred,[])). % so we skip here and set the constraint below | |
| 788 | get_single_component_constraint(param_constant-set(global(IndependentType)),Constraint) :- | |
| 789 | get_single_constant_or_set_operator_id(constant-global(IndependentType),TempOutSingle,ConstantSingle) , | |
| 790 | get_single_constant_or_set_operator_id(constant-set(global(IndependentType)),TempOutSet,ConstantSet) , ! , | |
| 791 | get_texpr_id(ConstantSingle,ConstantSingleName) , | |
| 792 | get_texpr_id(ConstantSet,ConstantSetName) , | |
| 793 | ParamId = b(identifier(ParamName),global(IndependentType),[synthesis(ConstantSingleName,output),synthesis(type,global(IndependentType)),synthesis(param_single,ParamName),synthesis(ConstantSetName,output),synthesis(type,set(global(IndependentType))),synthesis(param_set,ParamName)]) , % the same parameter identifier p for both constants c1 = p, c2 = {p} | |
| 794 | % set information of identifier node | |
| 795 | add_texpr_infos(TempOutSingle,[synthesis(ConstantSingleName,output),synthesis(type,global(IndependentType)),synthesis(param_single,ParamName)],OutSingle) , | |
| 796 | add_texpr_infos(TempOutSet,[synthesis(ConstantSetName,output),synthesis(type,set(global(IndependentType))),synthesis(param_set,ParamName)],OutSet) , | |
| 797 | atom_concat(p_,IndependentType,ParamName) , | |
| 798 | MachineSet = b(identifier(IndependentType),set(global(IndependentType)),[]) , | |
| 799 | Constraint = b(conjunct(b(conjunct(b(member(ParamId,MachineSet),pred,[]),b(equal(b(set_extension([ParamId]),set(global(IndependentType)),[]),OutSet),pred,[])),pred,[]),b(equal(ParamId,OutSingle),pred,[])),pred,[]). | |
| 800 | % constant :: (INTEGER,BOOLEAN,SET) | |
| 801 | get_single_component_constraint(constant-Type,Constraint) :- | |
| 802 | get_single_constant_or_set_operator_id(constant-Type,TempOut,Constant) , ! , | |
| 803 | get_texpr_id(Constant,ConstantName) , | |
| 804 | % set information of identifier node | |
| 805 | add_texpr_infos(TempOut,[synthesis(ConstantName,output),synthesis(type,Type)],Out) , | |
| 806 | Constraint = b(equal(Constant,Out),pred,[]). | |
| 807 | % bool_set, string_set, integer_set,.. | |
| 808 | get_single_component_constraint(Operator,Constraint) :- | |
| 809 | get_single_constant_or_set_operator_id(Operator,TempOut,b(_,Type,_)) , ! , | |
| 810 | unique_typed_id("constant_set",Type,b(identifier(ConstantName),Type,Info)) , | |
| 811 | add_texpr_infos(TempOut,[synthesis(ConstantName,output),synthesis(type,Type)],Out) , | |
| 812 | % TODO: define as subset to avoid infinite sets (virtual timeout) ? | |
| 813 | Constraint = b(equal(Out,b(identifier(ConstantName),Type,Info)),pred,[]). | |
| 814 | % set-expressions | |
| 815 | % SET :: INTEGER | |
| 816 | get_single_component_constraint(Operator,Constraint) :- | |
| 817 | member(Operator,[min,max]) , | |
| 818 | unique_typed_id("i",set(integer),TempIn) , | |
| 819 | unique_typed_id("o",integer,TempOut) , | |
| 820 | set_component_id(Operator,InternalName) , | |
| 821 | add_texpr_infos(TempIn,[synthesis(InternalName,input),synthesis(type,set(integer))],In) , | |
| 822 | add_texpr_infos(TempOut,[synthesis(InternalName,output),synthesis(type,integer)],Out) , | |
| 823 | Node =.. [Operator,In] , | |
| 824 | Constraint = b(equal(b(Node,integer,[]),Out),pred,[]). | |
| 825 | get_single_component_constraint(card-SetType,Constraint) :- | |
| 826 | unique_typed_id("i",SetType,TempIn) , | |
| 827 | unique_typed_id("o",integer,TempOut) , | |
| 828 | set_component_id(card,InternalName) , | |
| 829 | add_texpr_infos(TempIn,[synthesis(InternalName,input),synthesis(type,SetType)],In) , | |
| 830 | add_texpr_infos(TempOut,[synthesis(InternalName,output),synthesis(type,integer)],Out) , | |
| 831 | Constraint = b(equal(b(card(In),integer,[]),Out),pred,[]). | |
| 832 | % SET :: SET(SET) | |
| 833 | get_single_component_constraint(Operator-SetType,Constraint) :- | |
| 834 | member(Operator,[pow_subset,pow_subset1,fin_subset,fin1_subset]) , | |
| 835 | unique_typed_id("i",SetType,TempIn) , | |
| 836 | unique_typed_id("o",set(SetType),TempOut) , | |
| 837 | set_component_id(Operator,NOperator) , | |
| 838 | add_texpr_infos(TempIn,[synthesis(NOperator,input),synthesis(type,SetType)],In) , | |
| 839 | add_texpr_infos(TempOut,[synthesis(NOperator,output),synthesis(type,set(SetType))],Out) , | |
| 840 | Node =.. [Operator,In] , | |
| 841 | Constraint = b(equal(b(Node,set(SetType),[]),Out),pred,[]). | |
| 842 | % SEQ(TYPE) :: SET(SEQ(TYPE)) | |
| 843 | get_single_component_constraint(Operator-SetType,Constraint) :- | |
| 844 | member(Operator,[seq,seq1,iseq]) , | |
| 845 | SetType = set(InnerType) , | |
| 846 | unique_typed_id("i",SetType,TempIn) , | |
| 847 | unique_typed_id("o",set(seq(InnerType)),TempOut) , | |
| 848 | set_component_id(Operator,InternalName) , | |
| 849 | add_texpr_infos(TempIn,[synthesis(InternalName,input),synthesis(type,SetType)],In) , | |
| 850 | add_texpr_infos(TempOut,[synthesis(InternalName,output),synthesis(type,set(seq(InnerType)))],Out) , | |
| 851 | Node =.. [Operator,In] , | |
| 852 | Constraint = b(equal(b(Node,set(seq(InnerType)),[]),Out),pred,[]). | |
| 853 | % SEQ(TYPE) :: SET(SEQ(TYPE)) | |
| 854 | get_single_component_constraint(perm-SeqType,b(equal(b(perm(In),OutputType,[]),Out),pred,[])) :- | |
| 855 | get_perm_component_output_type(SeqType,OutputType) , | |
| 856 | unique_typed_id("i",SeqType,TempIn) , | |
| 857 | unique_typed_id("o",OutputType,TempOut) , | |
| 858 | set_component_id(perm,InternalName) , | |
| 859 | add_texpr_infos(TempIn,[synthesis(InternalName,input),synthesis(type,SeqType)],In) , | |
| 860 | add_texpr_infos(TempOut,[synthesis(InternalName,output),synthesis(type,OutputType)],Out). | |
| 861 | % SEQ(TYPE) :: SET(SEQ(TYPE)) | |
| 862 | get_single_component_constraint(interval,b(equal(b(interval(In1,In2),set(integer),[]),Out),pred,[])) :- | |
| 863 | unique_typed_id("i",integer,TempIn1) , | |
| 864 | unique_typed_id("i",integer,TempIn2) , | |
| 865 | unique_typed_id("o",set(integer),TempOut) , | |
| 866 | set_component_id(interval,InternalName) , | |
| 867 | add_texpr_infos(TempIn1,[synthesis(InternalName,left_input),synthesis(type,integer)],In1) , | |
| 868 | add_texpr_infos(TempIn2,[synthesis(InternalName,right_input),synthesis(type,integer)],In2) , | |
| 869 | add_texpr_infos(TempOut,[synthesis(InternalName,output),synthesis(type,set(integer))],Out). | |
| 870 | % SET :: SET | |
| 871 | get_single_component_constraint(Operator-SetType,Constraint) :- | |
| 872 | member(Operator,[closure,reflexive_closure]) , | |
| 873 | unique_typed_id("i",SetType,TempIn) , | |
| 874 | unique_typed_id("o",SetType,TempOut) , | |
| 875 | set_component_id(Operator,NOperator) , | |
| 876 | add_texpr_infos(TempIn,[synthesis(NOperator,input),synthesis(type,SetType)],In) , | |
| 877 | add_texpr_infos(TempOut,[synthesis(NOperator,output),synthesis(type,SetType)],Out) , | |
| 878 | Node =.. [Operator,In] , | |
| 879 | Constraint = b(equal(b(Node,SetType,[]),Out),pred,[]). | |
| 880 | % (SET,SET) :: SET | |
| 881 | get_single_component_constraint(Operator-SetType,Constraint) :- | |
| 882 | member(Operator,[union,intersection,concat,insert_front,insert_tail,restrict_front, | |
| 883 | restrict_tail,overwrite,set_subtraction,image,cartesian_product, | |
| 884 | domain_restriction,domain_subtraction,range_restriction,range_subtraction]) , | |
| 885 | get_single_component_constraint_aux3(Operator-SetType,TempIn1,TempIn2,TempOut,Operator) , | |
| 886 | set_component_id(Operator,NOperator) , | |
| 887 | get_texpr_type(TempIn1,In1Type) , | |
| 888 | get_texpr_type(TempIn2,In2Type) , | |
| 889 | get_texpr_type(TempOut,OutType) , | |
| 890 | add_texpr_infos(TempIn1,[synthesis(NOperator,left_input),synthesis(type,In1Type)],In1) , | |
| 891 | add_texpr_infos(TempIn2,[synthesis(NOperator,right_input),synthesis(type,In2Type)],In2) , | |
| 892 | add_texpr_infos(TempOut,[synthesis(NOperator,output),synthesis(type,OutType)],Out) , | |
| 893 | Node =.. [Operator,In1,In2] , | |
| 894 | Constraint = b(equal(b(Node,SetType,[]),Out),pred,[]). | |
| 895 | get_single_component_constraint(Operator-SetType,Constraint) :- | |
| 896 | member(Operator,[first,last,front,tail,general_union,general_intersection,reverse,range,domain]) , | |
| 897 | get_single_component_constraint_aux3(Operator-SetType,TempIn,_,TempOut,Operator) , | |
| 898 | set_component_id(Operator,NOperator) , | |
| 899 | get_texpr_type(TempIn,InType) , | |
| 900 | get_texpr_type(TempOut,OutType) , | |
| 901 | add_texpr_infos(TempIn,[synthesis(NOperator,input),synthesis(type,InType)],In) , | |
| 902 | add_texpr_infos(TempOut,[synthesis(NOperator,output),synthesis(type,OutType)],Out) , | |
| 903 | Node =.. [Operator,In] , | |
| 904 | Constraint = b(equal(b(Node,SetType,[]),Out),pred,[]). | |
| 905 | get_single_component_constraint(size-SetType,Constraint) :- | |
| 906 | get_fn_types(SetType,integer,Type) , | |
| 907 | unique_typed_id("i",seq(Type),TempIn) , | |
| 908 | unique_typed_id("o",integer,TempOut) , | |
| 909 | set_component_id(size,NOperator) , | |
| 910 | add_texpr_infos(TempIn,[synthesis(NOperator,input),synthesis(type,seq(Type))],In) , | |
| 911 | add_texpr_infos(TempOut,[synthesis(NOperator,output),synthesis(type,integer)],Out) , | |
| 912 | Constraint = b(equal(b(size(In),integer,[]),Out),pred,[]). | |
| 913 | ||
| 914 | % (INTEGER,INTEGER) :: BOOLEAN || (BOOLEAN,BOOLEAN) :: BOOLEAN || (SET,SET) :: BOOLEAN | |
| 915 | get_single_component_constraint(Operator,Truth) :- | |
| 916 | get_single_component_constraint_aux2(Operator,TempIn1,TempIn2,TempOut,Op) , | |
| 917 | set_component_id(Op,NOperator) , | |
| 918 | add_texpr_infos(TempIn1,[synthesis(NOperator,left_input)],In1) , | |
| 919 | add_texpr_infos(TempIn2,[synthesis(NOperator,right_input)],In2) , | |
| 920 | add_texpr_infos(TempOut,[synthesis(NOperator,output)],Out) , | |
| 921 | TempTrueNode =.. [Op,In1,In2] , | |
| 922 | TrueNode = b(TempTrueNode,pred,[]) , | |
| 923 | BoolNodeTrue = b(equal(Out,b(boolean_true,boolean,[])),pred,[]) , | |
| 924 | create_equivalence(TrueNode,BoolNodeTrue,Truth). | |
| 925 | ||
| 926 | get_single_component_constraint_aux2(Operator-Type,In1,In2,Out,Operator) :- | |
| 927 | member(Operator,[equal,not_equal,subset,subset_strict,not_subset,not_subset_strict]) , ! , | |
| 928 | unique_typed_id("i",Type,TempIn1) , | |
| 929 | unique_typed_id("i",Type,TempIn2) , | |
| 930 | unique_typed_id("o",boolean,TempOut) , | |
| 931 | add_texpr_infos(TempIn1,[synthesis(type,Type)],In1) , | |
| 932 | add_texpr_infos(TempIn2,[synthesis(type,Type)],In2) , | |
| 933 | add_texpr_infos(TempOut,[synthesis(type,pred)],Out). | |
| 934 | get_single_component_constraint_aux2(Operator-SetType,In1,In2,Out,Operator) :- | |
| 935 | member(Operator,[member,not_member]) , ! , | |
| 936 | (SetType = set(Type) ; SetType = seq(Type)) , | |
| 937 | unique_typed_id("i",Type,TempIn1) , | |
| 938 | unique_typed_id("i",SetType,TempIn2) , | |
| 939 | unique_typed_id("o",boolean,TempOut) , | |
| 940 | add_texpr_infos(TempIn1,[synthesis(type,Type)],In1) , | |
| 941 | add_texpr_infos(TempIn2,[synthesis(type,SetType)],In2) , | |
| 942 | add_texpr_infos(TempOut,[synthesis(type,pred)],Out). | |
| 943 | % greater,greater_equal,less,.. | |
| 944 | get_single_component_constraint_aux2(Operator,In1,In2,Out,Operator) :- | |
| 945 | unique_typed_id("i",integer,TempIn1) , | |
| 946 | unique_typed_id("i",integer,TempIn2) , | |
| 947 | unique_typed_id("o",boolean,TempOut) , | |
| 948 | add_texpr_infos(TempIn1,[synthesis(type,integer)],In1) , | |
| 949 | add_texpr_infos(TempIn2,[synthesis(type,integer)],In2) , | |
| 950 | add_texpr_infos(TempOut,[synthesis(type,pred)],Out). | |
| 951 | ||
| 952 | % set- and seq-expressions | |
| 953 | get_single_component_constraint_aux3(Operator-SetType,TempIn,_,TempOut,Operator) :- | |
| 954 | member(Operator,[general_union,general_intersection]) , | |
| 955 | unique_typed_id("i",SetType,TempIn) , | |
| 956 | SetType = set(InnerType) , | |
| 957 | unique_typed_id("o",InnerType,TempOut). | |
| 958 | get_single_component_constraint_aux3(image-SetType,TempIn1,TempIn2,TempOut,image) :- | |
| 959 | get_fn_types(SetType,A,B) , | |
| 960 | unique_typed_id("i",set(couple(A,B)),TempIn1) , | |
| 961 | unique_typed_id("i",set(A),TempIn2) , | |
| 962 | unique_typed_id("o",set(B),TempOut). | |
| 963 | get_single_component_constraint_aux3(cartesian_product-SetType,TempIn1,TempIn2,TempOut,cartesian_product) :- | |
| 964 | SetType = set(InnerType) , % TODO: what about cartesian product of two differently typed sets? | |
| 965 | unique_typed_id("i",set(InnerType),TempIn1) , | |
| 966 | unique_typed_id("i",set(InnerType),TempIn2) , | |
| 967 | unique_typed_id("o",set(couple(InnerType,InnerType)),TempOut). | |
| 968 | get_single_component_constraint_aux3(Operator-SetType,TempIn1,TempIn2,TempOut,Operator) :- | |
| 969 | member(Operator,[domain_restriction,domain_subtraction]) , | |
| 970 | get_fn_types(SetType,A,B) , | |
| 971 | unique_typed_id("i",set(A),TempIn1) , | |
| 972 | unique_typed_id("i",set(couple(A,B)),TempIn2) , | |
| 973 | unique_typed_id("o",set(couple(A,B)),TempOut). | |
| 974 | get_single_component_constraint_aux3(Operator-SetType,TempIn1,TempIn2,TempOut,Operator) :- | |
| 975 | member(Operator,[range_restriction,range_subtraction]) , | |
| 976 | get_fn_types(SetType,A,B) , | |
| 977 | unique_typed_id("i",set(couple(A,B)),TempIn1) , | |
| 978 | unique_typed_id("i",set(B),TempIn2) , | |
| 979 | unique_typed_id("o",set(couple(A,B)),TempOut). | |
| 980 | get_single_component_constraint_aux3(reverse-SeqType,TempIn,_,TempOut,reverse) :- | |
| 981 | unique_typed_id("i",SeqType,TempIn) , | |
| 982 | unique_typed_id("o",SeqType,TempOut). | |
| 983 | get_single_component_constraint_aux3(domain-SetType,TempIn,_,TempOut,domain) :- | |
| 984 | get_fn_types(SetType,A,_) , | |
| 985 | unique_typed_id("i",SetType,TempIn) , | |
| 986 | unique_typed_id("o",set(A),TempOut). | |
| 987 | get_single_component_constraint_aux3(range-SetType,TempIn,_,TempOut,range) :- | |
| 988 | get_fn_types(SetType,_,B) , | |
| 989 | unique_typed_id("i",SetType,TempIn) , | |
| 990 | unique_typed_id("o",set(B),TempOut). | |
| 991 | get_single_component_constraint_aux3(Operator-SetType,TempIn1,TempIn2,TempOut,Operator) :- | |
| 992 | member(Operator,[union,intersection,set_subtraction]) , | |
| 993 | unique_typed_id("i",SetType,TempIn1) , | |
| 994 | unique_typed_id("i",SetType,TempIn2) , | |
| 995 | unique_typed_id("o",SetType,TempOut). | |
| 996 | get_single_component_constraint_aux3(overwrite-SetType,TempIn1,TempIn2,TempOut,overwrite) :- | |
| 997 | get_fn_types(SetType,integer,Type) , | |
| 998 | unique_typed_id("i",seq(Type),TempIn1) , | |
| 999 | unique_typed_id("i",seq(Type),TempIn2) , | |
| 1000 | unique_typed_id("o",seq(Type),TempOut). | |
| 1001 | get_single_component_constraint_aux3(concat-SeqType,TempIn1,TempIn2,TempOut,concat) :- | |
| 1002 | unique_typed_id("i",SeqType,TempIn1) , | |
| 1003 | unique_typed_id("i",SeqType,TempIn2) , | |
| 1004 | unique_typed_id("o",SeqType,TempOut). | |
| 1005 | get_single_component_constraint_aux3(Operator-SetType,TempIn,_,TempOut,Operator) :- | |
| 1006 | member(Operator,[first,last]) , | |
| 1007 | unique_typed_id("i",SetType,TempIn) , | |
| 1008 | (SetType = seq(InnerType) ; SetType = set(couple(integer,InnerType))) , | |
| 1009 | unique_typed_id("o",InnerType,TempOut). | |
| 1010 | get_single_component_constraint_aux3(Operator-SetType,TempIn,_,TempOut,Operator) :- | |
| 1011 | member(Operator,[front,tail]) , | |
| 1012 | unique_typed_id("i",SetType,TempIn) , | |
| 1013 | unique_typed_id("o",SetType,TempOut). | |
| 1014 | get_single_component_constraint_aux3(insert_front-SetType,TempIn1,TempIn2,TempOut,insert_front) :- | |
| 1015 | get_fn_types(SetType,integer,InnerType) , | |
| 1016 | unique_typed_id("i",InnerType,TempIn1) , | |
| 1017 | unique_typed_id("i",SetType,TempIn2) , | |
| 1018 | unique_typed_id("o",SetType,TempOut). | |
| 1019 | get_single_component_constraint_aux3(insert_tail-SetType,TempIn1,TempIn2,TempOut,insert_tail) :- | |
| 1020 | get_fn_types(SetType,integer,InnerType) , | |
| 1021 | unique_typed_id("i",SetType,TempIn1) , | |
| 1022 | unique_typed_id("i",InnerType,TempIn2) , | |
| 1023 | unique_typed_id("o",SetType,TempOut). | |
| 1024 | get_single_component_constraint_aux3(Operator-SetType,TempIn1,TempIn2,TempOut,Operator) :- | |
| 1025 | member(Operator,[restrict_front,restrict_tail]) , | |
| 1026 | unique_typed_id("i",SetType,TempIn1) , | |
| 1027 | unique_typed_id("i",integer,TempIn2) , | |
| 1028 | unique_typed_id("o",SetType,TempOut). | |
| 1029 | ||
| 1030 | % Operators | |
| 1031 | % Use boolean instead of pred_true/pred_false. We can't define identifier ASTs of type predicate. | |
| 1032 | get_logical_constraint(implication,In1,In2,Out,Truth,Falsity) :- | |
| 1033 | Truth = b(conjunct(b(disjunct( | |
| 1034 | b(equal(In1,b(boolean_false,boolean,[])),pred,[]), | |
| 1035 | b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]), | |
| 1036 | b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) , | |
| 1037 | Falsity = b(conjunct(b(conjunct( | |
| 1038 | b(equal(In1,b(boolean_true,boolean,[])),pred,[]), | |
| 1039 | b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]), | |
| 1040 | b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]). | |
| 1041 | get_logical_constraint(equivalence,In1,In2,Out,Truth,Falsity) :- | |
| 1042 | get_logical_constraint(implication,In1,In2,Out,TruthImpl1,FalsityImpl1) , | |
| 1043 | get_logical_constraint(implication,In2,In1,Out,TruthImpl2,FalsityImpl2) , | |
| 1044 | Truth = b(conjunct(TruthImpl1,TruthImpl2),pred,[]) , | |
| 1045 | Falsity = b(disjunct(FalsityImpl1,FalsityImpl2),pred,[]). | |
| 1046 | get_logical_constraint(conjunct,In1,In2,Out,Truth,Falsity) :- | |
| 1047 | Truth = b(conjunct(b(conjunct( | |
| 1048 | b(equal(In1,b(boolean_true,boolean,[])),pred,[]), | |
| 1049 | b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]), | |
| 1050 | b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) , | |
| 1051 | Falsity = b(conjunct(b(disjunct( | |
| 1052 | b(equal(In1,b(boolean_false,boolean,[])),pred,[]), | |
| 1053 | b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]), | |
| 1054 | b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]). | |
| 1055 | get_logical_constraint(disjunct,In1,In2,Out,Truth,Falsity) :- | |
| 1056 | Truth = b(conjunct(b(disjunct( | |
| 1057 | b(equal(In1,b(boolean_true,boolean,[])),pred,[]), | |
| 1058 | b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]), | |
| 1059 | b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) , | |
| 1060 | Falsity = b(conjunct(b(conjunct( | |
| 1061 | b(equal(In1,b(boolean_false,boolean,[])),pred,[]), | |
| 1062 | b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]), | |
| 1063 | b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]). | |
| 1064 | ||
| 1065 | get_fn_types(seq(Type),integer,Type). | |
| 1066 | get_fn_types(set(couple(A,B)),A,B). | |
| 1067 | ||
| 1068 | % Get the output type of permutations component, i.e., perm(s) for a sequence s. | |
| 1069 | get_perm_component_output_type(set(CoupleType),set(seq(CoupleType))) :- | |
| 1070 | CoupleType = couple(integer,_). | |
| 1071 | get_perm_component_output_type(seq(InnerType),set(seq(couple(integer,InnerType)))). | |
| 1072 | ||
| 1073 | % Add prefix "l" to Var for connectivity constraint, add the type to the location variables | |
| 1074 | % information and adopt the given information which encodes the location variables reference, | |
| 1075 | % e.g. [synthesis(type,integer),synthesis(left_input,greater)] | |
| 1076 | get_location_var_from_ast_node(b(identifier(Name),_,Info),b(identifier(LocationName),integer,Info)) :- | |
| 1077 | ! , atom_concat(l,Name,LocationName). | |
| 1078 | get_location_var_from_ast_node(b(_,Type,Info),b(identifier(LocationName),integer,Info)) :- | |
| 1079 | get_location_var_from_ast_node_aux(Type,ValueCode) , | |
| 1080 | % set input/output enumeration as prefix to get unique name | |
| 1081 | % output location names are like 'lovalue0boolean_true' | |
| 1082 | member(synthesis(example(ExampleCount)),Info) , | |
| 1083 | number_codes(ExampleCount,ExampleCountCode) , | |
| 1084 | (member(synthesis(input(C)),Info) | |
| 1085 | -> number_codes(C,NC) , | |
| 1086 | append([[105,110,112,117,116],NC,ExampleCountCode],CCode) | |
| 1087 | ; member(synthesis(output(C)),Info) , | |
| 1088 | number_codes(C,NumberCodes) , | |
| 1089 | append([[111,118,97,108,117,101],NumberCodes,ExampleCountCode],CCode)) , | |
| 1090 | append(CCode,ValueCode,Codes) , | |
| 1091 | atom_codes(LocationName,[108|Codes]). | |
| 1092 | ||
| 1093 | get_location_var_from_ast_node_aux(Type,ValueCode) :- | |
| 1094 | Type =.. [Functor|_] , | |
| 1095 | atom_codes(Functor,ValueCode). | |
| 1096 | ||
| 1097 | % Enumerate used components for identifier nodes information so we definitely | |
| 1098 | % know which input/output locations belong together if a component is used multiple times. | |
| 1099 | % Here, the library components are represented as tuples of the component name and its internal name with id as postfix. | |
| 1100 | set_component_id(Component,ComponentWithId) :- | |
| 1101 | used_library(Components) , | |
| 1102 | retract(used_library(_)) , | |
| 1103 | length(Components,OpAmount) , | |
| 1104 | ComponentId is OpAmount + 1 , | |
| 1105 | atom_number_concat(Component,ComponentId,ComponentWithId) , | |
| 1106 | assert(used_library([(Component,ComponentWithId)|Components])). | |
| 1107 | ||
| 1108 | % Evaluate M := |I| + N, i.e., the amount of variables considered in the examples plus the amount of library components. | |
| 1109 | % We do not consider machine constants as explicit library components since their values are defined by the machine properties, i.e., the amount | |
| 1110 | % of machine constants is not considered within N. Therefore, we have to add x lines to the program where x is the amount of machine constants. | |
| 1111 | % Moreover, we may consider operation parameters if present which we handle equivalent to machine constants. | |
| 1112 | % Generally, the value of M determines the amount of lines in the program | |
| 1113 | get_line_amount(Operation,Components,InputVars,M) :- | |
| 1114 | additional_set_constants(AdditionalSetConstants) , | |
| 1115 | length(AdditionalSetConstants,AC) , | |
| 1116 | length(InputVars,I) , | |
| 1117 | length(Components,N) , | |
| 1118 | b_get_machine_constants(MachineConstants) , | |
| 1119 | % if the operation exists consider the amount of operation parameters for that we consider synthesis constants | |
| 1120 | (ground(Operation) , b_get_machine_operation(Operation,_,OperationParameters,_) | |
| 1121 | -> length(OperationParameters,OperationParameterAmount) | |
| 1122 | ; OperationParameterAmount = 0) , | |
| 1123 | length(MachineConstants,AmountOfMachineConstants) , | |
| 1124 | M is I + N + AmountOfMachineConstants + AC + OperationParameterAmount. | |
| 1125 | ||
| 1126 | % Set the location variables of the program parameters and output given by I/O-Examples. | |
| 1127 | % Each input parameters are defined in the first lines of the program | |
| 1128 | set_input_location_vars(InputValueNodes,InputLocations) :- | |
| 1129 | set_input_location_vars(InputValueNodes,0,[],InputLocationsList) , | |
| 1130 | conjunct_predicates(InputLocationsList,InputLocations). | |
| 1131 | set_input_location_vars([],_,Acc,Acc). | |
| 1132 | set_input_location_vars([InputValueNode|R],C,Acc,InputLocations) :- | |
| 1133 | get_location_var_from_ast_node(InputValueNode,InputLocationNode) , | |
| 1134 | InputLocation = b(equal(InputLocationNode,b(integer(C),integer,[])),pred,[]) , | |
| 1135 | C1 is C + 1 , | |
| 1136 | set_input_location_vars(R,C1,[InputLocation|Acc],InputLocations). | |
| 1137 | % We dispose output values in descending order starting at the last line of the program | |
| 1138 | set_output_location_vars(OutputValueNodes,M,OutputLocations,OutputLocationVars) :- | |
| 1139 | M1 is M - 1 , | |
| 1140 | set_output_location_vars(OutputValueNodes,M1,[],OutputLocationsList,[],OutputLocationVars) , | |
| 1141 | conjunct_predicates(OutputLocationsList,OutputLocations). | |
| 1142 | set_output_location_vars([],_,Acc,Acc,VarAcc,VarAcc). | |
| 1143 | set_output_location_vars([OutputValueNode|R],C,Acc,OutputLocations,VarAcc,OutputLocationVars) :- | |
| 1144 | get_location_var_from_ast_node(OutputValueNode,OutputLocationNode) , | |
| 1145 | OutputLocation = b(equal(OutputLocationNode,b(integer(C),integer,[])),pred,[]) , | |
| 1146 | C1 is C - 1 , | |
| 1147 | add_texpr_infos(OutputLocationNode,[synthesis(program_line(C))],NewOutputLocationNode) , | |
| 1148 | set_output_location_vars(R,C1,[OutputLocation|Acc],OutputLocations,[NewOutputLocationNode|VarAcc],OutputLocationVars). | |
| 1149 | ||
| 1150 | % Enumerate input nodes in the info to use within the connectivity constraint, the corresponding machine variable names have already been added to each node's info. | |
| 1151 | % We also enumerate the examples in the order they are given to get unique identifier names for program input and output parameter later on and especially unique names that | |
| 1152 | % can be reconstructed using the node's info. Using unique_typed_id/3 we get like any unique identifier without any pattern to reconstruct later on. | |
| 1153 | enumerate_inputs_and_outputs(ExampleCount,InputValues,StateType,InputNodes) :- | |
| 1154 | enumerate_inputs_and_outputs(ExampleCount,InputValues,StateType,0,InputNodes). | |
| 1155 | enumerate_inputs_and_outputs(_,[],_,_,[]). | |
| 1156 | enumerate_inputs_and_outputs(ExampleCount,[b(Node,Type,Info)|R],input,C,[b(Node,Type,[synthesis(input(C)),synthesis(example(ExampleCount)),synthesis(type,Type)|Info])|T]) :- | |
| 1157 | C1 is C + 1 , | |
| 1158 | enumerate_inputs_and_outputs(ExampleCount,R,input,C1,T). | |
| 1159 | enumerate_inputs_and_outputs(ExampleCount,[b(Node,Type,Info)|R],output,C,[b(Node,Type,[synthesis(output(C)),synthesis(example(ExampleCount)),synthesis(type,Type)|Info])|T]) :- | |
| 1160 | C1 is C + 1 , | |
| 1161 | enumerate_inputs_and_outputs(ExampleCount,R,output,C1,T). | |
| 1162 | ||
| 1163 | atom_number_concat(Atom,Number,Concatenation) :- | |
| 1164 | number_codes(Number,NumberCodes) , | |
| 1165 | atom_codes(Atom,AtomCodes) , | |
| 1166 | append(AtomCodes,NumberCodes,ConcatCodes) , | |
| 1167 | atom_codes(Concatenation,ConcatCodes). | |
| 1168 | ||
| 1169 | % Get an output ĺocation variable for a specific location value. | |
| 1170 | get_output_location_for_location_value(LocationVars,SolutionBindings,LocationValue,OutputLocationVar) :- | |
| 1171 | get_binding_for_name_or_value(SolutionBindings,OutputLocationName,LocationValue) , | |
| 1172 | atom_concat(lo,_,OutputLocationName) , ! , | |
| 1173 | member(OutputLocationVar,LocationVars) , OutputLocationVar = b(identifier(OutputLocationName),integer,_). | |
| 1174 | % Return a node for the location value in case there is no explicit operators' output mapped, thus, it is an input parameter. | |
| 1175 | % We know the first input parameter is in the first line of the program etc. which will not change, therefore we | |
| 1176 | % do not need the explicit location variable name but only the location value. | |
| 1177 | get_output_location_for_location_value(_,_,int(Value),b(integer(Value),integer,[])). | |
| 1178 | ||
| 1179 | % add input location variables since the program asts contain explicit values | |
| 1180 | accumulate_used_location_var_aux(Operator,LocationVars,Acc,NewAcc) :- | |
| 1181 | findall(LocationVar,(member(LocationVar,LocationVars) , LocationVar = b(_,_,Info) , | |
| 1182 | member(synthesis(Operator,LocationType),Info) , | |
| 1183 | (LocationType = left_input ; LocationType = right_input)),InputLocationVars) , | |
| 1184 | append(Acc,InputLocationVars,NewAcc). | |
| 1185 | ||
| 1186 | :- spec_pre(get_used_location_vars_and_op_names/6,[ast,list(ast),list(ast),list(atom),var,var]). | |
| 1187 | :- spec_invariant(get_used_location_vars_and_op_names/6,[ast,list(ast),list(ast),list(atom),list(ast),list(atom)]). | |
| 1188 | :- spec_post(get_used_location_vars_and_op_names/6,[ast,list(ast),list(ast),list(atom),var,var], | |
| 1189 | [ast,list(ast),list(ast),list(atom),list(ast),list(atom)]). | |
| 1190 | get_used_location_vars_and_op_names(b(Node,_,Info),LocationVars,LocationAcc,OpAcc,UsedLocationVars,UsedOperatorNames) :- | |
| 1191 | Node =.. [if_then_else,Condition,TrueOut,FalseOut] , | |
| 1192 | accumulate_used_location_var(Info,LocationVars,LocationAcc,OpAcc,LocationAcc1,OpAcc1) , | |
| 1193 | get_used_location_vars_and_op_names(Condition,LocationVars,LocationAcc1,OpAcc1,LocationAcc2,OpAcc2) , | |
| 1194 | get_used_location_vars_and_op_names(TrueOut,LocationVars,LocationAcc2,OpAcc2,LocationAcc3,OpAcc3) , | |
| 1195 | get_used_location_vars_and_op_names(FalseOut,LocationVars,LocationAcc3,OpAcc3,UsedLocationVars,UsedOperatorNames) , !. | |
| 1196 | get_used_location_vars_and_op_names(b(Node,_,Info),LocationVars,LocationAcc,OpAcc,UsedLocationVars,UsedOperatorNames) :- | |
| 1197 | Node =.. [_,LeftAST,RightAST] , | |
| 1198 | is_ast(LeftAST) , is_ast(RightAST) , | |
| 1199 | accumulate_used_location_var(Info,LocationVars,LocationAcc,OpAcc,LocationAcc1,OpAcc1) , | |
| 1200 | get_used_location_vars_and_op_names(LeftAST,LocationVars,LocationAcc1,OpAcc1,LocationAcc2,OpAcc2) , | |
| 1201 | get_used_location_vars_and_op_names(RightAST,LocationVars,LocationAcc2,OpAcc2,UsedLocationVars,UsedOperatorNames) , !. | |
| 1202 | %findall(ParameterLocation,(member(ParameterLocation,LocationVars) , | |
| 1203 | % ParameterLocation = b(_,_,Info) , member(synthesis(input(_)),Info)),ParameterLocations) , | |
| 1204 | %append(TempUsedLocationVars,ParameterLocations,UsedLocationVars). | |
| 1205 | get_used_location_vars_and_op_names(b(Node,_,Info),LocationVars,LocationAcc,OpAcc,UsedLocationVars,UsedOperatorNames) :- | |
| 1206 | Node =.. [_,AST] , | |
| 1207 | accumulate_used_location_var(Info,LocationVars,LocationAcc,OpAcc,NewLocationAcc,NewOpAcc) , | |
| 1208 | (is_ast(AST) | |
| 1209 | -> get_used_location_vars_and_op_names(AST,LocationVars,NewLocationAcc,NewOpAcc,UsedLocationVars,UsedOperatorNames) | |
| 1210 | ; UsedLocationVars = NewLocationAcc , UsedOperatorNames = NewOpAcc). | |
| 1211 | get_used_location_vars_and_op_names(_,_,_,_,Acc,Acc). | |
| 1212 | ||
| 1213 | accumulate_used_location_var(Info,LocationVars,LocationAcc,OpAcc,NewLocationAcc,[Op|OpAcc]) :- | |
| 1214 | member(synthesis(Op,output),Info) , | |
| 1215 | \+member(Op,OpAcc) , | |
| 1216 | member(b(identifier(_),integer,IdInfo),LocationVars) , | |
| 1217 | member(synthesis(Op,output),IdInfo) , | |
| 1218 | accumulate_used_location_var_aux(Op,LocationVars,LocationAcc,NewLocationAcc). | |
| 1219 | accumulate_used_location_var(_,_,LocationAcc,OpAcc,LocationAcc,OpAcc). | |
| 1220 | ||
| 1221 | :- spec_pre(get_input_location_nodes_for_operator_name/4,[atom,list(ast),list(ast),var]). | |
| 1222 | :- spec_invariant(get_input_location_nodes_for_operator_name/4,[atom,list(ast),list(ast),list(ast)]). | |
| 1223 | :- spec_post(get_input_location_nodes_for_operator_name/4,[atom,list(ast),list(ast),var], | |
| 1224 | [atom,list(ast),list(ast),list(ast)]). | |
| 1225 | get_input_location_nodes_for_operator_name(_,[],Acc,Acc). | |
| 1226 | get_input_location_nodes_for_operator_name(OperatorName,[LocationVar|T],Acc,InputLocations) :- | |
| 1227 | LocationVar = b(identifier(_),integer,Info) , | |
| 1228 | member(synthesis(OperatorName,LocationType),Info) , | |
| 1229 | LocationType \= output , ! , | |
| 1230 | get_input_location_nodes_for_operator_name(OperatorName,T,[LocationVar|Acc],InputLocations). | |
| 1231 | get_input_location_nodes_for_operator_name(OperatorName,[_|T],Acc,InputLocations) :- | |
| 1232 | get_input_location_nodes_for_operator_name(OperatorName,T,Acc,InputLocations). | |
| 1233 | ||
| 1234 | %get_output_location_node_for_operator_name(OperatorName,[OutputLocationNode|_],OutputLocationNode) :- | |
| 1235 | % OutputLocationNode = b(identifier(_),integer,Info) , | |
| 1236 | % member(synthesis(OperatorName,output),Info) , !. | |
| 1237 | %get_output_location_node_for_operator_name(OperatorName,[_|T],OutputLocationNode) :- | |
| 1238 | % get_output_location_node_for_operator_name(OperatorName,T,OutputLocationNode). | |
| 1239 | ||
| 1240 | is_constant(b(identifier(Constant),_,_)) :- | |
| 1241 | atom_concat(constant,_,Constant). | |
| 1242 | is_constant(b(_,_,Info)) :- | |
| 1243 | member(synthesis(OpName,output),Info) , | |
| 1244 | atom_concat(constant,_,OpName). | |
| 1245 | ||
| 1246 | exclude_solution_for_further_search(UsedOperatorNames,LocationVars,SolutionBindings,Exclusion) :- | |
| 1247 | maplist(exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings),UsedOperatorNames,TExclusionList) , | |
| 1248 | remove_dups(TExclusionList,ExclusionList) , | |
| 1249 | disjunct_predicates(ExclusionList,TempExclusion) , | |
| 1250 | exclude_solution_for_further_search_aux(TempExclusion,Exclusion). | |
| 1251 | ||
| 1252 | exclude_solution_for_further_search_aux(b(falsity,_,_),b(truth,pred,[])) :- !. | |
| 1253 | exclude_solution_for_further_search_aux(Exclusion,Exclusion). | |
| 1254 | ||
| 1255 | % constants: Inequality with the input location it is mapped to or with the explicit location value | |
| 1256 | % in case the constant is the program output. | |
| 1257 | exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :- | |
| 1258 | atom_concat(constant,_,OperatorName) , ! , | |
| 1259 | get_location_var_node_by_info_term(LocationVars,synthesis(OperatorName,output),ConstantLocation) , | |
| 1260 | ConstantLocation = b(identifier(ConstantLocationName),integer,_) , | |
| 1261 | get_binding_for_name_or_value(SolutionBindings,ConstantLocationName,LocationValue) , | |
| 1262 | get_binding_for_name_or_value(SolutionBindings,MappedInputLocationName,LocationValue) , | |
| 1263 | MappedInputLocationName \= ConstantLocationName , | |
| 1264 | % exclude connection for all constants to prevent swapping with other constants of the same type | |
| 1265 | findall(E,(member(ConstantNode,LocationVars) , is_constant(ConstantNode) , ConstantNode = b(identifier(CName),_,_) , | |
| 1266 | get_binding_for_name_or_value(SolutionBindings,CName,LValue) , | |
| 1267 | ConstantLocationName \= CName , | |
| 1268 | exclude_output_to_input_mapping_for_constant_aux(LocationVars,LValue,ConstantLocation,CName,E)),TExclusions) , | |
| 1269 | flatten(TExclusions,Exclusions) , | |
| 1270 | exclude_output_to_input_mapping_for_constant_aux(LocationVars,LocationValue,ConstantLocation,MappedInputLocationName,TExclusion) , | |
| 1271 | conjunct_predicates([TExclusion|Exclusions],Exclusion). | |
| 1272 | exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :- | |
| 1273 | get_location_var_node_by_info_term(LocationVars,synthesis(OperatorName,output),ConstantLocation) , | |
| 1274 | ConstantLocation = b(identifier(ConstantLocationName),integer,_) , | |
| 1275 | get_binding_for_name_or_value(SolutionBindings,ConstantLocationName,LocationValue) , | |
| 1276 | get_binding_for_name_or_value(SolutionBindings,MappedInputLocationName,LocationValue) , | |
| 1277 | MappedInputLocationName \= ConstantLocationName , | |
| 1278 | exclude_output_to_input_mapping_for_constant_aux(LocationVars,LocationValue,ConstantLocation,MappedInputLocationName,Exclusion). | |
| 1279 | % Exclude the mapping of a given operators input locations to its corresponding output locations for the given solution. | |
| 1280 | exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :- | |
| 1281 | get_input_location_nodes_for_operator_name(OperatorName,LocationVars,[],InputLocations) , InputLocations \= [] , | |
| 1282 | maplist(exclude_specific_input_output_mapping(LocationVars,SolutionBindings),InputLocations,InputOutputExclusions) , | |
| 1283 | disjunct_predicates(InputOutputExclusions,Exclusion). | |
| 1284 | ||
| 1285 | exclude_output_to_input_mapping_for_constant_aux(LocationVars,_,ConstantLocation,MappedInputLocationName,Exclusion) :- | |
| 1286 | member(MappedInputLocationVar,LocationVars) , MappedInputLocationVar = b(identifier(MappedInputLocationName),_,_) , | |
| 1287 | create_texpr(not_equal(ConstantLocation,MappedInputLocationVar),pred,[],Exclusion). | |
| 1288 | %exclude_output_to_input_mapping_for_constant_aux(_,LocationValue,ConstantLocation,_,Exclusion) :- | |
| 1289 | % create_texpr(not_equal(ConstantLocation,b(value(LocationValue),integer,[])),pred,[],Exclusion). | |
| 1290 | ||
| 1291 | exclude_specific_input_output_mapping(LocationVars,SolutionBindings,b(identifier(Id),integer,Info),Exclusion) :- | |
| 1292 | get_binding_for_name_or_value(SolutionBindings,Id,LocationValue) , | |
| 1293 | get_output_location_for_location_value(LocationVars,SolutionBindings,LocationValue,OutputLocationVar) , | |
| 1294 | create_texpr(not_equal(b(identifier(Id),integer,Info),OutputLocationVar),pred,[],Exclusion). | |
| 1295 | exclude_specific_input_output_mapping(_,_,_,b(falsity,pred,[])). | |
| 1296 | ||
| 1297 | % Using a component several times, e.g. with internal names add1,add2, we don't want to | |
| 1298 | % swap both components when searching for a further solution. | |
| 1299 | get_prevent_component_swap_constraint(UsedLVars,SolutionBindings,LocationVars,Constraint) :- | |
| 1300 | get_input_location_vars_for_outputs(UsedLVars,LocationVars,OutputInputsTuples) , | |
| 1301 | maplist(exclude_swapping_for_component(SolutionBindings,LocationVars),OutputInputsTuples,TExclusions) , | |
| 1302 | remove_dups(TExclusions,Exclusions) , | |
| 1303 | conjunct_predicates(Exclusions,Constraint). | |
| 1304 | ||
| 1305 | % TODO: Maybe consider constants too? | |
| 1306 | get_input_location_vars_for_outputs(UsedLVars,LocationVars,OutputInputsTuples) :- | |
| 1307 | % create tuples of component and an empty list to use as an accumulator | |
| 1308 | findall((Component,[]),(member(OutLVar,UsedLVars) , get_texpr_info(OutLVar,Info) , | |
| 1309 | member(synthesis(Component,output),Info)),Acc) , | |
| 1310 | get_input_location_vars_for_outputs_aux(LocationVars,Acc,OutputInputsTuples). | |
| 1311 | get_input_location_vars_for_outputs_aux([],Acc,Acc). | |
| 1312 | get_input_location_vars_for_outputs_aux([LocationVar|T],Acc,OutputInputsTuples) :- | |
| 1313 | get_texpr_info(LocationVar,Info) , | |
| 1314 | (member(synthesis(Component,left_input),Info) ; member(synthesis(Component,right_input),Info) ; member(synthesis(Component,input),Info)) , | |
| 1315 | member((Component,Inputs),Acc) , | |
| 1316 | delete(Acc,(Component,Inputs),TempAcc) , | |
| 1317 | remove_dups([LocationVar|Inputs],InputLVars), | |
| 1318 | NewTuple = (Component,InputLVars) , | |
| 1319 | \+member(NewTuple,Acc) , % no duplicates | |
| 1320 | get_input_location_vars_for_outputs_aux(T,[NewTuple|TempAcc],OutputInputsTuples). | |
| 1321 | get_input_location_vars_for_outputs_aux([_|T],Acc,OutputInputsTuples) :- | |
| 1322 | get_input_location_vars_for_outputs_aux(T,Acc,OutputInputsTuples). | |
| 1323 | ||
| 1324 | % Given a tuple of an output location var and the corresponding component's inputs. | |
| 1325 | % We search for the output locations that are mapped to the input locations. | |
| 1326 | % Then, we search all equivalent component inputs and exclude mapping the output locations to | |
| 1327 | % the equivalent input location. | |
| 1328 | % Thus, we exclude swapping two equivalent operators when searching for a further solution for a given | |
| 1329 | % synthesized program. | |
| 1330 | exclude_swapping_for_component(SolutionBindings,LocationVars,(OutLVar,InLVars),ExclusionConstraint) :- | |
| 1331 | maplist(get_lvar_name_and_input_type,InLVars,InLVarNames,InLVarTypes) , | |
| 1332 | % get the location values the inputs of OutLVar are mapped to | |
| 1333 | maplist(get_binding_for_name_or_value(SolutionBindings),InLVarNames,InLVarValues) , | |
| 1334 | % create tuples of (lvar,lvalue) | |
| 1335 | zip(InLVarNames,InLVarValues,VarValueTuples) , | |
| 1336 | zip(InLVarNames,InLVarTypes,VarTypeTuples) , | |
| 1337 | % then, get the output locations those inputs are mapped to | |
| 1338 | maplist(get_corresponding_mapped_location(SolutionBindings,LocationVars),VarValueTuples,CorrespondingLocations) , | |
| 1339 | % and create tuples of output locations and the type of the input they are mapped to, i.e., | |
| 1340 | % either left_input or right_input | |
| 1341 | findall((OutLVarName,InputType),(member((InLVar,OutLVarName),CorrespondingLocations) , | |
| 1342 | member((InLVar,InputType),VarTypeTuples)),OutLVarInTypeTuples) , | |
| 1343 | exclude_swapping_for_component_aux(LocationVars,(OutLVar,OutLVarInTypeTuples),ExclusionConstraint). | |
| 1344 | exclude_swapping_for_component_aux(LocationVars,(OutLVarName,OutLVarInTypeTuples),ExclusionConstraint) :- | |
| 1345 | get_equivalent_input_location_nodes(OutLVarName,LocationVars,EquivalentInputLocations) , | |
| 1346 | % find pairs of output and input location that correspond (are mapped) to the same input type, i.e. | |
| 1347 | % either left_input, right_input or input | |
| 1348 | findall(Exclusion,(member((CorOutLVarName,InputType),OutLVarInTypeTuples) , | |
| 1349 | get_location_var_node_by_name(CorOutLVarName,LocationVars,OutLVarNode) , | |
| 1350 | member((InLVarNode,InputType),EquivalentInputLocations) , | |
| 1351 | create_texpr(not_equal(OutLVarNode,InLVarNode),pred,[],Exclusion)),Exclusions) , | |
| 1352 | conjunct_predicates(Exclusions,ExclusionConstraint). | |
| 1353 | ||
| 1354 | % Get all input locations that are equivalent to the component that LocationVarName belongs to. | |
| 1355 | % Don't consider exactly the same location var. | |
| 1356 | get_equivalent_input_location_nodes(LocationVarName,LocationVars,InputLocations) :- | |
| 1357 | delete_numbers_from_atom(LocationVarName,RawName) , | |
| 1358 | get_equivalent_input_location_nodes_aux(LocationVarName,RawName,LocationVars,[],InputLocations). | |
| 1359 | get_equivalent_input_location_nodes_aux(_,_,[],Acc,Acc). | |
| 1360 | get_equivalent_input_location_nodes_aux(LocationVarName,RawName,[LocationVar|T],Acc,InputLocations) :- | |
| 1361 | get_texpr_info(LocationVar,Info) , | |
| 1362 | member(synthesis(LVarName,InputType),Info) , | |
| 1363 | (InputType = left_input ; InputType = right_input ; InputType = input) , | |
| 1364 | delete_numbers_from_atom(LVarName,RawLVarName) , | |
| 1365 | RawLVarName = RawName , | |
| 1366 | % not exactly the same location | |
| 1367 | LVarName \= LocationVarName , | |
| 1368 | \+member((LocationVar,InputType),Acc) , % no duplicates | |
| 1369 | get_equivalent_input_location_nodes_aux(LocationVarName,RawName,T,[(LocationVar,InputType)|Acc],InputLocations). | |
| 1370 | get_equivalent_input_location_nodes_aux(LocationVarName,RawName,[_|T],Acc,InputLocations) :- | |
| 1371 | get_equivalent_input_location_nodes_aux(LocationVarName,RawName,T,Acc,InputLocations). | |
| 1372 | ||
| 1373 | % Given a tuple of location var name and mapped value, we search for the other location var that | |
| 1374 | % is mapped to this location value (line of the program). | |
| 1375 | get_corresponding_mapped_location(SolutionBindings,_,(LVarName,LVarValue),(LVarName,LVarName2)) :- | |
| 1376 | get_binding_for_name_or_value(SolutionBindings,LVarName2,LVarValue) , | |
| 1377 | delete_numbers_from_atom(LVarName2,RawName) , | |
| 1378 | RawName \= constant , | |
| 1379 | LVarName \= LVarName2. | |
| 1380 | ||
| 1381 | get_lvar_name_and_input_type(b(identifier(LVarName),integer,Info),LVarName,InputType) :- | |
| 1382 | get_input_type_from_info(Info,InputType). | |
| 1383 | ||
| 1384 | get_input_type_from_info(Info,left_input) :- | |
| 1385 | member(synthesis(_,left_input),Info). | |
| 1386 | get_input_type_from_info(Info,right_input) :- | |
| 1387 | member(synthesis(_,right_input),Info). | |
| 1388 | get_input_type_from_info(Info,input) :- | |
| 1389 | member(synthesis(_,input),Info). |