1%QUESTO DEVE DIVENTARE IL MODULO CHE GESTISCEL'ATTRIBUTO RESTRICTIONS 2 3%------------------------------------- 4% Marco Gavanelli 5% 3 October 2003 6%------------------------------------- 7 8% This module defines an attribute that tells if a variable 9% is quantified existentially or universally. 10 11% It also applies Quantifier Restrictions. 12 13% The possible quantifications are: 14% exists (existentially quantified variable whose scope is a single implication) 15% existsf (existentially quantified variable whose scope is the whole tuple) 16% forall (universally quantified variable whose scope is a single implication) 17% forallf (universally quantified variable whose scope is the whole tuple) 18 19% The quantifier restrictions are imposed through the predicate st/1 (such that) 20% They can be any predicate: be warned that they will be called if all the 21% involved variables are quantified (existsf). Typically, you may want to impose 22% quantifier restrictions that have the same syntax as clpfd constraints. 23 24% Suggested use: 25% 1. impose the quantification 26% 2. impose the quantifier restrictions. 27% (should also work the other way around, but probably less efficiently 28% or with less complete inferences). 29 30% Example, to impose that X and Y are universally quantified, and we 31% have a quantifier restriction X<Y: 32% ?- forall(X), forall(Y), st(X#<Y). 33% forall(X), 34% forall(Y), 35% st(X,X#<Y), 36% st(Y,X#<Y) ? 37% yes 38 39% If all the variables in a quantifer restriction become quantified existsf 40% the quantifier restriction becomes a constraint. E.g.: 41% ?- forall(X), st(X#>0), existsf(Y), X=Y. 42% Y = X, 43% existsf(X), 44% X in 1..sup, 45% st(X,X#>0) ? 46% 47% As you see, the program is not very smart in removing quantifier 48% restrictions that have become constraints. This should be only an issue 49% of efficiency. 50 51% The program tries to make some (not very smart) check of entailment among 52% quantifier restrictions to avoid imposing redundant restrictions. E.g.: 53% ?- forall(X), st(X in 1..sup), st(X in 3..10). 54% forall(X), 55% st(X,X in 1..sup) ? 56% yes 57% 58% Currently, it considers only constraint "in". E.g.: 59% ?- forall(X), st(X #>0), st(X in 3..10). 60% forall(X), 61% st(X,X#>0), 62% st(X,X in 3..10) ? 63% yes 64% 65% and it is order dependent: 66% ?- forall(X), st(X in 3..10), st(X in inf..50). 67% forall(X), 68% st(X,X in 3..10), 69% st(X,X in inf..50) ? 70% yes 71 72:- module(restrictions, 73 [ 74 set_restriction/1, 75 set_restriction/2, 76 get_restrictions/2, 77 set_restriction_list/1, 78 set_restriction_list/2, 79 st/1, st/2]). 80 81:- use_module(library(chr)). 82%:- use_module(library(atts)). 83:- use_module(library(lists)). 84:- use_module(library(clpfd)). 85:- use_module(library(terms)). 86%:- use_module(domains). 87%:-use_module(sets). 88%:- writeln('CARICO REIFIED_UNIF DA QUANTIF'). 89:-use_module(reified_unif). 90%:- writeln('CARICato REIFIED_UNIF DA QUANTIF'). 91%:- ensure_loaded(load_solver). 92%:- writeln('CARICO solver DA QUANTIF'). 93:- use_module(solver). 94%:- writeln('CARICato solver DA QUANTIF'). 95:- use_module(prolog_version). 96:- (is_dialect(swi) -> use_module(swi_specific) ; true). 97:- use_module(quant). 98 99:- attribute(restrictions/1). 100 101% SICStus Unification handler 102verify_attributes(Var, Other, Goals) :- 103% (get_atts(Var, quant(Da)) 104% -> quant_handler(Var,Other,GoalsQuant,Da) 105% ; GoalsQuant=[]), 106 (get_atts(Var, restrictions(Ra)) 107 -> restrictions_handler(Var,Other,GoalsRestr,Ra) 108 ; restrictions_handler(Var,Other,GoalsRestr,[])), 109 Goals=GoalsRestr. 110% append(GoalsQuant,GoalsRestr,Goals). 111 112restrictions_handler(Var,Other,Goals,RL):- 113 nonvar(Other),!, 114 Goals = [set_restriction_list(RL,Var)]. 115 116restrictions_handler(Var,Other,GoalsRestr,RL):- 117 var(Other), 118 %( (is_quantified(Var,existsf) ; is_quantified(Other,existsf) ) 119 % -> Goals1 = [turn_to_constraints(RL)] 120 % ; Goals1 = []), 121 get_restrictions(Other,OtherRes), 122 append(OtherRes,RL,AllRes), 123 %put_atts(Var,restrictions([])), Non indispensabile: 124 % potrebbero rimanere delle restrizioni sulle variabili existsf 125 GoalsRestr=[set_restriction_list(AllRes,Var)]. 126 127% SWI Unification handler 128attr_unify_hook(AttValue, Other):- 129 (AttValue = restrictions(RL) -> true ; write('*** ERROR IN UNIFICATION OF RESTRICTIONS ***'), nl), 130 (var(Other) 131 -> get_restrictions(Other,OtherRes), 132 append(OtherRes,RL,AllRes), 133 set_restriction_list(AllRes,Other) 134 ; set_restriction_list(RL,Other) 135 ). 136 137% This predicate is invoked by SICStus when the computation terminates 138% to print the constraint store. We use it to print the quantification 139% and the restrictions 140attribute_goal(Var, T) :- % interpretation as goal 141 (get_quant(Var,Q) 142 -> Tq =.. [Q,Var] 143 ; true 144 ), 145 (get_atts(Var, restrictions(R)) 146 -> put_st(R,List,Var), 147 list_conj(List,Rc), 148 (var(Tq) -> T=Rc 149 ; T =..[Q,Var,R] 150 ) 151 ; nonvar(Tq), T=Tq % Se entrambi var, fallisci e non stampi niente 152 ). 153% Queste servono perche' altrimenti la attribute_goal (che serve a visualizzare 154% il risultato) si rifiuta di mostrare un termine che non e` callable 155forallf(_,_). 156existsf(_,_). 157forall(_,_). 158exists(_,_). 159 160list_conj([X],X):- !. 161list_conj([X,Y|T],(X,Tc)):- 162 list_conj([Y|T],Tc). 163 164put_st([],[],_). 165put_st([H|T],[st(V,H)|T1],V):- 166 put_st(T,T1,V). 167 168 169get_restrictions(X,Res):- 170% var(X), 171 get_atts(X, restrictions(Res1)), 172 !, 173 Res=Res1. 174get_restrictions(_,[]). 175 176/* 177% Adds a domain restriction to the variable 178set_restriction(_,R):- var(R),!,write('Unbound Restriction Error'),fail. 179set_restriction(_V,Res):- 180 is_term_quantified(Res,existsf),!, 181 call(Res). 182set_restriction(V,R):- 183 get_restrictions(V,RL),!, 184 rewrite_restriction(R,Res), 185 (restriction_entailed(Res,RL) 186 -> true 187 ; put_atts(V,restrictions([Res|RL]))). 188% No restriction has been imposed yet 189set_restriction(V,Res):- 190 put_atts(V,restrictions([Res])). 191*/ 192 193% Adds a domain restriction to the variable 194set_restriction(_,R):- var(R),!,write('Unbound Restriction Error'),fail. 195set_restriction(_V,Res):- 196% var(V), 197 is_term_quantified(Res,existsf),!, 198 call(Res). 199% MarcoG: 10 may 2005 200% If V has become ground (it usedto be universal, but unified with 201% existential may become ground), then we accept it. 202% If the restrictions were all existential, they were checked by the previous 203% clause. Otherwise, the restriction will continue to insist on the other 204% (universally quant) variables it involves 205set_restriction(V,_):- 206 ground(V),!. 207set_restriction(V,Res):- 208% var(V), 209 get_restrictions(V,[]),!, 210 put_atts(V,restrictions([Res])). 211set_restriction(V,R):- 212% var(V), 213 get_restrictions(V,RL), 214 rewrite_restriction(R,Res), 215 (restriction_entailed(Res,RL) 216 -> true 217 ; put_atts(V,restrictions([Res|RL]))). 218% No restriction has been imposed yet 219 220% Imposes a list of restrictions on the variables V 221set_restriction_list([],_). 222set_restriction_list([H|T],V):- 223 set_restriction(V,H), 224 set_restriction_list(T,V). 225 226% Imposes a list of restrictions on all the variables 227% they involve. 228set_restriction_list([]). 229set_restriction_list([H|T]):- 230 set_restriction(H), 231 set_restriction_list(T). 232 233% Adds the restriction to all the variables appearing in R 234set_restriction(R):- 235 term_variables_bag(R,Vars), 236 multivar_restr1(Vars,R). 237 238% Syntactic sugar: "such that" 239st(V,Res):- 240 set_restriction(V,Res). 241st(Res):- 242 set_restriction(Res). 243 244multivar_restr1([],R):- 245 !, 246 call(R). 247multivar_restr1(Vars,R):- 248 multivar_restr(Vars,R). 249 250multivar_restr([],_). 251multivar_restr([H|T],R):- 252 set_restriction(H,R), 253 multivar_restr(T,R)