%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% GASP 29/09/2008 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% SICSTUS 4 clpfd code for computing answer sets %%% Copia Destra @ by DE GRAPPA research group %%% Alessandro Dal Palu' Agostino Dovier %%% Enrico Pontelli Gianfranco Rossi %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Current limits: admitted predicates of arity 0, 1, 2, or 3 only. %%% All constants must be numbers between 0 and bigM-1 %%% Predicate arguments must be expressions with expected value in 0..bigM-1 %%% (e.g., q(a), p(f(0,1)) are not admitted) %%% It accepts "interval facts" (e.g. p(1..3)) %%% Note: To be soon extended with cardinality constraints %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Libraries, operators, and general parameters %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- use_module(library(clpfd)). :- use_module(library(lists)). :- use_module(library(terms)). :- use_module(library(file_systems)). :- op(200,fx,not). :- op(150,fx,'1'). :- op(100,xf,'1'). %%%%%%%%%%%%%%%%%%%%%%%%%%% %%% OPTIONAL: setting the working directory my_cd('C:/agostino/lavori/incorso/gasp'). :-my_cd(WD),file_systems:current_directory(_,WD). :-prolog_flag(unknown,_,fail). bigM(645). %%% NOTE: 645^3 < maxint for clpfd builtin('<'). %%% For arity 4 use 127 builtin('='). builtin('=='). builtin('neq'). %%% go/1 and /2 compute all stable models, go/3 one per time %%% They take the Program as input and computes stable model(s) %%% Launch as :- go('filename.lp'). [default: all solutions and printed] %%% or :- go('filename.lp',write). [The same] %%% or :- go('filename.lp',nowrite). [solutions are hidden] %%% or :- go('filename.lp',Model, write/nowrite) [One solution per time] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% go(Program) :- go(Program,write). go(Program,WriteFlag) :- go(Program,_,WriteFlag), fail. go(_,_) :- sol(N), statistics(runtime,[T,_]), it(IT), TotT is (T - IT)/1000, format("### Computed ~d stable model(s) in ~2F s ###\n",[N,TotT]), write('############################################ END'). go(Program,Model,WriteFlag) :- reset, read_program(Program,ProgList), empty_domains(ProgList,IniDoms), split_facts(ProgList,Facts,Rules,Flag), %%% separates facts and rules and writetime('### Loading time: '), %%% tests if it is definite (Flag) facts(Facts,IniDoms,FactDoms), %%% FactDoms: facts are true ( Flag=0, % definite tp(Rules,FactDoms,Model), writeln('### P is a definite program. Its minimum model is:'), write_model(WriteFlag,Model) ; (Flag=1;Flag=2), %%% =1 without constraints =2 with constraints wf(Rules, FactDoms, WFModel), ( wf_stable(WFModel,Flag),!, % writeln('### There is a wellfounded model'), write_model(WriteFlag,WFModel),!, Model=WFModel ; writeln('### There are no wellfounded models. ###'), fixpoint(Rules,WFModel,Model), writetime('### Next stable model computed in time: '),%%% write_model(WriteFlag,Model) ) ; Flag=3, %%% =3 with function(s) wf(Rules, FactDoms, WFModel), fun_fixpoint(Rules,WFModel,Model,Program), writetime('### Next Stable model computed in: '),%%% write_model(WriteFlag,Model) ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% MODELS: %%% Each predicate p of arity N is assigned to a term %%% - atom(p,N,POSDOM,NEGDOM) %%% where POSDOM,NEGDOM are fdsets. %%% - POSDOM is the set of true values for p %%% - NEGDOM is the set of false values for p %%% If the program is definite, then NEGDOM=[] %%% otherwise NEGDOM contains elements to satisfy negative %%% literals when looking for stable models %%% A model is a list of those atoms (actually, the list of POSDOM) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% For arity 0 predicates, DOM =[] means false, DOM = [0] true %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% empty_domains sets to [] all domains for non-builtin predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% empty_domains([],[]). empty_domains([rule(A,B,C)|R], DOMS) :- append([A,B,C], ATOMS), atom_dom(ATOMS, DOMS1), empty_domains(R, DOMS2), disj_union(DOMS1,DOMS2,DOMS). atom_dom([],[atom(false,0,[],[])]). %%% atom_dom([A|R],S) :- A =.. [P|_], builtin(P),!, atom_dom(R,S). atom_dom([A|R],[atom(P,N,[],[])|S]) :- A =.. [P|Args], length(Args,N), atom_dom(R,S). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Standard T_P of logic programming (see below notes for negative %%% literals) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% tp(ProgList,I,M) :- tp_step(ProgList,I,I1,0,F),!, %% tp_step is deterministic. (F=0,!, M = I1; %% we added a ! to avoid to enter tp(ProgList,I1,M)). %% failing occurrences of tp_step tp_step([],I,I,F,F). tp_step([Rule|ProgList],I,I1,F0,F2) :- apply_def_rule(Rule,I,Inew,F0,F1), tp_step(ProgList,Inew,I1,F1,F2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% update_dom computes the effect of T_P on a single rule %%%%% T_P considers also negation for its use in S.M. search %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% apply_def_rule(rule([H],PBody,NBody),I,[atom(F,ARITY,NEWPDOM,NEG)|PARTI],F0,F1) :- copy_term([H,PBody,NBody],[H1,PBody1,NBody1]), %%% variable renaming term_variables([H1,PBody1],VARS), %%% collect fresh vars bigM(M),M1 is M-1,domain(VARS,0,M1), %%% fix (wide) domains for the fresh vars H1 =..[F|ARGS], tuple_num(ARGS,VAR,ARITY), select(atom(F,ARITY,OLD,NEG),I,PARTI), %%% ( build_constraint(PBody1,I,1,pos), %%% C3 = 1 iff the positive body is satisfied by I build_constraint(NBody1,I,1,negknown), %%% C4 = 1 iff the negative body is satisfied by I nin_set(ARITY,VAR,OLD), %%% do not apply if head is already true nin_set(ARITY,VAR,NEG), %%% consistency check findall(X,(X #= VAR,labeling([ff],VARS)),[L|IST]), list_to_fdset([L|IST],SET), fdset_union(OLD,SET,NEWPDOM), F1=1, !; NEWPDOM=OLD, F1 = F0 ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% Computing Standard (definite) T_P %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% build_constraint returns a constraint that must hold for %%%% the rule is applied %%%% Negative literals treatment: if Sign=negknown, %%%% it is implemented as: %%%%% - A in T_P(I,J) iff (A :- B, not C) in P and %%%%% B in I and C in J %%%%% (I true facts, J false facts) %%%% Otherwise it is left as a constraint (neg) as called by %%%% the wellfounded part. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% build_constraint is used for computing wellfouned sets %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% build_constraint([R|Rs],I,C,Sign):- %%% Built-in ATOMS R =.. [F|ARGS], builtin(F),!, expression(F,ARGS,C2), C #<=> C2 #/\ C1, build_constraint(Rs,I,C1,Sign). build_constraint([R|Rs],I,C,Sign):- %%% Other ATOMS R =.. [F|ARGS],!, tuple_num(ARGS,VAR,ARITY), member(atom(F,ARITY,DOMF,NDOMF),I), ( Sign=neg,!, %%% Negative unknown nin_set(ARITY,VAR,DOMF,C2); Sign=pos,!, %%% Positive C2 #<=> VAR in_set DOMF; Sign=negknown, %%% Negative known C2 #<=> VAR in_set NDOMF ), build_constraint(Rs,I,C1,Sign), C #<=> C1 #/\ C2. build_constraint([],_,1,_). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% facts adds the domain values imposed by (ground) facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% facts([],DOMS,DOMS). facts([rule([A],[],[])|R],OLDDOMS,NEWDOMS) :- A =..[P|ARGS], tuple_num(ARGS,D,ARITY), select(atom(P,ARITY,PDOM,NEG),OLDDOMS,PARTDOMS), fdset_add_element(PDOM,D,NEWPDOM), facts(R,[atom(P,ARITY,NEWPDOM,NEG)|PARTDOMS],NEWDOMS). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% well founded models computed as described in: %%% Improving the Alternating Fixpoint: The Transformation Approach %%% by Zukowski, Brass, and Freitag %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% wf(ProgList,Empty, M) :- def_rules(ProgList,DefProg), alternating(DefProg, Empty,Empty,K0), %% K0 = lfp(T_P) alternating(ProgList, K0, Empty,U0), %% U0 = lpf(T_{P,K0}) wf(ProgList,Empty, K0, U0, M). wf(ProgList,Empty,Ki,Ui,M) :- alternating(ProgList, Ui, Empty,Ki1), % Ki1 = lfp(T_{P,U_{i}}) alternating(ProgList, Ki1,Empty,Ui1), % Ui1 = lfp(T_{P,K_i1}) (Ki1==Ki, Ui1==Ui, !, wellfoundedmodel(Ki,Ui,M); wf(ProgList,Empty,Ki1,Ui1,M)). %%% W*_P = K union {not(A) : A in U} wellfoundedmodel([],_,[]). wellfoundedmodel([atom(P,AR,PDOM,_)|K],U,[atom(P,AR,PDOM,NDOM)|M]) :- select(atom(P,AR,UDOM,_),U,RU), complement_set(AR,UDOM,NDOM), wellfoundedmodel(K,RU,M). alternating(ProgList,J,I,M) :- wf_step(ProgList,J,I,I1),!, (I == I1, !, M = I; alternating(ProgList,J,I1,M)). wf_step([],_J,I,I). wf_step([Rule|ProgList],J,I,I1) :- alternating_apply_rule(Rule,J,I,Inew), wf_step(ProgList,J,Inew,I1). %%% T_{P,J}(I) = { A : (A :- PBody, neg NBody) in P , %%% PBody \subseteq I and %%% NBody \cap J = \emptyset } alternating_apply_rule(rule([H],PBody,NBody),J,I,[atom(F,ARITY,NEWPDOM,NEG)|PARTI]) :- copy_term([H,PBody,NBody],[H1,PBody1,NBody1]), %%% variable renaming term_variables([H1,PBody1],VARS), %%% collect fresh vars bigM(M),M1 is M-1,domain(VARS,0,M1), %%% fix (wide) domains for the fresh vars build_constraint(PBody1,I,C1,pos), %%% C = 1 iff the body is satisfied by I build_constraint(NBody1,J,C2,neg), H1 =..[F|ARGS], tuple_num(ARGS,VAR,ARITY), select(atom(F,ARITY,OLD,NEG),I,PARTI), nin_set(ARITY,VAR,OLD,C3), %%% do not apply if head is already true %%% nin_set(ARITY,VAR,NEG,C4), %%% consistency check findall(X,(C1+C2+C3 #>= 3, X #= VAR,labeling([ff],VARS)),LIST), list_to_fdset(LIST,SET), fdset_union(OLD,SET,NEWPDOM). %%% Test if a well-founded model is complete, hence stable wf_stable([],_). wf_stable([atom(false,_,_,_)|M],1) :- %% particular case !, wf_stable(M,1). %% for constraints-free programs wf_stable([atom(_,AR,PDOM,NDOM)|M],Flag) :- complement_set(AR,PDOM,NDOM), wf_stable(M,Flag). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Non determinsitic fixpoint procedure. %%% lev_fixpoint is used to avoid some symmetries %%% e.g. equivalent sequences of independent rules applications %%% [e.g. (1,2) (2,1)] %%% A simpler fixpoint rule (slow_fixpoint) is at the end of the file %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Observe that the same atom can be introduce by two rules %%% (eg one chosen ND and the other by tp and vice versa) %%% In this case we compute several equal models. This is bad. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% fixpoint(Rules,I1,I2) :- lev_fixpoint(Rules,I1,I2,[],0). %%% This first clause of lev_fixpoint is redundant (the second is complete) %%% However, it avoids some recomputations of "collect_applicable_rules" lev_fixpoint(Rules,I1,I2, PrevRules,PrevIndex) :- length(PrevRules,N), N > 0, PrevIndex < N, !, P1 is PrevIndex + 1, ( Index in P1 .. N, nth1(Index,PrevRules,GRULE), apply_rule(GRULE, I1, M, _), tp(Rules,M,IN2), constraints_check(IN2), lev_fixpoint(Rules,IN2,I2,PrevRules,Index); %% lev_fixpoint(Rules,I1,I2,PrevRules,N) ). lev_fixpoint(Rules,I1,I2, PrevRules,PrevIndex) :- collect_applicable_rules(Rules,I1,ApplRules), %%% slow point (ApplRules=[], % tp(Rules,I1,IT1), % constraints_check(IT1), !, I2=I1; %%%IT1=I2; %% no rules -> stable model diff_list(ApplRules,PrevRules,NewRules), %%% diff_list -> n log n append(PrevRules,NewRules,NewLevelledRules), length(NewLevelledRules,N), P1 is PrevIndex + 1, Index in P1 .. N, nth1(Index,NewLevelledRules,GRULE), %% position according to order (deterministic!) apply_rule_1(GRULE, I1, IN, _), tp(Rules,IN,IN2), constraints_check(IN2), lev_fixpoint(Rules,IN2,I2,NewLevelledRules,Index)). %%%%%%%%% constraints_check/1 %%% Tests if the constraints are verified. %%% Observe that for each constraint :- Goal %%% we add a rule %%% false :- Goal, not false. %%% When false is present in a model -> %%% a constraint has been falsified (Goal is true in the Model) %%% Using apply_rule1 should be useless constraints_check(Model) :- member(atom(false,0,[],_),Model). %%%%% collect_applicable_rules/3 % collects all the applicable rules given the interpretation I. % Notice the (non standard) the use of findall/4 to avoid an append collect_applicable_rules([Rule|Rules],I,List):- collect_applicable_rules(Rules,I,B), findall(GroundRule,(apply_rule(Rule,I, M, GroundRule),constraints_check(M)),List,B). collect_applicable_rules([],_I,[]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% non deterministic rule application: apply_rule (_1) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% used for building the set of applicable rules (constraints included) %% cannot include apply_rule_1, otherwise if a constraint cannot be satisfied, %% it results that the rule is not applicable apply_rule(rule([H],Bpos,Bneg),I1,I2,rule([H1],Bpos1,Bneg1)) :- Bneg \= [], %%% Must have negative literals copy_term([H,Bpos,Bneg],[H1,Bpos1,Bneg1]), H1 =.. [F|ARGS], term_variables([H1,Bpos1],VARS), %%% All vars are in the positive part bigM(M), M1 is M-1, domain(VARS,0,M1), build_constraint(Bpos1,I1,1,pos), %%% 1 means positive part is satisfied build_constraint(Bneg1,I1,1,neg), %%% 1 means negative part is satisfied tuple_num(ARGS,Arg,ARITY), member(atom(F,ARITY,PDOM,_),I1), nin_set(ARITY,Arg,PDOM), %%% This avoids to use the same rule twice labeling([ff],VARS), %%% Positive part satisfied dom_update(Bneg1,I1,I2). %%% Update negative part %%% apply_rule_1 unfolds apply_rule optimizing the constraint case apply_rule_1(rule([false],Bpos,Bneg),I1,I2,rule([false],Bpos1,Bneg1)) :- !, Bneg \= [], %%% Must have negative literals copy_term([Bpos,Bneg],[Bpos1,Bneg1]), sub_list(Bneg1, BnegNOC, BnegC), BnegC=[_|_], %% at least one element in BnegC term_variables(Bpos1,VARS), %%% All vars are in the positive part bigM(M), M1 is M-1, domain(VARS,0,M1), build_constraint(Bpos1,I1,1,pos), %%% 1 means positive part is satisfied build_constraint(BnegNOC,I1,1,neg), %%% a part of the negative part is satisfied build_constraint(BnegC,I1,1,pos), %%% the rest is falsified labeling([ff],VARS), %%% Positive part satisfied dom_update(Bneg1,I1,I2). %%% Update negative part apply_rule_1(rule([H],Bpos,Bneg),I1,I2,rule([H1],Bpos1,Bneg1)) :- H\=false,!, Bneg \= [], %%% Must have negative literals copy_term([H,Bpos,Bneg],[H1,Bpos1,Bneg1]), H1 =.. [F|ARGS], term_variables([H1,Bpos1],VARS), %%% All vars are in the positive part bigM(M), M1 is M-1, domain(VARS,0,M1), build_constraint(Bpos1,I1,1,pos), %%% 1 means positive part is satisfied build_constraint(Bneg1,I1,1,neg), %%% 1 means negative part is satisfied tuple_num(ARGS,Arg,ARITY), member(atom(F,ARITY,PDOM,_),I1), nin_set(ARITY,Arg,PDOM), %%% This avoids to use the same rule twice labeling([ff],VARS), %%% Positive part satisfied dom_update(Bneg1,I1,I2). %%% Update negative part %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% domain updating %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% dom_update([],I,I). dom_update([A|R],I1,I2) :- A =.. [F|ARGS], tuple_num(ARGS,D,ARITY), select(atom(F,ARITY,PDOM,NEGDOM),I1,Irest), fdset_add_element(NEGDOM,D,NEWDOM), %% if D is already in NEGDOM dom_update(R,[atom(F,ARITY,PDOM,NEWDOM)|Irest],I2).%% then NEWDOM=NEGDOM %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% expression parses algebraic expressions into FD expressions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% expression(F,[TX,TY],C2) :- term_conv(TX,TERMX), term_conv(TY,TERMY), (F = '=', !, C2 #<=> TERMX #= TERMY; F = '==',!, C2 #<=> TERMX #= TERMY; F = '<', !, C2 #<=> TERMX #< TERMY; F = 'neq', !, C2 #<=> TERMX #\= TERMY). term_conv(V,V) :- var(V),!. term_conv(N,N) :- number(N),!. %% binary functions term_conv(TI,TO) :- TI =.. [OP,A,B],!, term_conv(A,A1), term_conv(B,B1), (OP = '+', !, TO #= A1 + B1; OP = '-', !, TO #= A1 - B1; OP = '/', !, TO #= A1 / B1; OP = 'mod',!, TO #= A1 mod B1; OP = '*', TO #= A1 * B1). %% unary functions term_conv(TI,TO) :- TI =.. [OP,A], term_conv(A,A1), OP = 'abs', !, TO #= abs(A1). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%% PARSING PHASE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %(ok)%%%%%%%%%%%%% read_program/2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% Given a prolog file name ProgFile %%%%% output a list of clauses in the form %%%%% rule([H],Body+,Body-) %%%%% where H is rule head atom %%%%% Body+ is the list of positive atoms in body %%%%% Body- is the list of atoms occuring negated in body %%%%% example ProgList=[rule([p],[q,r(X)],[s(X,a)]), %%% p :- q,r(X),not s(X,a). %%%%% rule([p],[],[q]), %%% p :- not q. %%%%% rule([],[a],[b]), ] %%% :- a, not b. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% read_program(ProgFile,ProgList) :- see(ProgFile), read_all(ProgList), writeln('### Program read without errors ###'), seen. read_all([Rule|ProgList]) :- read(Clause), Clause \== end_of_file, !, ( Clause = ('1'({ A : B })'1' :- C),!, %%% Aggregate clause split_pos_neg(C,P,N), %%% restricted syntax Rule = rule([A],[B|P],N) %%% Use with parsimony ; Clause = (A :- B),!, %% Rules with Body split_pos_neg(B,P,N), Rule = rule([A],P,N) ; Clause = (:- B),!, %%% Constraints split_pos_neg(B,P,N), %%% Introduced faked rules Rule = rule([false],P,[false|N]) ; Rule = rule([Clause],[],[])), %% Facts read_all(ProgList). read_all([]). %(ok)%%%%%%% input rules split_pos_neg/3 and split_facts/3 split_pos_neg((not C1,D),R1,[C1|R2]):- !, split_pos_neg(D,R1,R2). split_pos_neg((C,D),[C|R1],R2):- !, split_pos_neg(D,R1,R2). split_pos_neg(not A,[],[A]):- !. split_pos_neg(P,[P],[]). %%%% The 4th parameter of split_facts is %%%% 0 for definite program, %%%% 1 for general programs without constraints and %%%% 2 for programs with constraints or functions %%%% 3 for programs with functions split_facts([],[],[],0). split_facts([rule([INTERVAL],[],[])|ProgList], %%% This is the case of "domain" [rule([H1],[],[])|Facts], %%% predicates, such as p(1..3). [rule([H2],[H3, X = Y + 1, X < B + 1],[])|Rules],ND):- INTERVAL =.. [P,A..B], !, H1 =..[P,A], H2 =..[P,X], H3 =..[P,Y], split_facts(ProgList,Facts,Rules,ND). split_facts([rule([FUNCTION],_,_)|ProgList], Facts,Rules,3):- %%% case of functions FUNCTION =.. [assignment|_],!, split_facts(ProgList,Facts,Rules,_). split_facts([rule(A,[],[])|ProgList],[rule(A,[],[])|Facts],Rules,ND):- !, split_facts(ProgList,Facts,Rules,ND). split_facts([rule(A,B,[])|ProgList], Facts,[rule(A,B,[])|Rules],ND):- !, split_facts(ProgList,Facts,Rules,ND). split_facts([rule([false],B,C)|ProgList],Facts,[rule([false],B,C)|Rules],Flag):- !, split_facts(ProgList,Facts,Rules,ND), Flag is max(ND,2). split_facts([NRULE|ProgList], Facts,[NRULE|Rules],Flag):- split_facts(ProgList,Facts,Rules,ND), Flag is max(ND,1). def_rules([],[]). def_rules([rule(_,_,[_|_])|ProgList], Defrules) :- !, def_rules(ProgList,Defrules). def_rules([RULE|ProgList],[RULE|Defrules]) :- def_rules(ProgList,Defrules). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%% AUXILIARY PREDICATES %%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% tuple_num returns the code VAL associated to a tuple %%%% and the arity AR of a tuple %%%% it works for N <= 3. It is easy to be extended %%%% It is called by most of the predicates tuple_num(ARGS,VAL,ARITY) :- (ARGS = [],!, VAL=0, ARITY=0; ARGS = [VAL],!, ARITY=1; ARGS = [Arg1,Arg2],!, bigM(M), ARITY=2, VAL #= M*Arg1+Arg2; ARGS = [Arg1,Arg2,Arg3], bigM(M), ARITY=3, VAL #= M*M*Arg1+M*Arg2+Arg3). %%% num_tuple it the reverse function (from VAL to ARGS) num_tuple(ARGS,VAL,ARITY) :- (ARITY=0,!, ARGS = [], VAL=0 ; ARITY=1,!, ARGS = [VAL] ; ARITY=2,!, bigM(M), Arg1 is VAL//M, Arg2 is VAL mod M, ARGS = [Arg1,Arg2]; ARITY=3,!, bigM(M), Arg1 is VAL//(M*M), Arg2 is (VAL-Arg1*M*M)//M, Arg3 is VAL mod M, ARGS = [Arg1,Arg2,Arg3]). %%% pair_proj is biderectional and works for pairs pair_proj(PAIR,X,Y) :- bigM(M), PAIR #= M*X + Y, X #= PAIR/M, Y #= PAIR mod M. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% nin_set/4 sets the constraint C to 1 iff %% X is not in SET. %% nin_set/3 adds the constraint X is not in SET. nin_set(ARITY,X,SET,C) :- complement_set(ARITY,SET,COMPL), C #<=> X in_set COMPL. nin_set(ARITY,X,SET) :- complement_set(ARITY,SET,COMPL), X in_set COMPL. %% complement set computes the complement wrt a universe set %% of the fd_set UDOM. The universe set changes according to the %% arity complement_set(AR,UDOM,NDOM) :- bigM(M), (AR=0,!,VAL=0; AR=1,!,VAL is M -1; AR=2,!,VAL is M*M -1; AR=3,VAL is M*M*M -1), fdset_interval(Universe,0,VAL), fdset_subtract(Universe,UDOM,NDOM). %%% diff_list(X,Y,Z) returns in Z the list of elements in X and not in Y %%% nlogn version (if sort is n log n) diff_list(ApplRules,PrevRules,NewRules) :- sort(PrevRules,SortedPrevRules), %% SORT is not important here. sort(ApplRules,SortedApplRules), %% Only to fast the rest extract_new_rules(SortedPrevRules,SortedApplRules,NewRules). extract_new_rules([A|R1],[A|R2],R3):- !, extract_new_rules(R1,R2,R3). extract_new_rules([A|R1],[B|R2],R3):- compare(<,A,B),!, extract_new_rules(R1,[B|R2],R3). extract_new_rules([A|R1],[B|R2],[B|R3]):- % compare(>,A,B),!, extract_new_rules([A|R1],R2,R3). extract_new_rules([],A,A):-!. extract_new_rules(_,[],[]). %%% disj_union appends two lists and sort them without repetitions disj_union(A,B,C) :- append(A,B,D), sort(D,C). %%% remove_dups(D,C). %%% computes non-deterministically P(List) i.e. lists with elements from input list %%% third arg -> complement sub_list([],[],[]). sub_list([A|R],[A|R1],R2):- sub_list(R,R1,R2). sub_list([A|R],R1,[A|R2]):- sub_list(R,R1,R2). %%% increasing(List) :- lex_chain([List],[increasing]), labeling([],List). %%% Reset of global parameters (timings, number of solutions) reset :- statistics(runtime,[It,_]), %% RETRACT ALL VALUES retractall(sol(_)), retractall(it(_)), %% ASSERT INITIAL VALUES assert(sol(0)), assert(it(It)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%% PRINTING PREDICATES %%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% writeln(A) :- write(A),nl. write_list([]):-nl. write_list([A|R]) :- writeln(A), write_list(R). writetime(String) :- statistics(runtime,[_,T]), write(String),write(T),writeln(' ms ###'). %%%% write_model/2: if the flag is "write" prints a stable model write_model(write,MOD) :- !, retract(sol(N)),N1 is N+1,assert(sol(N1)), writeln('###############################################'), writeln('############# Computed model ##################'), writeln('###############################################'), write_fdmodel(MOD), writeln('###############################################'). write_model(_,_) :- writeln('### Computed model not printed, as required ###'), retract(sol(N)),N1 is N+1,assert(sol(N1)). write_fdmodel([]). write_fdmodel([atom(false,0,_,_)|R]):- !, write_fdmodel(R). write_fdmodel([atom(P,0,Dom,_)|R]):- format("### ~a/0: ",[P]), (Dom=[],!, writeln(false); writeln(true)), write_fdmodel(R). write_fdmodel([atom(P,1,Dom,_)|R]):- format("### ~a/1: ",[P]), fdset_to_list(Dom,LDom), writelist(LDom), write_fdmodel(R). write_fdmodel([atom(P,2,Dom,_)|R]):- format("### ~a/2: ",[P]), fdset_to_list(Dom,LDom),write_proj(2,LDom), write_fdmodel(R). write_fdmodel([atom(P,3,Dom,_)|R]):- format("### ~a/3: ",[P]), fdset_to_list(Dom,LDom), write_proj(3,LDom), write_fdmodel(R). write_proj(_,[]) :- nl. write_proj(2,[D|R]) :- bigM(M), X is D//M, Y is D mod M, format("(~d,~d) ",[X,Y]), write_proj(2,R). write_proj(3,[D|R]) :- bigM(M), X is D//(M*M), Y is (D-X*M*M)//M, Z is D mod M, format("(~d,~d,~d) ",[X,Y,Z]), write_proj(3,R). writelist([]) :- nl. writelist([D|R]) :- write(D),write(' '), writelist(R). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% EXTRA CODE 1. SIMPLE ASP COMPUTATION (without ordering control) %%% It can replace fixpoint predicate %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% slow_fixpoint(Rules,I0,M) :- (nd_choice(Rules,I0,I1), tp(Rules,I1,I2), constraints_check(I2), slow_fixpoint(Rules,I2,M); stable(Rules,I0),!, M=I0). nd_choice([Rule|_], I1,I2 ) :- apply_rule(Rule, I1, I2,_). nd_choice([_|Rules], I1, I2 ) :- nd_choice(Rules, I1, I2). stable(Rules,I0) :- constraints_check(I0), \+ nd_choice(Rules,I0,_). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% BETA PART: Functions-driven fixpoint, fun_fixpoint(Rules,I1,I2,Program) :- writeln('### Started function part '), functions(I1,Inew,Program), %%% Constraint-based function tp(Rules,Inew,Ineww), constraints_check(Ineww), fixpoint(Rules,Ineww,I2). functions(WFModel, [atom(assignment,2,ASS,NDOM)|RModel],Program) :- member(atom(domain,1,NUM,_),WFModel), %%% general: function domain member(atom(range,1,RAN,_),WFModel), %%% general: function range select(atom(assignment,2,_,NDOM),WFModel,RModel), %%% general: function fdset_size(NUM,L), length(Xs,L), length(Ys,L), funbuild(Xs,Ys,NUM,RAN,FUN), %%% general: map of (X,Y) increasing(Xs), %% general: removes symmetries and grounds the domain %% all_different(Ys), %%% use for one-to-one functions constraint_adhoc(Program,FUN,RModel), labeling([],FUN), list_to_fdset(FUN,ASS). funbuild([],[],_,_,[]). funbuild([X|Xs],[Y|Ys],DOM,RAN,[D|Fun]) :- X in_set DOM, Y in_set RAN, tuple_num([X,Y],D,2), funbuild(Xs,Ys,DOM,RAN,Fun). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% AD-HOC PART %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% constraint_adhoc(Program,FUN,Model) :- ( Program='test3.lp' -> constraint_test3(FUN),!; Program='test4.lp' -> constraint_queens(FUN),!; Program='test5.lp' -> constraint_schur(FUN),!; Program='test6.lp' -> constraint_marriage(Model,FUN),!; true ). %%% :- domain(X),range(Y), assignment(X,Y), X < Y. %%%%% Do not consider "domain" and "range" %%%%% One occurrence of "assignment" => one level of recursion %%%%% only one built-in atom "X= Y, %%% The complement of the atom constraint_test3(FUN). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% From "queens" %%% TWO ASP CONSTRAINTS constraint_queens(FUN) :- constraint_queens_horizontal(FUN), constraint_queens_diagonal(FUN). %%% Horizontal %%% :- assignment(X1,Y1), assignment(X2,Y2), %%% Y1==Y2,neq(X1,X2). %%% Two "assignment": double recursion %%% two built-in atoms constraint_queens_horizontal([]). constraint_queens_horizontal([PAIR|FUN]) :- constraint_queens_horizontal_2(PAIR,FUN), constraint_queens_horizontal(FUN). constraint_queens_horizontal_2(_,[]). constraint_queens_horizontal_2(PAIR1,[PAIR2|FUN]) :- pair_proj(PAIR1,X1,Y1), pair_proj(PAIR2,X2,Y2), (X1 \= X2,!,Y1 #\= Y2; true), %%% Actually, since we know that X1 < X2 %%% thus one could write simply Y1 #\= Y2 constraint_queens_horizontal_2(PAIR1,FUN). %%% Diagonal %%%:- assignment(X1,Y1), assignment(X2,Y2), %%% neq(X1,X2), abs(X1-X2) == abs(Y1-Y2). %%% Two "assignments": double recursion %%% Two built-in atoms constraint_queens_diagonal([]). constraint_queens_diagonal([PAIR|FUN]) :- constraint_queens_diagonal_2(PAIR,FUN), constraint_queens_diagonal(FUN). constraint_queens_diagonal_2(_,[]). constraint_queens_diagonal_2(PAIR1,[PAIR2|FUN]) :- pair_proj(PAIR1,X1,Y1), pair_proj(PAIR2,X2,Y2), %%% (X1 \= X2,!, abs(X1-X2) #\= abs(Y1-Y2); true), %%% The complement of the atom %%% Actually, we know that X1 < X2 %%% thus one could write simply abs(X1-X2) #\= abs(Y1-Y2) constraint_queens_diagonal_2(PAIR1,FUN). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% From Schur %%% :- assignment(X1,Y), assignment(X2,Y), assignment(X3,Y), %%% X3 = X1+X2. %%% Three assignments: triple recursion. %%% TAKE CARE THAT HERE RECURSION USES <= !!! constraint_schur([]). constraint_schur([PAIR|FUN]) :- constraint_schur2(PAIR,[PAIR|FUN]), constraint_schur(FUN). constraint_schur2(_,[]). constraint_schur2(PAIR1,[PAIR2|FUN]) :- constraint_schur3(PAIR1,PAIR2,[PAIR2|FUN]), constraint_schur2(PAIR1,FUN). constraint_schur3(_,_,[]). constraint_schur3(PAIR1,PAIR2,[PAIR3|FUN]) :- pair_proj(PAIR1,X1,Y1), pair_proj(PAIR2,X2,Y2), pair_proj(PAIR3,X3,Y3), %%% we know that Xi's are ground %%%(Y1 #= Y2 #/\ Y1 #= Y3) #=> (X3 #\= X1 + X2), (X3 =:= X1+X2,!,(Y1 #= Y2 #=> Y1 #\= Y3); true), constraint_schur3(PAIR1,PAIR2,FUN). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% :- hate(X,Y),assignment(X,Y). %%% 1 occ of assignment: one recursion %%% predicate non built.in hate: the model is needed %%% as parameter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% constraint_marriage(Model,FUN) :- member(atom(hate,2,EDGES,_),Model), constraint_marriage_rec(FUN,EDGES). constraint_marriage_rec([],_). constraint_marriage_rec([PAIR|FUN],EDGES) :- nin_set(2,PAIR,EDGES), constraint_marriage_rec(FUN,EDGES). %%%%%%%%% END %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%