| 1 | :- module(ast_to_difference_logic, [rewrite_to_idl/2, | |
| 2 | rewrite_to_idl_no_zero/2, | |
| 3 | rewrite_inequality_to_idl_disj_no_zero/2, | |
| 4 | remove_zero_var/2, | |
| 5 | remove_idl_origin_from_info/2, | |
| 6 | get_int_value/2]). | |
| 7 | ||
| 8 | :- use_module(library(lists), [maplist/3, select/3]). | |
| 9 | :- use_module(probsrc(preferences)). | |
| 10 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 11 | ||
| 12 | add_original_constraint_to_info(_, [], []). | |
| 13 | add_original_constraint_to_info(Constraint, [DLConstraint|T], [NDLConstraint|NT]) :- | |
| 14 | DLConstraint = b(Node,Type,Info), | |
| 15 | NDLConstraint = b(Node,Type,[idl_origin(Constraint)|Info]), | |
| 16 | add_original_constraint_to_info(Constraint, T, NT). | |
| 17 | ||
| 18 | rewrite_to_idl_no_zero(Constraint, ConjList) :- | |
| 19 | rewrite_to_idl(Constraint, TConjList), | |
| 20 | maplist(remove_zero_var, TConjList, ConjList). | |
| 21 | ||
| 22 | remove_zero_var(b(less_equal(Sub,Cst),pred,Info), b(less_equal(NSub,Cst),pred,Info)) :- | |
| 23 | Sub = b(minus(_,_),integer,_), | |
| 24 | remove_zero_var_from_sub(Sub, NSub). | |
| 25 | remove_zero_var(b(negation(Term),pred,Info), New) :- | |
| 26 | !, | |
| 27 | remove_zero_var(Term, NewTerm), | |
| 28 | New = b(negation(NewTerm),pred,Info). | |
| 29 | remove_zero_var(b(conjunct(C1,C2),pred,Info), Out) :- | |
| 30 | !, | |
| 31 | remove_zero_var(C1, NC1), | |
| 32 | remove_zero_var(C2, NC2), | |
| 33 | Out = b(conjunct(NC1,NC2),pred,Info). | |
| 34 | remove_zero_var(b(disjunct(C1,C2),pred,Info), Out) :- | |
| 35 | !, | |
| 36 | remove_zero_var(C1, NC1), | |
| 37 | remove_zero_var(C2, NC2), | |
| 38 | Out = b(disjunct(NC1,NC2),pred,Info). | |
| 39 | remove_zero_var(Term, Term). | |
| 40 | ||
| 41 | remove_zero_var_from_sub(b(minus(b(identifier('_zero'),integer,_),Rhs),integer,Info), NSub) :- | |
| 42 | !, | |
| 43 | NSub = b(unary_minus(Rhs),integer,Info). | |
| 44 | remove_zero_var_from_sub(b(minus(Lhs, b(identifier('_zero'),integer,_)),integer,_), NSub) :- | |
| 45 | !, | |
| 46 | NSub = Lhs. | |
| 47 | remove_zero_var_from_sub(Sub, Sub). | |
| 48 | ||
| 49 | is_idl_candidate(negation(Pred)) :- | |
| 50 | Pred = b(Node,_,_), | |
| 51 | is_idl_candidate(Node). | |
| 52 | is_idl_candidate(less(_,_)). | |
| 53 | is_idl_candidate(less_equal(_,_)). | |
| 54 | is_idl_candidate(greater(_,_)). | |
| 55 | is_idl_candidate(greater_equal(_,_)). | |
| 56 | is_idl_candidate(equal(_,_)). | |
| 57 | is_idl_candidate(not_equal(_,_)). | |
| 58 | ||
| 59 | %% rewrite_to_idl(+Constraint, -ConjList). | |
| 60 | % Returns a list of conjuncts. | |
| 61 | % The constraint is normalized by AST cleanup and only <, <= or its negations or =, negated /= are used on the top level. | |
| 62 | rewrite_to_idl(Constraint, ConjList) :- | |
| 63 | Constraint = b(Node,pred,_), | |
| 64 | is_idl_candidate(Node), | |
| 65 | temporary_set_preference(normalize_ast_sort_commutative, true), | |
| 66 | clean_up_pred(Constraint, _, Clean), | |
| 67 | reset_temporary_preference(normalize_ast_sort_commutative), | |
| 68 | rewrite_to_idl_clean(Clean, TConjList), | |
| 69 | add_original_constraint_to_info(Constraint, TConjList, ConjList). | |
| 70 | ||
| 71 | remove_idl_origin_from_info(b(Node,Type,Info), NewNode) :- | |
| 72 | select(idl_origin(_), Info, NInfo), | |
| 73 | !, | |
| 74 | NewNode = b(Node,Type,NInfo). | |
| 75 | remove_idl_origin_from_info(Ast, Ast). | |
| 76 | ||
| 77 | %% rewrite_inequality_to_idl_disj_no_zero(+Inequality, -DLConstraint). | |
| 78 | rewrite_inequality_to_idl_disj_no_zero(Inequality, DLConstraint) :- | |
| 79 | ( Inequality = b(not_equal(Lhs,Rhs),pred,ConjInfo) | |
| 80 | ; Inequality = b(negation(b(equal(Lhs,Rhs),pred,ConjInfo)),pred,[]) | |
| 81 | ), | |
| 82 | rewrite_to_idl_pos(b(equal(Lhs,Rhs),pred,ConjInfo), ConjList),!, | |
| 83 | ConjList = [TArg1,TArg2], | |
| 84 | remove_zero_var(TArg1, Arg1), | |
| 85 | remove_zero_var(TArg2, Arg2), | |
| 86 | NArg1 = b(negation(Arg1),pred,[]), | |
| 87 | NArg2 = b(negation(Arg2),pred,[]), | |
| 88 | DLConstraint = b(disjunct(NArg1,NArg2),pred,[idl_origin(Inequality)]). | |
| 89 | ||
| 90 | rewrite_to_idl_clean(b(negation(Inequality),pred,_), Out) :- | |
| 91 | % not(x/=y) -> x=y | |
| 92 | Inequality = b(not_equal(Lhs,Rhs),pred,EqInfo), | |
| 93 | !, | |
| 94 | Equality = b(equal(Lhs,Rhs),pred,EqInfo), | |
| 95 | rewrite_to_idl_pos(Equality, Out). | |
| 96 | rewrite_to_idl_clean(b(negation(Constraint),pred,Info), Out) :- | |
| 97 | !, | |
| 98 | rewrite_to_idl_pos(Constraint, ConjList), | |
| 99 | % negation of /= is covered above, other operators provide singleton list | |
| 100 | ConjList = [DLConstraint], | |
| 101 | Out = [b(negation(DLConstraint),pred,Info)]. | |
| 102 | rewrite_to_idl_clean(Constraint, DLConstraint) :- | |
| 103 | rewrite_to_idl_pos(Constraint, DLConstraint). | |
| 104 | ||
| 105 | % TO DO: do not use b/3 on top level of first argument | |
| 106 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 107 | % c <= x-y -> y-x <= -c | |
| 108 | Constraint = b(less_equal(Constant,Rhs),pred,Info), | |
| 109 | get_int_value(Constant, CVal), | |
| 110 | rewrite_to_difference(Rhs, TRhs), | |
| 111 | switch_arguments_in_difference(TRhs, NRhs), | |
| 112 | !, | |
| 113 | NCVal is CVal * -1, | |
| 114 | NConstraint = b(less_equal(NRhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 115 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 116 | % x+-y <= c -> x-y <= c | x-y <= c -> x-y <= c | |
| 117 | % x <= c -> x-_zero <= c | -x <= c -> _zero-x <= c | |
| 118 | Constraint = b(less_equal(Lhs,Constant),pred,Info), | |
| 119 | get_int_value(Constant, _), | |
| 120 | rewrite_to_difference(Lhs, NLhs), | |
| 121 | !, | |
| 122 | NConstraint = b(less_equal(NLhs,Constant),pred,Info). | |
| 123 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 124 | % x <= y -> x-y <= 0 | |
| 125 | Constraint = b(less_equal(Id1,Id2),pred,Info), | |
| 126 | Id1 = b(identifier(_),_,_), | |
| 127 | Id2 = b(identifier(_),_,_), | |
| 128 | !, | |
| 129 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 130 | NConstraint = b(less_equal(NLhs,b(integer(0),integer,[])),pred,Info). | |
| 131 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 132 | % -x <= y -> y-x <= 0 | |
| 133 | Constraint = b(less_equal(Id1,Id2),pred,Info), | |
| 134 | Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]), | |
| 135 | Id2 = b(identifier(_),_,_), | |
| 136 | !, | |
| 137 | NLhs = b(minus(Id2,Id1),integer,[]), | |
| 138 | NConstraint = b(less_equal(NLhs,b(integer(0),integer,[])),pred,Info). | |
| 139 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 140 | % c <= y -> _zero-y <= -c | c <= -y -> y-_zero <= -c | |
| 141 | Constraint = b(less_equal(Constant,Id2),pred,Info), | |
| 142 | get_int_value(Constant, CVal), | |
| 143 | ( Id2 = b(identifier(Id2Name),integer,Id2Info) | |
| 144 | -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[]) | |
| 145 | ; Id2 = b(unary_minus(NegId2),integer,[]) | |
| 146 | ), | |
| 147 | rewrite_to_difference(NegId2, Diff), | |
| 148 | !, | |
| 149 | NCVal is CVal * -1, | |
| 150 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 151 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 152 | % c1 <= y-c2 -> _zero-y <= -c2-c1 | c1 <= -y-c2 -> y-_zero <= -c2-c1 | |
| 153 | Constraint = b(less_equal(Constant1,AddOrSub),pred,Info), | |
| 154 | get_int_value(Constant1, CVal1), | |
| 155 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2), | |
| 156 | get_int_value(Constant2, CVal2), | |
| 157 | ( Id2 = b(identifier(Id2Name),integer,Id2Info) | |
| 158 | -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[]) | |
| 159 | ; Id2 = b(unary_minus(NegId2),integer,[]) | |
| 160 | ), | |
| 161 | rewrite_to_difference(NegId2, Diff), | |
| 162 | !, | |
| 163 | NCVal is CVal2 + CVal1 * -1, | |
| 164 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 165 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 166 | % x <= y-c -> x-y <= -c | x <= y+c -> x-y <= c | |
| 167 | Constraint = b(less_equal(Id1,AddOrSub),pred,Info), | |
| 168 | Id1 = b(identifier(_),_,_), | |
| 169 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant), | |
| 170 | !, | |
| 171 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 172 | NConstraint = b(less_equal(NLhs,Constant),pred,Info). | |
| 173 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 174 | % x - c <= y -> x-y <= c | x + c <= y -> x-y <= -c | |
| 175 | Constraint = b(less_equal(AddOrSub,Id2),pred,Info), | |
| 176 | Id2 = b(identifier(_),_,_), | |
| 177 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant), | |
| 178 | get_int_value(Constant, CVal), | |
| 179 | !, | |
| 180 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 181 | NCVal is CVal * -1, | |
| 182 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 183 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 184 | % x - c1 <= c2 -> x-_zero <= c2+c1 | x + c1 <= c2 -> x-_zero <= c2-c1 | |
| 185 | Constraint = b(less_equal(AddOrSub,Constant2),pred,Info), | |
| 186 | get_int_value(Constant2, CVal2), | |
| 187 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1), | |
| 188 | get_int_value(Constant1, CVal1), | |
| 189 | !, | |
| 190 | rewrite_to_difference(Id1, Diff), | |
| 191 | NCVal is CVal2 + CVal1 * -1, | |
| 192 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 193 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 194 | % x+c1 <= y-c2 -> x-y <= -c2-c1 | x + c1 <= y+c2 -> x-y <= c2-c1 | |
| 195 | % x-c1 <= y-c2 -> x-y <= -c2+c1 | x-c1 <= y+c2 -> x-y <= c2+c1 | |
| 196 | Constraint = b(less_equal(AddOrSub1,AddOrSub2),pred,Info), | |
| 197 | get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1), | |
| 198 | get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2), | |
| 199 | get_int_value(Constant1, CVal1), | |
| 200 | get_int_value(Constant2, CVal2), | |
| 201 | !, | |
| 202 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 203 | NCVal is CVal2 + CVal1 * -1, | |
| 204 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 205 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 206 | % c < x-y -> y-x <= -c-1 | |
| 207 | Constraint = b(less(Constant,Rhs),pred,Info), | |
| 208 | get_int_value(Constant, CVal), | |
| 209 | rewrite_to_difference(Rhs, TRhs), | |
| 210 | switch_arguments_in_difference(TRhs, NRhs), | |
| 211 | !, | |
| 212 | NCVal is CVal * -1 - 1, | |
| 213 | NConstraint = b(less_equal(NRhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 214 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 215 | % x+-y < c -> x-y <= c-1 | x-y < c -> x-y <= c-1 | |
| 216 | % x < c -> x-_zero <= -c-1 | -x < c -> _zero-x <= -c-1 | |
| 217 | Constraint = b(less(Lhs,Constant),pred,Info), | |
| 218 | get_int_value(Constant, CVal), | |
| 219 | rewrite_to_difference(Lhs, NLhs), | |
| 220 | !, | |
| 221 | NCVal is CVal - 1, | |
| 222 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 223 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 224 | % x < y -> x-y <= -1 | |
| 225 | Constraint = b(less(Id1,Id2),pred,Info), | |
| 226 | Id1 = b(identifier(_),_,_), | |
| 227 | Id2 = b(identifier(_),_,_), | |
| 228 | !, | |
| 229 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 230 | NConstraint = b(less_equal(NLhs,b(integer(-1),integer,[])),pred,Info). | |
| 231 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 232 | % -x < y -> y-x <= -1 | |
| 233 | Constraint = b(less(Id1,Id2),pred,Info), | |
| 234 | Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]), | |
| 235 | Id2 = b(identifier(_),_,_), | |
| 236 | !, | |
| 237 | NLhs = b(minus(Id2,Id1),integer,[]), | |
| 238 | NConstraint = b(less_equal(NLhs,b(integer(-1),integer,[])),pred,Info). | |
| 239 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 240 | % c < y -> _zero-y <= -c-1 | c < -y -> y-_zero <= -c-1 | |
| 241 | Constraint = b(less(Constant,Id2),pred,Info), | |
| 242 | get_int_value(Constant, CVal), | |
| 243 | ( Id2 = b(identifier(Id2Name),integer,Id2Info) | |
| 244 | -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[]) | |
| 245 | ; Id2 = b(unary_minus(NegId2),integer,[]) | |
| 246 | ), | |
| 247 | rewrite_to_difference(NegId2, Diff), | |
| 248 | !, | |
| 249 | NCVal is CVal * -1 - 1, | |
| 250 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 251 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 252 | % c1 < y-c2 -> _zero-y <= -c2-c1-1 | c1 <= -y-c2 -> y-_zero <= -c2-c1-1 | |
| 253 | Constraint = b(less(Constant1,AddOrSub),pred,Info), | |
| 254 | get_int_value(Constant1, CVal1), | |
| 255 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2), | |
| 256 | get_int_value(Constant2, CVal2), | |
| 257 | ( Id2 = b(identifier(Id2Name),integer,Id2Info) | |
| 258 | -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[]) | |
| 259 | ; Id2 = b(unary_minus(NegId2),integer,[]) | |
| 260 | ), | |
| 261 | rewrite_to_difference(NegId2, Diff), | |
| 262 | !, | |
| 263 | NCVal is CVal2 + CVal1 * -1 - 1, | |
| 264 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 265 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 266 | % x < y-c -> x-y <= -c-1 | x < y+c -> x-y <= c-1 | |
| 267 | Constraint = b(less(Id1,AddOrSub),pred,Info), | |
| 268 | Id1 = b(identifier(_),_,_), | |
| 269 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant), | |
| 270 | get_int_value(Constant, CVal), | |
| 271 | !, | |
| 272 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 273 | NCVal is CVal - 1, | |
| 274 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 275 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 276 | % x-c < y -> x-y <= c-1 | x+c < y -> x-y <= -c-1 | |
| 277 | Constraint = b(less(AddOrSub,Id2),pred,Info), | |
| 278 | Id2 = b(identifier(_),_,_), | |
| 279 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant), | |
| 280 | get_int_value(Constant, CVal), | |
| 281 | !, | |
| 282 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 283 | NCVal is CVal * -1 - 1, | |
| 284 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 285 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 286 | % x - c1 < c2 -> x-_zero <= c2+c1-1 | x + c1 < c2 -> x-_zero <= c2-c1-1 | |
| 287 | Constraint = b(less(AddOrSub,Constant2),pred,Info), | |
| 288 | get_int_value(Constant2, CVal2), | |
| 289 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1), | |
| 290 | rewrite_to_difference(Id1, Diff), | |
| 291 | get_int_value(Constant1, CVal1), | |
| 292 | !, | |
| 293 | rewrite_to_difference(Id1, Diff), | |
| 294 | NCVal is CVal2 + CVal1 * -1 - 1, | |
| 295 | NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info). | |
| 296 | rewrite_to_idl_pos(Constraint, [NConstraint]) :- | |
| 297 | % x+c1 < y-c2 -> x-y <= -c2-c1-1 | x+c1 < y+c2 -> x-y <= c2-c1-1 | |
| 298 | % x-c1 < y-c2 -> x-y <= -c2+c1-1 | x-c1 < y+c2 -> x-y <= c2+c1-1 | |
| 299 | Constraint = b(less(AddOrSub1,AddOrSub2),pred,Info), | |
| 300 | get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1), | |
| 301 | get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2), | |
| 302 | get_int_value(Constant1, CVal1), | |
| 303 | get_int_value(Constant2, CVal2), | |
| 304 | !, | |
| 305 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 306 | NCVal is CVal2 + CVal1 * -1 - 1, | |
| 307 | NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info). | |
| 308 | rewrite_to_idl_pos(Constraint, ConjList) :- | |
| 309 | % c = _ -> rewrite(_ = c) | |
| 310 | Constraint = b(equal(Constant,Rhs),pred,Info), | |
| 311 | get_int_value(Constant, _), | |
| 312 | \+ get_int_value(Rhs, _), | |
| 313 | !, | |
| 314 | rewrite_to_idl_pos(b(equal(Rhs,Constant),pred,Info), ConjList). | |
| 315 | rewrite_to_idl_pos(Constraint, [NC1,NC2]) :- | |
| 316 | % x-y = c -> x-y <= c & y-x <= -c | x+-y = c -> x-y <= c & y-x <= -c | |
| 317 | Constraint = b(equal(Lhs,Constant),pred,Info), | |
| 318 | get_int_value(Constant, CVal), | |
| 319 | !, | |
| 320 | rewrite_to_difference(Lhs, Diff), | |
| 321 | switch_arguments_in_difference(Diff, SDiff), | |
| 322 | NCVal is CVal * -1, | |
| 323 | NC1 = b(less_equal(Diff,Constant),pred,Info), | |
| 324 | NC2 = b(less_equal(SDiff,b(integer(NCVal),integer,[])),pred,Info). | |
| 325 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 326 | % x = y-c -> rewrite(x-y = -c) | x = y+c -> rewrite(x-y = c) | |
| 327 | Constraint = b(equal(Id1,AddOrSub),pred,Info), | |
| 328 | Id1 = b(identifier(_),_,_), | |
| 329 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant), | |
| 330 | !, | |
| 331 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 332 | rewrite_to_idl_pos(b(equal(NLhs,Constant),pred,Info), NConstraint). | |
| 333 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 334 | % x-c1 = y-c2 -> rewrite(x-y = -c2+c1) | x-c1 = y+c2 -> rewrite(x-y = c1+c2) | |
| 335 | % x+c1 = y-c2 -> rewrite(x-y = -c2-c1) | x+c1 = y+c2 -> rewrite(x-y = c1-c2) | |
| 336 | Constraint = b(equal(AddOrSub1,AddOrSub2),pred,Info), | |
| 337 | get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1), | |
| 338 | get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2), | |
| 339 | get_int_value(Constant1, CVal1), | |
| 340 | get_int_value(Constant2, CVal2), | |
| 341 | !, | |
| 342 | NCVal is CVal2 + CVal1 * -1, | |
| 343 | NLhs = b(minus(Id1,Id2),integer,[]), | |
| 344 | rewrite_to_idl_pos(b(equal(NLhs,b(integer(NCVal),integer,[])),pred,Info), NConstraint). | |
| 345 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 346 | % x = y -> rewrite(x-y = 0) | |
| 347 | Constraint = b(equal(Id1,Id2),pred,Info), | |
| 348 | Id1 = b(identifier(_),_,_), | |
| 349 | Id2 = b(identifier(_),_,_), | |
| 350 | !, | |
| 351 | Constraint2 = b(equal(b(minus(Id1,Id2),integer,[]),b(integer(0),integer,[])),pred,Info), | |
| 352 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 353 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 354 | % -x = -y -> rewrite(y-x = 0) | |
| 355 | Constraint = b(equal(Id1,Id2),pred,Info), | |
| 356 | Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]), | |
| 357 | Id2 = b(unary_minus(PosId2),integer,[]), | |
| 358 | !, | |
| 359 | Constraint2 = b(equal(b(minus(PosId2,Id1),integer,[]),b(integer(0),integer,[])),pred,Info), | |
| 360 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 361 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 362 | % x-c = y -> rewrite(x-y = c) | x+c = y -> rewrite(x-y = -c) | |
| 363 | Constraint = b(equal(AddOrSub,Id2),pred,Info), | |
| 364 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant), | |
| 365 | Id2 = b(identifier(_),_,_), | |
| 366 | get_int_value(Constant, CVal), | |
| 367 | !, | |
| 368 | NCVal is CVal * -1, | |
| 369 | Constraint2 = b(equal(b(minus(Id1,Id2),integer,[]),b(integer(NCVal),integer,[])),pred,Info), | |
| 370 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 371 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 372 | % c1 = y-c2 -> rewrite(y = c1+c2) | c1 = y+c2 -> rewrite(y = c1-c2) | |
| 373 | Constraint = b(equal(Constant1,AddOrSub),pred,Info), | |
| 374 | get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2), | |
| 375 | get_int_value(Constant1, CVal1), | |
| 376 | get_int_value(Constant2, CVal2), | |
| 377 | !, | |
| 378 | NCVal is CVal1 + CVal2 * -1, | |
| 379 | Constraint2 = b(equal(Id2,b(integer(NCVal),integer,[])),pred,Info), | |
| 380 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 381 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 382 | % x-c1 = c2 -> rewrite(x = c2+c1) | x+c1 = c2 -> rewrite(x = c2-c1) | |
| 383 | Constraint = b(equal(AddOrSub,Constant2),pred,Info), | |
| 384 | get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1), | |
| 385 | get_int_value(Constant1, CVal1), | |
| 386 | get_int_value(Constant2, CVal2), | |
| 387 | !, | |
| 388 | NCVal is CVal2 + CVal1 * -1, | |
| 389 | Constraint2 = b(equal(Id1,b(integer(NCVal),integer,[])),pred,Info), | |
| 390 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 391 | rewrite_to_idl_pos(Constraint, NConstraint) :- | |
| 392 | % x = c -> rewrite(x-_zero = c) | -x = c -> rewrite(_zero-x = c) | |
| 393 | Constraint = b(equal(Id1,Constant),pred,Info), | |
| 394 | Id1 = b(identifier(_),_,_), | |
| 395 | get_int_value(Constant, _), | |
| 396 | !, | |
| 397 | rewrite_to_difference(Id1, Diff), | |
| 398 | Constraint2 = b(equal(Diff,Constant),pred,Info), | |
| 399 | rewrite_to_idl_pos(Constraint2, NConstraint). | |
| 400 | ||
| 401 | get_args_of_add_or_minus_to_addition(b(add(Id,Constant),integer,_), Id, Constant) :- | |
| 402 | Id = b(identifier(_),integer,_), | |
| 403 | get_int_value(Constant, _). | |
| 404 | get_args_of_add_or_minus_to_addition(b(minus(Id,Constant),integer,_), Id, b(integer(NCVal),integer,[])) :- | |
| 405 | % x-c -> x+-c | |
| 406 | Id = b(identifier(_),integer,_), | |
| 407 | get_int_value(Constant, CVal), | |
| 408 | NCVal is CVal * -1. | |
| 409 | ||
| 410 | switch_arguments_in_difference(b(minus(Lhs,Rhs),integer,Info), b(minus(Rhs,Lhs),integer,Info)). | |
| 411 | ||
| 412 | %% rewrite_to_difference(+IdOrDiff, -Diff). | |
| 413 | % Possibly introduce artificial variable _zero. | |
| 414 | rewrite_to_difference(Id, Diff) :- | |
| 415 | % x -> x-_zero | |
| 416 | Id = b(identifier(_),integer,_), | |
| 417 | !, | |
| 418 | Diff = b(minus(Id,b(identifier('_zero'),integer,[])),integer,[]). | |
| 419 | rewrite_to_difference(UId, Diff) :- | |
| 420 | % -x -> _zero-x | |
| 421 | UId = b(unary_minus(b(identifier(IdName),integer,IdInfo)),integer,_), | |
| 422 | !, | |
| 423 | Diff = b(minus(b(identifier('_zero'),integer,[]),b(identifier(IdName),integer,IdInfo)),integer,[]). | |
| 424 | rewrite_to_difference(Add, Diff) :- | |
| 425 | % x+-y -> x-y | |
| 426 | Add = b(add(b(identifier(V1),integer,Info1),b(unary_minus(Id2),integer,_)),integer,InfoAdd), | |
| 427 | Id2 = b(identifier(_),integer,_), | |
| 428 | Diff = b(minus(b(identifier(V1),integer,Info1),Id2),integer,InfoAdd). | |
| 429 | rewrite_to_difference(Diff, Diff) :- | |
| 430 | % difference of positive integer ids | |
| 431 | Diff = b(minus(b(identifier(_),integer,_),b(identifier(_),integer,_)),_,_). | |
| 432 | ||
| 433 | %% get_int_value(+IntegerAst, -Value). | |
| 434 | get_int_value(b(integer(Value),integer,_), Value). | |
| 435 | get_int_value(b(value(int(Value)),integer,_), Value). |