% MODULO CHE GESTISCE L'ATTRIBUTO QUANT %------------------------------------- % 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(quant, [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, is_universal/1, is_existential/1, print_quant/0, print_quant/1 %FOR THE DEBUGGER ]). :- use_module(library(chr)). :- use_module(prolog_version). %:- use_module(library(atts)). :- use_module(library(lists)). :- use_module(library(clpfd)). :- use_module(library(terms)). %:- use_module(domains). %:-use_module(sets). %:- writeln('CARICO REIFIED_UNIF DA QUANTIF'). :-use_module(reified_unif). %:- writeln('CARICato REIFIED_UNIF DA QUANTIF'). %:- ensure_loaded(load_solver). %:- writeln('CARICO solver DA QUANTIF'). :- use_module(solver). %:- writeln('CARICato solver DA QUANTIF'). :- (is_dialect(swi) -> use_module(swi_specific) ; true). :- use_module(sciff_options). :- attribute(quant/1). %%% Needed by SICStus % 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):- !. % SICStus unification handler verify_attributes(Var, Other, Goals) :- (get_atts(Var, quant(Da)) -> quant_handler(Var,Other,Goals,Da) ; Goals=[]). % (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 = [] ). % SWI unification handler attr_unify_hook(AttValue, Other):- %quant_handler(_Var,Other,Goals,Da):- AttValue = quant(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)) ; put_atts(Other, quant(Da))% rescue intersection ) ; update_term_quantification(Other,Da) ). % 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)), get_option(print_quant,on) -> T =.. [Q,Var] ; false % if no attribute, fail (print nothing) ). % Version for SWI attribute_goals(Var, Out, Rest):- (get_atts(Var, quant(Q)), get_option(print_quant,on) -> T =.. [Q,Var], [T|Rest]=Out ; Out=Rest % if no attribute, print nothing ). %% MG 9 aug 09 %% The goal_expansion version was used in SICStus before adding the compatibility with SWI. %% It could probably work, but there is probably some problem with modules. %% we should probably remove module quantif and have only quant.pl and restrictions.pl % goal_expansion(get_quant(X, Dom),_,_,get_atts(X, quant(Dom)),[]). %% I restore the previous version, without goal_expansion 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). /*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),!. %MG: 9 aug 09: Questo non ricordo perche' c'e`. % Puo` darsi che nella stampa del termine sotto SICStus lui trovi clp_constraint % e si rifiuti di stamparlo se non e` callable, per cui deve essere definito come % predicato. 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(')'), restrictions: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).