/* A minimal FlatZinc interpreter for B-Prolog that just meets the requirements for MiniZinc Challenge 2011. It reuses the FlatZinc interpreter originally developed for ECLiPSe by Joachim Schimpf. by Neng-Fa Zhou, last updated July 31, 2011. The following global constraints should not be decomposed by mzn2fzn: all_different_int(A) count(A,V,N) element(I,A,V) cumulative(As,Ad,Ar,Cap) The following examples illustrate the two different ways to use the interpreter to solve "zebra.fzn": 1. load and run ?- load(flatzinc). ?- solve(zebra). 2. run as a command-line bp flatzinc.out -g "fzn_main,halt" zebra.fzn */ fzn_main:- get_main_args(L), (process_args(L,File),atom(File)-> true ; format("Usage: bp flatzinc.out -g main [-a-f] FlagZincFile~n"),halt ), format("% solving(~w)~n",[File]), solve(File). process_args([],_File):-!. process_args(['-a'|As],File):-!, global_set(fzn_all_solution,1), process_args(As,File). process_args(['-f'|As],File):-!, global_set(fzn_free_order,1), process_args(As,File). process_args(['-g',_|As],File):-!, process_args(As,File). process_args([File|As],File):- process_args(As,File). solve(File) :- format("% loading ~w~n",[File]), check_input_file(File,File1,"fzn"),!,% built-in in B-Prolog see(File1), fzn_interpret, seen. fzn_interpret:- new_hashtable(SymTable), read_flatzinc_item(Item), fzn_interpret(Item,SymTable,[],[],[]),!. fzn_interpret:- writeln('=====UNSATISFIABLE====='). % fzn_interpret(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(Item,SymTable,PVars,SVars,OutAnns):- % writeln(fzn_interpret(Item)),fail. fzn_interpret(satisfy(SolveAnns),SymTable,PVars,SVars,OutAnns) => proc_solve_annotations(satisfy,SolveAnns,SymTable,PVars,SVars,OutAnns,LabelGoal), % writeln(user,LabelGoal), % frozen(Frozen),writeln(user,Frozen), call(LabelGoal). fzn_interpret(minimize(SolveAnns,Expr),SymTable,PVars,SVars,OutAnns) => fzn_eval_expr(Expr,SymTable,Obj), proc_solve_annotations(minof(Obj),SolveAnns,SymTable,PVars,SVars,OutAnns,LabelGoal), call(LabelGoal). fzn_interpret(maximize(SolveAnns,Expr),SymTable,PVars,SVars,OutAnns) => fzn_eval_expr(Expr,SymTable,Obj), proc_solve_annotations(maxof(Obj),SolveAnns,SymTable,PVars,SVars,OutAnns,LabelGoal), call(LabelGoal). fzn_interpret((Type:IdentAnns)=Init,SymTable,PVars,SVars,OutAnns) => detach_annotations(IdentAnns,Ident,Anns), ( Type = array_of([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(Type,Ident,Anns,SymTable,PVars,PVars1,SVars,SVars1,OutAnns,OutAnns1,InitVal) ; fzn_declare_var(VarType,Ident,Anns,SymTable,PVars,PVars1,SVars,SVars1,OutAnns,OutAnns1), hashtable_get(SymTable,Ident,BPVar), BPVar=InitVal ) ; % a simple parameter fzn_eval_expr(Init,SymTable,BPVar), hashtable_put(SymTable,Ident,BPVar), PVars=PVars1,SVars=SVars1,OutAnns=OutAnns1 ), read_flatzinc_item(NItem), fzn_interpret(NItem,SymTable,PVars1,SVars1,OutAnns1). fzn_interpret((Type:IdentAnns),SymTable,PVars,SVars,OutAnns) => detach_annotations(IdentAnns,Ident,Anns), ( Type = array_of([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",[Ident]) ), read_flatzinc_item(NItem), fzn_interpret(NItem,SymTable,PVars1,SVars1,OutAnns1). fzn_interpret(constraint(ElmAnns),SymTable,PVars,SVars,OutAnns) => detach_annotations(ElmAnns,Constraint,_Anns), fzn_eval_expr(Constraint,SymTable,BPConstraint), call(BPConstraint), read_flatzinc_item(NItem), fzn_interpret(NItem,SymTable,PVars,SVars,OutAnns). fzn_interpret(predicate(_Elms),SymTable,PVars,SVars,OutAnns) => read_flatzinc_item(NItem), fzn_interpret(NItem,SymTable,PVars,SVars,OutAnns). fzn_declare_array(Max,ElmInstType,Ident,Anns,Init,SymTable,PVars0,PVars,OutAnns0,OutAnns):- functor(BPArr,v,Max), (ElmInstType = var(ElmType) ->true; ElmType = ElmInstType), hashtable_put(SymTable,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",[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) => fd_new_var(Var), fzn_register_var(int,Ident,Anns,SymTable,PVars0,PVars,SVars0,SVars,OutAnns0,OutAnns,Var). fzn_declare_var(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):- % writeln(Anns), hashtable_put(SymTable,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):- arg(I,BPArr,Var), 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) => fd_new_domain(Var). fzn_declare_array_var(Var,Min..Max) => domain(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=(_.._) => Result=Exp. % a set fzn_eval_expr(Ident,SymTable,Result),atom(Ident) => hashtable_get(SymTable,Ident,Result). fzn_eval_expr(X,_SymTable,Result),integer(X) => Result = X. fzn_eval_expr(FZElms,SymTable,Array),FZElms = [_|_] => length(FZElms,N), functor(Array,v,N), eval_fz_elms(FZElms,SymTable,1,Array). fzn_eval_expr(Ident[I0],SymTable,Elm) => fzn_eval_expr(I0,SymTable,I), ( integer(I) -> true ; fzn_error("Non-integer subscript ~w",[I])), hashtable_get(SymTable,Ident,Array), arg(I,Array,Elm). fzn_eval_expr(Comp,SymTable,Result) => functor(Comp,F,N), functor(BPComp,F,N), fzn_eval_expr_args(Comp,SymTable,BPComp,N), fzn_term_to_bp(BPComp,Result). fzn_eval_expr_args(_Comp,_SymTable,_BPComp,I):-I==0,!. fzn_eval_expr_args(Comp,SymTable,BPComp,I):- arg(I,Comp,A), fzn_eval_expr(A,SymTable,B), arg(I,BPComp,B), I1 is I-1, fzn_eval_expr_args(Comp,SymTable,BPComp,I1). eval_fz_elms([],_SymTable,_I,_Array). eval_fz_elms([E|Es],SymTable,I,Array):- fzn_eval_expr(E,SymTable,Elm), arg(I,Array,Elm), I1 is I+1, eval_fz_elms(Es,SymTable,I1,Array). %%% :-mode fzn_term_to_bp(+,-). fzn_term_to_bp(set_in(X,DomExp),(X in Dom)):-(DomExp='{}'(Dom)->true;DomExp=Dom). % Min..Max or {Dom} fzn_term_to_bp(set_in_reif(X,DomExp,B),((X in Dom) #<=> B)):-(DomExp='{}'(Dom)->true;DomExp=Dom). % fzn_term_to_bp(array_bool_and(Array,B),fd_minimum(L11,B)):-Array=..[_|L1],(L1==[]->L11=[1];L11=L1). fzn_term_to_bp(array_bool_or(Array,B),fd_maximum(L11,B)):-Array=..[_|L1],(L1==[]->L11=[0];L11=L1). % fzn_term_to_bp(array_bool_element(I,Array,E),element(I,List,E)):-Array=..[_|List]. fzn_term_to_bp(array_int_element(I,Array,E),element(I,List,E)):-Array=..[_|List]. fzn_term_to_bp(array_var_bool_element(I,Array,E),element(I,List,E)):-Array=..[_|List]. fzn_term_to_bp(array_var_int_element(I,Array,E),element(I,List,E)):-Array=..[_|List]. % fzn_term_to_bp(bool2int(X,Y),true):-X=Y. fzn_term_to_bp(bool_and(X,Y,Z),clp_interp_and(X,Y,Z)). %Z #= (X#/\Y) fzn_term_to_bp(bool_clause(Ps,Ns),(fd_maximum(L11,B1),fd_minimum(L22,B2),B1#>=B2)):- Ps=..[_|L1],Ns=..[_|L2], (L1==[]->L11=[0];L11=L1), (L2==[]->L22=[1];L22=L2). fzn_term_to_bp(bool_eq(X,Y),true):-X=Y. fzn_term_to_bp(bool_eq_reif(X,Y,B),reify_eq_constr(B,X,Y)). fzn_term_to_bp(bool_le(X,Y),X #=< Y). fzn_term_to_bp(bool_le_reif(X,Y,B),reify_ge_constr(B,Y,X)). fzn_term_to_bp(bool_lt(X,Y),X #< Y). fzn_term_to_bp(bool_lt_reif(X,Y,B),B#=(X #< Y)). fzn_term_to_bp(bool_not(X,Y),clp_interp_not(X,Y)). fzn_term_to_bp(bool_or(X,Y,Z),clp_interp_or(X,Y,Z)). %Z #= (X#\/Y) fzn_term_to_bp(bool_xor(X,Y,Z),clp_interp_xor(X,Y,Z)). %Z #= (X#\=Y) % fzn_term_to_bp(int_negate(X,Z),Z #= -X). fzn_term_to_bp(int_plus(X,Y,Z),Z #= X+Y). fzn_term_to_bp(int_minus(X,Y,Z),Z #= X-Y). fzn_term_to_bp(int_times(X,Y,Z),Z #= X*Y). fzn_term_to_bp(int_abs(X,Z),Z #= abs(X)). fzn_term_to_bp(int_div(Dividend,Divisor,Quotient),Quotient #= Dividend//Divisor). fzn_term_to_bp(int_mod(Dividend,Divisor,Remainder),Remainder #= Dividend mod Divisor). fzn_term_to_bp(int_min(X,Y,Z),Z #= min(X,Y)). fzn_term_to_bp(int_max(X,Y,Z),Z #= max(X,Y)). fzn_term_to_bp(int_eq(X,Y),true):-X = Y. fzn_term_to_bp(int_ne(X,Y),X#\=Y). fzn_term_to_bp(int_le(X,Y),X #=< Y). fzn_term_to_bp(int_lt(X,Y),X #< Y). fzn_term_to_bp(int_ge(X,Y),X #>= Y). fzn_term_to_bp(int_gt(X,Y),X #> Y). fzn_term_to_bp(int_eq_reif(X,Y,B),reify_eq_constr(B,X,Y)). fzn_term_to_bp(int_ne_reif(X,Y,B),reify_neq_constr(B,X,Y)). fzn_term_to_bp(int_le_reif(X,Y,B),reify_ge_constr(B,Y,X)). fzn_term_to_bp(int_lt_reif(X,Y,B),B #<=> (X #< Y)). fzn_term_to_bp(int_ge_reif(X,Y,B),reify_ge_constr(B,X,Y)). fzn_term_to_bp(int_gt_reif(X,Y,B),B #<=> (X #> Y)). fzn_term_to_bp(int_lin_eq(Cs,Xs,Rhs),CXs #= Rhs) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_ne(Cs,Xs,Rhs),CXs #\= Rhs):- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_le(Cs,Xs,Rhs),CXs #=< Rhs):- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_ge(Cs,Xs,Rhs),CXs #>= Rhs):- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_lt(Cs,Xs,Rhs),CXs #< Rhs):- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_gt(Cs,Xs,Rhs),CXs #> Rhs):- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_eq_reif(Cs,Xs,Rhs,B),B #<=> (CXs #= Rhs)) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_ne_reif(Cs,Xs,Rhs,B),B #<=> (CXs #\= Rhs)) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_le_reif(Cs,Xs,Rhs,B),B #<=> (CXs #=< Rhs)) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_ge_reif(Cs,Xs,Rhs,B),B #<=> (CXs #>= Rhs)) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_lt_reif(Cs,Xs,Rhs,B),B #<=> (CXs #< Rhs)) :- vector_sum(Cs,Xs,CXs). fzn_term_to_bp(int_lin_gt_reif(Cs,Xs,Rhs,B),B #<=> (CXs #> Rhs)) :- vector_sum(Cs,Xs,CXs). % global constraints fzn_term_to_bp(all_different_int(Vec),all_distinct(List)):-Vec=..[_|List]. fzn_term_to_bp(count(Vec,V,N),count(V,List,#=,N)):-Vec=..[_|List]. fzn_term_to_bp(cumulative(SVec,DVec,RVec,Cap),cumulative(SList,DList,RList,Cap)):- SVec=..[_|SList], DVec=..[_|DList], RVec=..[_|RList]. fzn_term_to_bp(element_int(I,Vec,Y),element(I,List,Y)):-Vec=..[_|List]. fzn_term_to_bp(element_bool(I,Vec,Y),element(I,List,Y)):-Vec=..[_|List]. vector_sum(Cs,Xs,CXs) :- functor(Cs,_,N), functor(Xs,_,N), vector_sum(Cs,Xs,CXs,1,N). vector_sum(Cs,Xs,CXs,N,N) => CXs=C*X, arg(N,Cs,C), arg(N,Xs,X). vector_sum(Cs,Xs,CXs,I,N) => CXs=(C*X+CXsR), arg(I,Cs,C), arg(I,Xs,X), I1 is I+1, vector_sum(Cs,Xs,CXsR,I1,N). %%%% % 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,LabelGoal):- detach_annotations(SolveAnns,_,Anns), (global_get(fzn_free_order,1) -> LabelCall=true; solve_annotations_to_label(Anns,SymTable,LabelCall)), reverse(PVars,RPVars), reverse(SVars,RSVars), reverse(OutAnns,ROutAnns), Enum=(LabelCall,labeling_ffc(RPVars),labeling_ffc(RSVars),fzn_output(ROutAnns)), (SolveType==satisfy-> (global_get(fzn_all_solution,1)-> LabelGoal=(Enum,global_set(fzn_solution_found,1),fail; (global_get(fzn_solution_found,1)->writeln('==========');writeln('=====UNSATISFIABLE====='))); LabelGoal=(Enum->true;writeln('=====UNSATISFIABLE====='))) ;SolveType=minof(Obj)-> LabelGoal=(minof(Enum,Obj,format("% obj = ~w~n",[Obj]))->writeln('=========='); writeln('=====UNSATISFIABLE=====')) ;SolveType=maxof(Obj) -> LabelGoal=(maxof(Enum,Obj,format("% obj = ~w~n",[Obj]))->writeln('=========='); writeln('=====UNSATISFIABLE=====')) ), writeln('% solving...'). solve_annotations_to_label([],_SymTable,Call) => Call=true. solve_annotations_to_label([SearchAnn|SearchAnns],SymTable,Call) => Call=(LabelCall1,LabelCall2), solve_annotation_to_label(SearchAnn,SymTable,LabelCall1), solve_annotations_to_label(SearchAnns,SymTable,LabelCall2). solve_annotation_to_label(bool_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Call) => solve_annotation_to_label(int_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Call). solve_annotation_to_label(int_search(FZVars,VarChoiceAnn,AssignmentAnn,_),SymTable,Call) => fzn_eval_expr(FZVars,SymTable,BPVec), BPVec=..[_|BPVars], fzn_to_bp_option(VarChoiceAnn,Options,Options1), fzn_to_bp_option(AssignmentAnn,Options1,[]), Call=labeling(Options,BPVars). solve_annotation_to_label(seq_search(SearchAnns),SymTable,Call) => solve_annotations_to_label(SearchAnns,SymTable,Call). 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_error("Unsupported solve annotation: ~w",[Ann]). fzn_error(Format,Ts):- format(Format,Ts), throw(fzn_interpretation_error). fzn_output([]) => format("----------~n"). fzn_output([output_var(Ident,Type,Var)|L]) => format("~w = ",[Ident]), fzn_write(Type,Var),writeln(';'), fzn_output(L). fzn_output([output_array(Ident,Ranges,ElmType,BPArr)|L]) => length(Ranges,Dim), format("~w = array~wd(",[Ident,Dim]), foreach(Range in Ranges,format("~w,",[Range])), fzn_write(ElmType,BPArr), format(");~n"), fzn_output(L). fzn_write(bool,Term):-integer(Term),!, (Term==1->write(true);write(false)). fzn_write(_,Term):-integer(Term),!, write(Term). fzn_write(Type,Term):- (ground(Term)-> functor(Term,_,N), write('['), fzn_write_array(Type,Term,1,N), write(']') ;fzn_error("fzn_write requires ground data: ~w",[Term])). fzn_write_array(Type,Array,N,N) => arg(N,Array,A), fzn_write(Type,A). fzn_write_array(Type,Array,I,N) => arg(I,Array,A), fzn_write(Type,A), write(','), I1 is I+1, fzn_write_array(Type,Array,I1,N). /* %---------------------------------------------------------------------- % BEGIN LICENSE BLOCK % Version: CMPL 1.1 % % The contents of this file are subject to the Cisco-style Mozilla Public % License Version 1.1 (the "License"); you may not use this file except % in compliance with the License. You may obtain a copy of the License % at www.eclipse-clp.org/license. % % Software distributed under the License is distributed on an "AS IS" % basis,WITHOUT WARRANTY OF ANY KIND,either express or implied. See % the License for the specific language governing rights and limitations % under the License. % % The Original Code is The Zinc Modelling Tools for ECLiPSe % The Initial Developer of the Original Code is Joachim Schimpf % with support from Cisco Systems and NICTA Victoria. % Portions created by the Initial Developer are % Copyright (C) 2007 Cisco Systems,Inc. All Rights Reserved. % % Contributor(s): Joachim Schimpf % % END LICENSE BLOCK %---------------------------------------------------------------------- % A parser for FlatZinc,based on 'Specification of FlatZinc' (Nov 7 2007). % It reads and returns one item at a time,as an ECLiPSe structure which % closely resembles the FZ input. % % For FlatZinc,it seems an item-wise parser is a good idea,since the % items can be processed one at a time by ECLiPSe to set up the model. */ read_flatzinc(File):- format("reading ~w~n",[File]), see(File), repeat, (read_flatzinc_item(Term)->writeln(Term),fail;true), seen. read_flatzinc_item(Term) :- tokenize_flatzinc_item(Tokens,[]), % fails on eof ( item(Term,Tokens,[]) -> true ; syntax_error("Syntax error in: ~w",[Tokens]) ). % Items -------------------------------- item(VarDecl) --> [var],!, non_array_ti_expr_tail(Type), expect(:), ident_anns(IdentAnns), ( [=] -> { VarDecl = ((var(Type):IdentAnns)=Value) }, non_array_flat_expr(Value) ; { VarDecl = (var(Type):IdentAnns) } ). item((Type:IdentAnns)=Value) --> non_array_ti_expr_tail(Type), [:],!, ident_anns(IdentAnns), expect(=), non_array_flat_expr(Value). item(Decl) --> [array],!, expect_list(['[',i(1),(..)]), int_literal(Max), expect_list([']',of]), array_decl_tail(array_of([1..Max],ElmType),ElmType,Decl). item(constraint(ElmAnns)) --> [constraint],!, constraint_elem(Elm), ( [::] -> { ElmAnns = ::(Elm,Anns) }, annotations_tail(Anns) ; { ElmAnns = Elm } ). item(Solve) --> [solve],!, ( [::] -> { SolveAnns = ::(solve,Anns) }, solve_annotations(Anns) ; { SolveAnns = solve } ), solve_kind(SolveAnns,Solve). item(output(List)) --> [output],!, expect('['), nonempty_output_elem_list(List). item(predicate(Pred)) --> [predicate],!, pred_decl(Pred). array_decl_tail(Type,InstElmType,Decl) --> [var],!, { InstElmType = var(ElmType) }, non_array_ti_expr_tail(ElmType), expect(:), ident_anns(IdentAnns), ( [=] -> { Decl = ((Type:IdentAnns) = Value) }, array_literal(Value) ; { Decl = (Type:IdentAnns) } ). array_decl_tail(Type,ElmType,(Type:IdentAnns)=Value) --> non_array_ti_expr_tail(ElmType), [:],!, ident_anns(IdentAnns), expect(=), array_literal(Value). constraint_elem(Elm) --> [ident(Ident),'('],!, nonempty_expr_list(Params), { Elm =.. [Ident|Params], % avoid clash with array subscript notation ( functor(Elm,subscript,2) -> syntax_error("Illegal constraint name: ~w",[Elm]) ; true ) }. constraint_elem(Elm) --> variable_expr(Elm). solve_kind(SolveAnns,satisfy(SolveAnns)) --> [satisfy],!. solve_kind(SolveAnns,minimize(SolveAnns,Expr)) --> [minimize],!, variable_expr(Expr). solve_kind(SolveAnns,maximize(SolveAnns,Expr)) --> [maximize],!, variable_expr(Expr). % Output-Item (obsolete) -------------------------------- output_elem(show(Expr)) --> [show],!, expect('('), flat_expr(Expr), expect(')'). output_elem(show_cond(E1,E2,E3)) --> [show_cond],!, expect('('), flat_expr(E1),expect(','), flat_expr(E2),expect(','), flat_expr(E3), expect(')'). output_elem(Expr) --> [str(Expr)]. nonempty_output_elem_list([E|Es]) --> output_elem(E), ( [','] -> output_elem_list(Es) ; expect(']'),{Es = []} ). output_elem_list(Es) --> ( [']'] -> {Es = []} ; nonempty_output_elem_list(Es) ). % Predicate-Decl -------------------------------- pred_decl(Pred) --> [ident(Ident),'('], nonempty_pred_args(Params), { Pred =.. [Ident|Params] }. nonempty_pred_args([E|Es]) --> pred_arg(E), ( [','] -> pred_args(Es) ; expect(')'),{Es = []} ). pred_args(Es) --> ( [')'] -> {Es = []} ; nonempty_pred_args(Es) ). pred_arg(TypeIdent) --> pred_arg_type(Type), ( [:] -> {TypeIdent = (Type:Ident)}, [ident(Ident)] ; {TypeIdent = Type} ). pred_arg_type(var(Type)) --> [var],!, non_array_ti_expr_tail(Type). pred_arg_type(Type) --> non_array_ti_expr_tail(Type). pred_arg_type(array_of([Range],VarElmType)) --> [array],!, expect('['), ( [int] -> {Range = int} ; {Range = 1..Max}, expect_list([i(1),(..)]),int_literal(Max) ), expect_list([']',of]), ( [var] -> {VarElmType=var(ElmType)} ; {VarElmType=ElmType} ), non_array_ti_expr_tail(ElmType). % Type-Inst -------------------------------- non_array_ti_expr_tail(Type) --> ( [set] -> { Type = set_of(ElmType) }, expect('of'), scalar_ti_expr_tail(ElmType) ; scalar_ti_expr_tail(Type) ). scalar_ti_expr_tail(bool) --> [bool],!. scalar_ti_expr_tail(int) --> [int],!. scalar_ti_expr_tail(float) --> [float],!. scalar_ti_expr_tail('{}'(Ints)) --> ['{'],!,nonempty_int_list(Ints). scalar_ti_expr_tail(Min..Max) --> int_literal(Min),!,expect(..),int_literal(Max). scalar_ti_expr_tail(Min..Max) --> float_literal(Min),!,expect(..),float_literal(Max). nonempty_int_list([E|Es]) --> int_literal(E), ( [','] -> int_list(Es) ; expect('}'),{Es = []} ). int_list(Es) --> ( ['}'] -> {Es = []} ; nonempty_int_list(Es) ). % Expressions -------------------------------- % Rules have been reordered such that cuts do not cut valid alternatives % (i.e. rules that match a prefix of another rule must come later). flat_expr(Expr) --> non_array_flat_expr(Expr),!. flat_expr(Expr) --> array_literal(Expr). non_array_flat_expr(Expr) --> set_literal(Expr),!. non_array_flat_expr(Expr) --> scalar_flat_expr(Expr). scalar_flat_expr(Expr) --> bool_literal(Expr),!. scalar_flat_expr(Expr) --> int_literal(Expr),!. scalar_flat_expr(Expr) --> float_literal(Expr),!. scalar_flat_expr(Expr) --> [str(Expr)],!. scalar_flat_expr(Expr) --> array_access_expr(Expr),!. scalar_flat_expr(Expr) --> [ident(Expr)]. int_flat_expr(Expr) --> int_literal(Expr),!. int_flat_expr(Expr) --> array_access_expr(Expr),!. int_flat_expr(Expr) --> [ident(Expr)]. variable_expr(Expr) --> array_access_expr(Expr),!. variable_expr(Expr) --> [ident(Expr)]. array_access_expr(Ident[Index]) --> [ident(Ident),'['], int_index_expr(Index), expect(']'). int_index_expr(Expr) --> [ident(Expr)],!. int_index_expr(Expr) --> int_literal(Expr). bool_literal(false) --> [false],!. bool_literal(true) --> [true]. int_literal(SignedInt) --> ( [-] -> [i(Int)],{SignedInt is -Int} ; [i(Int)],{SignedInt = Int} ). float_literal(SignedFloat) --> ( [-] -> [f(Float)],{SignedFloat is -Float} ; [f(Float)],{SignedFloat = Float} ). set_literal('{}'(List)) --> ['{'],!, sfe_list(List). set_literal(Min..Max) --> int_flat_expr(Min), [..],!, int_flat_expr(Max). nonempty_sfe_list([E|Es]) --> scalar_flat_expr(E), ( [','] -> sfe_list(Es) ; expect('}'),{Es = []} ). sfe_list(Es) --> ( ['}'] -> {Es = []} ; nonempty_sfe_list(Es) ). array_literal(Array) --> ['['],!, nafe_list(Array). nonempty_nafe_list([E|Es]) --> non_array_flat_expr(E), ( [','] -> nafe_list(Es) ; expect(']'),{Es = []} ). nafe_list(Es) --> ( [']'] -> {Es = []} ; nonempty_nafe_list(Es) ). % Miscellaneous Elements -------------------------------- ident_anns(IdentAnns) --> [ident(Ident)], ( [::] -> { IdentAnns = ::(Ident,Anns) }, annotations_tail(Anns) ; { IdentAnns = Ident } ). annotations_tail(Anns) --> annotation(Ann), ( [::] -> { Anns = ::(Ann,Anns1) }, annotations_tail(Anns1) ; { Anns = Ann } ). annotation(Ann) --> [ident(Ident)], ( ['('] -> nonempty_expr_list(Params), {Ann =.. [Ident|Params]} ; {Ann = Ident} ). solve_annotations(Anns) --> solve_annotation(Ann), ( [::] -> { Anns = ::(Ann,Anns1) }, solve_annotations(Anns1) ; { Anns = Ann } ). solve_annotation(Ann) --> [ident(seq_search)],!, ['('], ['['], comma_separated_annotations(Anns), [']'], [')'], % {Ann = .. [seq_search|Anns]}. {Ann = seq_search(Anns)}. solve_annotation(Ann) --> annotation(Ann). comma_separated_annotations(Anns) --> annotation(Ann), ([','] -> {Anns=[Ann|Anns1]}, comma_separated_annotations(Anns1) ; {Anns=[Ann]} ). nonempty_expr_list([E|Es]) --> flat_expr(E), ( [','] -> expr_list(Es) ; expect(')'),{Es = []} ). expr_list(Es) --> ( [')'] -> {Es = []} ; nonempty_expr_list(Es) ). % Auxiliaries ------------------------------ expect_list([]) --> []. expect_list([Token|Tokens]) --> expect(Token), expect_list(Tokens). expect(Expected) --> [Token], ( {Token == Expected} -> [] ; syntax_error("Unexpected Token,expected ~w,found ~w", [Expected,Token]) ). syntax_error(Message,Culprit) --> { syntax_error(Message,Culprit) }. syntax_error(Message,Culprit) :- format(user,"Syntax error: ",[]), format(user,Message,Culprit), nl(user), abort. %---------------------------------------------------------------------- % Tokenizer % Tokenize the input stream up until the next semicolon (or eof). % Return a list of tokens,not including the terminating semicolon. % On end-of-file,fail. %---------------------------------------------------------------------- tokenize_flatzinc_item(Tokens,TokensR) :- b_NEXT_TOKEN_ff(Type,BPToken), % B-Prolog's tokenizer Type\==8, tokenize_flatzinc_item(Type,BPToken,Tokens,TokensR). % fails on end-of-file,when Type=8 tokenize_flatzinc_item(8,_,Tokens,TokensR) => Tokens=TokensR. % end-of-file tokenize_flatzinc_item(7,_,Tokens,TokensR) => Tokens=TokensR. % semicolon tokenize_flatzinc_item(0,Punc,Tokens,TokensR) => % punctuation Tokens=[Punc|Tokens1], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). tokenize_flatzinc_item(1,Atom,Tokens,TokensR) => % Prolog var Tokens=[ident(Atom)|Tokens1], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). tokenize_flatzinc_item(3,I,Tokens,TokensR) => % integer Tokens=[i(I)|Tokens1], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). tokenize_flatzinc_item(4,Atom,Tokens,TokensR) => % atom (keyword(Atom)->Tokens=[Atom|Tokens1];Tokens=[ident(Atom)|Tokens1]), b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). tokenize_flatzinc_item(2,Atom,Tokens,TokensR) => % atom( (keyword(Atom)->Tokens=[Atom|Tokens1];Tokens=[ident(Atom)|Tokens1]), Tokens1=['('|Tokens2], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens2,TokensR). tokenize_flatzinc_item(5,_,Tokens,TokensR) => % end-of-clause '.' Tokens=['.'|Tokens1], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). tokenize_flatzinc_item(9,Str,Tokens,TokensR) => % string Tokens=[str(Str)|Tokens1], b_NEXT_TOKEN_ff(Type,BPToken), tokenize_flatzinc_item(Type,BPToken,Tokens1,TokensR). % This differs slightly from the keyword list provided in the Flatzinc spec. % We do not treat constraint names (like div,intersect) as keywords. % We treat relevant punctuation as keywords,everything else is an identifier. keyword(..). keyword(:). keyword(::). keyword(;). keyword(=). keyword(-). keyword(+). keyword(annotation). keyword(any). keyword(array). keyword(bool). keyword(case). keyword(constraint). keyword(else). keyword(elseif). keyword(endif). keyword(enum). keyword(false). keyword(float). keyword(function). keyword(if). keyword(include). keyword(int). keyword(let). keyword(list). keyword(maximize). keyword(minimize). keyword(of). keyword(output). % obsolete keyword(par). keyword(predicate). keyword(record). keyword(satisfy). keyword(set). keyword(show). % obsolete keyword(show_cond). % obsolete keyword(solve). keyword(string). keyword(test). keyword(then). keyword(true). keyword(tuple). keyword(type). keyword(var). keyword(where).