1% MODULO CHE GESTISCE L'ATTRIBUTO QUANT 2 3 4%------------------------------------- 5% Marco Gavanelli 6% 3 October 2003 7%------------------------------------- 8 9% This module defines an attribute that tells if a variable 10% is quantified existentially or universally. 11 12% It also applies Quantifier Restrictions. 13 14% The possible quantifications are: 15% exists (existentially quantified variable whose scope is a single implication) 16% existsf (existentially quantified variable whose scope is the whole tuple) 17% forall (universally quantified variable whose scope is a single implication) 18% forallf (universally quantified variable whose scope is the whole tuple) 19 20% The quantifier restrictions are imposed through the predicate st/1 (such that) 21% They can be any predicate: be warned that they will be called if all the 22% involved variables are quantified (existsf). Typically, you may want to impose 23% quantifier restrictions that have the same syntax as clpfd constraints. 24 25% Suggested use: 26% 1. impose the quantification 27% 2. impose the quantifier restrictions. 28% (should also work the other way around, but probably less efficiently 29% or with less complete inferences). 30 31% Example, to impose that X and Y are universally quantified, and we 32% have a quantifier restriction X<Y: 33% ?- forall(X), forall(Y), st(X#<Y). 34% forall(X), 35% forall(Y), 36% st(X,X#<Y), 37% st(Y,X#<Y) ? 38% yes 39 40% If all the variables in a quantifer restriction become quantified existsf 41% the quantifier restriction becomes a constraint. E.g.: 42% ?- forall(X), st(X#>0), existsf(Y), X=Y. 43% Y = X, 44% existsf(X), 45% X in 1..sup, 46% st(X,X#>0) ? 47% 48% As you see, the program is not very smart in removing quantifier 49% restrictions that have become constraints. This should be only an issue 50% of efficiency. 51 52% The program tries to make some (not very smart) check of entailment among 53% quantifier restrictions to avoid imposing redundant restrictions. E.g.: 54% ?- forall(X), st(X in 1..sup), st(X in 3..10). 55% forall(X), 56% st(X,X in 1..sup) ? 57% yes 58% 59% Currently, it considers only constraint "in". E.g.: 60% ?- forall(X), st(X #>0), st(X in 3..10). 61% forall(X), 62% st(X,X#>0), 63% st(X,X in 3..10) ? 64% yes 65% 66% and it is order dependent: 67% ?- forall(X), st(X in 3..10), st(X in inf..50). 68% forall(X), 69% st(X,X in 3..10), 70% st(X,X in inf..50) ? 71% yes 72 73:- module(quant, 74 [quant/2, 75 set_term_quantification/2, 76 get_quant/2, 77 set_quant/2, 78 is_term_quantified/2, 79 is_unquantified/1, 80 forall/1, forallf/1, exists/1, existsf/1, 81 is_universal/1, 82 is_existential/1, 83 print_quant/0, print_quant/1 %FOR THE DEBUGGER 84 ]). 85 86:- use_module(library(chr)). 87:- use_module(prolog_version). 88%:- use_module(library(atts)). 89:- use_module(library(lists)). 90:- use_module(library(clpfd)). 91:- use_module(library(terms)). 92%:- use_module(domains). 93%:-use_module(sets). 94%:- writeln('CARICO REIFIED_UNIF DA QUANTIF'). 95:-use_module(reified_unif). 96%:- writeln('CARICato REIFIED_UNIF DA QUANTIF'). 97%:- ensure_loaded(load_solver). 98%:- writeln('CARICO solver DA QUANTIF'). 99:- use_module(solver). 100%:- writeln('CARICato solver DA QUANTIF'). 101:- (is_dialect(swi) -> use_module(swi_specific) ; true). 102:- use_module(sciff_options). 103 104:- attribute(quant/1). %%% Needed by SICStus 105% can be forall, exists (or free) or 106% forallf (forall flagged), existsf (exists flagged) 107 108% Syntactic Sugar 109% Let's skip one passage .... 110forall(X):- put_atts(X, quant(forall)). %quant(X,forall). 111forallf(X):- put_atts(X, quant(forallf)). %quant(X,forallf). 112exists(X):- put_atts(X, quant(exists)). %quant(X,exists). 113existsf(X):- put_atts(X, quant(existsf)), %quant(X,existsf), 114 get_restrictions(X,Res), 115 set_restriction_list(Res,X). 116 117 118% Ver 1.1: Unification of quantifiers is given by the following rules 119% unify_quant(+Q1,+Q2,-Qout) 120unify_quant(X,X,X):- !. 121unify_quant(forall,Y,Y):- !. 122unify_quant(Y,forall,Y):- !. 123 124unify_quant(forallf,Y,Y):- !. 125unify_quant(Y,forallf,Y):- !. 126unify_quant(existsf,_,existsf):- !. 127unify_quant(_,existsf,existsf):- !. 128 129% SICStus unification handler 130verify_attributes(Var, Other, Goals) :- 131 (get_atts(Var, quant(Da)) 132 -> quant_handler(Var,Other,Goals,Da) 133 ; Goals=[]). 134% (get_atts(Var, restrictions(Ra)) 135% -> restrictions_handler(Var,Other,GoalsRestr,Ra) 136% ; restrictions_handler(Var,Other,GoalsRestr,[])), 137% append(GoalsQuant,GoalsRestr,Goals). 138 139quant_handler(_Var,Other,Goals,Da):- 140 ( var(Other) -> % must be attributed then 141 ( get_atts(Other, quant(Db)) -> % has a quantification? 142 unify_quant(Da,Db,Dc), 143 put_atts(Other,quant(Dc)), 144 Goals = [] % NON FA NIENTE! 145 ; Goals = [], 146 put_atts(Other, quant(Da))% rescue intersection 147 ) 148 ; update_term_quantification(Other,Da), 149 Goals = [] 150 ). 151 152% SWI unification handler 153attr_unify_hook(AttValue, Other):- 154%quant_handler(_Var,Other,Goals,Da):- 155 AttValue = quant(Da), 156 ( var(Other) -> % must be attributed then 157 ( get_atts(Other, quant(Db)) -> % has a quantification? 158 unify_quant(Da,Db,Dc), 159 put_atts(Other,quant(Dc)) 160 ; put_atts(Other, quant(Da))% rescue intersection 161 ) 162 ; update_term_quantification(Other,Da) 163 ). 164 165% This predicate is invoked by SICStus when the computation terminates 166% to print the constraint store. We use it to print the quantification 167% and the restrictions 168attribute_goal(Var, T) :- % interpretation as goal 169 (get_atts(Var, quant(Q)), get_option(print_quant,on) 170 -> T =.. [Q,Var] 171 ; false % if no attribute, fail (print nothing) 172 ). 173 174 175% Version for SWI 176attribute_goals(Var, Out, Rest):- 177 (get_atts(Var, quant(Q)), get_option(print_quant,on) 178 -> T =.. [Q,Var], [T|Rest]=Out 179 ; Out=Rest % if no attribute, print nothing 180 ).
goal_expansion(get_quant(X, Dom),_,_,get_atts(X, quant(Dom)),[]).
% I restore the previous version, without goal_expansion191get_quant(X, Dom) :- 192 get_atts(X, quant(Dom)). 193% Reads or sets the quantification for a variable 194/*quant(X, Dom) :- slightly slower 195 var(Dom), 196 var(X),!, 197 get_atts(X, quant(Dom)). 198quant(X,_Dom):- nonvar(X),!. 199quant(X, Value) :- 200 put_atts(X, quant(Value)). 201*/ 202% set_quant(X,Dom): same as quant(X,Dom), but assumes that Dom is nonvar. 203set_quant(X, Dom) :- 204 (var(X) 205 -> put_atts(X, quant(Dom)) 206 ; true). 207quant(X, Dom) :- 208 (var(X) 209 -> (var(Dom) 210 -> get_atts(X, quant(Dom)) 211 ; put_atts(X, quant(Dom)) 212 ) 213 ; true). 214 215% update_term_quantiication(+Term,+Quantification), 216% Updates the quantification for all the variables 217% in a term. The difference wrt set_term_quantification/2 218% is that set_... gives the new quantification 219% to all the variables, while update_... uses a priority: 220% existsf has higher priority than forallf 221% Note that this problem come from not-allowed programs! 222update_term_quantification(T,Q) :- 223 var(T), !, update_quant(T,Q). 224update_term_quantification(T,_) :- 225 ground(T), !. 226update_term_quantification([H|T],Q) :-!, 227 update_term_quantification(H,Q), 228 update_term_quantification(T,Q). 229update_term_quantification(T,Q) :- 230 T =.. [_|Args], 231 update_term_quantification(Args,Q). 232 233update_quant(T,Q):- 234 (get_quant(T,Qold) 235 -> unify_quant(Q,Qold,Qnew) 236 ; Q=Qnew), 237 set_quant(T,Qnew). 238 239 240% Sets the quantification for all the variables 241% in a term 242set_term_quantification(T,Q) :- 243 var(T), !, set_quant(T,Q). 244set_term_quantification(T,_) :- 245 atom(T), !. 246set_term_quantification([H|T],Q) :-!, 247 set_term_quantification(H,Q), 248 set_term_quantification(T,Q). 249set_term_quantification(T,Q) :- 250 T =.. [_|Args], 251 set_term_quantification(Args,Q). 252 253% Checks if all the variables in Term are 254% quantified Quant 255%is_term_quantified(?Term,+Quant) 256is_term_quantified(Term,Quant):- 257 var(Term),!, 258 get_quant(Term,Quant). 259is_term_quantified(Term,Quant):- 260 functor(Term,_,N), 261 is_quantified_arg(N,Term,Quant). 262 263is_quantified_arg(0,_,_):- !. 264is_quantified_arg(N,Term,Quant):- 265 arg(N,Term,Xn), 266 is_term_quantified(Xn,Quant), 267 N1 is N-1, 268 is_quantified_arg(N1,Term,Quant). 269 270% Checks if all the variables in Term are 271% unquantified 272%is_unquantified(?Term) 273is_unquantified(Term):- 274 var(Term),!, 275 \+ get_quant(Term,_). 276is_unquantified(Term):- 277 functor(Term,_,N), 278 is_unquantified_arg(N,Term). 279 280is_unquantified_arg(0,_):- !. 281is_unquantified_arg(N,Term):- 282 arg(N,Term,Xn), 283 is_unquantified(Xn), 284 N1 is N-1, 285 is_unquantified_arg(N1,Term). 286 287/*is_universal(X):- this version is slightly slower 288 var(X), 289 (get_quant(X,forall) 290 -> true 291 ; get_quant(X,forallf)).*/ 292 293is_universal(X):- 294 var(X), 295 get_quant(X,Q), 296 (Q=forall ; Q=forallf),!. 297 298/*is_existential(X):- this version is slightly slower 299 var(X), 300 (get_quant(X,exists) 301 -> true 302 ; get_quant(X,existsf)).*/ 303 304is_existential(X):- 305 var(X), 306 get_quant(X,Q), 307 (Q=exists ; Q=existsf),!. 308 309%MG: 9 aug 09: Questo non ricordo perche' c'e`. 310% Puo` darsi che nella stampa del termine sotto SICStus lui trovi clp_constraint 311% e si rifiuti di stamparlo se non e` callable, per cui deve essere definito come 312% predicato. 313clp_constraint(A):- 314 call(A). 315 316% QUESTO NON FUNZIONA, PER CUI L'HO TOLTO. 317%% quantif=[113,117,97,110,116,105,102] 318%debugger_command_hook(unknown([113,117,97,110,116,105,102],Warning),Actions):- 319% Actions=true, 320% print_goal. 321% 322%debugger_command_hook(unknown(Line,Warning),Actions):- 323% write(unknown(Line,Warning)), nl, write('ancora'), 324% execution_state([show(Show),goal(_:G)]), 325% execution_state([goal(G)]), nl, 326% write('current goal: '), write(G). 327% 328%%debugger_command_hook(unknown([0'N|ArgCodes],_), Actions) :- 329%% Actions = true, % don't change the action variables 330%% % [] would mean [print,ask] :-). 331%% name_current_subterm(ArgCodes). 332% 333%print_goal:- 334% execution_state(break_level(BL)), 335% write(break(BL)), 336% execution_state(break_level(BL),user:goal(G)), 337% write('current goal: '), write(G). 338 339 340 341%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55 342% 343% La seconda e` un po' piu` utile. Volevo estendere il debugger di Sicstus per 344% visualizzare anche la quantificazione delle variabili e le quantifier 345% restrictions. Non sono riuscito a fare quello che volevo, ma ho ottenuto 346% un'approssimazione. Si usa cosi`: 347% durante il trace (non il chr_trace!) hai un goal che puo` essere 348% 349% Call: modulo:predicato(A,B,C) 350% 351% e tu vuoi sapere come sono quantificate A, B e C. Allora fai un "b" (break 352% level) e Sicstus ti permette di inserire un goal. Il goal da eseguire e` 353% 354% print_quant(modulo). 355% 356% o, se il modulo non c'e`, basta print_quant. Ho dovuto usare questa sintassi 357% assurda per via del sistema dei moduli, che con i metapredicati diventa una 358% pena. Lui dovrebbe stamparti la quantificazione di tutte le variabili che 359% compaiono nel goal. A questo punto esci dal break level (^D in linux o ^Z in 360% windows) e continui dov'eri. 361 362print_quant:- 363 print_quant(user). 364 365print_quant(M):- 366 execution_state(break_level(BL)), 367 BL1 is BL-1, 368 execution_state(break_level(BL1),M:goal(G)), 369 print_quantified(G). 370 371print_quantified(G):- 372 var(G), get_quant(G,Q),!, write(Q), write('('), write(G), write(')'), 373 restrictions:get_restrictions(G,R), write(R), nl. 374print_quantified(G):- 375 var(G),!, write('unquantified('), write(G), write(')\n'). 376print_quantified(G):- 377 ground(G),!. 378print_quantified(G):- 379 functor(G,suspension,_),!. 380print_quantified(G):- 381 G =.. [_,X|Par], 382 print_quantified(X), 383 print_quantified(Par)