1:- module(casp_clpq, 2 [ is_clpq_var/1, 3 clpqr_dump_constraints/3, 4 disequality_clpq/2, 5 entails/2, 6 entail_terms/2, 7 dual_clpq/2, 8 apply_clpq_constraints/1, 9 dump_clpq_var/3, 10 inf/2, 11 sup/2, 12 13 op(700, xfx, #=), 14 op(700, xfx, #<>), 15 op(700, xfx, #<), 16 op(700, xfx, #=<), 17 op(700, xfx, #>), 18 op(700, xfx, #>=) 19 ]).

Extension of the constraint solver CLP(Q)

This module inport the constraint solve package for CLP(Q) and extend its functionalities (among others) with: dual_clpq/2 provide the dual of a constraint store in run-time to evaluate the forall/4 predicate. pretty_print/1 used by portray_attribute/2 to print the constraints of a variable.

author: - Joaquin Arias */

32:- use_module(disequality, [get_neg_var/2]). 33 34:- use_module(library(clpq)). 35:- use_module(library(clpr), []). % avoid undef 36:- use_module(library(clpqr/dump), [dump/3]). 37:- use_module(library(apply), [maplist/3, include/3]). 38:- use_module(library(debug), [assertion/1]). 39:- use_module(library(edinburgh), [display/1]). 40:- use_module(library(lists), [reverse/2]). 41:- use_module(library(prolog_code), [comma_list/2]). 42 43clpqr_dump_constraints(Target, NewVars, Constraints), is_list(Target) => 44 maplist(to_clpq_var, Target, Target2), 45 dump(Target2, NewVars, Constraints0), 46 maplist(ciao_constraint, Constraints0, Constraints). 47 48to_clpq_var(X, V) :- 49 ( is_clpq_var(X) 50 -> V = X 51 ; true 52 ). 53 54ciao_constraint(A=B, Ciao) => Ciao = (A#=B). 55ciao_constraint(A-B=\=0, Ciao) => Ciao = (A#<>B). 56ciao_constraint(A>B, Ciao) => Ciao = (A#>B). 57ciao_constraint(A>=B, Ciao) => Ciao = (A#>=B). 58ciao_constraint(A<B, Ciao) => Ciao = (A#<B). 59ciao_constraint(A=<B, Ciao) => Ciao = (A#=<B). 60 61clpq_entailed(Ciao) :- 62 trans_meta_clp(Ciao, ClpQ), 63 entailed(ClpQ). 64 65clpq_meta(C) :- 66 clpqr_meta(C). 67 68% from Ciao library/clpqr/clpqr_meta.pl 69clpqr_meta(Ciao) :- 70 trans_meta_clp(Ciao, ClpQ), 71 {ClpQ}.

78trans_meta_clp((A,B), ClpQ) => 79 trans_meta_clp(A, AR), 80 trans_meta_clp(B, BR), 81 ClpQ = (AR,BR). 82trans_meta_clp((A;B), ClpQ) => 83 trans_meta_clp(A, AR), 84 trans_meta_clp(B, BR), 85 ClpQ = (AR;BR). 86trans_meta_clp([], _) => 87 assertion(fail). 88trans_meta_clp(List, ClpQ), is_list(List) => 89 comma_list(Conj, List), 90 trans_meta_clp(Conj, ClpQ). 91trans_meta_clp(A#=B, ClpQ) => ClpQ = (A =:= B). 92trans_meta_clp(A#<>B, ClpQ) => ClpQ = (A =\= B). 93trans_meta_clp(A#<B, ClpQ) => ClpQ = (A < B). 94trans_meta_clp(A#=<B, ClpQ) => ClpQ = (A =< B). 95trans_meta_clp(A#>B, ClpQ) => ClpQ = (A > B). 96trans_meta_clp(A#>=B, ClpQ) => ClpQ = (A >= B). 97% for bec_light.pl 98trans_meta_clp(A < B, ClpQ) => ClpQ = (A < B). 99trans_meta_clp(A > B, ClpQ) => ClpQ = (A > B).

105is_clpq_var(X) :- 106 attvar(X), 107 clp_type(X, clpq). 108 109apply_clpq_constraints(A #<> B + C) :- 110 get_neg_var(A,[Num]), 111 number(Num), 112 Num is B + C, !. 113apply_clpq_constraints(A #<> B) :- !, % JW: Why not simply {A =\= B}? 114 ( apply_clpq_constraints(A #< B) 115 ; apply_clpq_constraints(A #> B) 116 ). 117apply_clpq_constraints(Constraints) :- 118 clpq_meta(Constraints). 119 120dump_clpq_var([Ground], [NewVar], Constraints) :- 121 ground(Ground), 122 Constraints = [NewVar #= Ground]. 123dump_clpq_var(Var, NewVar, Constraints) :- 124 \+ ground(Var), 125 clpqr_dump_constraints([Var], [NewVar], Constraints). 126 127dual_clpq([Unique], [Dual]) :- 128 dual_clpq_(Unique, Dual). 129dual_clpq([Init, Next|Is], Dual) :- 130 ( dual_clpq([Init], Dual) 131 ; dual_clpq([Next|Is], NextDual), 132 Dual = [Init|NextDual] 133 ). 134 135dual_clpq_(A #< B, A #>= B). 136dual_clpq_(A #=< B, A #> B). 137dual_clpq_(A #> B, A #=< B). 138dual_clpq_(A #>= B, A #< B). 139dual_clpq_(A #<> B, A #= B). 140%dual_clpq_(A #= B, A .<>. B). 141dual_clpq_(A #= B, A #> B). 142dual_clpq_(A #= B, A #< B). 143 144 145disequality_clpq(A, B) :- 146 \+ is_clpq_var(B), !, 147 ( apply_clpq_constraints([A #> B]) 148 ; apply_clpq_constraints([A #< B]) 149 ). 150 151% Success if StoreA >= StoreB 152entails(VarA, (VarB, StoreB)) :- 153 dump_clpq_var(VarA, VarB, StoreA), 154 clpq_meta(StoreB), 155 clpq_entailed(StoreA). 156 157% Success if StoreA >= StoreB 158store_entails(StoreA, StoreB) :- 159 clpq_meta(StoreB), 160 clpq_entailed(StoreA). 161 162% Success if S >= Goal 163entail_terms(Goal, S) :- 164 \+ Goal \= S, 165 clp_varset(Goal, VsGoal), 166 VsGoal \= [], 167 clp_varset(S, VsS), 168 clpqr_dump_constraints(VsGoal, DumpVars, StoreGoal), 169 clpqr_dump_constraints(VsS, DumpVars, StoreVsS), 170 store_entails(StoreVsS,StoreGoal). 171 172clp_varset(Term, ClpVars) :- 173 term_attvars(Term, Vars), 174 include(is_clpq_var, Vars, ClpVars). 175 176% :- set_prolog_flag(write_attributes, portray). 177 178itf:attr_portray_hook(_, A) :- 179 \+ \+ ( clpqr_dump_constraints([A], [X], Constraints), 180 ( Constraints == [] 181 -> write(A) 182 ; reverse(Constraints, RC), 183 pretty_print(RC, X) 184 ) 185 ). 186 187pretty_print([], _). 188pretty_print([C], X) :- pretty_print_(C, X). 189pretty_print([C1, C2|Cs], X) :- pretty_print_(C1, X), display(', '), pretty_print([C2|Cs], X). 190 191pretty_print_(nonzero(Var), X) => 192 ( Var == X 193 -> format('nonzero(\u2627)') 194 ; write(nonzero(Var)) 195 ). 196pretty_print_(C, X), compound(C), C =.. [Op, A, B] => 197 ( pretty_op(Op, Pretty) 198 -> true 199 ; Pretty = Op 200 ), 201 pretty_print_(A, X), format(' ~q ', [Pretty]), pretty_print_(B, X), !. 202pretty_print_(A, X) => 203 ( A == X 204 -> format('\u2627') 205 ; write(A) 206 ). 207 208pretty_op(#<, <). 209pretty_op(#=<, =<). 210pretty_op(#>, >). 211pretty_op(#>=, >=). 212pretty_op(#=, =). 213pretty_op(#<>, \=)