%------------------------------------- % Marco Gavanelli % 3 October 2003 %------------------------------------- % This module defines an attribute that tells if a variable % is quantified existentially or universally. % It also applies Quantifier Restrictions. % The possible quantifications are: % exists (existentially quantified variable whose scope is a single implication) % existsf (existentially quantified variable whose scope is the whole tuple) % forall (universally quantified variable whose scope is a single implication) % forallf (universally quantified variable whose scope is the whole tuple) % The quantifier restrictions are imposed through the predicate st/1 (such that) % They can be any predicate: be warned that they will be called if all the % involved variables are quantified (existsf). Typically, you may want to impose % quantifier restrictions that have the same syntax as clpfd constraints. % Suggested use: % 1. impose the quantification % 2. impose the quantifier restrictions. % (should also work the other way around, but probably less efficiently % or with less complete inferences). % Example, to impose that X and Y are universally quantified, and we % have a quantifier restriction X0), existsf(Y), X=Y. % Y = X, % existsf(X), % X in 1..sup, % st(X,X#>0) ? % % As you see, the program is not very smart in removing quantifier % restrictions that have become constraints. This should be only an issue % of efficiency. % The program tries to make some (not very smart) check of entailment among % quantifier restrictions to avoid imposing redundant restrictions. E.g.: % ?- forall(X), st(X in 1..sup), st(X in 3..10). % forall(X), % st(X,X in 1..sup) ? % yes % % Currently, it considers only constraint "in". E.g.: % ?- forall(X), st(X #>0), st(X in 3..10). % forall(X), % st(X,X#>0), % st(X,X in 3..10) ? % yes % % and it is order dependent: % ?- forall(X), st(X in 3..10), st(X in inf..50). % forall(X), % st(X,X in 3..10), % st(X,X in inf..50) ? % yes :- module(quantif, [quant/2, set_term_quantification/2, get_quant/2, set_quant/2, is_term_quantified/2, is_unquantified/1, forall/1, forallf/1, exists/1, existsf/1, set_restriction/1, set_restriction/2, get_restrictions/2, set_restriction_list/1, set_restriction_list/2, st/1, st/2, is_universal/1, is_existential/1, print_quant/0, print_quant/1]). :- use_module(library(chr)). :- use_module(library(atts)). :- use_module(library(lists)). :- use_module(library(clpfd)). :- use_module(library(terms)). %:- use_module(domains). %:-use_module(sets). :-use_module(reified_unif). %:- ensure_loaded(solver). :- use_module(solver). :- attribute quant/1, restrictions/1. % can be forall, exists (or free) or % forallf (forall flagged), existsf (exists flagged) % Syntactic Sugar % Let's skip one passage .... forall(X):- put_atts(X, quant(forall)). %quant(X,forall). forallf(X):- put_atts(X, quant(forallf)). %quant(X,forallf). exists(X):- put_atts(X, quant(exists)). %quant(X,exists). existsf(X):- put_atts(X, quant(existsf)), %quant(X,existsf), get_restrictions(X,Res), set_restriction_list(Res,X). % Ver 1.1: Unification of quantifiers is given by the following rules % unify_quant(+Q1,+Q2,-Qout) unify_quant(X,X,X):- !. unify_quant(forall,Y,Y):- !. unify_quant(Y,forall,Y):- !. unify_quant(forallf,Y,Y):- !. unify_quant(Y,forallf,Y):- !. unify_quant(existsf,_,existsf):- !. unify_quant(_,existsf,existsf):- !. verify_attributes(Var, Other, Goals) :- (get_atts(Var, quant(Da)) -> quant_handler(Var,Other,GoalsQuant,Da) ; GoalsQuant=[]), (get_atts(Var, restrictions(Ra)) -> restrictions_handler(Var,Other,GoalsRestr,Ra) ; restrictions_handler(Var,Other,GoalsRestr,[])), append(GoalsQuant,GoalsRestr,Goals). quant_handler(_Var,Other,Goals,Da):- ( var(Other) -> % must be attributed then ( get_atts(Other, quant(Db)) -> % has a quantification? unify_quant(Da,Db,Dc), put_atts(Other,quant(Dc)), Goals = [] % NON FA NIENTE! ; Goals = [], put_atts(Other, quant(Da))% rescue intersection ) ; update_term_quantification(Other,Da), Goals = [] ). restrictions_handler(Var,Other,Goals,RL):- nonvar(Other),!, Goals = [set_restriction_list(RL,Var)]. restrictions_handler(Var,Other,GoalsRestr,RL):- var(Other), %( (is_quantified(Var,existsf) ; is_quantified(Other,existsf) ) % -> Goals1 = [turn_to_constraints(RL)] % ; Goals1 = []), get_restrictions(Other,OtherRes), append(OtherRes,RL,AllRes), %put_atts(Var,restrictions([])), Non indispensabile: % potrebbero rimanere delle restrizioni sulle variabili existsf GoalsRestr=[set_restriction_list(AllRes,Var)]. % Maybe it should always return true; see predicate frozen/2 % in the SICStus manual. %attribute_goal(Var, quant(Var,Dom)) :- % interpretation as goal % get_atts(Var, quant(Dom)). % This predicate is invoked by SICStus when the computation terminates % to print the constraint store. We use it to print the quantification % and the restrictions attribute_goal(Var, T) :- % interpretation as goal (get_atts(Var, quant(Q)) -> Tq =.. [Q,Var] ; true ), (get_atts(Var, restrictions(R)) -> put_st(R,List,Var), list_conj(List,Rc), (var(Tq) -> T=Rc ; T =..[Q,Var,R] ) ; nonvar(Tq), T=Tq % Se entrambi var, fallisci e non stampi niente ). % Queste servono perche' altrimenti la attribute_goal (che serve a visualizzare % il risultato) si rifiuta di mostrare un termine che non e` callable forallf(_,_). existsf(_,_). forall(_,_). exists(_,_). list_conj([X],X):- !. list_conj([X,Y|T],(X,Tc)):- list_conj([Y|T],Tc). put_st([],[],_). put_st([H|T],[st(V,H)|T1],V):- put_st(T,T1,V). /* get_quant(X, Dom) :- get_atts(X, quant(Dom)). % Reads or sets the quantification for a variable quant(X, Dom) :- var(Dom), !, get_atts(X, quant(Dom)). quant(X, Value) :- put_atts(X, quant(Value)). */ % New version of May 4th 2005 %goal_expansion(get_quant(X, Dom),quantif,get_atts(X, quant(Dom))):- write('ESPANDO'). %term_expansion(get_quant(X, Dom),get_atts(X, quant(Dom))). get_quant(X, Dom) :- get_atts(X, quant(Dom)). % Reads or sets the quantification for a variable /*quant(X, Dom) :- slightly slower var(Dom), var(X),!, get_atts(X, quant(Dom)). quant(X,_Dom):- nonvar(X),!. quant(X, Value) :- put_atts(X, quant(Value)). */ % set_quant(X,Dom): same as quant(X,Dom), but assumes that Dom is nonvar. set_quant(X, Dom) :- (var(X) -> put_atts(X, quant(Dom)) ; true). quant(X, Dom) :- (var(X) -> (var(Dom) -> get_atts(X, quant(Dom)) ; put_atts(X, quant(Dom)) ) ; true). % update_term_quantiication(+Term,+Quantification), % Updates the quantification for all the variables % in a term. The difference wrt set_term_quantification/2 % is that set_... gives the new quantification % to all the variables, while update_... uses a priority: % existsf has higher priority than forallf % Note that this problem come from not-allowed programs! update_term_quantification(T,Q) :- var(T), !, update_quant(T,Q). update_term_quantification(T,_) :- ground(T), !. update_term_quantification([H|T],Q) :-!, update_term_quantification(H,Q), update_term_quantification(T,Q). update_term_quantification(T,Q) :- T =.. [_|Args], update_term_quantification(Args,Q). update_quant(T,Q):- (get_quant(T,Qold) -> unify_quant(Q,Qold,Qnew) ; Q=Qnew), set_quant(T,Qnew). % Sets the quantification for all the variables % in a term set_term_quantification(T,Q) :- var(T), !, set_quant(T,Q). set_term_quantification(T,_) :- atom(T), !. set_term_quantification([H|T],Q) :-!, set_term_quantification(H,Q), set_term_quantification(T,Q). set_term_quantification(T,Q) :- T =.. [_|Args], set_term_quantification(Args,Q). % Checks if all the variables in Term are % quantified Quant %is_term_quantified(?Term,+Quant) is_term_quantified(Term,Quant):- var(Term),!, get_quant(Term,Quant). is_term_quantified(Term,Quant):- functor(Term,_,N), is_quantified_arg(N,Term,Quant). is_quantified_arg(0,_,_):- !. is_quantified_arg(N,Term,Quant):- arg(N,Term,Xn), is_term_quantified(Xn,Quant), N1 is N-1, is_quantified_arg(N1,Term,Quant). % Checks if all the variables in Term are % unquantified %is_unquantified(?Term) is_unquantified(Term):- var(Term),!, \+ get_quant(Term,_). is_unquantified(Term):- functor(Term,_,N), is_unquantified_arg(N,Term). is_unquantified_arg(0,_):- !. is_unquantified_arg(N,Term):- arg(N,Term,Xn), is_unquantified(Xn), N1 is N-1, is_unquantified_arg(N1,Term). get_restrictions(X,Res):- % var(X), get_atts(X, restrictions(Res1)), !, Res=Res1. get_restrictions(_,[]). /* % Adds a domain restriction to the variable set_restriction(_,R):- var(R),!,write('Unbound Restriction Error'),fail. set_restriction(_V,Res):- is_term_quantified(Res,existsf),!, call(Res). set_restriction(V,R):- get_restrictions(V,RL),!, rewrite_restriction(R,Res), (restriction_entailed(Res,RL) -> true ; put_atts(V,restrictions([Res|RL]))). % No restriction has been imposed yet set_restriction(V,Res):- put_atts(V,restrictions([Res])). */ % Adds a domain restriction to the variable set_restriction(_,R):- var(R),!,write('Unbound Restriction Error'),fail. set_restriction(_V,Res):- % var(V), is_term_quantified(Res,existsf),!, call(Res). % MarcoG: 10 may 2005 % If V has become ground (it usedto be universal, but unified with % existential may become ground), then we accept it. % If the restrictions were all existential, they were checked by the previous % clause. Otherwise, the restriction will continue to insist on the other % (universally quant) variables it involves set_restriction(V,_):- ground(V),!. set_restriction(V,Res):- % var(V), get_restrictions(V,[]),!, put_atts(V,restrictions([Res])). set_restriction(V,R):- % var(V), get_restrictions(V,RL), rewrite_restriction(R,Res), (restriction_entailed(Res,RL) -> true ; put_atts(V,restrictions([Res|RL]))). % No restriction has been imposed yet % Imposes a list of restrictions on the variables V set_restriction_list([],_). set_restriction_list([H|T],V):- set_restriction(V,H), set_restriction_list(T,V). % Imposes a list of restrictions on all the variables % they involve. set_restriction_list([]). set_restriction_list([H|T]):- set_restriction(H), set_restriction_list(T). % Adds the restriction to all the variables appearing in R set_restriction(R):- term_variables_bag(R,Vars), multivar_restr1(Vars,R). % Syntactic sugar: "such that" st(V,Res):- set_restriction(V,Res). st(Res):- set_restriction(Res). multivar_restr1([],R):- !, call(R). multivar_restr1(Vars,R):- multivar_restr(Vars,R). multivar_restr([],_). multivar_restr([H|T],R):- set_restriction(H,R), multivar_restr(T,R). /*is_universal(X):- this version is slightly slower var(X), (get_quant(X,forall) -> true ; get_quant(X,forallf)).*/ is_universal(X):- var(X), get_quant(X,Q), (Q=forall ; Q=forallf),!. /*is_existential(X):- this version is slightly slower var(X), (get_quant(X,exists) -> true ; get_quant(X,existsf)).*/ is_existential(X):- var(X), get_quant(X,Q), (Q=exists ; Q=existsf),!. clp_constraint(A):- call(A). % QUESTO NON FUNZIONA, PER CUI L'HO TOLTO. %% quantif=[113,117,97,110,116,105,102] %debugger_command_hook(unknown([113,117,97,110,116,105,102],Warning),Actions):- % Actions=true, % print_goal. % %debugger_command_hook(unknown(Line,Warning),Actions):- % write(unknown(Line,Warning)), nl, write('ancora'), % execution_state([show(Show),goal(_:G)]), % execution_state([goal(G)]), nl, % write('current goal: '), write(G). % %%debugger_command_hook(unknown([0'N|ArgCodes],_), Actions) :- %% Actions = true, % don't change the action variables %% % [] would mean [print,ask] :-). %% name_current_subterm(ArgCodes). % %print_goal:- % execution_state(break_level(BL)), % write(break(BL)), % execution_state(break_level(BL),user:goal(G)), % write('current goal: '), write(G). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55 % % La seconda e` un po' piu` utile. Volevo estendere il debugger di Sicstus per % visualizzare anche la quantificazione delle variabili e le quantifier % restrictions. Non sono riuscito a fare quello che volevo, ma ho ottenuto % un'approssimazione. Si usa cosi`: % durante il trace (non il chr_trace!) hai un goal che puo` essere % % Call: modulo:predicato(A,B,C) % % e tu vuoi sapere come sono quantificate A, B e C. Allora fai un "b" (break % level) e Sicstus ti permette di inserire un goal. Il goal da eseguire e` % % print_quant(modulo). % % o, se il modulo non c'e`, basta print_quant. Ho dovuto usare questa sintassi % assurda per via del sistema dei moduli, che con i metapredicati diventa una % pena. Lui dovrebbe stamparti la quantificazione di tutte le variabili che % compaiono nel goal. A questo punto esci dal break level (^D in linux o ^Z in % windows) e continui dov'eri. print_quant:- print_quant(user). print_quant(M):- execution_state(break_level(BL)), BL1 is BL-1, execution_state(break_level(BL1),M:goal(G)), print_quantified(G). print_quantified(G):- var(G), get_quant(G,Q),!, write(Q), write('('), write(G), write(')'), get_restrictions(G,R), write(R), nl. print_quantified(G):- var(G),!, write('unquantified('), write(G), write(')\n'). print_quantified(G):- ground(G),!. print_quantified(G):- functor(G,suspension,_),!. print_quantified(G):- G =.. [_,X|Par], print_quantified(X), print_quantified(Par).