| 1 | | % (c) 2009-2019 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(eval_strings,[ |
| 6 | | add_last_expression_to_unit_tests/0, print_last_expression/0, indent_print_last_expression/0, |
| 7 | | unsat_core_last_expression/0, |
| 8 | | last_expression_type/1, last_expression/3, get_last_result_value/3, |
| 9 | | print_last_info/0, print_last_value/0, browse_repl_lets/0, |
| 10 | | toggle_eval_det/0, toggle_normalising/0, |
| 11 | | eval_string/2,eval_string/3,eval_string/4,eval_string_with_time_out/4, |
| 12 | | eval_codes/6, |
| 13 | | eval_expression_codes/6, |
| 14 | | eval_file/5, |
| 15 | | toggle_observe_evaluation/0, |
| 16 | | set_eval_dot_file/1, unset_eval_dot_file/0, |
| 17 | | reset_eval_strings/0, |
| 18 | | get_error_positions/1]). |
| 19 | | |
| 20 | | :- use_module(library(lists)). |
| 21 | | |
| 22 | | :- use_module(error_manager). |
| 23 | | :- use_module(tools). |
| 24 | | :- use_module(debug). |
| 25 | | :- use_module(external_functions,[observe_parameters/2]). |
| 26 | | :- use_module(kernel_objects,[max_cardinality/2]). |
| 27 | | %:- use_module(b_ast_cleanup,[get_sorted_ids/2,not_occurs_in_predicate/2]). % TO DO: move predicate calling this to another module |
| 28 | | :- use_module(preferences,[get_computed_preference/2, get_preference/2, |
| 29 | | temporary_set_preference/3, reset_temporary_preference/2]). |
| 30 | | |
| 31 | | |
| 32 | | :- use_module(module_information,[module_info/2]). |
| 33 | | :- module_info(group,repl). |
| 34 | | :- module_info(description,'Tools to evaluate B expressions and predicates passed as strings.'). |
| 35 | | |
| 36 | | :- use_module(bmachine,[b_get_machine_constants/1,b_get_machine_variables/1, |
| 37 | | b_parse_machine_expression_from_codes/6, |
| 38 | | b_parse_machine_predicate_from_codes_open/5, |
| 39 | | b_parse_machine_formula_from_codes/7]). |
| 40 | | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). |
| 41 | | |
| 42 | | % GENERAL EVAL for Expressions & Predicates |
| 43 | | |
| 44 | | eval_string(String,StringResult) :- eval_string(String,StringResult,_EnumWarning,_). |
| 45 | | eval_string(String,StringResult,EnumWarning) :- eval_string(String,StringResult,EnumWarning,_). |
| 46 | | eval_string(String,StringResult,EnumWarning,LocalState) :- % String is an atom |
| 47 | | atom_codes(String,Codes), |
| 48 | | eval_codes(Codes,exists,StringResult,EnumWarning,LocalState,_). |
| 49 | | eval_string_with_time_out(String,StringResult,EnumWarning,LocalState) :- |
| 50 | | atom_codes(String,Codes), |
| 51 | | eval_codes_with_time_out(Codes,exists,StringResult,EnumWarning,LocalState,_). |
| 52 | | |
| 53 | | % evaluate a single formula from a file |
| 54 | | eval_file(Filename,OuterQuantifier,StringResult,EnumWarning,TypeInfo) :- |
| 55 | | read_string_from_file(Filename,Codes), |
| 56 | | eval_codes_with_time_out(Codes,OuterQuantifier,StringResult,EnumWarning,_,TypeInfo), |
| 57 | | debug_println(19,eval_file(Filename,StringResult,EnumWarning)). |
| 58 | | |
| 59 | | |
| 60 | | %:- use_module(library(timeout)). |
| 61 | | :- use_module(tools_meta,[safe_time_out/3]). |
| 62 | | eval_codes_with_time_out(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo) :- |
| 63 | | %format("Eval: ~s~n",[Codes]), |
| 64 | | get_computed_preference(debug_time_out,DTO), |
| 65 | | %print(debug_time_out(DTO)),nl, |
| 66 | | safe_time_out(eval_codes(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo),DTO,TimeOutRes), |
| 67 | | (TimeOutRes=time_out -> |
| 68 | | StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl, |
| 69 | | EnumWarning = time_out |
| 70 | | ; true). |
| 71 | | |
| 72 | | :- use_module(tools_meta,[call_residue/2]). |
| 73 | | :- volatile current_codes/1. |
| 74 | | :- dynamic current_codes/1. |
| 75 | | set_current_codes(C) :- retractall(current_codes(_)), assert(current_codes(C)). |
| 76 | | %eval_codes(C,_,Res,E,L) :- print(eval_codes(C)),nl,fail. |
| 77 | | eval_codes(E,Q,Res,EnumWarning,LS,TypeInfo) :- |
| 78 | | call_residue(eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo),Residue), |
| 79 | | (Residue = [] -> true ; |
| 80 | | eval_det -> print('Call residue in eval_codes: '),print_term_summary(Residue),nl |
| 81 | | ; add_internal_error('Call residue in eval_codes: ',Residue) %,tools_printing:print_goal(Residue) |
| 82 | | ). |
| 83 | | eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo) :- |
| 84 | | set_error_context(eval_codes), |
| 85 | | reset_repl_lets, % remove invalid lets if required |
| 86 | | on_exception(enumeration_warning(Cause,ID,_,_,_), |
| 87 | | eval_codes_aux0(E,Q,Res,EnumWarning,LS,TypeInfo), |
| 88 | | (get_time_out_message(Cause,ID,CauseStr), |
| 89 | | add_message(eval_strings,'TIME-OUT forced by ',CauseStr), |
| 90 | | EnumWarning = true, |
| 91 | | Res = 'TIME-OUT' |
| 92 | | )), |
| 93 | | clear_error_context. |
| 94 | | |
| 95 | | get_time_out_message(kodkod_timeout,_ProblemId,Msg) :- !, Msg = 'KODKOD'. |
| 96 | | get_time_out_message(_,_,'ENUMERATION WARNING'). |
| 97 | | |
| 98 | | eval_codes_aux0("$$",_,Res,false,[],print_last_expression) :- !, Res='', |
| 99 | | print_last_expression. |
| 100 | | eval_codes_aux0("$",_,Res,false,[],print_last_info) :- !, Res='', |
| 101 | | print_last_info. |
| 102 | | eval_codes_aux0(Codes,_,Res,false,[],set_eval_repeat) :- append("!r",Rest,Codes), |
| 103 | | number_codes(Nr,Rest), !, Res='', |
| 104 | | set_eval_repeat(Nr). |
| 105 | | eval_codes_aux0(Codes,_OuterQuantifier,Res,false,LocalState,list) :- |
| 106 | | ( append(":list ",Rest,Codes), |
| 107 | | scan_identifier(Rest,IDCodes,Rest2), atom_codes(ID,IDCodes) |
| 108 | | ; |
| 109 | | Codes = ":list", ID=help, Rest2=[]), |
| 110 | | !, |
| 111 | | (just_whitespace(Rest2) -> true ; add_error(eval_strings,'Ignoring extra argument: ',Rest2)), |
| 112 | | list_information(ID,Res,LocalState). |
| 113 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- |
| 114 | | append(":check ",Rest,Codes), |
| 115 | | TypeInfo=predicate(_), |
| 116 | | !, |
| 117 | | debug_println(20,check_recognised), |
| 118 | | (eval_codes_aux(Rest,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) |
| 119 | | -> (Res== 'TRUE' -> true ; |
| 120 | | atom_codes(S,Rest), add_error(check,':check predicate not TRUE: ',S) |
| 121 | | ) |
| 122 | | ; atom_codes(S,Rest), add_error(check,':check illegal predicate: ',S) |
| 123 | | ). |
| 124 | | eval_codes_aux0(Codes,_OuterQuantifier,RRes,EnumWarning,LocalState,TypeInfo) :- |
| 125 | | append(":exec ",Rest,Codes), |
| 126 | | TypeInfo=subst, |
| 127 | | !, |
| 128 | | debug_println(4,'parsing substitution'), |
| 129 | | repl_parse_substitution(Rest,Statement), |
| 130 | | pp_eval_expr(Statement), |
| 131 | | enter_new_error_scope(ScopeID,eval_codes_aux0),clear_all_errors_in_error_scope(ScopeID), |
| 132 | | (user:tcltk_add_user_executed_statement(Statement,Updates,NewID) |
| 133 | | -> format('Successfully executed statement leading to state: ~w~n',[NewID]), |
| 134 | | Res = 'TRUE',LocalState=Updates |
| 135 | | ; translate:translate_substitution(Statement,Str), |
| 136 | | format_with_colour(user_output,[red],'Could not execute statement: ~w~n',[Str]), |
| 137 | | Res = 'FALSE',LocalState=[] |
| 138 | | ), |
| 139 | | EnumWarning=false, |
| 140 | | print('Execution result: '),display_and_set_result(ScopeID,Res,RRes,EnumWarning), |
| 141 | | (LocalState=[] -> true ; print('Updates:'),nl,display_solution(unknown,LocalState)). |
| 142 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- % let ID = EXPR construct |
| 143 | | (append("let ",Rest,Codes) ; append(":let ",Rest,Codes)), |
| 144 | | scan_identifier(Rest,IDCodes,Rest2), |
| 145 | | atom_codes(ID,IDCodes), |
| 146 | | scan_to_equal(Rest2,Rest3), |
| 147 | | !, |
| 148 | | debug_println(20,let_recognised(ID)), |
| 149 | | eval_codes_aux(Rest3,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo), |
| 150 | | (store_let_id_last_value(ID) -> true ; format_with_colour(user_error,[red],'### Could not store let: ~w~n',[ID])). |
| 151 | | eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :s ID : store ID extracted from last predicate |
| 152 | | (append(":s ",Rest,Codes) ; append(":store ",Rest,Codes)), |
| 153 | | scan_identifier(Rest,IDCodes,Rest2), |
| 154 | | atom_codes(ID,IDCodes), |
| 155 | | Rest2=[], % TO DO: allow whitespace |
| 156 | | !, |
| 157 | | (get_last_predicate_value_for_id(ID,T,Val) |
| 158 | | -> store_let_id_last_value(ID), translate:translate_bvalue_with_limit(Val,50,VS), |
| 159 | | format('Stored ~w = ~w~n',[ID,VS]), Res=Val, TypeInfo = T |
| 160 | | ; format_with_colour(user_error,[red],'### Could not find value for ~w in last predicate~n',[ID]), Res=error, TypeInfo=error), |
| 161 | | EnumWarning=false, LocalState=[]. |
| 162 | | eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :u ID : remove let for ID |
| 163 | | (append(":u ",Rest,Codes) ; append(":unlet ",Rest,Codes)), |
| 164 | | scan_identifier(Rest,IDCodes,Rest2), |
| 165 | | atom_codes(ID,IDCodes), |
| 166 | | Rest2=[], % TO DO: allow whitespace |
| 167 | | !, |
| 168 | | (retract(stored_let_value(ID,_,_)) -> |
| 169 | | format('Undefined let ~w~n',[ID]), Res=ID, TypeInfo = unlet, |
| 170 | | reset_parse_cache % TO DO: maybe remove just all cached expressions using ID |
| 171 | | ; format_with_colour(user_error,[red],'### Could not find let for ~w. Use :b to browse your lets.~n',[ID]), Res=error, TypeInfo=error), |
| 172 | | EnumWarning=false, LocalState=[]. |
| 173 | | eval_codes_aux0(":b",_,Res,EnumWarning,LocalState,browsing) :- |
| 174 | | !,EnumWarning=false, LocalState=[], |
| 175 | | get_repl_lets_info(Res), print(repl_lets(Res)),nl. |
| 176 | | eval_codes_aux0([58,116,32|Expression],_,Res,EnumWarning,LocalState,typing) :- % :t Expression Haskell like command |
| 177 | | % Should we always enable this command ? |
| 178 | | !, EnumWarning=false, LocalState=[], |
| 179 | | repl_typing_scope(TypingScope), |
| 180 | | (b_parse_machine_expression_from_codes(Expression,TypingScope,_Typed,Type,true,Error) |
| 181 | | -> (Error=none |
| 182 | | -> translate:pretty_type(Type,PrettyType), |
| 183 | | (max_cardinality(Type,Card) -> true ; Card='??'), |
| 184 | | ajoin([PrettyType,' /* card=',Card,' */'],Res), |
| 185 | | print(Res),nl |
| 186 | | ; (Error=type_error -> get_type_error(Res) ; Res = 'SYNTAX ERROR'), |
| 187 | | print_red('Not a valid expression'),nl) |
| 188 | | ; print_red('Parsing failed'),nl, |
| 189 | | Res = 'SYNTAX ERROR'). |
| 190 | | % TO DO: add bind(VAR,EXPR_Val) for next eval |
| 191 | | eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_), |
| 192 | | (append(":cvc ",PredCodes,Codes) ; append(":cvc4 ",PredCodes,Codes)), |
| 193 | | !, |
| 194 | | solve_using_smt_solver(cvc4,PredCodes,OuterQuantifier,Res,LocalState,TypeInfo). |
| 195 | | eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_), |
| 196 | | append(":z3 ",PredCodes,Codes), |
| 197 | | !, |
| 198 | | solve_using_smt_solver(z3,PredCodes,OuterQuantifier,Res,LocalState,TypeInfo). |
| 199 | | eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_), |
| 200 | | append(":z3-file ",FileCodes,Codes), |
| 201 | | !, |
| 202 | | atom_codes(File,FileCodes), |
| 203 | | format_with_colour(user_output,[dark_gray],'Reading Z3 predicate from file ~w~n',[File]), |
| 204 | | tools:read_string_from_file(File,PredCodes), |
| 205 | | debug_format(19,'Predicate read from file:~n~s~n',[PredCodes]), |
| 206 | | solve_using_smt_solver(z3,PredCodes,OuterQuantifier,Res,LocalState,TypeInfo). |
| 207 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- %TypeInfo=predicate(_), |
| 208 | | append(":kodkod ",PredCodes,Codes), !, |
| 209 | | temporary_set_preference(try_kodkod_on_load,true,CHG), |
| 210 | | call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo), |
| 211 | | reset_temporary_preference(try_kodkod_on_load,CHG)). |
| 212 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- |
| 213 | | append(":chr ",PredCodes,Codes), !, |
| 214 | | temporary_set_preference(use_chr_solver,true,CHG), |
| 215 | | call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo), |
| 216 | | reset_temporary_preference(use_chr_solver,CHG)). |
| 217 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- |
| 218 | | append(":cse ",PredCodes,Codes), !, |
| 219 | | temporary_set_preference(use_common_subexpression_elimination,true,CHG), |
| 220 | | call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo), |
| 221 | | reset_temporary_preference(use_common_subexpression_elimination,CHG)). |
| 222 | | |
| 223 | | |
| 224 | | eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- |
| 225 | | eval_codes_aux(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo). |
| 226 | | |
| 227 | | eval_codes_aux(Expression,_,Res,EnumWarning,LocalState,TypeInfo) :- TypeInfo=expression(_), |
| 228 | | repl_parse_expression(Expression,Typed,Type,Error), |
| 229 | | (Error=none ; Error=type_error), |
| 230 | | !, |
| 231 | | eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo). |
| 232 | | eval_codes_aux(Expression,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- |
| 233 | | TypeInfo=predicate(_), |
| 234 | | repl_parse_predicate(Expression,OuterQuantifier,Typed,TypeInfo), |
| 235 | | !, |
| 236 | | eval_predicate(Typed,Res,EnumWarning,LocalState). |
| 237 | | eval_codes_aux(_E,_,Res,false,[],TypeInfo) :- |
| 238 | | %findall(S,check_error_occured(S,_),L), print(errs(L)),nl, |
| 239 | | (check_error_occured(type_expression_error,_) -> Res = 'TYPE ERROR', TI = error |
| 240 | | ; Res = 'SYNTAX ERROR', TI = syntax_error |
| 241 | | ), |
| 242 | | show_error_pos, |
| 243 | | ((nonvar(TypeInfo),TypeInfo=predicate(_)) -> print('Not a valid predicate'),nl |
| 244 | | ; (nonvar(TypeInfo),TypeInfo=expression(_)) -> print('Not a valid expression'),nl |
| 245 | | ; print('Not a valid expression or predicate'),nl |
| 246 | | ), |
| 247 | | TypeInfo=TI. |
| 248 | | |
| 249 | | % ------------------ |
| 250 | | |
| 251 | | % a separate predicate for evaluating expressions |
| 252 | | eval_expression_codes(Expression,Res,EnumWarning,LocalState,Typed,TypeInfo) :- |
| 253 | | repl_parse_expression(Expression,Typed,Type,Error), |
| 254 | | (Error=none ; Error=type_error), |
| 255 | | eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo). |
| 256 | | eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo) :- |
| 257 | | (Error=type_error |
| 258 | | -> show_error_pos,print('TYPE ERROR'),nl, |
| 259 | | get_type_error(Res), EnumWarning=false, LocalState=[], TypeInfo=error |
| 260 | | ; pp_eval_expr(Typed), |
| 261 | | (Type=pred |
| 262 | | -> eval_predicate(Typed,Res,EnumWarning,LocalState) % happens for DEFINITIONS ?? |
| 263 | | % TypeInfo unification will fail ??? TO DO : investigate !! |
| 264 | | ; eval_expression(Typed,Res),EnumWarning=false,LocalState=[]), |
| 265 | | extract_type_information(Typed,TypeInfo) |
| 266 | | ). |
| 267 | | |
| 268 | | % optionally cache parsing results, avoid overhead of Java B parser call and socket communication |
| 269 | | % especially useful for latex_processor with while loops |
| 270 | | :- dynamic parse_expr_cache/5, parse_pred_cache/5. |
| 271 | | :- use_module(library(terms),[term_hash/2]). |
| 272 | | %:- use_module(hit_profiler,[add_profile_hit/1]). |
| 273 | | repl_parse_expression(Expression,Typed,Type,Error) :- |
| 274 | | get_preference(repl_cache_parsing,true), |
| 275 | | term_hash(Expression,H), |
| 276 | | (parse_expr_cache(H,Expression,Typed,Type,Error) -> ! |
| 277 | | ; parse_pred_cache(H,Expression,_,_,_) -> !, fail % we have already parsed it as a predicate; fail so that we call repl_parse_predicate later |
| 278 | | ). |
| 279 | | %hit_profiler:add_profile_hit(parse_expr_cache). |
| 280 | | repl_parse_expression(Expression,Typed,Type,Error) :- hit_profiler:add_profile_hit(parse_expr), |
| 281 | | set_current_codes(Expression), |
| 282 | | debug_println(20,parsing_as_expression(Expression)), |
| 283 | | %open('repl_parsing.txt',append,S),format(S,'~s~n',[Expression]),close(S), |
| 284 | | repl_typing_scope(TypingScope), |
| 285 | | b_parse_machine_expression_from_codes(Expression,TypingScope,Typed,Type,false,Error), |
| 286 | | debug_println(20,parse_result(Error,Type)), |
| 287 | | (get_preference(repl_cache_parsing,true) -> term_hash(Expression,H),assert(parse_expr_cache(H,Expression,Typed,Type,Error)) |
| 288 | | ; true). |
| 289 | | |
| 290 | | repl_parse_predicate(Expression,OuterQuantifier,Typed,TypeInfo) :- |
| 291 | | get_preference(repl_cache_parsing,true), |
| 292 | | term_hash(Expression,H), |
| 293 | | parse_pred_cache(H,Expression,OuterQuantifier,Typed,TypeInfo),!. |
| 294 | | repl_parse_predicate(Expression,OuterQuantifier,Typed,TypeInfo) :- |
| 295 | | debug_println(20,parsing_as_predicate(Expression)), |
| 296 | | repl_typing_scope(TypingScope), |
| 297 | | b_parse_machine_predicate_from_codes_open(OuterQuantifier,Expression, % will also mark outer variables so that they are not removed |
| 298 | | [],TypingScope,Typed),!, |
| 299 | | %print(Typed),nl, |
| 300 | | debug_println(20,eval_predicate(Typed)), |
| 301 | | pp_eval_expr(Typed), |
| 302 | | extract_type_information(Typed,TypeInfo), |
| 303 | | (get_preference(repl_cache_parsing,true) -> term_hash(Expression,H), |
| 304 | | assert(parse_pred_cache(H,Expression,OuterQuantifier,Typed,TypeInfo)) |
| 305 | | ; true). |
| 306 | | |
| 307 | | repl_parse_substitution(Codes,Typed) :- |
| 308 | | repl_typing_scope(TypingScope), append(SubstScope,[variables],TypingScope), % remove variables; otherwise we get clash warnings |
| 309 | | temporary_set_preference(allow_local_operation_calls,true,CHNG), |
| 310 | | b_parse_machine_formula_from_codes(substitution,Codes,[operation_bodies|SubstScope], |
| 311 | | Typed,_Type,true,Error), |
| 312 | | reset_temporary_preference(allow_local_operation_calls,CHNG), |
| 313 | | (Error=none -> true ; add_error(eval_strings,'Error occured while parsing substitution: ',Error),fail). |
| 314 | | |
| 315 | | |
| 316 | | % repeat a pretty-printed version of the expression/predicate that is evaluated |
| 317 | | pp_eval_expr(Typed) :- |
| 318 | | % nl,nl,print('SOLVING:'),nl,nested_print_bexpr(Typed),nl,nl, |
| 319 | | % get_texpr_type(Typed,Type), |
| 320 | | (preferences:get_preference(repl_unicode,true) -> |
| 321 | | translate_subst_or_bexpr_in_mode(unicode,Typed,UnicodeString), |
| 322 | | format(' ~w ~w~n',['\x21DD\',UnicodeString]) |
| 323 | | ; true). |
| 324 | | |
| 325 | | extract_type_information(b(exists(Parameters,_Typed),pred,_),predicate(exists(Parameters))) :- !. |
| 326 | | extract_type_information(b(forall(Parameters,_LHS,_RHS),pred,_),predicate(forall(Parameters))) :- !. |
| 327 | | extract_type_information(b(_,pred,_),predicate(no_outer_quantifier)) :- !. |
| 328 | | extract_type_information(b(_,T,_),expression(T)). |
| 329 | | |
| 330 | | %:- use_module(library(timeout)). |
| 331 | | %:- use_module(library(file_systems)). |
| 332 | | |
| 333 | | % |
| 334 | | % |
| 335 | | % eval_rule_file removed; now use: probcli -eval_rule_file /Users/leuschel/svn_root/NewProBPrivate/examples/B/Siemens/RuleValidation/Deploy/AssociativityXY_3_type.v /Users/leuschel/svn_root/NewProBPrivate/examples/B/Siemens/RuleValidation/MainRuleBaseFile.mch |
| 336 | | |
| 337 | | % performance benchmark: |
| 338 | | % time(eval_strings:test_parser('examples/Rules/sample.rule')). |
| 339 | | % time(eval_strings:test_parser('examples/Rules/sample2.rule')). |
| 340 | | % time(eval_strings:test_parser('examples/Rules/sudoku.rule')). |
| 341 | | :- public test_parser/1. |
| 342 | | test_parser(File) :- print(processing_rule_file(File)),nl, |
| 343 | | read_string_from_file(File,Codes),print(parsing),nl, |
| 344 | | repl_typing_scope(TypingScope), |
| 345 | | b_parse_machine_predicate_from_codes_open(exists,Codes,[],TypingScope, |
| 346 | | _Typed), |
| 347 | | print(done),nl. |
| 348 | | |
| 349 | | |
| 350 | | % ---------- |
| 351 | | % EXPRESSIONS |
| 352 | | % ---------- |
| 353 | | |
| 354 | | :- use_module(state_space,[current_state_id/1]). |
| 355 | | :- use_module(store). |
| 356 | | :- use_module(translate). |
| 357 | | :- use_module(b_interpreter). |
| 358 | | :- use_module(prob2_interface,[get_state/2]). |
| 359 | | |
| 360 | | :- meta_predicate probcli_clpfd_overflow_mnf_call1(0). |
| 361 | | :- meta_predicate probcli_clpfd_overflow_call1(0). |
| 362 | | |
| 363 | | :- dynamic last_expansion_time/1. |
| 364 | | |
| 365 | | get_cur_state_for_repl(State) :- retractall(last_expansion_time(_)), |
| 366 | | statistics(walltime,[T1,_]), |
| 367 | | get_cur_state2(State1), |
| 368 | | add_prob_deferred_set_elements_to_store(State1,State2,visible), |
| 369 | | extend_state_with_stored_lets(State2,State), |
| 370 | | statistics(walltime,[T2,_]), Delta is T2-T1, |
| 371 | | assert(last_expansion_time(Delta)). |
| 372 | | get_cur_state2(EState) :- current_state_id(CurID), get_state(CurID,EState),!. |
| 373 | | % TO DO: we could try and get only those identifiers that are really used |
| 374 | | get_cur_state2([]). % happens if no machine loaded |
| 375 | | |
| 376 | | |
| 377 | | :- use_module('kodkod/kodkod', [current_solver_is_not_incremental/0]). |
| 378 | | replace_expression_by_kodkod_if_enabled(Typed,NewExpression) :- |
| 379 | | (replace_expression_by_kodkod_if_enabled_aux(Typed,NewExpression) -> true |
| 380 | | ; NewExpression=Typed). |
| 381 | | replace_expression_by_kodkod_if_enabled_aux(Typed,NewExpression) :- |
| 382 | | % do :kodkod replacment inside set comprehensions |
| 383 | | get_texpr_expr(Typed,comprehension_set(Ids,Pred)), |
| 384 | | \+ current_solver_is_not_incremental, % otherwise we cannot get all solutions |
| 385 | | replace_kodkod_if_enabled(Ids,Pred,NewPred), % TO DO: we could pass a parameter that says we want all solutions here |
| 386 | | get_preference(kodkod_symmetry_level,Symm), |
| 387 | | ((Symm > 0 , Pred \= NewPred) |
| 388 | | -> get_texpr_ids(Ids,I), |
| 389 | | add_warning(kodkod,'KODKOD_SYMMETRY > 0, not all solutions to set comprehension may be computed: ',I) |
| 390 | | ; true), |
| 391 | | get_texpr_info(Typed,Info),get_texpr_type(Typed,Type), |
| 392 | | create_texpr(comprehension_set(Ids,NewPred),Type,Info,NewExpression). |
| 393 | | |
| 394 | | % EnumWarnings are no longer returned but thrown if problematic |
| 395 | | eval_expression(Typed,RRes) :- |
| 396 | | get_cur_state_for_repl(EState), |
| 397 | | eval_expression(EState,Typed,RRes). |
| 398 | | |
| 399 | | eval_expression(EState,Typed,RRes) :- eval_expression(EState,Typed,RRes,_PrologTerm). |
| 400 | | |
| 401 | | eval_expression(EState,Typed,RRes,NValue) :- %% print('Start Eval Expression: '),nl,flush_output, |
| 402 | | enter_new_error_scope(ScopeID,eval_expression), |
| 403 | | clear_all_errors_in_error_scope(ScopeID), |
| 404 | | replace_expression_by_kodkod_if_enabled(Typed,Typed2), |
| 405 | | set_last_expression(expr,Typed2,exception), |
| 406 | | debug_println(5,'Start Eval Expression'), |
| 407 | | (probcli_clpfd_overflow_mnf_call1(b_interpreter:b_compute_expression_nowf(Typed2,[],EState,Value)) |
| 408 | | -> true |
| 409 | | ; set_last_expression(expr,Typed2,error),fail % probably wd-error |
| 410 | | ), |
| 411 | | !, |
| 412 | | debug_println(5,'Normalising Value'), |
| 413 | | normalise_eval_value(Value,NValue), |
| 414 | | set_last_expression(expr,Typed2,NValue), |
| 415 | | debug_println(5,'Translating Value'), |
| 416 | | translate:translate_bvalue_for_expression(NValue,Typed2,Result), |
| 417 | | %get_only_critical_enum_warning(EnumWarning), |
| 418 | | start_terminal_colour([dark_gray],user_output), |
| 419 | | format(user_output,'Expression Value = ~n',[]), |
| 420 | | reset_terminal_colour(user_output), |
| 421 | | display_and_set_result(ScopeID,Result,RRes,false), |
| 422 | | display_dot_expr_result(Typed2,NValue). % TO DO: if we have a let with ID: use ID rather than result |
| 423 | | eval_expression(_,_,Cause,error) :- |
| 424 | | get_fail_error_cause(Cause), |
| 425 | | exit_error_scope(_ScopeID,_,eval_expression). |
| 426 | | |
| 427 | | |
| 428 | | :- dynamic normalising_off/0. |
| 429 | | toggle_normalising :- print('% Normalising Result Values: '), |
| 430 | | (retract(normalising_off) -> print('ON') |
| 431 | | ; assert(normalising_off),print('OFF')),nl. |
| 432 | | |
| 433 | | |
| 434 | | normalise_eval_value(Value,NValue) :- normalising_off,!, |
| 435 | | start_norm_timer(NT,NWT), |
| 436 | | NValue=Value, stop_norm_timer(NT,NWT). |
| 437 | | normalise_eval_value(Value,NValue) :- |
| 438 | | %EXPAND=limit(100000), % expand up until 100,000 elements; don't expand SYMBOLIC |
| 439 | | EXPAND=force, % don't expand definitely infinite sets + sets known larger than 20,000 |
| 440 | | debug_println(20,normalising(Value)), |
| 441 | | start_norm_timer(NT,NWT), |
| 442 | | ( store:normalise_value_for_var(eval_strings,EXPAND,Value,NValue), |
| 443 | | stop_norm_timer(NT,NWT) |
| 444 | | -> true |
| 445 | | ; stop_norm_timer(NT,NWT), |
| 446 | | print_red('Could not normalise value:'),nl, |
| 447 | | NValue=Value |
| 448 | | ). |
| 449 | | |
| 450 | | get_fail_error_cause(Cause) :- |
| 451 | | logged_error(identifier_not_found,_B,_C,_D), % print(logged_error(identifier_not_found,B,_C,_D)), |
| 452 | | %atom_codes(B,Codes), append("Cannot find identifier",_,Codes), |
| 453 | | !, |
| 454 | | Cause = 'IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST'. |
| 455 | | get_fail_error_cause('NOT-WELL-DEFINED'). |
| 456 | | |
| 457 | | get_type_error(Cause) :- logged_error(A,B,_C,_D), % print(logged_error(A,B,C,D)), |
| 458 | | A=type_expression_error, |
| 459 | | atom_codes(B,Codes), |
| 460 | | append("Unknown identifier",_,Codes),!, |
| 461 | | Cause = 'UNKNOWN IDENTIFIER(S)'. |
| 462 | | get_type_error('TYPE ERROR'). |
| 463 | | |
| 464 | | |
| 465 | | % ---------- |
| 466 | | % PREDICATES |
| 467 | | % ---------- |
| 468 | | |
| 469 | | :- use_module(kernel_waitflags). |
| 470 | | :- use_module(b_enumerate,[b_tighter_enumerate_values/2]). |
| 471 | | :- use_module(bsyntaxtree). |
| 472 | | |
| 473 | | |
| 474 | | :- volatile eval_repeat/1. |
| 475 | | :- dynamic eval_repeat/1. |
| 476 | | |
| 477 | | set_eval_repeat(X) :- format('Finding ~w first solutions for predicates~n',[X]), |
| 478 | | retractall(eval_repeat(_)),assert(eval_repeat(X)). |
| 479 | | |
| 480 | | :- use_module(succeed_max,[succeed_max_call_id/3]). %succeed_max_call_id('$setup_constants',member(_,_),1) |
| 481 | | test_bool_exists(EState, Parameters,Typed,LocalState,WF) :- eval_repeat(Nr), |
| 482 | | format_with_colour(user_output,[dark_gray],'** Finding first ~w solutions~n',[Nr]), |
| 483 | | call_residue(succeed_max_call_id(test_bool_exists,eval_strings:test_bool_exists2(EState, Parameters,Typed,LocalState,WF),Nr),Residue), |
| 484 | | print('SOLUTION = '),display_solution(Parameters,LocalState), |
| 485 | | (Residue = [] -> true ; print_red('RESIDUE = '), print_red(Residue),nl), |
| 486 | | fail. |
| 487 | | test_bool_exists(EState, Parameters,Typed,LocalState,WF) :- |
| 488 | ? | test_bool_exists2(EState, Parameters,Typed,LocalState,WF). |
| 489 | | |
| 490 | ? | test_bool_exists2(EState, Parameters,Typed,LocalState,WF) :- \+ eval_det, !, |
| 491 | | % evaluate component wise |
| 492 | ? | init_wait_flags(WF), |
| 493 | ? | b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive), |
| 494 | ? | append(LocalState,EState,State), |
| 495 | ? | b_interpreter_components:reset_unsat_component_info, |
| 496 | ? | b_interpreter_components:b_trace_test_components(Typed,State,TypedVals), |
| 497 | | \+ b_interpreter_components:unsat_component_exists. |
| 498 | | test_bool_exists2(EState, Parameters,Typed,LocalState,WF) :- |
| 499 | | init_wait_flags(WF), |
| 500 | | b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive), |
| 501 | | b_tighter_enumerate_values(TypedVals,WF), |
| 502 | | b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF). |
| 503 | | |
| 504 | | |
| 505 | | :- use_module(eventhandling,[announce_event/1]). |
| 506 | | |
| 507 | | eval_predicate(ExTyped,RRes,EnumWarning,LocalState) :- |
| 508 | | get_cur_state_for_repl(State), |
| 509 | | smt_solvers_interface:init, |
| 510 | | announce_event(start_solving), |
| 511 | | eval_predicate(State,ExTyped,RRes,EnumWarning,LocalState), |
| 512 | | announce_event(end_solving). |
| 513 | | |
| 514 | | :- use_module('kodkod/kodkod', [apply_kodkod/3]). |
| 515 | | replace_kodkod_if_enabled(Parameters,Typed,NewPredicate) :- |
| 516 | | b_get_machine_constants(Constants), |
| 517 | | b_get_machine_variables(Variables), |
| 518 | | append([Parameters,Variables,Constants],Identifiers), |
| 519 | | apply_kodkod(Identifiers,Typed,NewPredicate). |
| 520 | | |
| 521 | | eval_predicate(State,Typed,RRes,EnumWarning,LocalState) :- |
| 522 | | %b_ast_cleanup:predicate_level_optimizations(Typed,Typed2), % detect set partitions, ... no longer necessary ! as already called in b_ast_cleanup now |
| 523 | | eval_predicate_aux(State,Typed,RRes,EnumWarning,LocalState). |
| 524 | | eval_predicate_aux(State,ExTyped,RRes,EnumWarning,LocalState) :- |
| 525 | | %ExTyped=b(exists(Parameters,Typed),pred,_I), |
| 526 | | is_existential_quantifier(ExTyped,Parameters,Typed), |
| 527 | | !, |
| 528 | | %print('Existentially Quantified Predicate is '),flush_output, |
| 529 | | replace_kodkod_if_enabled(Parameters,Typed,NTyped), |
| 530 | | enter_new_error_scope(ScopeID,eval_predicate_exists), clear_all_errors_in_error_scope(ScopeID), |
| 531 | | set_last_expression(pred,ExTyped,exception), % in case an exception occurs |
| 532 | | (observe_parameters(true) -> observe_parameters(Parameters,LocalState) ; true), |
| 533 | | (probcli_clpfd_overflow_call1((test_bool_exists(State, Parameters,NTyped,LocalState,WF), |
| 534 | | eval_ground_wf(WF))) |
| 535 | | -> get_only_critical_enum_warning(EnumWarning), |
| 536 | | (eval_det -> Res = 'POSSIBLY TRUE' ; Res = 'TRUE'), |
| 537 | | set_last_expression(pred,ExTyped,true) |
| 538 | | ; get_enum_warning(EnumWarning), |
| 539 | | % The result has to be ground for the eclipse interface to work as intended. |
| 540 | | % Hence, we need to bind the LocalState (?) |
| 541 | | LocalState = [], |
| 542 | | Res = 'FALSE', set_last_expression(pred,ExTyped,false)), |
| 543 | | (eval_det -> portray_waitflags_and_frozen_state_info(WF,(LocalState,State)) ; true), |
| 544 | | print('Existentially Quantified Predicate over '), print_parameters(Parameters), |
| 545 | | print(' is '),display_and_set_result(ScopeID,Res,RRes,EnumWarning), |
| 546 | | (Res='FALSE' -> true |
| 547 | | ; print('Solution: '),nl, display_solution(Parameters,LocalState) |
| 548 | | ). |
| 549 | | eval_predicate_aux(State, ExTyped,RRes,EnumWarning,LocalState) :- |
| 550 | | ExTyped=b(forall(Parameters,TypedLHS,TypedRHS),pred,_I),!, |
| 551 | | %print('Universally Quantified Predicate is '),flush_output, |
| 552 | | enter_new_error_scope(ScopeID,eval_predicate_forall), clear_all_errors_in_error_scope(ScopeID), |
| 553 | | safe_create_texpr(negation(TypedRHS),pred,[try_smt],NegRHS), |
| 554 | | conjunct_predicates([TypedLHS,NegRHS],Conjunction), |
| 555 | | replace_kodkod_if_enabled(Parameters,Conjunction,NConjunction), |
| 556 | | %translate:print_bexpr(Conjunction), |
| 557 | | set_last_expression(pred,ExTyped,exception), % in case an exception occurs |
| 558 | | (probcli_clpfd_overflow_call1((test_bool_exists(State, Parameters,NConjunction,LocalState,WF), |
| 559 | | eval_ground_wf(WF))) |
| 560 | | -> get_only_critical_enum_warning(EnumWarning), |
| 561 | | (eval_det -> Res = 'POSSIBLY TRUE' ; Res = 'FALSE'), |
| 562 | | set_last_expression(pred,ExTyped,false) |
| 563 | | ; get_enum_warning(EnumWarning), |
| 564 | | % The result has to be ground for the eclipse interface to work as intended. |
| 565 | | % Hence, we need to bind the LocalState (?) |
| 566 | | LocalState = [], |
| 567 | | Res = 'TRUE', set_last_expression(pred,ExTyped,true)), |
| 568 | | print('Universally Quantified Predicate over '), print_parameters(Parameters), |
| 569 | | print(' is '), display_and_set_result(ScopeID,Res,RRes,EnumWarning), |
| 570 | | (Res='TRUE' -> true |
| 571 | | ; print('Counter example: '),nl, display_solution(Parameters,LocalState) |
| 572 | | ). |
| 573 | | eval_predicate_aux(State, Typed,RRes,EnumWarning,[]) :- |
| 574 | | enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID), |
| 575 | | debug_println(20,test_boolean_expression(Typed)), |
| 576 | | replace_kodkod_if_enabled([],Typed,NTyped), |
| 577 | | set_last_expression(pred,NTyped,exception), % in case an exception occurs |
| 578 | | % TO DO: the next does not decompose into components !?; either call solve_predicate if State=[] or call b_trace_test_components inside b_test_boolean_expression_wf |
| 579 | | (probcli_clpfd_overflow_call1(b_interpreter:b_test_boolean_expression_wf(NTyped,[],State)) |
| 580 | | -> Res='TRUE',set_last_expression(pred,Typed,true), |
| 581 | | get_only_critical_enum_warning(EnumWarning) |
| 582 | | ; Res='FALSE',set_last_expression(pred,Typed,false), |
| 583 | | get_enum_warning(EnumWarning) |
| 584 | | ), |
| 585 | | print('Predicate is '),display_and_set_result(ScopeID,Res,RRes,EnumWarning). |
| 586 | | |
| 587 | | get_enum_warning(EnumWarning) :- |
| 588 | | (event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical)) |
| 589 | | -> EnumWarning=true %,print(' ** ENUM WARNING ** ') |
| 590 | | ; EnumWarning=false). |
| 591 | | get_only_critical_enum_warning(EnumWarning) :- EnumWarning=false. |
| 592 | | % we no longer distinguish between critical & non-critical; also assuming_finite_closure now fails (renamed to checking_finite_closure) |
| 593 | | % Enumeration warning means that not all cases have been looked at, but if a result is true then it is guaranteed to be true |
| 594 | | |
| 595 | | % ((event_occurred_in_error_scope(enumeration_warning(_,_,_,_,Critical)), Critical \= non_critical) |
| 596 | | % -> EnumWarning=true %,print(' ** ENUM WARNING ** ') |
| 597 | | % ; EnumWarning=false). |
| 598 | | display_and_set_result(ScopeID,Res,RRes,EnumWarning) :- |
| 599 | | %error_manager:print_error_scopes, |
| 600 | | exit_error_scope(ScopeID,ErrOcc,display_and_set_result), |
| 601 | | ErrOcc=true, % TO DO: check which kind of error occured: could be CLPFD overflow |
| 602 | | !, |
| 603 | | show_error_pos, |
| 604 | | start_terminal_colour([red,bold],user_output), |
| 605 | | format(user_output,'POSSIBLY NOT-WELL-DEFINED (~w)',[Res]), |
| 606 | | reset_terminal_colour(user_output), |
| 607 | | print_enum_warning(EnumWarning), nl, |
| 608 | | get_fail_error_cause(RRes). % RRes = 'NOT-WELL-DEFINED' |
| 609 | | display_and_set_result(_,Res,RRes,EnumWarning) :- |
| 610 | | print_result(Res,EnumWarning), nl, |
| 611 | | (EnumWarning=false -> RRes=Res |
| 612 | | ; Res = 'TRUE' -> RRes=Res % enumeration warning does not matter when solution found |
| 613 | | ; RRes= 'UNKNOWN'). |
| 614 | | print_result('FALSE',false) :- !, |
| 615 | | start_terminal_colour(light_red,user_output), |
| 616 | | write('FALSE'),reset_terminal_colour(user_output). |
| 617 | | print_result('TRUE',false) :- !, |
| 618 | | start_terminal_colour(green,user_output), |
| 619 | | write('TRUE'),reset_terminal_colour(user_output). |
| 620 | | print_result(Res,false) :- !, write(Res). |
| 621 | | print_result(Res,_) :- |
| 622 | | start_terminal_colour([red,bold],user_output), |
| 623 | | format(user_output,'UNKNOWN [~w with ** ENUMERATION WARNING **]',Res), |
| 624 | | reset_terminal_colour(user_output). |
| 625 | | |
| 626 | | |
| 627 | | :- use_module(tools_printing,[print_red/1,print_green/1,format_with_colour/4]). |
| 628 | | print_enum_warning(false) :- !. |
| 629 | | print_enum_warning(_) :- print_red(' [** ENUMERATION WARNING **]'). |
| 630 | | |
| 631 | | :- use_module(graph_canon,[print_cstate_graph/2]). |
| 632 | | display_solution(Parameters,LocalState) :- |
| 633 | | set_last_solution(Parameters,LocalState), |
| 634 | | (eval_det |
| 635 | | -> % copy_term(LocalState,CLS), % avoid triggering co-routines via numbervars |
| 636 | | % tools_meta:safe_numbervars(CLS,0,_), |
| 637 | | print_solution_with_type(Parameters,LocalState) |
| 638 | | ; normalise_store(LocalState,NState) |
| 639 | | -> %translate:print_bstate(NState) |
| 640 | | print_solution_with_type(Parameters,NState), |
| 641 | | %visualize_graph:tcltk_print_state_as_graph_for_dot(NState,'~/Desktop/out.dot') |
| 642 | | display_dot_solution(NState) |
| 643 | | ; print_red('Could not normalise value(s):'),nl,translate:print_bstate(LocalState) |
| 644 | | ),nl. |
| 645 | | |
| 646 | | display_dot_expr_result(Expr,Value) :- |
| 647 | | (eval_dot_file(File) |
| 648 | | -> get_dot_expr_state(Expr,Value,NState,[]), |
| 649 | | debug_println(9,writing_dot_file(File)), |
| 650 | | print_cstate_graph(NState,File) |
| 651 | | ; true). |
| 652 | | |
| 653 | | % try and decompose an expression value into subvalues for better dot rendering |
| 654 | | get_dot_expr_state(b(couple(A,B),_,_),(VA,VB)) --> !, |
| 655 | | get_dot_expr_state(A,VA), |
| 656 | | get_dot_expr_state(B,VB). |
| 657 | | get_dot_expr_state(b(identifier(ID),_,_),Val) --> !, [bind(ID,Val)]. |
| 658 | | get_dot_expr_state(_,Val) --> [bind(result,Val)]. |
| 659 | | |
| 660 | | % display_dot_solution([bind(result,NValue)]). |
| 661 | | display_dot_solution(NState) :- |
| 662 | | (eval_dot_file(File) |
| 663 | | -> debug_println(9,writing_dot_file(File)), |
| 664 | | graph_canon:print_cstate_graph(NState,File) ; true). |
| 665 | | |
| 666 | | :- dynamic last_solution/2. |
| 667 | | set_last_solution(Parameters,LocalState) :- |
| 668 | | retractall(last_solution(_,_)), |
| 669 | | assert(last_solution(Parameters,LocalState)). |
| 670 | | |
| 671 | | % small utility to extract last result; if we had a predicate with just one existential variable extract its value: |
| 672 | | get_last_result_value(Parameter,Type,Value) :- |
| 673 | | get_last_predicate_value_for_typed_id(Parameter,[],T,V), % only allow single parameter; otherwise confusion may exist |
| 674 | | !,Value=V, Type=T. |
| 675 | | get_last_result_value(Expr,Type,Value) :- get_last_expr_type_and_value(Expr,Type,Value). |
| 676 | | |
| 677 | | convert_result(T,V,Type,Value) :- |
| 678 | | (convert_aux(T,V,Type,Value) -> true ; Type=T,Value=V). |
| 679 | | convert_aux(pred,true,boolean,pred_true). |
| 680 | | convert_aux(pred,false,boolean,pred_false). |
| 681 | | |
| 682 | | % try and extract a value for a give parameter from last solution for a predicate |
| 683 | | get_last_predicate_value_for_id(ID,Type,Val) :- |
| 684 | | get_texpr_id(Parameter,ID),get_last_predicate_value_for_typed_id(Parameter,_,Type,Val). |
| 685 | | get_last_predicate_value_for_typed_id(Parameter,Rest,Type,Value) :- |
| 686 | | last_expression(pred,_,true), |
| 687 | | last_solution(Parameters,LocalState), |
| 688 | | select(Parameter,Parameters,Rest), |
| 689 | | get_texpr_id(Parameter,ParameterID), |
| 690 | | get_texpr_type(Parameter,Type), |
| 691 | | member(bind(ParameterID,Value),LocalState). |
| 692 | | |
| 693 | | :- volatile eval_dot_file/1, observe_parameters/1. |
| 694 | | :- dynamic eval_dot_file/1, observe_parameters/1. |
| 695 | | observe_parameters(false). |
| 696 | | |
| 697 | | toggle_observe_evaluation :- |
| 698 | | (observe_parameters(false) |
| 699 | | -> print('Observing parameters'),nl, |
| 700 | | set_observe_evaluation(true) |
| 701 | | ; print('Observing OFF'),nl, |
| 702 | | set_observe_evaluation(false)). |
| 703 | | set_observe_evaluation(T) :- retractall(observe_parameters(_)), assert(observe_parameters(T)). |
| 704 | | set_eval_dot_file(F) :- unset_eval_dot_file, |
| 705 | | debug_println(5,setting_eval_dot_file(F)), |
| 706 | | assert(eval_dot_file(F)). |
| 707 | | unset_eval_dot_file :- retractall(eval_dot_file(_)). |
| 708 | | |
| 709 | | % print solution using type information |
| 710 | | print_solution_with_type([],[]). |
| 711 | | print_solution_with_type([Identifier|TT],[bind(Varname,Value)|VT]) :- |
| 712 | | def_get_texpr_id(Identifier,Varname), !, |
| 713 | | translate:translate_bvalue_for_expression(Value,Identifier,Result), |
| 714 | | print_binding(Varname,Result), |
| 715 | | (TT=[] -> nl ; print(' &'),nl,print_solution_with_type(TT,VT)). |
| 716 | | print_solution_with_type(unknown,[bind(Varname,Value)|VT]) :- !, |
| 717 | | translate:translate_bvalue_with_limit(Value,100,Result), |
| 718 | | print_binding(Varname,Result), |
| 719 | | (VT=[] -> nl ; print(' &'),nl,print_solution_with_type(unknown,VT)). |
| 720 | | print_solution_with_type(unknown,[]) :- !. |
| 721 | | print_solution_with_type(P,State) :- |
| 722 | | add_internal_error('Illegal call: ', print_solution_with_type(P,State)). |
| 723 | | |
| 724 | | print_binding(Varname,Result) :- |
| 725 | | print(' '),print(Varname), print(' = '), |
| 726 | | print(Result). |
| 727 | | |
| 728 | | :- use_module(state_space,[current_state_id/1]). |
| 729 | | :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate_in_state/5]). |
| 730 | | :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/4]). |
| 731 | | solve_using_smt_solver(Solver,PredCodes,OuterQuantifier,Res,LocalState,TypeInfo) :- |
| 732 | | repl_parse_predicate(PredCodes,OuterQuantifier,ExTyped,TypeInfo), % TO DO: make lets,... available |
| 733 | | (is_existential_quantifier(ExTyped,Parameters,Typed) -> true; Parameters=[],ExTyped = Typed), |
| 734 | | start_timer(T1,WT1), |
| 735 | | ((current_state_id(SID) |
| 736 | | -> smt_solve_predicate_in_state(SID,Solver,Typed,LocalState,Result) |
| 737 | | ; smt_solve_predicate(Solver,Typed,LocalState,Result)) |
| 738 | | -> stop_timer(T1,WT1), |
| 739 | | debug_println(9,smt_result(Solver,Result)), |
| 740 | | print('PREDICATE is '),display_smt_result(Result,Parameters,ExTyped,Res) |
| 741 | | ; stop_timer('FAILED',T1,WT1), Res = 'FAILED', |
| 742 | | set_last_expression(pred,ExTyped,failed), |
| 743 | | LocalState=[]). |
| 744 | | |
| 745 | | display_smt_result(solution(Bindings),Parameters,ExTyped,'TRUE') :- !, |
| 746 | | set_last_expression(pred,ExTyped,true), |
| 747 | | print_green('TRUE'),nl, |
| 748 | | findall(bind(ID,Val),member(binding(ID,Val,_),Bindings),LocalState), |
| 749 | | set_last_solution(Parameters,LocalState), |
| 750 | | (Bindings=[] -> true |
| 751 | | ; print('Solution: '),nl, |
| 752 | | findall(1,(member(binding(ID2,_,S2),Bindings),print_binding(ID2,S2),nl),_)). |
| 753 | | display_smt_result(contradiction_found,_,ExTyped,'FALSE') :- !, |
| 754 | | format_with_colour(user_output,[light_red],'FALSE',[]),nl, |
| 755 | | set_last_expression(pred,ExTyped,false). |
| 756 | | display_smt_result(no_solution_found(cvc4_unknown),_,ExTyped,'UNKNOWN') :- !, |
| 757 | | print_red('UNKNOWN'),nl, |
| 758 | | set_last_expression(pred,ExTyped,unknown). |
| 759 | | display_smt_result(no_solution_found(Reason),_,ExTyped,'UNKNOWN') :- !, |
| 760 | | print_red('UNKNOWN: '),print(Reason),nl, |
| 761 | | set_last_expression(pred,ExTyped,unknown). |
| 762 | | display_smt_result(Other,_,ExTyped,'UNKNOWN') :- !, |
| 763 | | print_red('*** UNKNOWN SMT RESULT ***: '),print(Other),nl, |
| 764 | | set_last_expression(pred,ExTyped,unknown). |
| 765 | | |
| 766 | | |
| 767 | | :- use_module(bsyntaxtree,[def_get_texpr_id/2]). |
| 768 | | print_parameters([]). |
| 769 | | print_parameters([TID]) :- !, print_id(TID). |
| 770 | | print_parameters([TID|T]) :- print_id(TID), print(','), print_parameters(T). |
| 771 | | print_id(TID) :- def_get_texpr_id(TID,ID), print(ID). |
| 772 | | |
| 773 | | |
| 774 | | |
| 775 | | %indent(X) :- X<1,!. |
| 776 | | %indent(X) :- print('+ '), X1 is X-1, indent(X1). |
| 777 | | |
| 778 | | % TOOLS |
| 779 | | % ----- |
| 780 | | |
| 781 | | |
| 782 | | % detecting existential quantifiers: so that the REPL can print the solutions for them |
| 783 | | % an example is the following test: |
| 784 | | % probcli -eval "#active,ready,waiting,rr.(active : POW(PID) & ready : POW(PID) & waiting : POW(PID) & active <: PID & ready <: PID & waiting <: PID & (ready /\ waiting = {}) & (active /\ (ready \/ waiting)) = {} & card(active) <= 1 & rr : waiting & active = {})" ../prob_examples/public_examples/B/Benchmarks/scheduler.mch |
| 785 | | % alternative would be to avoid optimizer to run at top-level |
| 786 | | is_existential_quantifier(b(EXISTS,pred,_),FullParameters,FullTypedBody) :- |
| 787 | | is_existential_aux(EXISTS,Parameters,TypedBody), |
| 788 | | (is_existential_quantifier(TypedBody,InnerPar,InnerBody) % recursively look inside |
| 789 | | -> append(Parameters,InnerPar,FullParameters), |
| 790 | | FullTypedBody = InnerBody |
| 791 | | ; FullTypedBody = TypedBody, FullParameters=Parameters). |
| 792 | | is_existential_aux(exists(Parameters,TypedBody),Parameters,TypedBody). |
| 793 | | is_existential_aux(let_predicate(Parameters,AssignmentExprs,Pred),Parameters,TypedBody) :- |
| 794 | | generate_let_equality_pred(Parameters,AssignmentExprs,EqPreds), |
| 795 | | append(EqPreds,[Pred],AllPreds), |
| 796 | | conjunct_predicates(AllPreds,TypedBody). |
| 797 | | is_existential_aux(conjunct(A,B),Parameters,TypedBody) :- |
| 798 | | is_existential_quantifier(A,Parameters,TAA), |
| 799 | | !, % then do not look if B is existential quantifier below |
| 800 | | b_ast_cleanup:get_sorted_ids(Parameters,SIds), |
| 801 | | b_ast_cleanup:not_occurs_in_predicate(SIds,B), |
| 802 | | \+ is_existential_quantifier(B,_,_), |
| 803 | | conjunct_predicates([TAA,B],TypedBody),!. |
| 804 | | is_existential_aux(conjunct(A,B),Parameters,TypedBody) :- |
| 805 | | is_existential_quantifier(B,Parameters,TBB), |
| 806 | | b_ast_cleanup:get_sorted_ids(Parameters,SIds), |
| 807 | | b_ast_cleanup:not_occurs_in_predicate(SIds,A), |
| 808 | | conjunct_predicates([A,TBB],TypedBody). |
| 809 | | % TO DO: treat lazy_let_pred |
| 810 | | |
| 811 | | generate_let_equality_pred([],[],[]). |
| 812 | | generate_let_equality_pred([ID|T],[Exp|TE],[EqPred|TR]) :- |
| 813 | | EqPred = b(equal(ID,Exp),pred,[]), % TO DO: update WD info |
| 814 | | generate_let_equality_pred(T,TE,TR). |
| 815 | | |
| 816 | | |
| 817 | | |
| 818 | | :- use_module(clpfd_interface,[clpfd_overflow_error_message/0]). |
| 819 | | |
| 820 | | |
| 821 | | :- use_module(tools_meta,[call_residue/2]). |
| 822 | | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). |
| 823 | | probcli_clpfd_overflow_mnf_call1(Call) :- |
| 824 | | call_residue(probcli_clpfd_overflow_mnf_call2(Call),Residue), |
| 825 | | (Residue = [] -> true |
| 826 | | ; add_internal_error('Call residue: ',Residue)). |
| 827 | | probcli_clpfd_overflow_mnf_call2(Call) :- start_timer(T1,WT1), |
| 828 | | catch_clpfd_overflow_call2( |
| 829 | | (Call->stop_timer(T1,WT1) |
| 830 | | ; stop_timer(T1,WT1),show_error_pos, |
| 831 | | print_red('Expression not well-defined !'),nl, |
| 832 | | fail), |
| 833 | | ( stop_timer(T1,WT1),clpfd_overflow_error_message, fail)). |
| 834 | | |
| 835 | | |
| 836 | | |
| 837 | | probcli_clpfd_overflow_call1(Call) :- |
| 838 | | call_residue(probcli_clpfd_overflow_call2(Call),Residue), |
| 839 | | (Residue = [] -> true |
| 840 | | ; add_internal_error('Call residue: ',Residue)). |
| 841 | | probcli_clpfd_overflow_call2(Call) :- start_timer(T1,WT1), |
| 842 | | catch_clpfd_overflow_call2( |
| 843 | | (Call -> stop_timer(T1,WT1) ; stop_timer(T1,WT1),fail), |
| 844 | | ( stop_timer(T1,WT1),clpfd_interface:clpfd_overflow_error_message, fail)). |
| 845 | | |
| 846 | | :- volatile last_eval_time/2. |
| 847 | | :- dynamic last_eval_time/2. |
| 848 | | start_timer(T1,WT1) :- retractall(last_eval_time(_,_)), retractall(last_norm_time(_,_)), |
| 849 | | statistics(runtime,[T1,_]), |
| 850 | | statistics(walltime,[WT1,_]). |
| 851 | | stop_timer(T1,WT1) :- |
| 852 | | statistics(runtime,[T2,_]), TotTime is T2-T1, |
| 853 | | statistics(walltime,[WT2,_]), WTotTime is WT2-WT1, |
| 854 | | retractall(last_eval_time(_,_)), |
| 855 | | debug_println(20,stopped_timer(TotTime,T2,T1)), |
| 856 | | assert(last_eval_time(TotTime,WTotTime)). |
| 857 | | stop_timer(Msg,T1,WT1) :- |
| 858 | | statistics(runtime,[T2,_]), TotTime is T2-T1, |
| 859 | | statistics(walltime,[WT2,_]), WTotTime is WT2-WT1, |
| 860 | | format_with_colour(user_output,[dark_gray],'~w ~w ms (~w ms walltime).~n',[Msg,TotTime,WTotTime]). |
| 861 | | |
| 862 | | :- volatile last_norm_time/2. |
| 863 | | :- dynamic last_norm_time/2. |
| 864 | | start_norm_timer(T1,WT1) :- retractall(last_norm_time(_,_)), |
| 865 | | statistics(runtime,[T1,_]), |
| 866 | | statistics(walltime,[WT1,_]). |
| 867 | | stop_norm_timer(T1,WT1) :- |
| 868 | | statistics(runtime,[T2,_]), TotTime is T2-T1, |
| 869 | | statistics(walltime,[WT2,_]), WTotTime is WT2-WT1, |
| 870 | | retractall(last_norm_time(_,_)), |
| 871 | | debug_println(20,stopped_norm_timer(TotTime,T2,T1)), |
| 872 | | assert(last_norm_time(TotTime,WTotTime)). |
| 873 | | |
| 874 | | |
| 875 | | :- volatile eval_det/0. |
| 876 | | :- dynamic eval_det/0. |
| 877 | | toggle_eval_det :- |
| 878 | | (retract(eval_det) -> print('% Going back to full enumeration') |
| 879 | | ; assert(eval_det), |
| 880 | | print('% Going to deterministic mode (for existentially quantified formulas)')),nl. |
| 881 | | |
| 882 | | set_eval_det :- eval_det -> true ; assert(eval_det). |
| 883 | | unset_eval_det :- retractall(eval_det). |
| 884 | | |
| 885 | | eval_ground_wf(WF) :- (eval_det -> ground_det_wait_flag(WF) ; ground_wait_flags(WF)). |
| 886 | | |
| 887 | | |
| 888 | | |
| 889 | | |
| 890 | | |
| 891 | | show_error_pos :- |
| 892 | | findall(error_pos(Line,Col,EndLine,EndCol),check_error_span_file_linecol(_Src,_File,Line,Col,EndLine,EndCol),Errs), |
| 893 | | !, |
| 894 | | show_error_pos(Errs,-100). |
| 895 | | |
| 896 | | :- use_module(tools_printing,[start_terminal_colour/2, reset_terminal_colour/1]). |
| 897 | | show_line(Line,FromCol,ToCol) :- % highlight if possible FromCol ToCol, Columns start at 0, ToCol is not included ?! |
| 898 | | % TO DO: handle multiple errors on line |
| 899 | | (current_codes(E),get_line(E,Line,ErrLine) |
| 900 | | -> append(ErrLine,[32],Errline2), % add one whitespace at end |
| 901 | | prefix_length(Errline2,Prefix,FromCol), |
| 902 | | format(user_output,'~n### ~s',[Prefix]), |
| 903 | | Len is ToCol - FromCol, |
| 904 | | sublist(Errline2,ErrStr,FromCol,Len,_), |
| 905 | | % start_terminal_colour([red_background,white,bold],user_output), |
| 906 | | start_terminal_colour([red,underline,bold],user_output), |
| 907 | | format(user_output,'~s',[ErrStr]), % Print Error Part in RED |
| 908 | | reset_terminal_colour(user_output), |
| 909 | | sublist(Errline2,Suffix,ToCol,_,0), |
| 910 | | format(user_output,'~s~n',[Suffix]) |
| 911 | | ; true). |
| 912 | | show_line(Line) :- |
| 913 | | (current_codes(E),get_line(E,Line,ErrLine) |
| 914 | | -> format('~n### ~s~n',[ErrLine]) |
| 915 | | ; true). |
| 916 | | show_error_pos([],_). |
| 917 | | show_error_pos([error_pos(Line,Col,EL,EC)|T],LastLine) :- %print(pos(Line,Col,EL,EC)),nl, |
| 918 | | (LastLine==Line -> true ; EL==Line,show_line(Line,Col,EC) -> true ; show_line(Line)), |
| 919 | | print('### '), indent_ws(Col), |
| 920 | | (EL=Line,EC>Col -> Len is EC-Col ; Len=1), |
| 921 | | underline(Len),nl, |
| 922 | | (Line>1 -> print('### Line: '), print(Line), |
| 923 | | print(' Column: '), print(Col),nl |
| 924 | | ; true), |
| 925 | | show_error_pos(T,Line). |
| 926 | | |
| 927 | | indent_ws(X) :- X<1,!. |
| 928 | | indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1). |
| 929 | | underline(0) :- !. |
| 930 | | underline(N) :- N>0, print('^'), N1 is N-1, underline(N1). |
| 931 | | |
| 932 | | get_line(_,Nr,R) :- Nr<1,!,R=[]. |
| 933 | | get_line([],_,R) :- !, R=[]. |
| 934 | | get_line(Codes,Nr,Res) :- is_newline(Codes,T),!, N1 is Nr-1, get_line(T,N1,Res). |
| 935 | | get_line([H|T],1,Res) :- !, Res=[H|RT], get_line(T,1,RT). |
| 936 | | get_line([_H|T],Nr,Res) :- get_line(T,Nr,Res). |
| 937 | | |
| 938 | | is_newline([10,13|T],T). |
| 939 | | is_newline([10|T],T). |
| 940 | | is_newline([13|T],T). |
| 941 | | |
| 942 | | %%%%% to show error position in Tcl/Tk console %%%%% |
| 943 | | get_error_positions(EPos) :- |
| 944 | | findall(error_pos(Line,Col,EndLine,EndCol),check_error_span_file_linecol(_Src,_File,Line,Col,EndLine,EndCol),Errs),!, |
| 945 | | get_error_position_string_l(Errs,EPos). |
| 946 | | |
| 947 | | get_error_position_string_l(List,EPos) :- |
| 948 | | maplist(get_error_position,List,StringList), |
| 949 | | haskell_csp:convert_string_list_to_string(StringList,EPos). |
| 950 | | |
| 951 | | get_error_position(error_pos(Line,Col,EL,EC),String) :- |
| 952 | | ((current_codes(E),get_line(E,Line,ErrLine)) |
| 953 | | -> atom_codes(N,ErrLine), |
| 954 | | atom_concat('### ',N, FirstLineAtom), |
| 955 | | atom_concat(FirstLineAtom,';',FirstLineAtom1) |
| 956 | | ; FirstLineAtom1 = '### ;'), |
| 957 | | get_ident_ws(Col,'',WS), |
| 958 | | (EL=Line,EC>Col -> Len is EC-Col ; Len=1), |
| 959 | | get_underlines(Len,'',Underlines), |
| 960 | | atom_concat('### ',WS,SecondLineAtom), |
| 961 | | atom_concat(SecondLineAtom,Underlines,SecondLineAtom1), |
| 962 | | atom_concat(SecondLineAtom1,';',SecondLineAtom2), |
| 963 | | atom_concat(FirstLineAtom1,SecondLineAtom2,String). |
| 964 | | |
| 965 | | get_ident_ws(X,WS,WS) :- |
| 966 | | X<1,!. |
| 967 | | get_ident_ws(X,WS,Res) :- |
| 968 | | atom_concat(WS,' ',WS1), |
| 969 | | X1 is X-1, |
| 970 | | get_ident_ws(X1,WS1,Res). |
| 971 | | |
| 972 | | get_underlines(0,U,U) :- !. |
| 973 | | get_underlines(X,U,Res) :- |
| 974 | | X>0, |
| 975 | | atom_concat(U,'^',U1), |
| 976 | | X1 is X-1, |
| 977 | | get_underlines(X1,U1,Res). |
| 978 | | |
| 979 | | :- volatile last_expression/3. |
| 980 | | :- dynamic last_expression/3. |
| 981 | | set_last_expression(Type,Expr,Value) :- retractall(last_expression(_,_,_)), |
| 982 | | assert(last_expression(Type,Expr,Value)). |
| 983 | | |
| 984 | | last_expression_type(Type) :- last_expression(Type,_,_). |
| 985 | | |
| 986 | | :- use_module(bsyntaxtree,[get_texpr_type/2]). |
| 987 | | |
| 988 | | print_last_info :- \+ last_expression(_,_Expr,_Value),!, |
| 989 | | print_red('Please evaluate an expression or predicate first.'),nl. |
| 990 | | print_last_info :- last_expression(Type,Expr,_Value), |
| 991 | | % for insertion into unit tests |
| 992 | | print('% Type: '), print_quoted(Type), |
| 993 | | (Type=expr,get_texpr_type(Expr,ET),pretty_type(ET,PrettyType) |
| 994 | | -> print(' : '), print(PrettyType), |
| 995 | | print(' [Card='), |
| 996 | | (max_cardinality(ET,Card) -> print(Card) ; print('??')), print(']') |
| 997 | | ; true),nl, |
| 998 | | |
| 999 | | print('% Eval Time: '), |
| 1000 | | (last_eval_time(Time,WTime) |
| 1001 | | -> format('~w ms (~w ms walltime)',[Time,WTime]), |
| 1002 | | (last_norm_time(NTime,NWTime) |
| 1003 | | -> format(' + Normalisation: ~w ms (~w ms walltime)',[NTime,NWTime]) |
| 1004 | | ; true), |
| 1005 | | (last_expansion_time(EWT) -> format(' + State expansion: ~w ms walltime',[EWT]) ; true) |
| 1006 | | ; print_red('*UNKNOWN*') |
| 1007 | | ),nl. |
| 1008 | | |
| 1009 | | |
| 1010 | | print_last_value :- \+ last_expression(_,_Expr,_Value),!, |
| 1011 | | print_red('Please evaluate an expression or predicate first.'),nl. |
| 1012 | | print_last_value :- last_expression(_Type,_Expr,Value), |
| 1013 | | print('Last Expression Value = '),nl, |
| 1014 | | translate:print_bvalue(Value),nl. |
| 1015 | | |
| 1016 | | print_last_expression :- \+ last_expression(_,_Expr,_Value),!, |
| 1017 | | print_red('Please evaluate an expression or predicate first.'),nl. |
| 1018 | | print_last_expression :- last_expression(_Type,Expr,Value), |
| 1019 | | print_last_info, |
| 1020 | | print('% '), translate:print_bexpr(Expr),nl, |
| 1021 | | (Value = false -> print_quoted(must_fail_det(1,"",Expr)),print('.'),nl |
| 1022 | | ; print_quoted(Expr),nl, |
| 1023 | | print('% = '),print_quoted(Value),nl). |
| 1024 | | |
| 1025 | | indent_print_last_expression :- \+ last_expression(_,_Expr,_Value),!, |
| 1026 | | print_red('Please evaluate an expression or predicate first.'),nl. |
| 1027 | | indent_print_last_expression :- last_expression(_Type,Expr,_Value), |
| 1028 | | nested_print_bexpr(Expr). |
| 1029 | | |
| 1030 | | :- use_module(unsat_cores,[unsat_core/2]). |
| 1031 | | unsat_core_last_expression :- \+ last_expression(pred,_Expr,_Value),!, |
| 1032 | | print_red('Please evaluate a predicate first.'),nl. |
| 1033 | | unsat_core_last_expression :- \+ last_expression(pred,_Expr,false),!, |
| 1034 | | print('The UNSAT CORE can only be computed for false predicates.'),nl. |
| 1035 | | unsat_core_last_expression :- last_expression(pred,Expr,_), |
| 1036 | | print('% COMPUTING UNSAT CORE: '), translate:print_bexpr(Expr),nl, |
| 1037 | | % maybe strip top-level existential quantifier |
| 1038 | | start_timer(T1,W1), |
| 1039 | | unsat_core(Expr,Core), |
| 1040 | | stop_timer('% Time to compute core: ',T1,W1), |
| 1041 | | print('% UNSAT CORE: '), nl, |
| 1042 | | translate:nested_print_bexpr_as_classicalb(Core), |
| 1043 | | print('% ----------'),nl. |
| 1044 | | |
| 1045 | | |
| 1046 | | :- use_module(library(system)). |
| 1047 | | add_last_expression_to_unit_tests :- \+ last_expression(_,_Expr,_Value),!, |
| 1048 | | print_red('Please evaluate an expression or predicate first.'),nl. |
| 1049 | | add_last_expression_to_unit_tests :- last_expression(Type,Expr,Value), |
| 1050 | | open_unit_test_file(S), !, write(S,' & '), nl(S), write(S,' ( '), |
| 1051 | | (print_unit_test_assertion(Type,Expr,Value,S) -> true ; print('PRINTING FAILED'),nl), |
| 1052 | | write(S,' ) '), datime(datime(Yr,Mon,Day,Hr,Min,_Sec)), |
| 1053 | | format(S,'/* ~w/~w/~w ~w:~w */',[Day,Mon,Yr,Hr,Min]), |
| 1054 | | nl(S), close(S). |
| 1055 | | add_last_expression_to_unit_tests :- print('Could not save expression to unit test file ($PROB_EX_DIR/B/Laws/REPL_UNIT_TESTS.def).'),nl. |
| 1056 | | |
| 1057 | | open_unit_test_file(S) :- |
| 1058 | | environ('PROB_EX_DIR',Dir), |
| 1059 | | atom_concat(Dir,'/B/Laws/REPL_UNIT_TESTS.def',REPLFILE), |
| 1060 | | print(opening(REPLFILE)),nl, |
| 1061 | | my_open(REPLFILE,append,S). |
| 1062 | | |
| 1063 | | |
| 1064 | | my_open(File,Mode,S) :- on_exception(error(existence_error(_,_),E), |
| 1065 | | open(File,Mode,S), add_error_fail(my_open,'File does not exist: ',File:E)). |
| 1066 | | |
| 1067 | | :- use_module(bsyntaxtree,[create_texpr/4, safe_create_texpr/4]). |
| 1068 | | print_unit_test_assertion(pred,Typed,true,S) :- |
| 1069 | | print_bexpr_stream(S,Typed). |
| 1070 | | print_unit_test_assertion(pred,Typed,false,S) :- |
| 1071 | | safe_create_texpr(negation(Typed),pred,[],Neg), |
| 1072 | | print_bexpr_stream(S,Neg). |
| 1073 | | print_unit_test_assertion(expr,Typed,Val,S) :- |
| 1074 | | print_bexpr_stream(S,Typed), write(S,' = '), print_bvalue_stream(S,Val). |
| 1075 | | |
| 1076 | | |
| 1077 | | :- use_module(tools_printing,[print_term_summary/1]). |
| 1078 | | portray_waitflags_and_frozen_state_info(WF,StateTerm) :- |
| 1079 | | portray_waitflags(WF), |
| 1080 | | print_term_summary(frozen_info_for_state(StateTerm)), |
| 1081 | | term_variables(StateTerm,Vars), |
| 1082 | | translate:l_print_frozen_info(Vars). |
| 1083 | | |
| 1084 | | %% Utilities for defining values inside the REPL using let : |
| 1085 | | % ---------------------- |
| 1086 | | % scanning code utilities to recognize let construct |
| 1087 | | scan_identifier([32|T],ID,Rest) :- scan_identifier(T,ID,Rest). |
| 1088 | | scan_identifier([H|T],[H|TID],Rest) :- letter(H), |
| 1089 | | scan_identifier2(T,TID,Rest). |
| 1090 | | scan_identifier2([],[],[]). |
| 1091 | | scan_identifier2([32|T],[],T). |
| 1092 | | scan_identifier2([61|T],[],[61|T]). |
| 1093 | | scan_identifier2([H|T],[H|TID],Rest) :- ( letter(H) ; H = 95 ; digit(H)), |
| 1094 | | scan_identifier2(T,TID,Rest). |
| 1095 | | letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95 |
| 1096 | | digit(X) :- X >= 48, X =< 57. |
| 1097 | | |
| 1098 | | scan_to_equal([32|T],Rest) :- scan_to_equal(T,Rest). |
| 1099 | | scan_to_equal([61|T],T). % "=" = [61] |
| 1100 | | |
| 1101 | | just_whitespace([32|T]) :- just_whitespace(T). |
| 1102 | | just_whitespace([]). |
| 1103 | | |
| 1104 | | :- dynamic stored_let_value/3. |
| 1105 | | store_let_id_last_value(ID) :- |
| 1106 | | retract(stored_let_value(ID,LastType,_)), |
| 1107 | | !, |
| 1108 | | get_last_value(ID,Type,Value), %print(updating(ID)),nl, |
| 1109 | | assert(stored_let_value(ID,Type,Value)), |
| 1110 | | (LastType=Type -> true ; reset_parse_cache). |
| 1111 | | store_let_id_last_value(ID) :- |
| 1112 | | get_cur_state_for_repl(State), member(bind(ID,_),State),!, |
| 1113 | | add_error(store_let_id_last_value,'Cannot redefine existing identifier using let: ',ID). |
| 1114 | | store_let_id_last_value(ID) :- |
| 1115 | | get_last_value(ID,Type,Value), |
| 1116 | | %print(store(ID,Type,Value)),nl, |
| 1117 | | assert(stored_let_value(ID,Type,Value)), |
| 1118 | | reset_parse_cache. |
| 1119 | | |
| 1120 | | extend_state_with_stored_lets(State,ExtendedState) :- |
| 1121 | | findall(bind(ID,Val),stored_let_value(ID,_,Val),ExtendedState,State). |
| 1122 | | |
| 1123 | | % construct the scope that the typechecker will use |
| 1124 | | repl_typing_scope([identifier(Ids),prob_ids(visible),S]) :- % promoted if we allow operation_call_in_expr |
| 1125 | | findall(b(identifier(ID),Type,[]),stored_let_value(ID,Type,_),Ids), |
| 1126 | | Ids \= [],!,get_main_repl_scope(S). |
| 1127 | | repl_typing_scope([prob_ids(visible),S]) :- get_main_repl_scope(S). |
| 1128 | | |
| 1129 | | get_main_repl_scope(assertions_scope) :- get_preference(allow_operation_calls_in_expr,true),!. |
| 1130 | | get_main_repl_scope(variables). |
| 1131 | | |
| 1132 | | get_last_value(ID,Type,Value) :- % first try and see if we had a predicate with identifier ID |
| 1133 | | get_last_predicate_value_for_id(ID,T,V), |
| 1134 | | !, |
| 1135 | | Type=T, Value=V. |
| 1136 | | get_last_value(_ID,Type,Value) :- get_last_expr_type_and_value(_,Type,Value). |
| 1137 | | |
| 1138 | | get_last_expr_type_and_value(Expr,Type,Value) :- |
| 1139 | | last_expression(_,Expr,V), |
| 1140 | | get_texpr_type(Expr,T), |
| 1141 | | convert_result(T,V,Type,Value). |
| 1142 | | |
| 1143 | | % display information about stored lets |
| 1144 | | browse_repl_lets :- \+ \+ stored_let_value(_,_,_), |
| 1145 | | print('Available let definitions:'),nl, |
| 1146 | | stored_let_value(ID,_,Value), |
| 1147 | | translate:translate_bvalue_with_limit(Value,50,VS), |
| 1148 | | format(' ~w = ~w~n',[ID,VS]), |
| 1149 | | fail. |
| 1150 | | browse_repl_lets. |
| 1151 | | |
| 1152 | | get_repl_lets_info(Lets) :- |
| 1153 | | findall(S, (stored_let_value(ID,_,Value), |
| 1154 | | translate:translate_bvalue_with_limit(Value,50,VS), |
| 1155 | | ajoin([ID,' = ',VS,'\n'],S)), |
| 1156 | | Lets). |
| 1157 | | |
| 1158 | | |
| 1159 | | list_information(INFO,Res,[INFO/BList]) :- !, |
| 1160 | | external_functions:'PROJECT_INFO'(string(INFO),BList,unknown,no_wf_available), |
| 1161 | | !, |
| 1162 | | translate:translate_bvalue_with_limit(BList,5000,Res), |
| 1163 | | format('~w~n',[Res]). |
| 1164 | | list_information(Arg,Res,[]) :- add_error(eval_strings,'Unknown argument for :list: ',Arg), |
| 1165 | | Res='ERROR'. |
| 1166 | | |
| 1167 | | |
| 1168 | | reset_eval_strings :- retractall(last_expression(_,_,_)), |
| 1169 | | retractall(last_solution(_,_)), |
| 1170 | | reset_parse_cache, |
| 1171 | | set_observe_evaluation(false), |
| 1172 | | retractall(eval_dot_file(_)), |
| 1173 | | retractall(stored_let_value(_,_,_)), |
| 1174 | | retractall(eval_repeat(_)), |
| 1175 | | unset_eval_det, |
| 1176 | | (reset_required -> true ; assert(reset_required)). % before next evaluation we need to remove invalid lets |
| 1177 | | |
| 1178 | | reset_parse_cache :- %print(reset_parse_cache),nl,nl, |
| 1179 | | retractall(parse_expr_cache(_,_,_,_,_)), |
| 1180 | | retractall(parse_pred_cache(_,_,_,_,_)). |
| 1181 | | |
| 1182 | | :- dynamic reset_required/0. |
| 1183 | | |
| 1184 | | reset_repl_lets :- retract(reset_required), |
| 1185 | | stored_let_value(ID,Type,Value), |
| 1186 | | (contains_invalid_user_set(Type) -> true |
| 1187 | | ; is_a_machine_identifier(ID)), % the ID now clashes |
| 1188 | | retract(stored_let_value(ID,Type,Value)), |
| 1189 | | print(removing_let(ID)),nl, |
| 1190 | | fail. |
| 1191 | | reset_repl_lets. |
| 1192 | | |
| 1193 | | % to do: write a proper predicate in bmachine and also collect other ids like freetypes ?! |
| 1194 | | is_a_machine_identifier(ID) :- bmachine:b_is_constant(ID). |
| 1195 | | is_a_machine_identifier(ID) :- bmachine:b_is_variable(ID). |
| 1196 | | is_a_machine_identifier(ID) :-b_global_sets:b_global_set(ID). |
| 1197 | | is_a_machine_identifier(ID) :-b_global_sets:lookup_global_constant(ID,_). |
| 1198 | | |
| 1199 | | % check if a type contains a user defined set which is no longer available in new machine or re-loaded machine |
| 1200 | | contains_invalid_user_set(global(G)) :- \+ b_global_sets:b_global_set(G). |
| 1201 | | contains_invalid_user_set(set(T)) :- contains_invalid_user_set(T). |
| 1202 | | contains_invalid_user_set(seq(T)) :- contains_invalid_user_set(T). |
| 1203 | | contains_invalid_user_set(couple(A,B)) :- |
| 1204 | | (contains_invalid_user_set(A) -> true ; contains_invalid_user_set(B)). |
| 1205 | | contains_invalid_user_set(freetype(_)). % TO DO: check |
| 1206 | | contains_invalid_user_set(record(Fields)) :- member(field(_,T),Fields), contains_invalid_user_set(T). |
| 1207 | | |
| 1208 | | |
| 1209 | | |
| 1210 | | |
| 1211 | | %% ------------------------------------ |
| 1212 | | %% DETERMINISTIC PROPAGATION UNIT TESTS |
| 1213 | | %% ------------------------------------ |
| 1214 | | |
| 1215 | | |
| 1216 | | % check that certain predicates are determined to be failing without enumeration |
| 1217 | | % to do: also add positive tests: certain predicates succeed with instantiating all variables |
| 1218 | | % eval_strings:must_fail_tests. |
| 1219 | | |
| 1220 | | must_fail_tests :- set_eval_det, |
| 1221 | | must_fail_det(Nr,Str,ExTyped), |
| 1222 | | check_failed(Nr,ExTyped), |
| 1223 | | Str \= [], |
| 1224 | | % print('PARSING: '),nl,name(SS,Str), print(SS),nl, |
| 1225 | | repl_typing_scope(TypingScope), |
| 1226 | | ( b_parse_machine_predicate_from_codes_open(exists,Str,[],TypingScope,NewTyped) -> |
| 1227 | | check_same_ast(Nr,NewTyped,ExTyped) |
| 1228 | | ; otherwise -> |
| 1229 | | print('*** Could not parse: '), print(Nr), nl |
| 1230 | | %add_error(must_fail_tests,'Could not parse saved string: ',Nr) |
| 1231 | | ), |
| 1232 | | fail. |
| 1233 | | must_fail_tests :- preferences:preference(use_clpfd_solver,true), |
| 1234 | | must_fail_clpfd_det(Nr,ExTyped), |
| 1235 | | test_enabled(Nr), |
| 1236 | | check_failed(Nr,ExTyped),fail. |
| 1237 | | must_fail_tests :- unset_eval_det. |
| 1238 | | |
| 1239 | | check_failed(Nr,ExTyped) :- |
| 1240 | | nl,print(Nr), print(' >>> '), translate:print_bexpr(ExTyped),nl, |
| 1241 | | (eval_predicate(ExTyped,Res,_,_) |
| 1242 | | -> (Res='FALSE' -> true ; |
| 1243 | | add_error(must_fail_tests,'Test has not failed deterministically: ',Nr)) |
| 1244 | | ; add_error(must_fail_tests,'eval_predicate failed: ',Nr) |
| 1245 | | ). |
| 1246 | | |
| 1247 | | :- use_module(self_check). |
| 1248 | | |
| 1249 | | :- assert_must_succeed(must_fail_tests). |
| 1250 | | |
| 1251 | | check_same_ast(Nr,A,B) :- % check equivalent to stored AST B, apart from pos |
| 1252 | | remove_pos(A,RA), |
| 1253 | | (RA=B -> true |
| 1254 | | ; add_error(check_same_ast,'AST not identical: ',Nr), |
| 1255 | | print('New AST:'),nl,print(A),nl, |
| 1256 | | print('Stored AST :'),nl,print(B),nl, |
| 1257 | | tools_printing:trace_unify(RA,B)). |
| 1258 | | % remove position Info |
| 1259 | | remove_pos(X,R) :- var(X),!,R=X. |
| 1260 | | remove_pos(pos(_,_,_,_,_,_),R) :- !, R=pos(_,_,_,_,_,_). |
| 1261 | | remove_pos(nodeid(_),R) :- !, R=nodeid(_). |
| 1262 | | remove_pos([removed_typing|T],R) :- !, % new info field |
| 1263 | | remove_pos(T,R). |
| 1264 | | remove_pos(X,R) :- atomic(X),!,R=X. |
| 1265 | | remove_pos(L,R) :- L=..[F|Args], l_remove_pos(Args,RA), R=..[F|RA]. |
| 1266 | | |
| 1267 | | l_remove_pos([],[]). |
| 1268 | | l_remove_pos([H|T],[RH|RT]) :- remove_pos(H,RH), l_remove_pos(T,RT). |
| 1269 | | |
| 1270 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 1271 | | :- if(environ(prob_release,true)). |
| 1272 | | must_fail_det(_Nr,_Str,_ExTyped) :- fail. |
| 1273 | | must_fail_clpfd_det(_Nr,_ExTyped) :- fail. |
| 1274 | | :- else. |
| 1275 | | % |
| 1276 | | must_fail_det(1,"#(x,y,z).(x:BOOL & x=z & z=y & x /= y)", |
| 1277 | | %b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,20,1,20)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,22,1,22)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,20,1,22))]),b(equal(b(identifier(z),boolean,[nodeid(pos(nan,1,1,26,1,26)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(nan,1,1,28,1,28)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,26,1,28))])),pred,[nodeid(pos(nan,1,1,11,1,28))]),b(not_equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,32,1,32)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(nan,1,1,37,1,37)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,32,1,37))])),pred,[nodeid(pos(nan,1,1,11,1,37))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,38))])). |
| 1278 | | b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(5,-1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(x),boolean,[nodeid(pos(13,-1,1,20,1,20)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(14,-1,1,22,1,22)),introduced_by(exists)])),pred,[nodeid(pos(12,-1,1,20,1,22))]),b(equal(b(identifier(z),boolean,[nodeid(pos(16,-1,1,26,1,26)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(17,-1,1,28,1,28)),introduced_by(exists)])),pred,[nodeid(pos(15,-1,1,26,1,28))])),pred,[nodeid(pos(7,-1,1,11,1,28))]),b(not_equal(b(identifier(x),boolean,[nodeid(pos(19,-1,1,32,1,32)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(20,-1,1,37,1,37)),introduced_by(exists)])),pred,[nodeid(pos(18,-1,1,32,1,37))])),pred,[nodeid(pos(6,-1,1,11,1,37))]),b(external_pred_call('LEQ_SYM_BREAK',[b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)])]),pred,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])),pred,[])),pred,[used_ids([]),prob_symmetry(x,y),nodeid(pos(2,-1,1,1,1,38))])). % with symmetry breaking |
| 1279 | | |
| 1280 | | |
| 1281 | | % |
| 1282 | | must_fail_det(2,"#x.(x:BOOL & (x=FALSE <=> x=TRUE))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,2,1,2)),introduced_by(exists)])],b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,15,1,15)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])),pred,[nodeid(pos(nan,1,1,15,1,17))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,29,1,29))])),pred,[nodeid(pos(nan,1,1,27,1,29))])),pred,[nodeid(pos(nan,1,1,15,1,29))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,34))])). |
| 1283 | | |
| 1284 | | % |
| 1285 | | must_fail_det(3,"#(b,c).(b:BOOL & b=c & b/=c)", |
| 1286 | | b(exists([b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(c),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,18,1,18)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,20,1,20)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,18,1,20))]),b(not_equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,24,1,24)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,24,1,27))])),pred,[nodeid(pos(nan,1,1,9,1,27))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,28))])). |
| 1287 | | |
| 1288 | | |
| 1289 | | % |
| 1290 | | must_fail_det(4,"#(e,s).(s<:INT & e:s & e/:s)", b(exists([b(identifier(e),integer,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,4)),introduced_by(exists)]),b(identifier(s),set(integer),[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,6)),introduced_by(exists)])],b(conjunct(b(conjunct(b(subset(b(identifier(s),set(integer),[nodeid(pos(8,-1,1,9,1,10)),introduced_by(exists)]),b(interval(b(min_int,integer,[nodeid(pos(9,-1,1,12,1,15))]),b(max_int,integer,[nodeid(pos(9,-1,1,12,1,15))])),set(integer),[was(integer_set('INT')),nodeid(pos(9,-1,1,12,1,15))])),pred,[nodeid(pos(7,-1,1,9,1,15))]),b(member(b(identifier(e),integer,[nodeid(pos(11,-1,1,18,1,19)),introduced_by(exists)]),b(identifier(s),set(integer),[nodeid(pos(12,-1,1,20,1,21)),introduced_by(exists)])),pred,[nodeid(pos(10,-1,1,18,1,21))])),pred,[nodeid(pos(6,-1,1,9,1,21))]),b(not_member(b(identifier(e),integer,[nodeid(pos(14,-1,1,24,1,25)),introduced_by(exists)]),b(identifier(s),set(integer),[nodeid(pos(15,-1,1,27,1,28)),introduced_by(exists)])),pred,[nodeid(pos(13,-1,1,24,1,28))])),pred,[nodeid(pos(5,-1,1,9,1,28))])),pred,[used_ids([]),nodeid(pos(2,-1,1,1,1,29))])). |
| 1291 | | |
| 1292 | | % |
| 1293 | | must_fail_det(5,"#(x,y,z,v,xz).(x:BOOL & x/=y & v/=z & x=v & (x=z <=> xz=TRUE) & (xz=FALSE => x=TRUE) & (xz=FALSE => x=FALSE))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)]),b(identifier(v),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,9,1,9)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,11,1,11)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,25,1,25)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(nan,1,1,28,1,28)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,25,1,28))]),b(not_equal(b(identifier(v),boolean,[nodeid(pos(nan,1,1,32,1,32)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,35,1,35)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,32,1,35))])),pred,[nodeid(pos(nan,1,1,16,1,35))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,39,1,39)),introduced_by(exists)]),b(identifier(v),boolean,[nodeid(pos(nan,1,1,41,1,41)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,39,1,41))])),pred,[nodeid(pos(nan,1,1,16,1,41))]),b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,46,1,46)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,48,1,48)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,46,1,48))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,54,1,54)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,57,1,57))])),pred,[nodeid(pos(nan,1,1,54,1,57))])),pred,[nodeid(pos(nan,1,1,46,1,57))])),pred,[nodeid(pos(nan,1,1,16,1,61))]),b(implication(b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,66,1,66)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,69,1,69))])),pred,[nodeid(pos(nan,1,1,66,1,69))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,78,1,78)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,80,1,80))])),pred,[nodeid(pos(nan,1,1,78,1,80))])),pred,[nodeid(pos(nan,1,1,66,1,80))])),pred,[nodeid(pos(nan,1,1,16,1,84))]),b(implication(b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,89,1,89)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,92,1,92))])),pred,[nodeid(pos(nan,1,1,89,1,92))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,101,1,101)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,103,1,103))])),pred,[nodeid(pos(nan,1,1,101,1,103))])),pred,[nodeid(pos(nan,1,1,89,1,103))])),pred,[nodeid(pos(nan,1,1,16,1,108))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,109))])). |
| 1294 | | |
| 1295 | | % |
| 1296 | | must_fail_det(6,"#(x,xz).((x : BOOL & xz : BOOL) & (((x = TRUE) <=> not(x = TRUE)) <=> (xz = TRUE) & ((x = TRUE) <=> not(x = TRUE)) <=> (xz = FALSE)))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,38,1,38)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,38,1,42))]),b(negation(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,56,1,56)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,60,1,60))])),pred,[nodeid(pos(nan,1,1,56,1,60))])),pred,[nodeid(pos(nan,1,1,52,1,64))])),pred,[nodeid(pos(nan,1,1,37,1,64))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,72,1,72)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,77,1,77))])),pred,[nodeid(pos(nan,1,1,72,1,77))])),pred,[nodeid(pos(nan,1,1,36,1,81))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,87,1,87)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,91,1,91))])),pred,[nodeid(pos(nan,1,1,87,1,91))]),b(negation(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,105,1,105)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,109,1,109))])),pred,[nodeid(pos(nan,1,1,105,1,109))])),pred,[nodeid(pos(nan,1,1,101,1,113))])),pred,[nodeid(pos(nan,1,1,86,1,113))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,121,1,121)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,126,1,126))])),pred,[nodeid(pos(nan,1,1,121,1,126))])),pred,[nodeid(pos(nan,1,1,85,1,131))])),pred,[nodeid(pos(nan,1,1,36,1,131))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,133))])). |
| 1297 | | |
| 1298 | | % |
| 1299 | | must_fail_det(7,"#(x,z,x2,xz).((((x : BOOL & z : BOOL) & x2 : BOOL) & xz : BOOL) & (((x2 /= z & x = x2) & ((x = TRUE) <=> (x2 = FALSE)) <=> (xz = TRUE)) & ((x = TRUE) <=> (x2 = FALSE)) <=> (xz = FALSE)))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(x2),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,10,1,10)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,70,1,70)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,76,1,76)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,70,1,76))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,80,1,80)),introduced_by(exists)]),b(identifier(x2),boolean,[nodeid(pos(nan,1,1,84,1,84)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,80,1,84))])),pred,[nodeid(pos(nan,1,1,70,1,84))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,92,1,92)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,92,1,96))]),b(equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,112,1,112))])),pred,[nodeid(pos(nan,1,1,107,1,112))])),pred,[nodeid(pos(nan,1,1,91,1,117))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,125,1,125)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,130,1,130))])),pred,[nodeid(pos(nan,1,1,125,1,130))])),pred,[nodeid(pos(nan,1,1,90,1,134))])),pred,[nodeid(pos(nan,1,1,69,1,134))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,141,1,141)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,145,1,145))])),pred,[nodeid(pos(nan,1,1,141,1,145))]),b(equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,156,1,156)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,161,1,161))])),pred,[nodeid(pos(nan,1,1,156,1,161))])),pred,[nodeid(pos(nan,1,1,140,1,166))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,174,1,174)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,179,1,179))])),pred,[nodeid(pos(nan,1,1,174,1,179))])),pred,[nodeid(pos(nan,1,1,139,1,184))])),pred,[nodeid(pos(nan,1,1,68,1,184))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,186))])). |
| 1300 | | |
| 1301 | | % |
| 1302 | | must_fail_det(8,"#(a,b).((a : BOOL & b : BOOL) & ((b = TRUE) <=> ((a = TRUE) <=> not(a = TRUE)) & (b = FALSE) <=> ((a = FALSE) <=> (a = TRUE))))", b(exists([b(identifier(a),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,35,1,35)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,39,1,39))])),pred,[nodeid(pos(nan,1,1,35,1,39))]),b(equivalence(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,51,1,51)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,51,1,55))]),b(negation(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,69,1,69)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,73,1,73))])),pred,[nodeid(pos(nan,1,1,69,1,73))])),pred,[nodeid(pos(nan,1,1,65,1,77))])),pred,[nodeid(pos(nan,1,1,50,1,77))])),pred,[nodeid(pos(nan,1,1,34,1,78))]),b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,83,1,83)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,87,1,87))])),pred,[nodeid(pos(nan,1,1,83,1,87))]),b(equivalence(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,100,1,100)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,104,1,104))])),pred,[nodeid(pos(nan,1,1,100,1,104))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,116,1,116)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,120,1,120))])),pred,[nodeid(pos(nan,1,1,116,1,120))])),pred,[nodeid(pos(nan,1,1,99,1,124))])),pred,[nodeid(pos(nan,1,1,82,1,125))])),pred,[nodeid(pos(nan,1,1,34,1,125))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,127))])). |
| 1303 | | |
| 1304 | | % |
| 1305 | | must_fail_det(9,[], % let predicate now also optimizes bool equalities: |
| 1306 | | %"#(a,b,c).(((a : BOOL & b : BOOL) & c : BOOL) & ((((b = TRUE) <=> (a = TRUE => a = FALSE) & b = TRUE) & (a = FALSE => c = FALSE)) & (a = FALSE => c = TRUE)))", |
| 1307 | | b(let_predicate([b(identifier(b),boolean,[nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],[b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])],b(exists([b(identifier(a),boolean,[nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,52,1,52)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,56,1,56))])),pred,[nodeid(pos(nan,1,1,52,1,56))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,67,1,67)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,71,1,71))])),pred,[nodeid(pos(nan,1,1,67,1,71))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,79,1,79)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,83,1,83))])),pred,[nodeid(pos(nan,1,1,79,1,83))])),pred,[nodeid(pos(nan,1,1,67,1,83))])),pred,[nodeid(pos(nan,1,1,51,1,88))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,105,1,105)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,109,1,109))])),pred,[nodeid(pos(nan,1,1,105,1,109))]),b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,118,1,118)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,122,1,122))])),pred,[nodeid(pos(nan,1,1,118,1,122))])),pred,[nodeid(pos(nan,1,1,105,1,122))])),pred,[]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,133,1,133)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,137,1,137))])),pred,[nodeid(pos(nan,1,1,133,1,137))]),b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,146,1,146)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,150,1,150))])),pred,[nodeid(pos(nan,1,1,146,1,150))])),pred,[nodeid(pos(nan,1,1,133,1,150))])),pred,[])),pred,[used_ids([b]),used_ids([b]),used_ids([a,b,c])])),pred,[nodeid(pos(nan,1,1,1,1,156))])). |
| 1308 | | |
| 1309 | | % |
| 1310 | | must_fail_det(10,"#(a,b,c).(((a : BOOL & b : BOOL) & c : BOOL) & (((b = TRUE) <=> (a = TRUE => a = FALSE) & (c = TRUE) <=> (a = b)) & (c = TRUE) <=> not(a = b)))", b(exists([b(identifier(a),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(c),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,51,1,51)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,51,1,55))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,66,1,66)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,70,1,70))])),pred,[nodeid(pos(nan,1,1,66,1,70))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,78,1,78)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,82,1,82))])),pred,[nodeid(pos(nan,1,1,78,1,82))])),pred,[nodeid(pos(nan,1,1,66,1,82))])),pred,[nodeid(pos(nan,1,1,50,1,87))]),b(equivalence(b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,92,1,92)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,92,1,96))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(exists)]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,111,1,111)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,107,1,111))])),pred,[nodeid(pos(nan,1,1,91,1,112))])),pred,[nodeid(pos(nan,1,1,50,1,112))]),b(equivalence(b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,118,1,118)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,122,1,122))])),pred,[nodeid(pos(nan,1,1,118,1,122))]),b(negation(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,136,1,136)),introduced_by(exists)]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,140,1,140)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,136,1,140))])),pred,[nodeid(pos(nan,1,1,132,1,141))])),pred,[nodeid(pos(nan,1,1,117,1,141))])),pred,[nodeid(pos(nan,1,1,49,1,141))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,143))]) |
| 1311 | | ). |
| 1312 | | |
| 1313 | | % "#(x,y,z).(((x : BOOL & y : BOOL) & z : BOOL) & ((TRUE:BOOL) => ((x : {TRUE}) <=> (y = TRUE) & (x = y) <=> (z = TRUE)) & x /= y <=> (z = TRUE)))" |
| 1314 | | must_fail_det(11,[], b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(7,1,4,3,4,3))]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(8,1,4,5,4,5))]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(9,1,4,7,4,7))])],b(implication(b(truth,pred,[nodeid(pos(19,1,4,29,4,34))]),b(conjunct(b(conjunct(b(equivalence(b(member(b(identifier(x),boolean,[nodeid(pos(26,1,4,40,4,40))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(28,1,4,43,4,46))])]),set(boolean),[nodeid(pos(27,1,4,42,4,47))])),pred,[nodeid(pos(25,1,4,40,4,47))]),b(equal(b(identifier(y),boolean,[nodeid(pos(30,1,4,53,4,53))]),b(boolean_true,boolean,[nodeid(pos(31,1,4,55,4,58))])),pred,[nodeid(pos(29,1,4,53,4,58))])),pred,[nodeid(pos(24,1,4,40,4,58))]),b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(34,1,4,64,4,64))]),b(identifier(y),boolean,[nodeid(pos(35,1,4,66,4,66))])),pred,[nodeid(pos(33,1,4,64,4,66))]),b(equal(b(identifier(z),boolean,[nodeid(pos(37,1,4,72,4,72))]),b(boolean_true,boolean,[nodeid(pos(38,1,4,74,4,77))])),pred,[nodeid(pos(36,1,4,72,4,77))])),pred,[nodeid(pos(32,1,4,64,4,77))])),pred,[nodeid(pos(23,1,4,40,4,77))]),b(equivalence(b(not_equal(b(identifier(x),boolean,[nodeid(pos(41,1,4,82,4,82))]),b(identifier(y),boolean,[nodeid(pos(42,1,4,85,4,85))])),pred,[nodeid(pos(40,1,4,82,4,85))]),b(equal(b(identifier(z),boolean,[nodeid(pos(44,1,4,90,4,90))]),b(boolean_true,boolean,[nodeid(pos(45,1,4,92,4,95))])),pred,[nodeid(pos(43,1,4,90,4,95))])),pred,[nodeid(pos(39,1,4,82,4,95))])),pred,[nodeid(pos(22,1,4,40,4,95))])),pred,[nodeid(pos(10,1,4,11,4,95))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,97))])). |
| 1315 | | |
| 1316 | | |
| 1317 | | must_fail_det(12,[], %"SIGMA(x,y).(x : 1 .. 10 & y : {1,2}|x) = 111", |
| 1318 | | b(equal(b(general_sum([b(identifier(x),integer,[nodeid(pos(nan,1,1,7,1,7)),introduced_by(general_sum)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,9,1,9)),introduced_by(general_sum)])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,13,1,13)),introduced_by(general_sum)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(10),integer,[nodeid(pos(nan,1,1,22,1,22))])),set(integer),[nodeid(pos(nan,1,1,17,1,22))])),pred,[nodeid(pos(nan,1,1,13,1,22))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(general_sum)]),b(set_extension([b(integer(1),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(integer(2),integer,[nodeid(pos(nan,1,1,34,1,34))])]),set(integer),[nodeid(pos(nan,1,1,31,1,35))])),pred,[nodeid(pos(nan,1,1,27,1,35))])),pred,[nodeid(pos(nan,1,1,13,1,35))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,37,1,37)),introduced_by(general_sum)])),integer,[nodeid(pos(nan,1,1,1,1,38))]),b(integer(111),integer,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))])). |
| 1319 | | |
| 1320 | | must_fail_det(13,[], %"PI(x,y).(x : 1 .. 10 & y : {1,2}|x) = 111", |
| 1321 | | b(equal(b(general_product([b(identifier(x),integer,[nodeid(pos(nan,1,1,4,1,4)),introduced_by(general_product)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,6,1,6)),introduced_by(general_product)])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,10,1,10)),introduced_by(general_product)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,14,1,14))]),b(integer(10),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,14,1,19))])),pred,[nodeid(pos(nan,1,1,10,1,19))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,24,1,24)),introduced_by(general_product)]),b(set_extension([b(integer(1),integer,[nodeid(pos(nan,1,1,29,1,29))]),b(integer(2),integer,[nodeid(pos(nan,1,1,31,1,31))])]),set(integer),[nodeid(pos(nan,1,1,28,1,32))])),pred,[nodeid(pos(nan,1,1,24,1,32))])),pred,[nodeid(pos(nan,1,1,10,1,32))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,34,1,34)),introduced_by(general_product)])),integer,[nodeid(pos(nan,1,1,1,1,35))]),b(integer(111),integer,[nodeid(pos(nan,1,1,39,1,39))])),pred,[nodeid(pos(nan,1,1,1,1,39))])). |
| 1322 | | |
| 1323 | | /* |
| 1324 | | must_fail_det(16,"union(ran(%x.((x <: {1,2,3,4} & card(x) > 0) & min(x) = 2|x))) = {1,2,3,4}", |
| 1325 | | b(equal(b(general_union(b(range(b(comprehension_set([b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))]),b(identifier('_lambda_result_'),set(integer),[lambda_result])],b(conjunct(b(conjunct(b(conjunct(b(subset(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))]),b(set_extension([b(integer(1),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(3),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(4),integer,[nodeid(pos(0,0,0,0,0,0))])]),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))]),b(greater(b(card(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(0),integer,[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))]),b(equal(b(min(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),integer,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(equal(b(identifier('_lambda_result_'),set(integer),[lambda_result]),b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[])),pred,[contains_wd_condition])),set(couple(set(integer),set(integer))),[contains_wd_condition,was(lambda),generated(quantified_union)])),set(set(integer)),[contains_wd_condition,generated(quantified_union)])),set(integer),[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(set_extension([b(integer(1),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(3),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(4),integer,[nodeid(pos(0,0,0,0,0,0))])]),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))])). |
| 1326 | | */ |
| 1327 | | |
| 1328 | | |
| 1329 | | % #(z,x,y).(((z : POW(POW(BOOL)) & x : POW(BOOL)) & y : INTEGER) & ((z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & (x : z) <=> (y = 2)) & y > 3)) |
| 1330 | | % check that we detect that z is a complete set, hence x:z and hence y=2 |
| 1331 | | must_fail_det(14,[], %"z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & (x:z <=> y=2) & y>3 ", |
| 1332 | | b(exists([b(identifier(z),set(set(boolean)),[]),b(identifier(x),set(boolean),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(empty_set,set(boolean),[nodeid(pos(nan,1,1,6,1,6))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])]),set(boolean),[nodeid(pos(nan,1,1,9,1,14))]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])]),set(boolean),[nodeid(pos(nan,1,1,16,1,22))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,30,1,30))])]),set(boolean),[nodeid(pos(nan,1,1,24,1,35))])]),set(set(boolean)),[nodeid(pos(nan,1,1,5,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(equivalence(b(member(b(identifier(x),set(boolean),[nodeid(pos(nan,1,1,41,1,41))]),b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,43,1,43))])),pred,[nodeid(pos(nan,1,1,41,1,43))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(integer(2),integer,[nodeid(pos(nan,1,1,51,1,51))])),pred,[nodeid(pos(nan,1,1,49,1,51))])),pred,[nodeid(pos(nan,1,1,41,1,51))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,56,1,56))]),b(integer(3),integer,[nodeid(pos(nan,1,1,58,1,58))])),pred,[nodeid(pos(nan,1,1,56,1,58))])),pred,[nodeid(pos(nan,1,1,1,1,58))])),pred,[used_ids([x,y,z])])). |
| 1333 | | |
| 1334 | | % #(z,x,y).(((z : POW(BOOL * BOOL) & x : BOOL * BOOL) & y : INTEGER) & ((z = {TRUE |-> FALSE,TRUE |-> TRUE,FALSE |-> FALSE,FALSE |-> TRUE} & (x : z) <=> (y = 2)) & y > 3)) |
| 1335 | | % check that we detect that z is a complete set, hence x:z and hence y=2 |
| 1336 | | must_fail_det(15,[], %" z = {(TRUE,FALSE),(TRUE,TRUE),(FALSE,FALSE),(FALSE,TRUE)} & (x:z <=> y=2) & y>3 ", |
| 1337 | | b(exists([b(identifier(z),set(couple(boolean,boolean)),[]),b(identifier(x),couple(boolean,boolean),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(couple(b(boolean_true,boolean,[nodeid(pos(nan,1,1,7,1,7))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,12,1,12))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,6,1,17))]),b(couple(b(boolean_true,boolean,[nodeid(pos(nan,1,1,20,1,20))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,19,1,29))]),b(couple(b(boolean_false,boolean,[nodeid(pos(nan,1,1,32,1,32))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,38,1,38))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,31,1,43))]),b(couple(b(boolean_false,boolean,[nodeid(pos(nan,1,1,46,1,46))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,52,1,52))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,45,1,56))])]),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,5,1,57))])),pred,[nodeid(pos(nan,1,1,1,1,57))]),b(equivalence(b(member(b(identifier(x),couple(boolean,boolean),[nodeid(pos(nan,1,1,62,1,62))]),b(identifier(z),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,64,1,64))])),pred,[nodeid(pos(nan,1,1,62,1,64))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,70,1,70))]),b(integer(2),integer,[nodeid(pos(nan,1,1,72,1,72))])),pred,[nodeid(pos(nan,1,1,70,1,72))])),pred,[nodeid(pos(nan,1,1,62,1,72))])),pred,[nodeid(pos(nan,1,1,1,1,73))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,77,1,77))]),b(integer(3),integer,[nodeid(pos(nan,1,1,79,1,79))])),pred,[nodeid(pos(nan,1,1,77,1,79))])),pred,[nodeid(pos(nan,1,1,1,1,79))])),pred,[used_ids([x,y,z])])). |
| 1338 | | |
| 1339 | | % #(z,x,y).(((z : POW(POW(BOOL)) & x : POW(POW(BOOL))) & y : INTEGER) & ((z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & x <: z <=> (y = 2)) & y > 3)) |
| 1340 | | must_fail_det(16,[],b(exists([b(identifier(z),set(set(boolean)),[]),b(identifier(x),set(set(boolean)),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(empty_set,set(boolean),[nodeid(pos(nan,1,1,6,1,6))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])]),set(boolean),[nodeid(pos(nan,1,1,9,1,14))]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])]),set(boolean),[nodeid(pos(nan,1,1,16,1,22))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,30,1,30))])]),set(boolean),[nodeid(pos(nan,1,1,24,1,35))])]),set(set(boolean)),[nodeid(pos(nan,1,1,5,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(equivalence(b(subset(b(identifier(x),set(set(boolean)),[nodeid(pos(nan,1,1,41,1,41))]),b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,44,1,44))])),pred,[nodeid(pos(nan,1,1,41,1,44))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(2),integer,[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,50,1,52))])),pred,[nodeid(pos(nan,1,1,41,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(integer(3),integer,[nodeid(pos(nan,1,1,59,1,59))])),pred,[nodeid(pos(nan,1,1,57,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))])),pred,[used_ids([x,y,z])])). |
| 1341 | | |
| 1342 | | % Eval Time: 0 ms (0 ms walltime) |
| 1343 | | % #(x).(x : INTEGER & ([111,222,333,444,555] |>> {x} = [111,222,333,444] & x > 555)) |
| 1344 | | must_fail_det(17,"#(x).(([111,222,333,444,555] |>> {x} = [111,222,333,444] & x > 555))", b(exists([b(identifier(x),integer,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])],b(conjunct(b(equal(b(range_subtraction(b(value(avl_set(node((int(3),int(333)),true,0,node((int(1),int(111)),true,1,empty,node((int(2),int(222)),true,0,empty,empty)),node((int(4),int(444)),true,1,empty,node((int(5),int(555)),true,0,empty,empty))))),set(couple(integer,integer)),[nodeid(pos(7,-1,1,8,1,28))]),b(set_extension([b(identifier(x),integer,[nodeid(pos(14,-1,1,35,1,35)),introduced_by(exists)])]),set(integer),[nodeid(pos(13,-1,1,34,1,36))])),set(couple(integer,integer)),[nodeid(pos(6,-1,1,8,1,36))]),b(value(avl_set(node((int(2),int(222)),true,1,node((int(1),int(111)),true,0,empty,empty),node((int(3),int(333)),true,1,empty,node((int(4),int(444)),true,0,empty,empty))))),set(couple(integer,integer)),[nodeid(pos(15,-1,1,40,1,56))])),pred,[nodeid(pos(5,-1,1,8,1,56))]),b(greater(b(identifier(x),integer,[nodeid(pos(21,-1,1,60,1,60)),introduced_by(exists)]),b(integer(555),integer,[nodeid(pos(22,-1,1,64,1,66))])),pred,[nodeid(pos(20,-1,1,60,1,66))])),pred,[nodeid(pos(4,-1,1,8,1,66))])),pred,[used_ids([]),nodeid(pos(2,-1,1,1,1,68))])). |
| 1345 | | |
| 1346 | | |
| 1347 | | % #(m,n).(m:30..100 & n:10..20 & m<n ) |
| 1348 | | must_fail_clpfd_det(101,b(exists([b(identifier(x),integer,[nodeid(pos(nan,1,1,3,1,3))])],b(conjunct(b(equal(b(range_subtraction(b(sequence_extension([b(integer(111),integer,[nodeid(pos(nan,1,1,9,1,9))]),b(integer(222),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(333),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(444),integer,[nodeid(pos(nan,1,1,21,1,21))]),b(integer(555),integer,[nodeid(pos(nan,1,1,25,1,25))])]),set(couple(integer,integer)),[nodeid(pos(nan,1,1,8,1,28))]),b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,35,1,35)),introduced_by(exists)])]),set(integer),[nodeid(pos(nan,1,1,34,1,36))])),set(couple(integer,integer)),[nodeid(pos(nan,1,1,8,1,36))]),b(sequence_extension([b(integer(111),integer,[nodeid(pos(nan,1,1,41,1,41))]),b(integer(222),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(333),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(integer(444),integer,[nodeid(pos(nan,1,1,53,1,53))])]),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,56))])),pred,[nodeid(pos(nan,1,1,8,1,56))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,60,1,60)),introduced_by(exists)]),b(integer(555),integer,[nodeid(pos(nan,1,1,64,1,64))])),pred,[nodeid(pos(nan,1,1,60,1,64))])),pred,[nodeid(pos(nan,1,1,8,1,64))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,68))])). |
| 1349 | | |
| 1350 | | % #(m,n).(m:30..101 & n:10..20 & n*n=m & m/=100) |
| 1351 | | must_fail_clpfd_det(102,b(exists([b(identifier(m),integer,[nodeid(pos(7,1,4,3,4,3))]),b(identifier(n),integer,[nodeid(pos(8,1,4,5,4,5))])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(m),integer,[nodeid(pos(13,1,4,9,4,9))]),b(interval(b(integer(30),integer,[nodeid(pos(15,1,4,11,4,12))]),b(integer(101),integer,[nodeid(pos(16,1,4,15,4,17))])),set(integer),[nodeid(pos(14,1,4,11,4,17))])),pred,[nodeid(pos(12,1,4,9,4,17))]),b(member(b(identifier(n),integer,[nodeid(pos(18,1,4,21,4,21))]),b(interval(b(integer(10),integer,[nodeid(pos(20,1,4,23,4,24))]),b(integer(20),integer,[nodeid(pos(21,1,4,27,4,28))])),set(integer),[nodeid(pos(19,1,4,23,4,28))])),pred,[nodeid(pos(17,1,4,21,4,28))])),pred,[nodeid(pos(11,1,4,9,4,28))]),b(equal(b(multiplication(b(identifier(n),integer,[nodeid(pos(24,1,4,32,4,32))]),b(identifier(n),integer,[nodeid(pos(25,1,4,34,4,34))])),integer,[nodeid(pos(23,1,4,32,4,34))]),b(identifier(m),integer,[nodeid(pos(26,1,4,36,4,36))])),pred,[nodeid(pos(22,1,4,32,4,36))])),pred,[nodeid(pos(10,1,4,9,4,36))]),b(not_equal(b(identifier(m),integer,[nodeid(pos(28,1,4,40,4,40))]),b(integer(100),integer,[nodeid(pos(29,1,4,43,4,45))])),pred,[nodeid(pos(27,1,4,40,4,45))])),pred,[nodeid(pos(9,1,4,9,4,45))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,46))])). |
| 1352 | | |
| 1353 | | % #(x,y).(y : BOOL & (x : NATURAL & (((x : {11}) <=> (y = TRUE) & x < 10) & (x : {12}) <=> (y = FALSE)))) |
| 1354 | | must_fail_clpfd_det(103,b(exists([b(identifier(x),integer,[nodeid(pos(7,1,4,3,4,3))]),b(identifier(y),boolean,[nodeid(pos(8,1,4,5,4,5))])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(12,1,4,9,4,9))]),b(integer_set('NATURAL'),set(integer),[nodeid(pos(13,1,4,11,4,17))])),pred,[nodeid(pos(11,1,4,9,4,17))]),b(conjunct(b(conjunct(b(equivalence(b(member(b(identifier(x),integer,[nodeid(pos(21,1,4,32,4,32))]),b(set_extension([b(integer(11),integer,[nodeid(pos(23,1,4,35,4,36))])]),set(integer),[nodeid(pos(22,1,4,34,4,37))])),pred,[nodeid(pos(20,1,4,32,4,37))]),b(equal(b(identifier(y),boolean,[nodeid(pos(25,1,4,43,4,43))]),b(boolean_true,boolean,[nodeid(pos(26,1,4,45,4,48))])),pred,[nodeid(pos(24,1,4,43,4,48))])),pred,[nodeid(pos(19,1,4,32,4,48))]),b(less(b(identifier(x),integer,[nodeid(pos(28,1,4,53,4,53))]),b(integer(10),integer,[nodeid(pos(29,1,4,55,4,56))])),pred,[nodeid(pos(27,1,4,53,4,56))])),pred,[nodeid(pos(18,1,4,32,4,56))]),b(equivalence(b(member(b(identifier(x),integer,[nodeid(pos(32,1,4,61,4,61))]),b(set_extension([b(integer(12),integer,[nodeid(pos(34,1,4,64,4,65))])]),set(integer),[nodeid(pos(33,1,4,63,4,66))])),pred,[nodeid(pos(31,1,4,61,4,66))]),b(equal(b(identifier(y),boolean,[nodeid(pos(36,1,4,72,4,72))]),b(boolean_false,boolean,[nodeid(pos(37,1,4,74,4,78))])),pred,[nodeid(pos(35,1,4,72,4,78))])),pred,[nodeid(pos(30,1,4,61,4,78))])),pred,[nodeid(pos(17,1,4,32,4,78))])),pred,[nodeid(pos(9,1,4,9,4,78))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,81))])). |
| 1355 | | |
| 1356 | | |
| 1357 | | % #(x,y).((x : INTEGER & y : INTEGER) & (({x} /<<: {11,12} <=> (y = 3) & x > 12) & y < 3)) |
| 1358 | | must_fail_clpfd_det(104,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equivalence(b(not_subset_strict(b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,2,1,2))])]),set(integer),[nodeid(pos(nan,1,1,1,1,3))]),b(set_extension([b(integer(11),integer,[nodeid(pos(nan,1,1,11,1,11))]),b(integer(12),integer,[nodeid(pos(nan,1,1,14,1,14))])]),set(integer),[nodeid(pos(nan,1,1,10,1,16))])),pred,[nodeid(pos(nan,1,1,1,1,16))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,22,1,22))]),b(integer(3),integer,[nodeid(pos(nan,1,1,24,1,24))])),pred,[nodeid(pos(nan,1,1,22,1,24))])),pred,[nodeid(pos(nan,1,1,1,1,24))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(12),integer,[nodeid(pos(nan,1,1,30,1,30))])),pred,[nodeid(pos(nan,1,1,28,1,30))])),pred,[nodeid(pos(nan,1,1,1,1,30))]),b(less(b(identifier(y),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(integer(3),integer,[nodeid(pos(nan,1,1,37,1,37))])),pred,[nodeid(pos(nan,1,1,35,1,37))])),pred,[nodeid(pos(nan,1,1,1,1,37))])),pred,[used_ids([x,y])])). |
| 1359 | | |
| 1360 | | % #(x,y).((x : 5 .. 10000 & x / y = 19000) & y : 1 .. 100) |
| 1361 | | must_fail_clpfd_det(105,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(5),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(10000),integer,[nodeid(pos(nan,1,1,6,1,6))])),set(integer),[nodeid(pos(nan,1,1,3,1,6))])),pred,[nodeid(pos(nan,1,1,1,1,6))]),b(equal(b(div(b(identifier(x),integer,[nodeid(pos(nan,1,1,14,1,14))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,16,1,16))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,14,1,16))]),b(integer(19000),integer,[nodeid(pos(nan,1,1,18,1,18))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,14,1,18))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,18))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(100),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,31))])),pred,[used_ids([x,y])])). |
| 1362 | | |
| 1363 | | % #(x,y).((x : 500 .. 10000 & 499 / y = x) & y : 1 .. 100) |
| 1364 | | must_fail_clpfd_det(106,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(500),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(10000),integer,[nodeid(pos(nan,1,1,8,1,8))])),set(integer),[nodeid(pos(nan,1,1,3,1,8))])),pred,[nodeid(pos(nan,1,1,1,1,8))]),b(equal(b(div(b(integer(499),integer,[nodeid(pos(nan,1,1,16,1,16))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,20,1,20))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,16,1,20))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,22,1,22))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,16,1,22))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,22))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(100),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,31))])),pred,[used_ids([x,y])])). |
| 1365 | | |
| 1366 | | % #(y,f,x).((((y : 1 .. 1000001 & f : 100001 .. 100005 --> 1 .. 9000) & x : dom(f)) & x : 2 .. 100003) & (x > 5000 => y : 2000001 .. 2000002)) |
| 1367 | | must_fail_clpfd_det(107,b(exists([b(identifier(y),integer,[]),b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(1000001),integer,[nodeid(pos(nan,1,1,6,1,6))])),set(integer),[nodeid(pos(nan,1,1,3,1,6))])),pred,[nodeid(pos(nan,1,1,1,1,6))]),b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,16,1,16))]),b(total_function(b(interval(b(integer(100001),integer,[nodeid(pos(nan,1,1,18,1,18))]),b(integer(100005),integer,[nodeid(pos(nan,1,1,26,1,26))])),set(integer),[nodeid(pos(nan,1,1,18,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,37,1,37))]),b(integer(9000),integer,[nodeid(pos(nan,1,1,40,1,40))])),set(integer),[nodeid(pos(nan,1,1,37,1,40))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,18,1,40))])),pred,[nodeid(pos(nan,1,1,16,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,48,1,48))]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,54,1,54))])),set(integer),[nodeid(pos(nan,1,1,50,1,55))])),pred,[nodeid(pos(nan,1,1,48,1,55))])),pred,[nodeid(pos(nan,1,1,1,1,55))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,59,1,59))]),b(interval(b(integer(2),integer,[nodeid(pos(nan,1,1,61,1,61))]),b(integer(100003),integer,[nodeid(pos(nan,1,1,64,1,64))])),set(integer),[nodeid(pos(nan,1,1,61,1,64))])),pred,[nodeid(pos(nan,1,1,59,1,64))])),pred,[nodeid(pos(nan,1,1,1,1,64))]),b(implication(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,74,1,74))]),b(integer(5000),integer,[nodeid(pos(nan,1,1,76,1,76))])),pred,[nodeid(pos(nan,1,1,74,1,76))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,84,1,84))]),b(interval(b(integer(2000001),integer,[nodeid(pos(nan,1,1,86,1,86))]),b(integer(2000002),integer,[nodeid(pos(nan,1,1,95,1,95))])),set(integer),[nodeid(pos(nan,1,1,86,1,95))])),pred,[nodeid(pos(nan,1,1,84,1,95))])),pred,[nodeid(pos(nan,1,1,74,1,95))])),pred,[nodeid(pos(nan,1,1,1,1,102))])),pred,[used_ids([f,x,y])])). |
| 1368 | | % #(f,x).((f : (BOOL * (123456 .. 123459)) * BOOL --> 1 .. 100 & x : dom(f)) & #(b,y,b2).(((b : BOOL & y : INTEGER) & b2 : BOOL) & (x = (b |-> y) |-> b2 & (y > 123459 or y < 123456)))) |
| 1369 | | must_fail_clpfd_det(108,b(exists([b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[]),b(identifier(x),couple(couple(boolean,integer),boolean),[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(cartesian_product(b(cartesian_product(b(bool_set,set(boolean),[nodeid(pos(nan,1,1,5,1,5))]),b(interval(b(integer(123456),integer,[nodeid(pos(nan,1,1,11,1,11))]),b(integer(123459),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,11,1,19))])),set(couple(boolean,integer)),[nodeid(pos(nan,1,1,5,1,25))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,27,1,27))])),set(couple(couple(boolean,integer),boolean)),[nodeid(pos(nan,1,1,5,1,27))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,37,1,37))]),b(integer(100),integer,[nodeid(pos(nan,1,1,40,1,40))])),set(integer),[nodeid(pos(nan,1,1,37,1,40))])),set(set(couple(couple(couple(boolean,integer),boolean),integer))),[nodeid(pos(nan,1,1,4,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(identifier(x),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,46,1,46))]),b(domain(b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[nodeid(pos(nan,1,1,52,1,52))])),set(couple(couple(boolean,integer),boolean)),[nodeid(pos(nan,1,1,48,1,53))])),pred,[nodeid(pos(nan,1,1,46,1,53))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(exists([b(identifier(b),boolean,[nodeid(pos(nan,1,1,59,1,59)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,61,1,61)),introduced_by(exists)]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,63,1,63)),introduced_by(exists)])],b(conjunct(b(equal(b(identifier(x),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,68,1,68))]),b(couple(b(couple(b(identifier(b),boolean,[nodeid(pos(nan,1,1,71,1,71)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,73,1,73)),introduced_by(exists)])),couple(boolean,integer),[nodeid(pos(nan,1,1,70,1,77))]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,75,1,75)),introduced_by(exists)])),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,70,1,77))])),pred,[nodeid(pos(nan,1,1,68,1,77))]),b(disjunct(b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,82,1,82)),introduced_by(exists)]),b(integer(123459),integer,[nodeid(pos(nan,1,1,84,1,84))])),pred,[nodeid(pos(nan,1,1,82,1,84))]),b(less(b(identifier(y),integer,[nodeid(pos(nan,1,1,94,1,94)),introduced_by(exists)]),b(integer(123456),integer,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,94,1,96))])),pred,[nodeid(pos(nan,1,1,82,1,96))])),pred,[nodeid(pos(nan,1,1,68,1,102))])),pred,[used_ids([x]),nodeid(pos(nan,1,1,57,1,103))])),pred,[nodeid(pos(nan,1,1,1,1,103))])),pred,[used_ids([f,x])])). |
| 1370 | | % #(f,x,y).((x : INTEGER & y : INTEGER) & ((f : 10 .. 200 --> 1 .. 200000 & x |-> y : f) & (x > 200 or x < 10))) |
| 1371 | | must_fail_clpfd_det(109,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(interval(b(integer(10),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(200),integer,[nodeid(pos(nan,1,1,8,1,8))])),set(integer),[nodeid(pos(nan,1,1,4,1,8))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,16,1,16))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,16,1,19))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,19))])),pred,[nodeid(pos(nan,1,1,1,1,19))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,32,1,32))])),couple(integer,integer),[nodeid(pos(nan,1,1,28,1,32))]),b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,36,1,36))])),pred,[nodeid(pos(nan,1,1,28,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(disjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,41,1,41))]),b(integer(200),integer,[nodeid(pos(nan,1,1,43,1,43))])),pred,[nodeid(pos(nan,1,1,41,1,43))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(10),integer,[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,50,1,52))])),pred,[nodeid(pos(nan,1,1,41,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,54))])),pred,[used_ids([f,x,y])])). |
| 1372 | | % #(f,b,x).((b : BOOL * BOOL & x : INTEGER) & ((f : BOOL * BOOL --> 100 .. 200000 & b |-> x : f) & (x > 200000 or x < 100))) |
| 1373 | | must_fail_clpfd_det(110,b(exists([b(identifier(f),set(couple(couple(boolean,boolean),integer)),[]),b(identifier(b),couple(boolean,boolean),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(couple(boolean,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(cartesian_product(b(bool_set,set(boolean),[nodeid(pos(nan,1,1,5,1,5))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,10,1,10))])),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,5,1,10))]),b(interval(b(integer(100),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,20,1,25))])),set(set(couple(couple(boolean,boolean),integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(b),couple(boolean,boolean),[nodeid(pos(nan,1,1,34,1,34))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,38,1,38))])),couple(couple(boolean,boolean),integer),[nodeid(pos(nan,1,1,34,1,38))]),b(identifier(f),set(couple(couple(boolean,boolean),integer)),[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,34,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))]),b(disjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,47,1,47))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,49,1,49))])),pred,[nodeid(pos(nan,1,1,47,1,49))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,59,1,59))]),b(integer(100),integer,[nodeid(pos(nan,1,1,61,1,61))])),pred,[nodeid(pos(nan,1,1,59,1,61))])),pred,[nodeid(pos(nan,1,1,47,1,61))])),pred,[nodeid(pos(nan,1,1,1,1,64))])),pred,[used_ids([b,f,x])])). |
| 1374 | | % #(f,g).(((f : 10001 .. 10110 --> NATURAL & !(x).(x : dom(f) => f(x) : dom(f))) & g : 20010 .. 20020 --> BOOL) & !(x).(x : dom(f) => f(x) : dom(g))) |
| 1375 | | must_fail_clpfd_det(111,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(g),set(couple(integer,boolean)),[])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,2,1,2))]),b(total_function(b(interval(b(integer(10001),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(10110),integer,[nodeid(pos(nan,1,1,12,1,12))])),set(integer),[nodeid(pos(nan,1,1,5,1,12))]),b(integer_set('NATURAL'),set(integer),[nodeid(pos(nan,1,1,22,1,22))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,5,1,22))])),pred,[nodeid(pos(nan,1,1,2,1,22))]),b(forall([b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33)),introduced_by(forall)])],b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,36,1,36)),introduced_by(forall)]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,42,1,42))])),set(integer),[nodeid(pos(nan,1,1,38,1,43))])),pred,[nodeid(pos(nan,1,1,36,1,43))]),b(member(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,48,1,48))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,50,1,50)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,48,1,51))]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,57,1,57))])),set(integer),[nodeid(pos(nan,1,1,53,1,58))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,48,1,58))])),pred,[used_ids([f]),nodeid(pos(nan,1,1,32,1,59))])),pred,[nodeid(pos(nan,1,1,2,1,59))]),b(member(b(identifier(g),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,63,1,63))]),b(total_function(b(interval(b(integer(20010),integer,[nodeid(pos(nan,1,1,65,1,65))]),b(integer(20020),integer,[nodeid(pos(nan,1,1,72,1,72))])),set(integer),[nodeid(pos(nan,1,1,65,1,72))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,82,1,82))])),set(set(couple(integer,boolean))),[nodeid(pos(nan,1,1,65,1,82))])),pred,[nodeid(pos(nan,1,1,63,1,82))])),pred,[nodeid(pos(nan,1,1,2,1,82))]),b(forall([b(identifier(x),integer,[nodeid(pos(nan,1,1,90,1,90)),introduced_by(forall)])],b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,93,1,93)),introduced_by(forall)]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,99,1,99))])),set(integer),[nodeid(pos(nan,1,1,95,1,100))])),pred,[nodeid(pos(nan,1,1,93,1,100))]),b(member(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,105,1,105))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,105,1,108))]),b(domain(b(identifier(g),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,114,1,114))])),set(integer),[nodeid(pos(nan,1,1,110,1,115))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,105,1,115))])),pred,[used_ids([f,g]),nodeid(pos(nan,1,1,89,1,116))])),pred,[nodeid(pos(nan,1,1,2,1,116))])),pred,[used_ids([f,g])])). |
| 1376 | | % #(f,x,y).((x : INTEGER & y : INTEGER) & ((f : 1001 .. 2001 --> 1900 .. 3333 & x |-> y : f) & y + 101 < x)) |
| 1377 | | must_fail_clpfd_det(112,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(2001),integer,[nodeid(pos(nan,1,1,11,1,11))])),set(integer),[nodeid(pos(nan,1,1,5,1,11))]),b(interval(b(integer(1900),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(integer(3333),integer,[nodeid(pos(nan,1,1,26,1,26))])),set(integer),[nodeid(pos(nan,1,1,20,1,26))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,5,1,26))])),pred,[nodeid(pos(nan,1,1,1,1,26))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,37,1,37))])),couple(integer,integer),[nodeid(pos(nan,1,1,33,1,37))]),b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,41,1,41))])),pred,[nodeid(pos(nan,1,1,33,1,41))])),pred,[nodeid(pos(nan,1,1,1,1,41))]),b(less(b(add(b(identifier(y),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(101),integer,[nodeid(pos(nan,1,1,47,1,47))])),integer,[nodeid(pos(nan,1,1,45,1,47))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,51,1,51))])),pred,[nodeid(pos(nan,1,1,45,1,51))])),pred,[nodeid(pos(nan,1,1,1,1,51))])),pred,[used_ids([f,x,y])])). |
| 1378 | | |
| 1379 | | % #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 <-> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 120) & card(r) = 3)) |
| 1380 | | must_fail_clpfd_det(113,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(relations(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(120),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(3),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])). |
| 1381 | | |
| 1382 | | % #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 +-> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 120) & card(r) = 3)) |
| 1383 | | must_fail_clpfd_det(114,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(partial_function(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(120),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(3),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])). |
| 1384 | | % #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 >+> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 104) & card(r) = 2)) |
| 1385 | | must_fail_clpfd_det(115,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(partial_injection(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(104),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(2),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])). |
| 1386 | | % #(s,x,b,y,b2).(((((s : POW((INTEGER * STRING) * BOOL) & x : INTEGER) & b : BOOL) & y : INTEGER) & b2 : BOOL) & (((s = {((1|->"a")|->TRUE),((2|->"a")|->FALSE),((3|->"b")|->FALSE),((4|->"b")|->FALSE)} & (x |-> "a") |-> b : s) & (y |-> "b") |-> b2 : s) & x > y)) |
| 1387 | | must_fail_clpfd_det(116,b(exists([b(identifier(s),set(couple(couple(integer,string),boolean)),[]),b(identifier(x),integer,[]),b(identifier(b),boolean,[]),b(identifier(y),integer,[]),b(identifier(b2),boolean,[])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(value(avl_set(node(((int(2),string(a)),pred_false),true,1,node(((int(1),string(a)),pred_true),true,0,empty,empty),node(((int(3),string(b)),pred_false),true,1,empty,node(((int(4),string(b)),pred_false),true,0,empty,empty))))),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,5,1,66))])),pred,[nodeid(pos(nan,1,1,1,1,66))]),b(member(b(couple(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,71,1,71))]),b(string(a),string,[nodeid(pos(nan,1,1,75,1,75))])),couple(integer,string),[nodeid(pos(nan,1,1,71,1,75))]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,81,1,81))])),couple(couple(integer,string),boolean),[nodeid(pos(nan,1,1,71,1,81))]),b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,85,1,85))])),pred,[nodeid(pos(nan,1,1,71,1,85))])),pred,[nodeid(pos(nan,1,1,1,1,85))]),b(member(b(couple(b(couple(b(identifier(y),integer,[nodeid(pos(nan,1,1,89,1,89))]),b(string(b),string,[nodeid(pos(nan,1,1,93,1,93))])),couple(integer,string),[nodeid(pos(nan,1,1,89,1,93))]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,99,1,99))])),couple(couple(integer,string),boolean),[nodeid(pos(nan,1,1,89,1,99))]),b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,104,1,104))])),pred,[nodeid(pos(nan,1,1,89,1,104))])),pred,[nodeid(pos(nan,1,1,1,1,104))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,108,1,108))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,110,1,110))])),pred,[nodeid(pos(nan,1,1,108,1,110))])),pred,[nodeid(pos(nan,1,1,1,1,110))])),pred,[used_ids([b,b2,s,x,y])])). |
| 1388 | | % #(f,v,x).(((f : POW((INTEGER * BOOL) * INTEGER) & v : INTEGER) & x : INTEGER) & ((f = {(11 |-> TRUE) |-> 3,(10 |-> TRUE) |-> 4,(2 |-> FALSE) |-> 5,(3 |-> FALSE) |-> v} & x |-> FALSE : dom(f)) & x |-> TRUE : dom(f))) |
| 1389 | | must_fail_clpfd_det(117,b(exists([b(identifier(f),set(couple(couple(integer,boolean),integer)),[]),b(identifier(v),integer,[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(couple(b(couple(b(integer(11),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])),couple(integer,boolean),[nodeid(pos(nan,1,1,5,1,10))]),b(integer(3),integer,[nodeid(pos(nan,1,1,17,1,17))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,5,1,17))]),b(couple(b(couple(b(integer(10),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))])),couple(integer,boolean),[nodeid(pos(nan,1,1,20,1,25))]),b(integer(4),integer,[nodeid(pos(nan,1,1,32,1,32))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,20,1,32))]),b(couple(b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,39,1,39))])),couple(integer,boolean),[nodeid(pos(nan,1,1,35,1,39))]),b(integer(5),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,35,1,47))]),b(couple(b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,53,1,53))])),couple(integer,boolean),[nodeid(pos(nan,1,1,49,1,53))]),b(identifier(v),integer,[nodeid(pos(nan,1,1,61,1,61))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,49,1,61))])]),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,4,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,66,1,66))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,70,1,70))])),couple(integer,boolean),[nodeid(pos(nan,1,1,66,1,70))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,82,1,82))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,78,1,83))])),pred,[nodeid(pos(nan,1,1,66,1,83))])),pred,[nodeid(pos(nan,1,1,1,1,83))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,87,1,87))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,91,1,91))])),couple(integer,boolean),[nodeid(pos(nan,1,1,87,1,91))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,102,1,102))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,98,1,103))])),pred,[nodeid(pos(nan,1,1,87,1,103))])),pred,[nodeid(pos(nan,1,1,1,1,103))])),pred,[used_ids([f,v,x])])). |
| 1390 | | % #(f,x).((f : POW((INTEGER * BOOL) * INTEGER) & x : INTEGER) & ((f = {((2|->FALSE)|->5),((3|->FALSE)|->77),((10|->TRUE)|->4),((11|->TRUE)|->3)} & x |-> FALSE : dom(f)) & x |-> TRUE : dom(f))) |
| 1391 | | must_fail_clpfd_det(118,b(exists([b(identifier(f),set(couple(couple(integer,boolean),integer)),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(value(avl_set(node(((int(3),pred_false),int(77)),true,1,node(((int(2),pred_false),int(5)),true,0,empty,empty),node(((int(10),pred_true),int(4)),true,1,empty,node(((int(11),pred_true),int(3)),true,0,empty,empty))))),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,4,1,63))])),pred,[nodeid(pos(nan,1,1,1,1,63))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,67,1,67))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,71,1,71))])),couple(integer,boolean),[nodeid(pos(nan,1,1,67,1,71))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,83,1,83))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,79,1,84))])),pred,[nodeid(pos(nan,1,1,67,1,84))])),pred,[nodeid(pos(nan,1,1,1,1,84))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,88,1,88))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,92,1,92))])),couple(integer,boolean),[nodeid(pos(nan,1,1,88,1,92))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,103,1,103))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,99,1,104))])),pred,[nodeid(pos(nan,1,1,88,1,104))])),pred,[nodeid(pos(nan,1,1,1,1,104))])),pred,[used_ids([f,x])])). |
| 1392 | | % #(a,v1,v2,w).((((a : POW(struct(x:INTEGER * INTEGER,y:INTEGER)) & v1 : INTEGER) & v2 : INTEGER) & w : INTEGER) & ((a = {rec(x:1 |-> 33,y:22),rec(x:2 |-> 34,y:44),rec(x:3 |-> 34,y:45)} & rec(x:v1 |-> v2,y:w) : a) & (v1 + v2) + w < 56)) |
| 1393 | | must_fail_clpfd_det(119,b(exists([b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[]),b(identifier(v1),integer,[]),b(identifier(v2),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(rec([field(x,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(33),integer,[nodeid(pos(nan,1,1,15,1,15))])),couple(integer,integer),[nodeid(pos(nan,1,1,12,1,17))])),field(y,b(integer(22),integer,[nodeid(pos(nan,1,1,21,1,21))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,6,1,23))]),b(rec([field(x,b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(integer(34),integer,[nodeid(pos(nan,1,1,34,1,34))])),couple(integer,integer),[nodeid(pos(nan,1,1,31,1,36))])),field(y,b(integer(44),integer,[nodeid(pos(nan,1,1,40,1,40))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,25,1,42))]),b(rec([field(x,b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,51,1,51))]),b(integer(34),integer,[nodeid(pos(nan,1,1,53,1,53))])),couple(integer,integer),[nodeid(pos(nan,1,1,50,1,55))])),field(y,b(integer(45),integer,[nodeid(pos(nan,1,1,59,1,59))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,44,1,61))])]),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,5,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(rec([field(x,b(couple(b(identifier(v1),integer,[nodeid(pos(nan,1,1,73,1,73))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,76,1,76))])),couple(integer,integer),[nodeid(pos(nan,1,1,72,1,78))])),field(y,b(identifier(w),integer,[nodeid(pos(nan,1,1,82,1,82))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,66,1,83))]),b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,85,1,85))])),pred,[nodeid(pos(nan,1,1,66,1,85))])),pred,[nodeid(pos(nan,1,1,1,1,85))]),b(less(b(add(b(add(b(identifier(v1),integer,[nodeid(pos(nan,1,1,89,1,89))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,92,1,92))])),integer,[nodeid(pos(nan,1,1,89,1,92))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,95,1,95))])),integer,[nodeid(pos(nan,1,1,89,1,95))]),b(integer(56),integer,[nodeid(pos(nan,1,1,98,1,98))])),pred,[nodeid(pos(nan,1,1,89,1,98))])),pred,[nodeid(pos(nan,1,1,1,1,98))])),pred,[used_ids([a,v1,v2,w])])). |
| 1394 | | % #(n,r1,a,b).((((n : INTEGER & r1 : POW(struct(x:INTEGER,y:INTEGER))) & a : INTEGER) & b : INTEGER) & ((({x|x : struct(x:INTEGER,y:INTEGER) & #(vv,ww).((x = rec(x:ww,y:vv) & vv : 1 .. n) & ww : 33 .. 34)} = r1 & n = 50) & rec(x:a,y:b) : r1) & rec(x:a + 2,y:b) : r1)) |
| 1395 | | must_fail_clpfd_det(120,b(exists([b(identifier(n),integer,[]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(comprehension_set([b(identifier(x),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,12,1,12)),introduced_by(comprehension_set)])],b(exists([b(identifier(vv),integer,[nodeid(pos(nan,1,1,6,1,6)),introduced_by(comprehension_set)]),b(identifier(ww),integer,[nodeid(pos(nan,1,1,9,1,9)),introduced_by(comprehension_set)])],b(conjunct(b(conjunct(b(equal(b(identifier(x),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,14,1,14)),introduced_by(comprehension_set)]),b(rec([field(x,b(identifier(ww),integer,[nodeid(pos(nan,1,1,22,1,22)),introduced_by(comprehension_set)])),field(y,b(identifier(vv),integer,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(comprehension_set)]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,16,1,29))])),pred,[nodeid(pos(nan,1,1,14,1,29))]),b(member(b(identifier(vv),integer,[nodeid(pos(nan,1,1,33,1,33)),introduced_by(comprehension_set)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,36,1,36))]),b(identifier(n),integer,[nodeid(pos(nan,1,1,39,1,39))])),set(integer),[nodeid(pos(nan,1,1,36,1,39))])),pred,[nodeid(pos(nan,1,1,33,1,39))])),pred,[nodeid(pos(nan,1,1,14,1,39))]),b(member(b(identifier(ww),integer,[nodeid(pos(nan,1,1,43,1,43)),introduced_by(comprehension_set)]),b(interval(b(integer(33),integer,[nodeid(pos(nan,1,1,46,1,46))]),b(integer(34),integer,[nodeid(pos(nan,1,1,50,1,50))])),set(integer),[nodeid(pos(nan,1,1,46,1,50))])),pred,[nodeid(pos(nan,1,1,43,1,50))])),pred,[nodeid(pos(nan,1,1,14,1,50))])),pred,[used_ids([n,vv,ww,x])])),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,1,1,53))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,1,1,55))]),b(equal(b(identifier(n),integer,[nodeid(pos(nan,1,1,60,1,60))]),b(integer(50),integer,[nodeid(pos(nan,1,1,62,1,62))])),pred,[nodeid(pos(nan,1,1,60,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(rec([field(x,b(identifier(a),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(y,b(identifier(b),integer,[nodeid(pos(nan,1,1,78,1,78))]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,68,1,79))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,81,1,81))])),pred,[nodeid(pos(nan,1,1,68,1,81))])),pred,[nodeid(pos(nan,1,1,1,1,81))]),b(member(b(rec([field(x,b(add(b(identifier(a),integer,[nodeid(pos(nan,1,1,92,1,92))]),b(integer(2),integer,[nodeid(pos(nan,1,1,94,1,94))])),integer,[nodeid(pos(nan,1,1,92,1,94))])),field(y,b(identifier(b),integer,[nodeid(pos(nan,1,1,98,1,98))]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,86,1,99))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,101,1,101))])),pred,[nodeid(pos(nan,1,1,86,1,101))])),pred,[nodeid(pos(nan,1,1,1,1,101))])),pred,[used_ids([a,b,n,r1])])). |
| 1396 | | % #(x,y).(y : INTEGER & (((rec(f:x) /= rec(f:y) & x : 1 .. 2) & y = 2) & rec(f:x) /= rec(f:1))) |
| 1397 | | must_fail_clpfd_det(121,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(rec([field(f,b(identifier(x),integer,[nodeid(pos(nan,1,1,7,1,7))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,1,1,8))]),b(rec([field(f,b(identifier(y),integer,[nodeid(pos(nan,1,1,19,1,19))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,13,1,20))])),pred,[nodeid(pos(nan,1,1,1,1,20))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,24,1,24))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(integer(2),integer,[nodeid(pos(nan,1,1,29,1,29))])),set(integer),[nodeid(pos(nan,1,1,26,1,29))])),pred,[nodeid(pos(nan,1,1,24,1,29))])),pred,[nodeid(pos(nan,1,1,1,1,29))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(integer(2),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[nodeid(pos(nan,1,1,33,1,35))])),pred,[nodeid(pos(nan,1,1,1,1,35))]),b(not_equal(b(rec([field(f,b(identifier(x),integer,[nodeid(pos(nan,1,1,45,1,45))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,39,1,46))]),b(rec([field(f,b(integer(1),integer,[nodeid(pos(nan,1,1,57,1,57))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,51,1,58))])),pred,[nodeid(pos(nan,1,1,39,1,58))])),pred,[nodeid(pos(nan,1,1,1,1,58))])),pred,[used_ids([x,y])])). |
| 1398 | | % #(x,y).(y : INTEGER & ((((x |-> (1 |-> 2)) /= (y |-> (1 |-> 2)) & x : 1 .. 2) & y = 2) & (x |-> (1 |-> 2)) /= (1 |-> (1 |-> 2)))) |
| 1399 | | must_fail_clpfd_det(122,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,2,1,2))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(2),integer,[nodeid(pos(nan,1,1,7,1,7))])),couple(integer,integer),[nodeid(pos(nan,1,1,4,1,8))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,9))]),b(couple(b(identifier(y),integer,[nodeid(pos(nan,1,1,15,1,15))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,18,1,18))]),b(integer(2),integer,[nodeid(pos(nan,1,1,20,1,20))])),couple(integer,integer),[nodeid(pos(nan,1,1,17,1,21))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,14,1,22))])),pred,[nodeid(pos(nan,1,1,1,1,22))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(2),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[nodeid(pos(nan,1,1,1,1,31))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(integer(2),integer,[nodeid(pos(nan,1,1,37,1,37))])),pred,[nodeid(pos(nan,1,1,35,1,37))])),pred,[nodeid(pos(nan,1,1,1,1,37))]),b(not_equal(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,42,1,42))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(2),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,41,1,49))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,55,1,55))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,58,1,58))]),b(integer(2),integer,[nodeid(pos(nan,1,1,60,1,60))])),couple(integer,integer),[nodeid(pos(nan,1,1,57,1,61))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,54,1,62))])),pred,[nodeid(pos(nan,1,1,41,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))])),pred,[used_ids([x,y])])). |
| 1400 | | % #(y,v).(v : INTEGER & (((rec(a:y,b:1,c:1 |-> 2) /= rec(a:v,b:1,c:1 |-> 2) & y : 1 .. 2) & v = 1) & rec(a:1,b:y,c:1 |-> 2) /= rec(a:v,b:2,c:1 |-> 2))) |
| 1401 | | must_fail_clpfd_det(123,b(exists([b(identifier(y),integer,[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(rec([field(a,b(identifier(y),integer,[nodeid(pos(nan,1,1,8,1,8))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,12,1,12))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(2),integer,[nodeid(pos(nan,1,1,19,1,19))])),couple(integer,integer),[nodeid(pos(nan,1,1,16,1,20))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,2,1,21))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,30,1,30))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,34,1,34))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,39,1,39))]),b(integer(2),integer,[nodeid(pos(nan,1,1,41,1,41))])),couple(integer,integer),[nodeid(pos(nan,1,1,38,1,42))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,24,1,43))])),pred,[nodeid(pos(nan,1,1,2,1,43))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,48,1,48))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(2),integer,[nodeid(pos(nan,1,1,53,1,53))])),set(integer),[nodeid(pos(nan,1,1,50,1,53))])),pred,[nodeid(pos(nan,1,1,48,1,53))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(equal(b(identifier(v),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(integer(1),integer,[nodeid(pos(nan,1,1,59,1,59))])),pred,[nodeid(pos(nan,1,1,57,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))]),b(not_equal(b(rec([field(a,b(integer(1),integer,[nodeid(pos(nan,1,1,70,1,70))])),field(b,b(identifier(y),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,79,1,79))]),b(integer(2),integer,[nodeid(pos(nan,1,1,81,1,81))])),couple(integer,integer),[nodeid(pos(nan,1,1,78,1,82))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,64,1,83))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,92,1,92))])),field(b,b(integer(2),integer,[nodeid(pos(nan,1,1,96,1,96))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,101,1,101))]),b(integer(2),integer,[nodeid(pos(nan,1,1,103,1,103))])),couple(integer,integer),[nodeid(pos(nan,1,1,100,1,104))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,86,1,105))])),pred,[nodeid(pos(nan,1,1,64,1,105))])),pred,[nodeid(pos(nan,1,1,1,1,106))])),pred,[used_ids([v,y])])). |
| 1402 | | % #(b,y,v).((b : BOOL & v : INTEGER) & ((((b = bool(rec(a:y,b:1,c:1 |-> 2) /= rec(a:v,b:1,c:1 |-> 2)) & y : 1 .. 2) & v = 1) & rec(a:1,b:y,c:1 |-> 2) /= rec(a:v,b:2,c:1 |-> 2)) & b = TRUE)) |
| 1403 | | must_fail_clpfd_det(124,b(exists([b(identifier(b),boolean,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,1,1,1))]),b(convert_bool(b(not_equal(b(rec([field(a,b(identifier(y),integer,[nodeid(pos(nan,1,1,14,1,14))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,18,1,18))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,23,1,23))]),b(integer(2),integer,[nodeid(pos(nan,1,1,25,1,25))])),couple(integer,integer),[nodeid(pos(nan,1,1,22,1,26))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,8,1,27))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,36,1,36))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,40,1,40))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(2),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,30,1,49))])),pred,[nodeid(pos(nan,1,1,8,1,49))])),boolean,[nodeid(pos(nan,1,1,3,1,50))])),pred,[nodeid(pos(nan,1,1,1,1,50))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,54,1,54))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,56,1,56))]),b(integer(2),integer,[nodeid(pos(nan,1,1,59,1,59))])),set(integer),[nodeid(pos(nan,1,1,56,1,59))])),pred,[nodeid(pos(nan,1,1,54,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))]),b(equal(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(integer(1),integer,[nodeid(pos(nan,1,1,65,1,65))])),pred,[nodeid(pos(nan,1,1,63,1,65))])),pred,[nodeid(pos(nan,1,1,1,1,65))]),b(not_equal(b(rec([field(a,b(integer(1),integer,[nodeid(pos(nan,1,1,76,1,76))])),field(b,b(identifier(y),integer,[nodeid(pos(nan,1,1,80,1,80))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,85,1,85))]),b(integer(2),integer,[nodeid(pos(nan,1,1,87,1,87))])),couple(integer,integer),[nodeid(pos(nan,1,1,84,1,88))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,70,1,89))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,98,1,98))])),field(b,b(integer(2),integer,[nodeid(pos(nan,1,1,102,1,102))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,107,1,107))]),b(integer(2),integer,[nodeid(pos(nan,1,1,109,1,109))])),couple(integer,integer),[nodeid(pos(nan,1,1,106,1,110))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,92,1,111))])),pred,[nodeid(pos(nan,1,1,70,1,111))])),pred,[nodeid(pos(nan,1,1,1,1,112))]),b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,116,1,116))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,118,1,118))])),pred,[nodeid(pos(nan,1,1,116,1,118))])),pred,[nodeid(pos(nan,1,1,1,1,118))])),pred,[used_ids([b,v,y])])). |
| 1404 | | % #(a,v1,v2,w).((((a : POW(struct(x:INTEGER * INTEGER,y:INTEGER,z:BOOL)) & v1 : INTEGER) & v2 : INTEGER) & w : INTEGER) & ((a = {rec(x:1 |-> 33,y:22,z:FALSE),rec(x:2 |-> 34,y:44,z:TRUE),rec(x:3 |-> 34,y:45,z:TRUE)} & rec(x:v1 |-> v2,y:w,z:TRUE) : a) & (v1 + v2) + w < 57)) |
| 1405 | | must_fail_clpfd_det(125,b(exists([b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[]),b(identifier(v1),integer,[]),b(identifier(v2),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(rec([field(x,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(33),integer,[nodeid(pos(nan,1,1,15,1,15))])),couple(integer,integer),[nodeid(pos(nan,1,1,12,1,17))])),field(y,b(integer(22),integer,[nodeid(pos(nan,1,1,21,1,21))])),field(z,b(boolean_false,boolean,[nodeid(pos(nan,1,1,26,1,26))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,6,1,31))]),b(rec([field(x,b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,40,1,40))]),b(integer(34),integer,[nodeid(pos(nan,1,1,42,1,42))])),couple(integer,integer),[nodeid(pos(nan,1,1,39,1,44))])),field(y,b(integer(44),integer,[nodeid(pos(nan,1,1,48,1,48))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,53,1,53))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,33,1,57))]),b(rec([field(x,b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,66,1,66))]),b(integer(34),integer,[nodeid(pos(nan,1,1,68,1,68))])),couple(integer,integer),[nodeid(pos(nan,1,1,65,1,70))])),field(y,b(integer(45),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,79,1,79))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,59,1,83))])]),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,5,1,84))])),pred,[nodeid(pos(nan,1,1,1,1,84))]),b(member(b(rec([field(x,b(couple(b(identifier(v1),integer,[nodeid(pos(nan,1,1,95,1,95))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,98,1,98))])),couple(integer,integer),[nodeid(pos(nan,1,1,94,1,100))])),field(y,b(identifier(w),integer,[nodeid(pos(nan,1,1,104,1,104))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,108,1,108))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,88,1,112))]),b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,114,1,114))])),pred,[nodeid(pos(nan,1,1,88,1,114))])),pred,[nodeid(pos(nan,1,1,1,1,114))]),b(less(b(add(b(add(b(identifier(v1),integer,[nodeid(pos(nan,1,1,118,1,118))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,121,1,121))])),integer,[nodeid(pos(nan,1,1,118,1,121))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,124,1,124))])),integer,[nodeid(pos(nan,1,1,118,1,124))]),b(integer(57),integer,[nodeid(pos(nan,1,1,127,1,127))])),pred,[nodeid(pos(nan,1,1,118,1,127))])),pred,[nodeid(pos(nan,1,1,1,1,127))])),pred,[used_ids([a,v1,v2,w])])). |
| 1406 | | % #(x).(x : INTEGER & ((((x > 0 & x mod 50 = 0) & x mod 61 = 0) & x mod 23 = 0) & x < 70150)) |
| 1407 | | must_fail_clpfd_det(126,b(exists([b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(integer(0),integer,[nodeid(pos(nan,1,1,5,1,5))])),pred,[nodeid(pos(nan,1,1,1,1,5))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,10,1,10))]),b(integer(50),integer,[nodeid(pos(nan,1,1,16,1,16))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,10,1,16))]),b(integer(0),integer,[nodeid(pos(nan,1,1,20,1,20))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,10,1,20))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,20))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,24,1,24))]),b(integer(61),integer,[nodeid(pos(nan,1,1,30,1,30))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,24,1,30))]),b(integer(0),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,24,1,35))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,35))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,39,1,39))]),b(integer(23),integer,[nodeid(pos(nan,1,1,45,1,45))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,39,1,45))]),b(integer(0),integer,[nodeid(pos(nan,1,1,50,1,50))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,39,1,50))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,50))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,54,1,54))]),b(integer(70150),integer,[nodeid(pos(nan,1,1,56,1,56))])),pred,[nodeid(pos(nan,1,1,54,1,56))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,56))])),pred,[used_ids([x])])). |
| 1408 | | % #(x,B,C).(((x : INTEGER & B : INTEGER) & C : BOOL) & (((((({x} : POW({101,102})) <=> B < 20 & x > 103) & B > 0) & B < 100) & (B = 19) <=> (C = TRUE)) & (C = FALSE => B < 20))) |
| 1409 | | must_fail_clpfd_det(127,b(exists([b(identifier(x),integer,[]),b(identifier('B'),integer,[]),b(identifier('C'),boolean,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equivalence(b(member(b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,3,1,3))])]),set(integer),[nodeid(pos(nan,1,1,2,1,4))]),b(pow_subset(b(value(avl_set(node(int(101),true,1,empty,node(int(102),true,0,empty,empty)))),set(integer),[nodeid(pos(nan,1,1,10,1,18))])),set(set(integer)),[nodeid(pos(nan,1,1,6,1,19))])),pred,[nodeid(pos(nan,1,1,2,1,19))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,25,1,25))]),b(integer(20),integer,[nodeid(pos(nan,1,1,27,1,27))])),pred,[nodeid(pos(nan,1,1,25,1,27))])),pred,[nodeid(pos(nan,1,1,2,1,27))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(integer(103),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[nodeid(pos(nan,1,1,33,1,35))])),pred,[nodeid(pos(nan,1,1,1,1,35))]),b(greater(b(identifier('B'),integer,[nodeid(pos(nan,1,1,40,1,40))]),b(integer(0),integer,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,40,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,46,1,46))]),b(integer(100),integer,[nodeid(pos(nan,1,1,48,1,48))])),pred,[nodeid(pos(nan,1,1,46,1,48))])),pred,[nodeid(pos(nan,1,1,1,1,48))]),b(equivalence(b(equal(b(identifier('B'),integer,[nodeid(pos(nan,1,1,55,1,55))]),b(integer(19),integer,[nodeid(pos(nan,1,1,57,1,57))])),pred,[nodeid(pos(nan,1,1,55,1,57))]),b(equal(b(identifier('C'),boolean,[nodeid(pos(nan,1,1,64,1,64))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,66,1,66))])),pred,[nodeid(pos(nan,1,1,64,1,66))])),pred,[nodeid(pos(nan,1,1,55,1,66))])),pred,[nodeid(pos(nan,1,1,1,1,70))]),b(implication(b(equal(b(identifier('C'),boolean,[nodeid(pos(nan,1,1,75,1,75))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,77,1,77))])),pred,[nodeid(pos(nan,1,1,75,1,77))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,86,1,86))]),b(integer(20),integer,[nodeid(pos(nan,1,1,88,1,88))])),pred,[nodeid(pos(nan,1,1,86,1,88))])),pred,[nodeid(pos(nan,1,1,75,1,88))])),pred,[nodeid(pos(nan,1,1,1,1,90))])),pred,[used_ids(['B','C',x])])). |
| 1410 | | |
| 1411 | | % Eval Time: 10 ms (0 ms walltime) |
| 1412 | | % #(r,x,y,z).(((r : POW((INTEGER * INTEGER) * INTEGER) & x : INTEGER) & z : INTEGER) & (((r = {((1|->2)|->3),((3|->4)|->5),((6|->7)|->8),((9|->10)|->11),((12|->13)|->14)} & (x |-> y) |-> z : r) & y : 10 .. 13) & z < 11)) |
| 1413 | | must_fail_clpfd_det(128,b(let_predicate([b(identifier(r),set(couple(couple(integer,integer),integer)),[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])],[b(value(avl_set(node(((int(6),int(7)),int(8)),true,0,node(((int(1),int(2)),int(3)),true,1,empty,node(((int(3),int(4)),int(5)),true,0,empty,empty)),node(((int(9),int(10)),int(11)),true,1,empty,node(((int(12),int(13)),int(14)),true,0,empty,empty))))),set(couple(couple(integer,integer),integer)),[nodeid(pos(29,-1,1,93,1,168))])],b(exists([b(identifier(x),integer,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)]),b(identifier(y),integer,[do_not_optimize_away,nodeid(pos(5,-1,1,7,1,7)),introduced_by(exists)]),b(identifier(z),integer,[do_not_optimize_away,nodeid(pos(6,-1,1,9,1,9)),introduced_by(exists)])],b(conjunct(b(conjunct(b(member(b(couple(b(couple(b(identifier(x),integer,[nodeid(pos(58,-1,1,173,1,173)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(59,-1,1,179,1,179)),introduced_by(exists)])),couple(integer,integer),[nodeid(pos(57,-1,1,173,1,179))]),b(identifier(z),integer,[nodeid(pos(60,-1,1,186,1,186)),introduced_by(exists)])),couple(couple(integer,integer),integer),[nodeid(pos(56,-1,1,173,1,186))]),b(identifier(r),set(couple(couple(integer,integer),integer)),[nodeid(pos(61,-1,1,190,1,190)),introduced_by(exists)])),pred,[nodeid(pos(55,-1,1,173,1,190))]),b(member(b(identifier(y),integer,[nodeid(pos(63,-1,1,195,1,195)),introduced_by(exists)]),b(interval(b(integer(10),integer,[nodeid(pos(65,-1,1,199,1,200))]),b(integer(13),integer,[nodeid(pos(66,-1,1,205,1,206))])),set(integer),[nodeid(pos(64,-1,1,199,1,206))])),pred,[nodeid(pos(62,-1,1,195,1,206))])),pred,[]),b(less(b(identifier(z),integer,[nodeid(pos(68,-1,1,211,1,211)),introduced_by(exists)]),b(integer(11),integer,[nodeid(pos(69,-1,1,215,1,216))])),pred,[nodeid(pos(67,-1,1,211,1,216))])),pred,[])),pred,[used_ids([r])])),pred,[nodeid(pos(2,-1,1,1,1,218))])). |
| 1414 | | |
| 1415 | | % Eval Time: 0 ms (0 ms walltime) |
| 1416 | | % #(f,a,b,c,x,r).(((((a : INTEGER & b : INTEGER) & c : INTEGER) & x : INTEGER) & r : INTEGER) & ((((((((f : 11 .. 23 +-> 1 .. 10 & f = {a |-> 2,b |-> 3,c |-> 4}) & card({a,b,c}) = 3) & f(x) = r) & a > b) & b > c) & x /= a) & /* falsity */ x /= x) & r /= b)) |
| 1417 | | must_fail_clpfd_det(129,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(x),integer,[]),b(identifier(r),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(11,-1,1,1,1,1))]),b(partial_function(b(interval(b(integer(11),integer,[nodeid(pos(14,-1,1,5,1,6))]),b(integer(23),integer,[nodeid(pos(15,-1,1,9,1,10))])),set(integer),[nodeid(pos(13,-1,1,5,1,10))]),b(interval(b(integer(1),integer,[nodeid(pos(17,-1,1,16,1,16))]),b(integer(10),integer,[nodeid(pos(18,-1,1,19,1,20))])),set(integer),[nodeid(pos(16,-1,1,16,1,20))])),set(set(couple(integer,integer))),[nodeid(pos(12,-1,1,5,1,20))])),pred,[nodeid(pos(10,-1,1,1,1,20))]),b(equal(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(20,-1,1,24,1,24))]),b(set_extension([b(couple(b(identifier(a),integer,[nodeid(pos(23,-1,1,29,1,29))]),b(integer(2),integer,[nodeid(pos(24,-1,1,33,1,33))])),couple(integer,integer),[nodeid(pos(22,-1,1,29,1,33))]),b(couple(b(identifier(b),integer,[nodeid(pos(26,-1,1,36,1,36))]),b(integer(3),integer,[nodeid(pos(27,-1,1,40,1,40))])),couple(integer,integer),[nodeid(pos(25,-1,1,36,1,40))]),b(couple(b(identifier(c),integer,[nodeid(pos(29,-1,1,43,1,43))]),b(integer(4),integer,[nodeid(pos(30,-1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(28,-1,1,43,1,47))])]),set(couple(integer,integer)),[nodeid(pos(21,-1,1,28,1,48))])),pred,[nodeid(pos(19,-1,1,24,1,48))])),pred,[nodeid(pos(9,-1,1,1,1,48))]),b(equal(b(card(b(set_extension([b(identifier(a),integer,[nodeid(pos(34,-1,1,58,1,58))]),b(identifier(b),integer,[nodeid(pos(35,-1,1,60,1,60))]),b(identifier(c),integer,[nodeid(pos(36,-1,1,62,1,62))])]),set(integer),[nodeid(pos(33,-1,1,57,1,63))])),integer,[nodeid(pos(32,-1,1,52,1,64))]),b(integer(3),integer,[nodeid(pos(37,-1,1,66,1,66))])),pred,[nodeid(pos(31,-1,1,52,1,66))])),pred,[nodeid(pos(8,-1,1,1,1,66))]),b(equal(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(40,-1,1,70,1,70))]),b(identifier(x),integer,[nodeid(pos(41,-1,1,72,1,72))])),integer,[contains_wd_condition,nodeid(pos(39,-1,1,70,1,73))]),b(identifier(r),integer,[nodeid(pos(42,-1,1,75,1,75))])),pred,[contains_wd_condition,nodeid(pos(38,-1,1,70,1,75))])),pred,[contains_wd_condition,nodeid(pos(7,-1,1,1,1,75))]),b(greater(b(identifier(a),integer,[nodeid(pos(44,-1,1,79,1,79))]),b(identifier(b),integer,[nodeid(pos(45,-1,1,81,1,81))])),pred,[nodeid(pos(43,-1,1,79,1,81))])),pred,[contains_wd_condition,nodeid(pos(6,-1,1,1,1,81))]),b(greater(b(identifier(b),integer,[nodeid(pos(47,-1,1,85,1,85))]),b(identifier(c),integer,[nodeid(pos(48,-1,1,87,1,87))])),pred,[nodeid(pos(46,-1,1,85,1,87))])),pred,[contains_wd_condition,nodeid(pos(5,-1,1,1,1,87))]),b(not_equal(b(identifier(x),integer,[nodeid(pos(50,-1,1,91,1,91))]),b(identifier(a),integer,[nodeid(pos(51,-1,1,94,1,94))])),pred,[nodeid(pos(49,-1,1,91,1,94))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,94))]),b(falsity,pred,[was(not_equal(b(identifier(x),integer,[nodeid(pos(53,-1,1,98,1,98))]),b(identifier(x),integer,[nodeid(pos(54,-1,1,101,1,101))]))),nodeid(pos(52,-1,1,98,1,101))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,101))]),b(not_equal(b(identifier(r),integer,[nodeid(pos(56,-1,1,105,1,105))]),b(identifier(b),integer,[nodeid(pos(57,-1,1,108,1,108))])),pred,[nodeid(pos(55,-1,1,105,1,108))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,108))])),pred,[used_ids([]),contains_wd_condition])). |
| 1418 | | |
| 1419 | | % Eval Time: 10 ms (0 ms walltime) |
| 1420 | | % #(f,aa,x,y,r,v).((f : POW(INTEGER * (INTEGER * INTEGER)) & r : INTEGER * INTEGER) & ((((((f = {aa |-> (1 |-> aa),x |-> (2 |-> x + 1),y |-> (3 |-> y + 1)} & x : 1 .. 2) & aa : 0 .. 1) & y : 3 .. 5) & r = f(v)) & v : 2 .. 4) & prj1(INTEGER,INTEGER)(r) /: 2 .. 3)) |
| 1421 | | % REQUIRES TRY_FIND_ABORT=FALSE |
| 1422 | | must_fail_clpfd_det(130,b(exists([b(identifier(f),set(couple(integer,couple(integer,integer))),[]),b(identifier(aa),integer,[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(r),couple(integer,integer),[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(integer,couple(integer,integer))),[nodeid(pos(9,-1,1,1,1,1))]),b(set_extension([b(couple(b(identifier(aa),integer,[nodeid(pos(12,-1,1,6,1,7))]),b(couple(b(integer(1),integer,[nodeid(pos(14,-1,1,12,1,12))]),b(identifier(aa),integer,[nodeid(pos(15,-1,1,14,1,15))])),couple(integer,integer),[nodeid(pos(13,-1,1,11,1,16))])),couple(integer,couple(integer,integer)),[nodeid(pos(11,-1,1,6,1,16))]),b(couple(b(identifier(x),integer,[nodeid(pos(17,-1,1,19,1,19))]),b(couple(b(integer(2),integer,[nodeid(pos(19,-1,1,24,1,24))]),b(add(b(identifier(x),integer,[nodeid(pos(21,-1,1,26,1,26))]),b(integer(1),integer,[nodeid(pos(22,-1,1,28,1,28))])),integer,[nodeid(pos(20,-1,1,26,1,28))])),couple(integer,integer),[nodeid(pos(18,-1,1,23,1,29))])),couple(integer,couple(integer,integer)),[nodeid(pos(16,-1,1,19,1,29))]),b(couple(b(identifier(y),integer,[nodeid(pos(24,-1,1,32,1,32))]),b(couple(b(integer(3),integer,[nodeid(pos(26,-1,1,37,1,37))]),b(add(b(identifier(y),integer,[nodeid(pos(28,-1,1,39,1,39))]),b(integer(1),integer,[nodeid(pos(29,-1,1,41,1,41))])),integer,[nodeid(pos(27,-1,1,39,1,41))])),couple(integer,integer),[nodeid(pos(25,-1,1,36,1,42))])),couple(integer,couple(integer,integer)),[nodeid(pos(23,-1,1,32,1,42))])]),set(couple(integer,couple(integer,integer))),[nodeid(pos(10,-1,1,5,1,43))])),pred,[nodeid(pos(8,-1,1,1,1,43))]),b(member(b(identifier(x),integer,[nodeid(pos(31,-1,1,47,1,47))]),b(interval(b(integer(1),integer,[nodeid(pos(33,-1,1,49,1,49))]),b(integer(2),integer,[nodeid(pos(34,-1,1,52,1,52))])),set(integer),[nodeid(pos(32,-1,1,49,1,52))])),pred,[nodeid(pos(30,-1,1,47,1,52))])),pred,[nodeid(pos(7,-1,1,1,1,52))]),b(member(b(identifier(aa),integer,[nodeid(pos(36,-1,1,56,1,57))]),b(interval(b(integer(0),integer,[nodeid(pos(38,-1,1,59,1,59))]),b(integer(1),integer,[nodeid(pos(39,-1,1,62,1,62))])),set(integer),[nodeid(pos(37,-1,1,59,1,62))])),pred,[nodeid(pos(35,-1,1,56,1,62))])),pred,[nodeid(pos(6,-1,1,1,1,62))]),b(member(b(identifier(y),integer,[nodeid(pos(41,-1,1,66,1,66))]),b(interval(b(integer(3),integer,[nodeid(pos(43,-1,1,68,1,68))]),b(integer(5),integer,[nodeid(pos(44,-1,1,71,1,71))])),set(integer),[nodeid(pos(42,-1,1,68,1,71))])),pred,[nodeid(pos(40,-1,1,66,1,71))])),pred,[nodeid(pos(5,-1,1,1,1,71))]),b(equal(b(identifier(r),couple(integer,integer),[nodeid(pos(46,-1,1,75,1,75))]),b(function(b(identifier(f),set(couple(integer,couple(integer,integer))),[nodeid(pos(48,-1,1,79,1,79))]),b(identifier(v),integer,[nodeid(pos(49,-1,1,81,1,81))])),couple(integer,integer),[contains_wd_condition,nodeid(pos(47,-1,1,79,1,82))])),pred,[contains_wd_condition,nodeid(pos(45,-1,1,75,1,82))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,82))]),b(member(b(identifier(v),integer,[nodeid(pos(51,-1,1,86,1,86))]),b(interval(b(integer(2),integer,[nodeid(pos(53,-1,1,88,1,88))]),b(integer(4),integer,[nodeid(pos(54,-1,1,91,1,91))])),set(integer),[nodeid(pos(52,-1,1,88,1,91))])),pred,[nodeid(pos(50,-1,1,86,1,91))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,91))]),b(not_member(b(first_of_pair(b(identifier(r),couple(integer,integer),[nodeid(pos(60,-1,1,117,1,117))])),integer,[nodeid(pos(56,-1,1,95,1,118))]),b(interval(b(integer(2),integer,[nodeid(pos(62,-1,1,123,1,123))]),b(integer(3),integer,[nodeid(pos(63,-1,1,126,1,126))])),set(integer),[nodeid(pos(61,-1,1,123,1,126))])),pred,[nodeid(pos(55,-1,1,95,1,126))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,126))])),pred,[used_ids([]),contains_wd_condition])). |
| 1423 | | |
| 1424 | | % Eval Time: 0 ms (0 ms walltime) |
| 1425 | | % #(f,aa,x,y,r,v).((f : POW(INTEGER * struct(p1:INTEGER,p2:INTEGER)) & r : struct(p1:INTEGER,p2:INTEGER)) & ((((((f = {aa |-> rec(p1:1,p2:aa),x |-> rec(p1:2,p2:x + 1),y |-> rec(p1:3,p2:y + 1)} & x : 1 .. 2) & aa : 0 .. 1) & y : 3 .. 5) & r = f(v)) & v : 2 .. 4) & r'p1 /: 2 .. 3)) |
| 1426 | | % REQUIRES TRY_FIND_ABORT=FALSE |
| 1427 | | must_fail_clpfd_det(131,b(exists([b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[]),b(identifier(aa),integer,[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(r),record([field(p1,integer),field(p2,integer)]),[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(9,-1,1,1,1,1))]),b(set_extension([b(couple(b(identifier(aa),integer,[nodeid(pos(12,-1,1,6,1,7))]),b(rec([field(p1,b(integer(1),integer,[nodeid(pos(16,-1,1,18,1,18))])),field(p2,b(identifier(aa),integer,[nodeid(pos(19,-1,1,23,1,24))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(13,-1,1,11,1,25))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(11,-1,1,6,1,25))]),b(couple(b(identifier(x),integer,[nodeid(pos(21,-1,1,28,1,28))]),b(rec([field(p1,b(integer(2),integer,[nodeid(pos(25,-1,1,39,1,39))])),field(p2,b(add(b(identifier(x),integer,[nodeid(pos(29,-1,1,44,1,44))]),b(integer(1),integer,[nodeid(pos(30,-1,1,46,1,46))])),integer,[nodeid(pos(28,-1,1,44,1,46))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(22,-1,1,32,1,47))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(20,-1,1,28,1,47))]),b(couple(b(identifier(y),integer,[nodeid(pos(32,-1,1,50,1,50))]),b(rec([field(p1,b(integer(3),integer,[nodeid(pos(36,-1,1,61,1,61))])),field(p2,b(add(b(identifier(y),integer,[nodeid(pos(40,-1,1,66,1,66))]),b(integer(1),integer,[nodeid(pos(41,-1,1,68,1,68))])),integer,[nodeid(pos(39,-1,1,66,1,68))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(33,-1,1,54,1,69))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(31,-1,1,50,1,69))])]),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(10,-1,1,5,1,70))])),pred,[nodeid(pos(8,-1,1,1,1,70))]),b(member(b(identifier(x),integer,[nodeid(pos(43,-1,1,74,1,74))]),b(interval(b(integer(1),integer,[nodeid(pos(45,-1,1,76,1,76))]),b(integer(2),integer,[nodeid(pos(46,-1,1,79,1,79))])),set(integer),[nodeid(pos(44,-1,1,76,1,79))])),pred,[nodeid(pos(42,-1,1,74,1,79))])),pred,[nodeid(pos(7,-1,1,1,1,79))]),b(member(b(identifier(aa),integer,[nodeid(pos(48,-1,1,83,1,84))]),b(interval(b(integer(0),integer,[nodeid(pos(50,-1,1,86,1,86))]),b(integer(1),integer,[nodeid(pos(51,-1,1,89,1,89))])),set(integer),[nodeid(pos(49,-1,1,86,1,89))])),pred,[nodeid(pos(47,-1,1,83,1,89))])),pred,[nodeid(pos(6,-1,1,1,1,89))]),b(member(b(identifier(y),integer,[nodeid(pos(53,-1,1,93,1,93))]),b(interval(b(integer(3),integer,[nodeid(pos(55,-1,1,95,1,95))]),b(integer(5),integer,[nodeid(pos(56,-1,1,98,1,98))])),set(integer),[nodeid(pos(54,-1,1,95,1,98))])),pred,[nodeid(pos(52,-1,1,93,1,98))])),pred,[nodeid(pos(5,-1,1,1,1,98))]),b(equal(b(identifier(r),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(58,-1,1,102,1,102))]),b(function(b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(60,-1,1,106,1,106))]),b(identifier(v),integer,[nodeid(pos(61,-1,1,108,1,108))])),record([field(p1,integer),field(p2,integer)]),[contains_wd_condition,nodeid(pos(59,-1,1,106,1,109))])),pred,[contains_wd_condition,nodeid(pos(57,-1,1,102,1,109))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,109))]),b(member(b(identifier(v),integer,[nodeid(pos(63,-1,1,113,1,113))]),b(interval(b(integer(2),integer,[nodeid(pos(65,-1,1,115,1,115))]),b(integer(4),integer,[nodeid(pos(66,-1,1,118,1,118))])),set(integer),[nodeid(pos(64,-1,1,115,1,118))])),pred,[nodeid(pos(62,-1,1,113,1,118))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,118))]),b(not_member(b(record_field(b(identifier(r),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(69,-1,1,122,1,122))]),p1),integer,[nodeid(pos(68,-1,1,122,1,125))]),b(interval(b(integer(2),integer,[nodeid(pos(72,-1,1,130,1,130))]),b(integer(3),integer,[nodeid(pos(73,-1,1,133,1,133))])),set(integer),[nodeid(pos(71,-1,1,130,1,133))])),pred,[nodeid(pos(67,-1,1,122,1,133))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,133))])),pred,[used_ids([]),contains_wd_condition])). |
| 1428 | | |
| 1429 | | % Eval Time: 0 ms (0 ms walltime) |
| 1430 | | % #(x,a).((x = (IF a < 10 THEN 0 ELSE 5 END ) & x : 6 .. 10) & a : 1 .. 23) |
| 1431 | | must_fail_clpfd_det(132,b(exists([b(identifier(x),integer,[]),b(identifier(a),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(x),integer,[nodeid(pos(5,-1,1,1,1,1))]),b(if_then_else(b(less(b(identifier(a),integer,[nodeid(pos(8,-1,1,8,1,8))]),b(integer(10),integer,[nodeid(pos(9,-1,1,10,1,11))])),pred,[nodeid(pos(7,-1,1,8,1,11))]),b(integer(0),integer,[nodeid(pos(10,-1,1,18,1,18))]),b(integer(5),integer,[nodeid(pos(11,-1,1,25,1,25))])),integer,[nodeid(pos(6,-1,1,5,1,29))])),pred,[nodeid(pos(4,-1,1,1,1,29))]),b(member(b(identifier(x),integer,[nodeid(pos(13,-1,1,33,1,33))]),b(interval(b(integer(6),integer,[nodeid(pos(15,-1,1,35,1,35))]),b(integer(10),integer,[nodeid(pos(16,-1,1,38,1,39))])),set(integer),[nodeid(pos(14,-1,1,35,1,39))])),pred,[nodeid(pos(12,-1,1,33,1,39))])),pred,[nodeid(pos(3,-1,1,1,1,39))]),b(member(b(identifier(a),integer,[nodeid(pos(18,-1,1,43,1,43))]),b(interval(b(integer(1),integer,[nodeid(pos(20,-1,1,45,1,45))]),b(integer(23),integer,[nodeid(pos(21,-1,1,48,1,49))])),set(integer),[nodeid(pos(19,-1,1,45,1,49))])),pred,[nodeid(pos(17,-1,1,43,1,49))])),pred,[nodeid(pos(2,-1,1,1,1,49))])),pred,[used_ids([])])). |
| 1432 | | |
| 1433 | | % Eval Time: 0 ms (0 ms walltime) |
| 1434 | | % #(x,bb).((x : INTEGER & bb : BOOL) & (((IF x < 10 THEN TRUE ELSE bb END ) = FALSE & x < 20) & (IF x < 12 THEN FALSE ELSE bb END ) = TRUE)) |
| 1435 | | must_fail_clpfd_det(133,b(exists([b(identifier(x),integer,[]),b(identifier(bb),boolean,[])],b(conjunct(b(conjunct(b(equal(b(if_then_else(b(less(b(identifier(x),integer,[nodeid(pos(7,-1,1,4,1,4))]),b(integer(10),integer,[nodeid(pos(8,-1,1,6,1,7))])),pred,[nodeid(pos(6,-1,1,4,1,7))]),b(boolean_true,boolean,[nodeid(pos(9,-1,1,14,1,17))]),b(identifier(bb),boolean,[nodeid(pos(10,-1,1,24,1,25))])),boolean,[nodeid(pos(5,-1,1,1,1,29))]),b(boolean_false,boolean,[nodeid(pos(11,-1,1,33,1,37))])),pred,[nodeid(pos(4,-1,1,1,1,37))]),b(less(b(identifier(x),integer,[nodeid(pos(13,-1,1,41,1,41))]),b(integer(20),integer,[nodeid(pos(14,-1,1,43,1,44))])),pred,[nodeid(pos(12,-1,1,41,1,44))])),pred,[nodeid(pos(3,-1,1,1,1,44))]),b(equal(b(if_then_else(b(less(b(identifier(x),integer,[nodeid(pos(18,-1,1,51,1,51))]),b(integer(12),integer,[nodeid(pos(19,-1,1,53,1,54))])),pred,[nodeid(pos(17,-1,1,51,1,54))]),b(boolean_false,boolean,[nodeid(pos(20,-1,1,61,1,65))]),b(identifier(bb),boolean,[nodeid(pos(21,-1,1,72,1,73))])),boolean,[nodeid(pos(16,-1,1,48,1,77))]),b(boolean_true,boolean,[nodeid(pos(22,-1,1,81,1,84))])),pred,[nodeid(pos(15,-1,1,48,1,84))])),pred,[nodeid(pos(2,-1,1,1,1,84))])),pred,[used_ids([])])). |
| 1436 | | |
| 1437 | | :- endif. |
| 1438 | | |
| 1439 | | test_enabled(130) :- get_preference(find_abort_values,false). |
| 1440 | | test_enabled(131) :- get_preference(find_abort_values,false). |