/* A minimal FlatZinc interpreter in Picat that just meets the requirements for MiniZinc Challenge 2013. It reuses the FlatZinc interpreter originally developed for ECLiPSe by Joachim Schimpf. ported to Picat by Neng-Fa Zhou with help by Hakan Kjellerstrand, July 2013. The following global constraints should not be decomposed by mzn2fzn: alldifferent/1, circuit/1, count_eq/3 (and friends) cumulative/4, element/3, subcircuit/1, The following examples illustrate the two different ways to use the interpreter to solve "zebra.fzn": 1. load and run Picat> load(flatzinc). Picat> main(["zebra"]). 2. run as a command-line picat flatzinc zebra */ import flatzinc_parser. import cp. /* use only ::/2 of cp */ import cp_connector. import sat_connector. main(Args) => get_global_map().put(fzn_num_solutions,0), (process_args(Args,File),nonvar(File) -> true ; printf("Usage: fzn_picat [-a][-f][-p N][-s][-n N] FlatZincFile%n"),halt ), printf("%% solving(%w)%n",File), get_global_map().put(count_solutions,0), if get_heap_map().has_key(fzn_show_stats) then statistics(runtime,_), statistics(backtracks, Backtracks1), fzn_interpret_file(File), statistics(backtracks, Backtracks2), statistics(runtime, [_,End]), T = End / 1000.0, Backtracks = Backtracks2 - Backtracks1, NSols = get_global_map().get(count_solutions), printf("%% CPU time %f seconds Backtracks: %d Solutions: %d%n", T, Backtracks, NSols) else fzn_interpret_file(File) end. process_args([],_File) => true. process_args(["-a"|As],File) => get_heap_map().put(fzn_all_solution,1), process_args(As,File). process_args(["-f"|As],File) => get_heap_map().put(fzn_free_order,1), process_args(As,File). process_args(["-s"|As],File) => get_heap_map().put(fzn_show_stats,1), process_args(As,File). process_args(["-p",_|As],File) => process_args(As,File). process_args(["-n",N|As],File) => % get N solutions NInt = N.to_integer(), if NInt > 0 then get_global_map().put(fzn_num_solutions,NInt), get_heap_map().put(fzn_all_solution,1) end, process_args(As,File). process_args([File|As],File1) => File1=File, process_args(As,File). fzn_interpret_file(File) => (append(_,".fzn",File) -> File1=File; File1 =File++".fzn"), printf("%% loading %s%n",File1), FD=open(File1), catch(fzn_interpret(FD),Exception, printf("%% %w%n",Exception)), close(FD). fzn_interpret(FD) ?=> new_map()=SymTable, read_flatzinc_item(FD) = Item, fzn_interpret(FD,Item,SymTable,[],[],[]). fzn_interpret(_FD) => % comes here if failure occurs during constraint generation println('=====UNSATISFIABLE====='). % fzn_interpret(FD,Item,SymTable,PVars,SVars,OutAnns) % Item: the current item % SymTable: the symbol table for arrays and variables % PVars: principal FD variables % SVars: secondary FD variables such as introduced and dependent variables % OutAnns: output annotations fzn_interpret(_FD,satisfy(SolveAnns),SymTable,PVars,SVars,OutAnns) => (get_heap_map().has_key(fzn_all_solution) -> proc_solve_annotations(all,SolveAnns,SymTable,PVars,SVars,OutAnns) ; proc_solve_annotations(one,SolveAnns,SymTable,PVars,SVars,OutAnns) ). fzn_interpret(_FD,minimize(SolveAnns,Expr),SymTable,PVars,SVars,OutAnns) => fzn_eval_expr(Expr,SymTable,Obj), proc_solve_annotations($min(Obj),SolveAnns,SymTable,PVars,SVars,OutAnns). fzn_interpret(_FD,maximize(SolveAnns,Expr),SymTable,PVars,SVars,OutAnns) => fzn_eval_expr(Expr,SymTable,Obj), proc_solve_annotations($max(Obj),SolveAnns,SymTable,PVars,SVars,OutAnns). fzn_interpret(FD,':'(Type,IdentAnns)=Init,SymTable,PVars,SVars,OutAnns) => detach_annotations(IdentAnns,Ident,Anns), ( Type = $array_of([range(1,Max)],ElmInstType) -> % initialised array-of-var,or partially initialised array-of-var fzn_declare_array(Max,ElmInstType,Ident,Anns,Init,SymTable,PVars,PVars1,OutAnns,OutAnns1), SVars=SVars1 ; Type = $var(VarType) -> fzn_eval_expr(Init,SymTable,InitVal), (ground(InitVal)-> fzn_register_var(VarType,Ident,Anns,SymTable,PVars,PVars1,SVars,SVars1,OutAnns,OutAnns1,InitVal) ; fzn_declare_var(VarType,Ident,Anns,SymTable,PVars,PVars1,SVars,SVars1,OutAnns,OutAnns1), SymTable.get(Ident)=BPVar, BPVar=InitVal ) ; % a simple parameter fzn_eval_expr(Init,SymTable,BPVar), SymTable.put(Ident,BPVar), PVars=PVars1,SVars=SVars1,OutAnns=OutAnns1 ), read_flatzinc_item(FD) = NItem, fzn_interpret(FD,NItem,SymTable,PVars1,SVars1,OutAnns1). fzn_interpret(FD,':'(Type,IdentAnns),SymTable,PVars,SVars,OutAnns) => detach_annotations(IdentAnns,Ident,Anns), ( Type = $array_of([range(1,Max)],ElmInstType) -> % an uninitialised array fzn_declare_array(Max,ElmInstType,Ident,Anns,_Init,SymTable,PVars,PVars1,OutAnns,OutAnns1), SVars=SVars1 ; Type = $var(VarType) -> fzn_declare_var(VarType,Ident,Anns,SymTable,PVars,PVars1,SVars,SVars1,OutAnns,OutAnns1) ; fzn_error("Uninitialized parameter: %w%n",Ident) ), read_flatzinc_item(FD) = NItem, fzn_interpret(FD,NItem,SymTable,PVars1,SVars1,OutAnns1). fzn_interpret(FD,constraint(ElmAnns),SymTable,PVars,SVars,OutAnns) => detach_annotations(ElmAnns,Constraint,_Anns), fzn_eval_expr(Constraint,SymTable,BPConstraint), (M=get_heap_map(), M.has_key(fzn_free_order), not M.has_key(fzn_all_solution) -> sat_connector.post(BPConstraint) ; cp_connector.post(BPConstraint) ), read_flatzinc_item(FD) = NItem, fzn_interpret(FD,NItem,SymTable,PVars,SVars,OutAnns). fzn_interpret(FD,predicate(_Elms),SymTable,PVars,SVars,OutAnns) => read_flatzinc_item(FD) = NItem, fzn_interpret(FD,NItem,SymTable,PVars,SVars,OutAnns). fzn_declare_array(Max,ElmInstType,Ident,Anns,Init,SymTable,PVars0,PVars,OutAnns0,OutAnns) => (Max==0 -> BPArr=v; BPArr = new_struct(v,Max)), (ElmInstType = $var(ElmType) ->true; ElmType = ElmInstType), SymTable.put(Ident,BPArr), (member($output_array(Ranges),Anns)-> OutAnns=[$output_array(Ident,Ranges,ElmType,BPArr)|OutAnns0] ; OutAnns=OutAnns0 ), (var(Init) -> fzn_declare_array_vars(ElmType,BPArr,1,Max,PVars0,PVars) ; ( fzn_eval_expr(Init,SymTable,BPArr), fzn_declare_array_vars(ElmType,BPArr,1,Max,PVars0,PVars) -> true ; fzn_error("Array initialization failed: %w%n",Ident) ) ). fzn_declare_var(bool,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns) => Var :: 0..1, fzn_register_var(bool,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var). fzn_declare_var(int,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns) => cp_connector.new_domain_var(Var), fzn_register_var(int,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var). fzn_declare_var(range(Min,Max),Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns) => Var :: Min..Max, fzn_register_var(int,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var). fzn_declare_var('{}'(Dom),Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns) => Var :: Dom, fzn_register_var(int,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var). fzn_register_var(Type,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var) => SymTable.put(Ident,Var), (membchk(var_is_introduced,Anns)-> PVars=PVars0,SVars=[Var|SVars0]; PVars=[Var|PVars0],SVars=SVars0 ), (membchk(output_var,Anns)-> OutAnns=[$output_var(Ident,Type,Var)|OutAnns0] ; OutAnns=OutAnns0 ). fzn_declare_array_vars(_Type,_BPArr,I,N,PVars0,PVars),I>N => PVars=PVars0. fzn_declare_array_vars(Type,BPArr,I,N,PVars0,PVars) => Var = BPArr[I], fzn_declare_array_var(Var,Type), (var(Var)->PVars1=[Var|PVars0];PVars1=PVars0), I1 is I+1, fzn_declare_array_vars(Type,BPArr,I1,N,PVars1,PVars). fzn_declare_array_var(Var,_), nonvar(Var) => true. fzn_declare_array_var(Var,bool) => Var :: 0..1. fzn_declare_array_var(Var,int) => cp_connector.new_domain_var(Var). fzn_declare_array_var(Var,range(Min,Max)) => Var :: Min..Max. fzn_declare_array_var(Var,'{}'(Dom)) => Var :: Dom. %%%% fzn_eval_expr(true,_SymTable,Result) => Result=1. fzn_eval_expr(false,_SymTable,Result) => Result=0. fzn_eval_expr([],_SymTable,Result) => Result=v. % an empty array fzn_eval_expr(Exp,_SymTable,Result),Exp='{}'(_) => Result=Exp. % a set fzn_eval_expr(Exp,_SymTable,Result),Exp=$range(_,_) => Result=Exp. % a set fzn_eval_expr(Ident,SymTable,Result),atom(Ident) => SymTable.get(Ident) = Result. fzn_eval_expr(X,_SymTable,Result),integer(X) => Result = X. fzn_eval_expr(FZElms,SymTable,Array),FZElms = [_|_] => FZElms.length = N, Array = new_struct(v,N), eval_fz_elms(FZElms,SymTable,1,Array). fzn_eval_expr(array_subscript(Ident,I0),SymTable,Elm) => fzn_eval_expr(I0,SymTable,I), ( integer(I) -> true ; fzn_error("Non-integer subscript %w%n",I)), SymTable.get(Ident)=Array, Array[I] = Elm. fzn_eval_expr(Comp,SymTable,Result) => N = Comp.length, BPComp = new_struct(Comp.name,N), fzn_eval_expr_args(Comp,SymTable,BPComp,N), Result=BPComp. fzn_eval_expr_args(_Comp,_SymTable,_BPComp,I),I==0 => true. fzn_eval_expr_args(Comp,SymTable,BPComp,I) => Comp[I] = A, fzn_eval_expr(A,SymTable,B), BPComp[I] = B, I1 is I-1, fzn_eval_expr_args(Comp,SymTable,BPComp,I1). eval_fz_elms([],_SymTable,_I,_Array) => true. eval_fz_elms([E|Es],SymTable,I,Array) => fzn_eval_expr(E,SymTable,Elm), Array[I] = Elm, I1 is I+1, eval_fz_elms(Es,SymTable,I1,Array). %%%% % Split ident and annotations and make a proper annotation list detach_annotations('::'(Ident0,Anns),Ident,AnnList) => Ident = Ident0, anns_to_list(Anns,AnnList). detach_annotations(IdentAnns,Ident,AnnList) => Ident = IdentAnns,AnnList = []. anns_to_list('::'(Ann,Anns),AnnList) => AnnList = [Ann|AnnList1], anns_to_list(Anns,AnnList1). anns_to_list(Ann,AnnList) => AnnList=[Ann]. proc_solve_annotations(SolveType,SolveAnns,SymTable,PVars,SVars,OutAnns) => append(PVars,SVars,AllVars), detach_annotations(SolveAnns,_,Anns), solve_annotations_to_label_args(Anns,SymTable,LabelCalls,[]), proc_solve(SolveType,LabelCalls,AllVars,OutAnns.reverse()). proc_solve(all,LabelCalls,AllVars,ROutAnns) ?=> cp_label_vars(LabelCalls,AllVars), fzn_output(ROutAnns), get_global_map().put(fzn_solution_found,1), FznNumSolutions = get_global_map().get(fzn_num_solutions), if FznNumSolutions == 0; get_global_map().get(count_solutions) < FznNumSolutions then fail end. proc_solve(all,_LabelCalls,_AllVars,_ROutAnns) => (get_global_map().has_key(fzn_solution_found) -> println('==========') ; println('=====UNSATISFIABLE=====') ). proc_solve(one,_LabelCalls,AllVars,ROutAnns), ready_to_use_sat => (sat_connector.call_solve([],AllVars) -> fzn_output(ROutAnns) ; println('=====UNSATISFIABLE=====') ). proc_solve(one,LabelCalls,AllVars,ROutAnns) => repost_sat_constrs_to_cp_if_any, (cp_label_vars(LabelCalls,AllVars) -> fzn_output(ROutAnns) ; println('=====UNSATISFIABLE=====') ). proc_solve(OpType@min(Obj),_LabelCalls,AllVars,ROutAnns), ready_to_use_sat => (sat_connector.call_solve($[OpType,report(fzn_output_obj(ROutAnns,Obj))],AllVars) -> printf("%% obj = %w%n",Obj), println('==========') ; println('=====UNSATISFIABLE=====') ). proc_solve(min(Obj),LabelCalls,AllVars,ROutAnns) => repost_sat_constrs_to_cp_if_any, (minof(cp_label_vars(LabelCalls,AllVars), Obj, fzn_output_obj(ROutAnns,Obj)) -> printf("%% obj = %w%n",Obj), println('==========') ; println('=====UNSATISFIABLE=====') ). proc_solve(OpType@max(Obj),_LabelCalls,AllVars,ROutAnns), ready_to_use_sat => (sat_connector.call_solve([OpType,$report(fzn_output_obj(ROutAnns,Obj))],AllVars) -> printf("%% obj = %w%n",Obj), println('==========') ; println('=====UNSATISFIABLE=====') ). proc_solve(max(Obj),LabelCalls,AllVars,ROutAnns) => repost_sat_constrs_to_cp_if_any, (maxof(cp_label_vars(LabelCalls,AllVars), Obj, fzn_output_obj(ROutAnns,Obj)) -> printf("%% obj = %w%n",Obj), println('==========') ; println('=====UNSATISFIABLE=====') ). repost_sat_constrs_to_cp_if_any => bp.cp_post_attached_constrs(_). % defined in B-Prolog, redirect all the constraints sent to SAT to CP ready_to_use_sat => M = get_heap_map(), M.has_key(fzn_free_order), not M.has_key(fzn_all_solution), not M.has_key(better_for_cp). %% use cp cp_label_vars(LabelCalls,AllVars) => foreach((Options,Vars) in LabelCalls) cp_connector.call_solve(Options,Vars, false) end, cp_connector.call_solve([],AllVars, true). solve_annotations_to_label_args([],_SymTable,Calls,CallsR) => Calls=CallsR. solve_annotations_to_label_args([SearchAnn|SearchAnns],SymTable,Calls,CallsR) => solve_annotation_to_label_args(SearchAnn,SymTable,Calls,Calls1), solve_annotations_to_label_args(SearchAnns,SymTable,Calls1,CallsR). solve_annotation_to_label_args(bool_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Calls,CallsR) => solve_annotation_to_label_args($int_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Calls,CallsR). solve_annotation_to_label_args(int_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Calls,CallsR) => fzn_eval_expr(FZVars,SymTable,BPVec), to_list(BPVec) = BPVars, fzn_to_bp_option(VarChoiceAnn,Options,Options1), fzn_to_bp_option(AssignmentAnn,Options1,[]), Calls=[(Options,BPVars)|CallsR]. solve_annotation_to_label_args(seq_search(SearchAnns),SymTable,Calls,CallsR) => solve_annotations_to_label_args(SearchAnns,SymTable,Calls,CallsR). fzn_to_bp_option(input_order,Os,OsR) => Os=OsR. fzn_to_bp_option(first_fail,Os,OsR) => Os=[ff|OsR]. fzn_to_bp_option(smallest,Os,OsR) => Os=[min|OsR]. fzn_to_bp_option(largest,Os,OsR) => Os=[max|OsR]. fzn_to_bp_option(occurrence,Os,OsR) => Os=[degree|OsR]. fzn_to_bp_option(most_constrained,Os,OsR) => Os=[ffc|OsR]. % fzn_to_bp_option(indomain,Os,OsR) => Os=OsR. fzn_to_bp_option(indomain_min,Os,OsR) => Os=OsR. fzn_to_bp_option(indomain_max,Os,OsR) => Os=[down|OsR]. fzn_to_bp_option(indomain_middle,Os,OsR) => Os=[updown|OsR]. fzn_to_bp_option(indomain_median,Os,OsR) => Os=[updown|OsR]. fzn_to_bp_option(indomain_split,Os,OsR) => Os=[split|OsR]. fzn_to_bp_option(indomain_reverse_split,Os,OsR) => Os=[reverse_split|OsR]. % fzn_to_bp_option(Ann,Os,OsR) => Os=OsR, fzn_warning("Unsupported solve annotation: %w%n",Ann). fzn_warning(Format,Arg) => print("%"), printf(Format,Arg). fzn_error(Format,Arg) => print("%"), printf(Format,Arg), throw(fzn_interpretation_error). %%%% fzn_output_obj(OutAnns,Obj) => printf("%% obj = %w%n",Obj), fzn_output(OutAnns). fzn_output([]) => println('----------'). fzn_output([output_var(Ident,Type,Var)|L]) => printf("%w = ",Ident), fzn_write(Type,Var), writeln(';'), fzn_output(L). fzn_output([output_array(Ident,Ranges,ElmType,BPArr)|L]) => length(Ranges) = Dim, printf("%w = array%wd(",Ident,Dim), foreach($range(Min,Max) in Ranges) printf("%w..%w,",Min,Max) end, fzn_write(ElmType,BPArr), println(");"), fzn_output(L). fzn_write(bool,Term), integer(Term) => (Term==1->write(true);write(false)). fzn_write(_,Term),integer(Term) => print(Term). fzn_write(Type,Term) => (ground(Term)-> Term.length = N, print('['), fzn_write_array(Type,Term,1,N), print(']') ; fzn_error("fzn_write requires ground data: %w%n",Term) ). fzn_write_array(Type,Array,N,N) => fzn_write(Type,Array[N]). fzn_write_array(Type,Array,I,N) => fzn_write(Type,Array[I]), print(','), I1 is I+1, fzn_write_array(Type,Array,I1,N).