1/* 2:- module(solver, 3 [is_constraint_functor/1, 4 restriction_entailed/2, 5 fd_or_num/1, 6 reified_equality_solver/3, 7 binary_domain/1, 8 cstr_var/1, 9 neq/2,lt/2,eq/2,gt/2,leq/2,geq/2, 10 is_identical/2, 11 impose_neg_constraints/3, 12 solver_search/1, 13 is_clp_functor/1, 14 solver_rewrite_constraint/2, 15 term_unify/2, 16 opposite/2, 17 rewrite_restriction/2, 18 rewrite_restr_rules/2, 19 add_default_domain/1, 20 term_equality/2, 21 is_number/1 22 ]). 23*/ 24:- use_module(reified_unif,[if_unary_substitute/4,inst/1,unify_constr/2]). 25:- use_module(library(clpr)). 26:- use_module(library(lists)). 27 28neq(A,B):- {A=\=B}. 29lt(A,B):- {A<B}. 30eq(A,B):- {A=B}. 31gt(A,B):- {A>B}. 32leq(A,B):- {A=<B}. 33geq(A,B):- {A>=B}. 34 35is_identical(A,B):- entailed(A=B). 36 37term_unify(X,Y):- unify_constr(X,Y). 38 39%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% used in ics_quant %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 40rel2clp(<>,neq). 41rel2clp(<,lt). 42rel2clp(=,eq). 43rel2clp(>,gt). 44rel2clp(=<,leq). 45rel2clp(>=,geq). 46rel2clp(clp_constraint,clp_constraint). 47rel2clp(st,st). /* MG: This is necessary because in Unfolding we call 48this module. Since there might remain some st, we have to recognize 49it as a constraint, otherwise the quantification will be wrong */ 50 51is_clp_functor(C):- member(C,[<>,<,=,>,=<,>=,clp_constraint,st]),!. 52 53solver_rewrite_constraint(Constraint,Constraint1):- 54 Constraint=..[F,Arg1,Arg2], 55 rel2clp(F,F1), 56 Constraint1=..[F1,Arg1,Arg2]. 57 58%%%%%%%%%%%%%%%%%%%%%%%%%% used in sokb_parser %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 59is_constraint_functor(F):- 60 rel2clp(_,F). 61 62%%%%%%%%%%%%%%%%%%%%%%%%%%% Used in quantif %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 63% Checks if the restriction is entailed by a set 64% of restrictions. 65% It is by far not complete!!! 66% Just a collection of simple rules in which entailment 67% is easy. 68 69% A restriction is entailed if it was already imposed 70restriction_entailed(R,[R1|_]):- 71 R == R1, !. 72%restriction_entailed(R, [R1|_]):- 73% is_unary(R), is_unary(R1), 74% unary_restriction_entailed(R,R1). 75 76%%%% MG (27 dec 2007) creazione di questo file. 77%%%% Per ora tolgo questa regola. Se ci viene in mente un metodo migliore per verificare l'entailment 78%%%% nel solver Q, possiamo metterla qui. Ci sarebbe una entailed/1, ma ha bisogno che i vincoli siano 79%%%% imposti 80%restriction_entailed(X in LowX..HighX,[X1 in Low1 .. High1|_]):- 81% X == X1, 82% leq(Low1,LowX), 83% leq(HighX,High1),!. 84restriction_entailed(R,[_|T]):- 85 restriction_entailed(R,T). 86 87is_unary(R):- 88 term_variables_bag(R,[_]). 89 90rewrite_restriction(R,R). 91rewrite_restr_rules(R,R). 92 93%%%%%%%%%%%%%%%%%%%%%%%%%%% Used in reified_unif %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 94fd_or_num(X) :- compound(X),!, X=rat(_,_). % is it a rational number? (clpq) 95fd_or_num(X) :- number(X),!. 96%fd_or_num(X) :- var(X),dump([X],_,[]),!. 97fd_or_num(X) :- %MG: it is a constrained variable if it has at least one of the attributes defined in the module clpr. 98 var(X), 99 clpr:dump([X],_,Store), 100 Store \= []. 101 102cstr_var(X) :- var(X), clpr:dump([X],_,Store), 103 Store \= []. 104 105is_number(X) :- compound(X),!, X=rat(_,_). % is it a rational number? (clpq) 106is_number(X) :- number(X),!. 107 108term_equality(A,B):- 109 fd_or_num(A), fd_or_num(B), !, eq(A,B). 110term_equality(A,X):- A=X. 111 112reified_equality_solver(X,Y,B):- entailed(X=Y),!, B=1. 113reified_equality_solver(X,Y,B):- entailed(X=\=Y),!, B=0. 114reified_equality_solver(X,Y,B):- {X=Y},B=1. 115reified_equality_solver(X,Y,B):- {X=\=Y},B=0. 116 117binary_domain(_). 118 119% MarcoG: This version opens several choice points. 120% Future work: improve it (possibly, as in the fd_solver version) 121% NOTE: This versione does not check if the various constraints 122% in disjunctions overlap or not. This is ok when we are inverting 123% interval constraints (eg A<X<B, that becomes A>=X \/ X>= B), 124% but in general this could give repeated solutions. 125% A possibility is the following (buggy: fails too often, probably due to st(...)) 126/* Intended for SICStus 3 127impose_neg_constraints(X,RL,Y):- 128 choose_constraint(R,RL,Pos,[]), 129 if_unary_substitute(X,R,Y,T), 130 once(opposite(T,Opp)), 131 call_constraints([Opp|Pos]). 132 133call_constraints([]). 134call_constraints([H|T]):- 135 functor(H,F,_), %write(H), 136 ((F=st;F=clp_constraint) -> call(H) ; 137 (is_clp_functor(F) 138 -> {H} 139 ; call(H) 140 )), 141 call_constraints(T). 142 143choose_constraint(X,[X],L,L):-!. 144choose_constraint(X,[X,_|_],L,L). 145choose_constraint(X,[Y|R],[Y|Lout],Lin):- 146 choose_constraint(X,R,Lout,Lin).*/ 147 148impose_neg_constraints(X,RL,Y):- 149 member(R,RL), 150 if_unary_substitute(X,R,Y,T), 151 once(opposite(T,Opp)), 152 functor(Opp,F,_), 153 (is_clp_functor(F) 154 -> {Opp} 155 ; call(Opp) 156 ). 157 158opposite({T},Opp):- 159 opposite(T,Opp). 160opposite(A=B,A=\=B). 161opposite(A=\=B,A=B). 162opposite(A<B,A>=B). 163opposite(A=<B,A>B). 164opposite(A>B,A=<B). 165opposite(A>=B,A<B). 166 167opposite(eq(A,B),neq(A,B)). 168opposite(neq(A,B),eq(A,B)). 169opposite(lt(A,B),geq(A,B)). 170opposite(leq(A,B),gt(A,B)). 171opposite(gt(A,B),leq(A,B)). 172opposite(geq(A,B),lt(A,B)). 173 174solver_search(L):- sumterm(L,X), %write(prima(LT1)), 175 bb_inf(L,X,_,LT1,0.01), 176 guided_labeling(L,LT1,X). 177 178guided_labeling([],[],_). 179guided_labeling([H|T],[H1|T1],F):- 180 {H=H1}, 181 guided_labeling(T,T1,F). 182guided_labeling([H|T],[H1|_],F):- 183 {H>=H1+1}, 184 bb_inf([H|T],F,_,Sol,0.01), 185 guided_labeling([H|T],Sol,F). 186guided_labeling([H|T],[H1|_],F):- 187 {H+1=<H1}, 188 bb_inf([H|T],F,_,Sol,0.01), 189 guided_labeling([H|T],Sol,F). 190 191 192 193sumterm([X],X):-!. 194sumterm([X|T],X+Y):- 195 sumterm(T,Y). 196 197 198%%%%%%%%%%%%%%%%%%%%%%%%%% used in sciff.pl %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 199add_default_domain(T):- 200 leq(T,1000), 201 geq(T,-1000)