| 1 | % (c) 2014-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(b_simplifier, [simplify_b_predicate/2, tcltk_simplify_b_predicate/2, tcltk_simplify_b_predicate_error/2]). | |
| 6 | ||
| 7 | /* Modules and Infos for the code coverage analysis */ | |
| 8 | :- use_module(probsrc(module_information)). | |
| 9 | :- module_info(group,model_checker). | |
| 10 | :- module_info(description,'This module provides predicates for simplifying B predicates'). | |
| 11 | ||
| 12 | % Classical B prolog modules | |
| 13 | :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2, get_texpr_type/2, create_texpr/4, | |
| 14 | same_texpr/2, different_texpr_values/2, | |
| 15 | is_truth/1, is_falsity/1, is_negation_of/2, | |
| 16 | is_a_conjunct/3, is_a_disjunct/3, is_an_implication/3, | |
| 17 | conjunct_predicates/2, disjunct_predicates/2, | |
| 18 | %% extract_info/3, | |
| 19 | create_negation/2, | |
| 20 | create_implication/3, create_equivalence/3, | |
| 21 | create_forall/3, create_exists/3]). | |
| 22 | :- use_module(probsrc(bmachine),[b_parse_machine_predicate/2]). | |
| 23 | :- use_module(probsrc(kernel_objects),[element_of_global_set/2]). | |
| 24 | ||
| 25 | %% :- use_module(probsrc(parsercall), [parse_predicate/2]). | |
| 26 | ||
| 27 | :- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2]). | |
| 28 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
| 29 | %% :- use_module(probsrc(debug), [debug_print/2, debug_println/2, debug_mode/1]). | |
| 30 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
| 31 | ||
| 32 | % Importing unit tests predicates | |
| 33 | :- use_module(probsrc(self_check)). | |
| 34 | ||
| 35 | % SICSTUS libraries | |
| 36 | :- use_module(library(avl)). | |
| 37 | ||
| 38 | %% atom_codes(String,Codes), | |
| 39 | %% debug_println(20,parsing_as_predicate(Codes)), | |
| 40 | %% eval_strings: repl_typing_scope(TypingScope), | |
| 41 | %% b_parse_machine_predicate_from_codes_open(exists,Codes, % will also mark outer variables so that they are not removed | |
| 42 | %% [],TypingScope,Typed), | |
| 43 | %% debug_println(20,eval_predicate(Typed)), | |
| 44 | ||
| 45 | tcltk_simplify_b_predicate_error(String,StringResult) :- | |
| 46 | if(tcltk_simplify_b_predicate(String,StringResult),true, | |
| 47 | (StringResult = 'Error or User-Interrupt')). | |
| 48 | ||
| 49 | % exported for the Tcl/Tk interface | |
| 50 | tcltk_simplify_b_predicate(String,StringResult) :- | |
| 51 | % parse also boolean expressions as predicates | |
| 52 | temporary_set_preference(bool_expression_as_predicate,true,Chg), | |
| 53 | %% atom_codes(String,Codes), | |
| 54 | %% parse_predicate(Codes,Tree), | |
| 55 | call_cleanup((b_parse_machine_predicate(String,Tree), | |
| 56 | simplify_b_predicate(Tree,Res), | |
| 57 | translate_bexpression(Res,StringResult)), | |
| 58 | reset_temporary_preference(bool_expression_as_predicate,Chg)). | |
| 59 | %extract_type_information(Typed,TypeInfo). | |
| 60 | ||
| 61 | simplify_b_predicate(Pred,Res) :- | |
| 62 | get_texpr_expr(Pred,Expr), | |
| 63 | get_texpr_type(Pred,Type), | |
| 64 | simplify_b_predicate2(Expr,Type,Res). | |
| 65 | ||
| 66 | simplify_b_predicate2(truth,Type,Res) :- !, | |
| 67 | create_texpr(truth,Type,[],Res). | |
| 68 | simplify_b_predicate2(falsity,Type,Res) :- !, | |
| 69 | create_texpr(falsity,Type,[],Res). | |
| 70 | simplify_b_predicate2(negation(BExpr),_Type,Res) :- !, | |
| 71 | simplify_negation(BExpr,Res). | |
| 72 | simplify_b_predicate2(conjunct(LHS,RHS),Type,Res) :- !, | |
| 73 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 74 | ( is_false_constant(SimplifiedLHS) -> % FALSE & f == FALSE | |
| 75 | create_texpr(falsity,Type,[],Res) | |
| 76 | ; is_true_constant(SimplifiedLHS) -> % TRUE & f == f | |
| 77 | simplify_b_predicate(RHS,Res) | |
| 78 | ; otherwise -> | |
| 79 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 80 | ( is_false_constant(SimplifiedRHS) -> % f & FALSE == FALSE | |
| 81 | create_texpr(falsity,Type,[],Res) | |
| 82 | ; is_true_constant(SimplifiedRHS) -> % f & TRUE == f | |
| 83 | Res = SimplifiedLHS | |
| 84 | ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f & f == f (idempotence) | |
| 85 | Res = SimplifiedLHS | |
| 86 | ; is_absorption_rule_conjunct(SimplifiedLHS,SimplifiedRHS,Res) -> % f & (f or g) == f (absorption) | |
| 87 | true | |
| 88 | ; test_transitivity(SimplifiedLHS,SimplifiedRHS,Res) -> % (f => g) & (g => h) == (f => h) | |
| 89 | true | |
| 90 | ; otherwise -> | |
| 91 | conjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res) | |
| 92 | ) | |
| 93 | ). | |
| 94 | simplify_b_predicate2(disjunct(LHS,RHS),Type,Res) :- !, | |
| 95 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 96 | ( is_true_constant(SimplifiedLHS) -> % TRUE or f == TRUE | |
| 97 | create_texpr(truth,Type,[],Res) | |
| 98 | ; is_false_constant(SimplifiedLHS) -> % FALSE or f == f | |
| 99 | simplify_b_predicate(RHS,Res) | |
| 100 | ; otherwise -> | |
| 101 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 102 | ( is_true_constant(SimplifiedRHS) -> % f or TRUE == TRUE | |
| 103 | create_texpr(truth,Type,[],Res) | |
| 104 | ; is_false_constant(SimplifiedRHS) -> % f or FALSE == f | |
| 105 | Res = SimplifiedLHS | |
| 106 | ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f or f == f (idempotence) | |
| 107 | Res = SimplifiedLHS | |
| 108 | ; is_absorption_rule_disjunct(LHS,RHS,Res) -> % f or (f & g) == f (absorption) | |
| 109 | true | |
| 110 | ; otherwise -> | |
| 111 | disjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res) | |
| 112 | ) | |
| 113 | ). | |
| 114 | simplify_b_predicate2(implication(LHS,RHS),_Type,Res) :- !, | |
| 115 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 116 | simplify_implication(LHS,SimplifiedRHS,Res). | |
| 117 | simplify_b_predicate2(equivalence(LHS,RHS),Type,Res) :- !, | |
| 118 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 119 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 120 | ( same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f <=> f == TRUE | |
| 121 | create_texpr(truth,Type,[],Res) | |
| 122 | ; is_negation_of(SimplifiedLHS,SimplifiedRHS) -> % f <=> not(f) == FALSE | |
| 123 | create_texpr(falsity,Type,[],Res) | |
| 124 | ; otherwise -> | |
| 125 | create_equivalence(SimplifiedLHS,SimplifiedRHS,Res) | |
| 126 | ). | |
| 127 | simplify_b_predicate2(equal(LHS,RHS),Type,Res) :- !, | |
| 128 | print(equal(LHS,RHS)),nl, | |
| 129 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 130 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 131 | (same_texpr(SimplifiedLHS,SimplifiedRHS) -> | |
| 132 | create_texpr(truth,Type,[],Res) | |
| 133 | ; different_texpr_values(SimplifiedLHS,SimplifiedRHS) -> | |
| 134 | create_texpr(falsity,Type,[],Res) | |
| 135 | ; otherwise -> | |
| 136 | compare('==',SimplifiedLHS,SimplifiedRHS,equal,Type,Res) | |
| 137 | %% extract_info(SimplifiedLHS,SimplifiedRHS,Info), | |
| 138 | %% create_texpr(equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res) | |
| 139 | ). | |
| 140 | simplify_b_predicate2(not_equal(LHS,RHS),Type,Res) :- !, | |
| 141 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 142 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 143 | (same_texpr(SimplifiedLHS,SimplifiedRHS) -> | |
| 144 | create_texpr(falsity,Type,[],Res) | |
| 145 | ; different_texpr_values(SimplifiedLHS,SimplifiedRHS) -> | |
| 146 | create_texpr(truth,Type,[],Res) | |
| 147 | ; otherwise -> | |
| 148 | compare('=\\=',SimplifiedLHS,SimplifiedRHS,not_equal,Type,Res) | |
| 149 | %% extract_info(SimplifiedLHS,SimplifiedRHS,Info), | |
| 150 | %% create_texpr(not_equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res) | |
| 151 | ). | |
| 152 | simplify_b_predicate2(greater(LHS,RHS),Type,Res) :- !, | |
| 153 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 154 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 155 | compare('>',SimplifiedLHS,SimplifiedRHS,greater,Type,Res). | |
| 156 | simplify_b_predicate2(greater_equal(LHS,RHS),Type,Res) :- !, | |
| 157 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 158 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 159 | compare('>=',SimplifiedLHS,SimplifiedRHS,greater_equal,Type,Res). | |
| 160 | simplify_b_predicate2(less(LHS,RHS),Type,Res) :- !, | |
| 161 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 162 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 163 | compare('<',SimplifiedLHS,SimplifiedRHS,less,Type,Res). | |
| 164 | simplify_b_predicate2(less_equal(LHS,RHS),Type,Res) :- !, | |
| 165 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 166 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 167 | compare('=<',SimplifiedLHS,SimplifiedRHS,less_equal,Type,Res). | |
| 168 | /* Add more sophisticated implementations for simplifying predicates with quatifiers: | |
| 169 | E.g.: !(x).(x:S => x<21) == max(S) < 21 | |
| 170 | !(x).(x:S => x/=3) == 3/:S */ | |
| 171 | % Quantified predcates | |
| 172 | % !(x).(P => Q) | |
| 173 | simplify_b_predicate2(forall(Ids,LHS,RHS),Type,Res) :- !, | |
| 174 | %% trace, | |
| 175 | simplify_b_predicate(RHS,SimplifiedRHS), | |
| 176 | (is_true_constant(SimplifiedRHS) -> | |
| 177 | create_texpr(truth,Type,[],Res) | |
| 178 | ; otherwise -> | |
| 179 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 180 | create_implication(SimplifiedLHS,SimplifiedRHS,ImplicationRes), | |
| 181 | create_forall(Ids,ImplicationRes,Res) | |
| 182 | ). | |
| 183 | % #(x).(P) | |
| 184 | simplify_b_predicate2(exists(Ids,Pred),Type,Res) :- !, | |
| 185 | simplify_b_predicate(Pred,SimplifiedPred), | |
| 186 | (is_true_constant(SimplifiedPred) -> | |
| 187 | create_texpr(truth,Type,[],Res) | |
| 188 | ; is_false_constant(SimplifiedPred) -> | |
| 189 | create_texpr(falsity,Type,[],Res) | |
| 190 | ; otherwise -> | |
| 191 | create_exists(Ids,SimplifiedPred,Res) | |
| 192 | ). | |
| 193 | % Simplifying membership relations | |
| 194 | simplify_b_predicate2(member(Element,Set),Type,Res) :- !, | |
| 195 | simplify_membership_predicate(Element,Set,Type,Res). | |
| 196 | simplify_b_predicate2(not_member(Element,Set),Type,Res) :- !, | |
| 197 | simplify_non_membership_predicate(Element,Set,Type,Res). | |
| 198 | % TODO: do we need to safe additional information about the predicates | |
| 199 | simplify_b_predicate2(BExpr,Type,Res) :- | |
| 200 | create_texpr(BExpr,Type,[],Res). | |
| 201 | %% (debug_mode(on) -> | |
| 202 | %% print('Construct not covered yet (b_simplifier):'),nl, | |
| 203 | %% print(BExpr),nl, | |
| 204 | %% translate:print_bexpr(Res),nl | |
| 205 | %% ; true). | |
| 206 | ||
| 207 | simplify_negation(negation(BExpr),Res) :- !, % double negation "not not f == f" | |
| 208 | simplify_b_predicate(BExpr,Res). | |
| 209 | simplify_negation(BExpr,Res) :- | |
| 210 | simplify_b_predicate(BExpr,SimplifiedBExpr), | |
| 211 | % Simplifications like "not(FALSE) == TRUE" and "not(TRUE) == FALSE" will be applied by create_negation/2 | |
| 212 | create_negation(SimplifiedBExpr,Res). | |
| 213 | ||
| 214 | simplify_implication(_LHS,SimplifiedRHS,Res) :- | |
| 215 | is_true_constant(SimplifiedRHS),!, % f => TRUE == TRUE | |
| 216 | create_texpr(truth,pred,[],Res). | |
| 217 | simplify_implication(LHS,SimplifiedRHS,Res) :- | |
| 218 | is_false_constant(SimplifiedRHS),!, % f => FALSE == neg(f) | |
| 219 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 220 | create_negation(SimplifiedLHS,Res). | |
| 221 | simplify_implication(LHS,SimplifiedRHS,Res) :- | |
| 222 | simplify_b_predicate(LHS,SimplifiedLHS), | |
| 223 | (is_false_constant(SimplifiedLHS) -> % FALSE => f == TRUE | |
| 224 | create_texpr(truth,pred,[],Res) | |
| 225 | ; is_true_constant(SimplifiedLHS) -> % TRUE => f == f | |
| 226 | Res = SimplifiedRHS | |
| 227 | ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f => f == TRUE | |
| 228 | create_texpr(truth,pred,[],Res) | |
| 229 | ; otherwise -> | |
| 230 | create_implication(SimplifiedLHS,SimplifiedRHS,Res) | |
| 231 | ). | |
| 232 | ||
| 233 | ||
| 234 | %%%%%%%%% This is too trivial, we should consider the absorption and transition rules w.r.t. the origin predicate %%%%%%%%% | |
| 235 | % P or (P & Q) == P | |
| 236 | is_absorption_rule_disjunct(LHS,RHS,Res) :- | |
| 237 | is_a_conjunct(RHS,P,Q), | |
| 238 | (same_texpr(LHS,P); same_texpr(LHS,Q)),!, | |
| 239 | Res = LHS. | |
| 240 | % (P & Q) or P == P | |
| 241 | is_absorption_rule_disjunct(LHS,RHS,Res) :- | |
| 242 | is_a_conjunct(LHS,P,Q), | |
| 243 | (same_texpr(RHS,P); same_texpr(RHS,Q)),!, | |
| 244 | Res = RHS. | |
| 245 | ||
| 246 | % P & (P or Q) == P | |
| 247 | is_absorption_rule_conjunct(LHS,RHS,Res) :- | |
| 248 | is_a_disjunct(RHS,P,Q), | |
| 249 | (same_texpr(LHS,P); same_texpr(LHS,Q)),!, | |
| 250 | Res = LHS. | |
| 251 | % (P or Q) & P == P | |
| 252 | is_absorption_rule_conjunct(LHS,RHS,Res) :- | |
| 253 | is_a_disjunct(LHS,P,Q), | |
| 254 | (same_texpr(RHS,P); same_texpr(RHS,Q)),!, | |
| 255 | Res = RHS. | |
| 256 | ||
| 257 | % (P => Q) & (Q => R) == (P => R) | |
| 258 | test_transitivity(LHS,RHS,Res) :- | |
| 259 | is_an_implication(LHS,P,Q), | |
| 260 | is_an_implication(RHS,Q1,R), | |
| 261 | same_texpr(Q,Q1),!, | |
| 262 | create_implication(P,R,Res). | |
| 263 | % (Q => R) & (P => Q) == (P => R) | |
| 264 | test_transitivity(LHS,RHS,Res) :- | |
| 265 | is_an_implication(LHS,Q,R), | |
| 266 | is_an_implication(RHS,P,Q1), | |
| 267 | same_texpr(Q,Q1),!, | |
| 268 | create_implication(P,R,Res). | |
| 269 | ||
| 270 | ||
| 271 | simplify_non_membership_predicate(Element,Set,Type,Res) :- | |
| 272 | b_integer_value(Element,IsIntValue,EX,_NewElement), | |
| 273 | IsIntValue, | |
| 274 | test_integer_membership(Set,EX,Type,Res1),!, | |
| 275 | (is_true_constant(Res1) -> | |
| 276 | create_texpr(falsity,Type,[],Res) | |
| 277 | ; is_false_constant(Res1) -> | |
| 278 | create_texpr(truth,Type,[],Res) | |
| 279 | ; otherwise -> | |
| 280 | add_internal_error('Internal error: Unexpected result from test_integer_membership/4 predicate in simplify_membership_predicate/4: ',Res1) | |
| 281 | ). | |
| 282 | simplify_non_membership_predicate(Element,Set,Type,Res) :- | |
| 283 | b_integer_value(Element,_IsIntValue,_EX,NewElement), | |
| 284 | create_texpr(not_member(NewElement,Set),Type,[],Res). | |
| 285 | ||
| 286 | simplify_membership_predicate(Element,Set,Type,Res) :- | |
| 287 | b_integer_value(Element,IsIntValue,EX,_NewElement), | |
| 288 | IsIntValue, | |
| 289 | test_integer_membership(Set,EX,Type,Res),!. | |
| 290 | simplify_membership_predicate(Element,Set,Type,Res) :- | |
| 291 | b_integer_value(Element,_IsIntValue,_EX,NewElement), | |
| 292 | create_texpr(member(NewElement,Set),Type,[],Res). | |
| 293 | ||
| 294 | ||
| 295 | test_integer_membership(b(empty_set,set(integer),_),_X,Type,Res) :- !, | |
| 296 | create_texpr(falsity,Type,[],Res). | |
| 297 | test_integer_membership(b(value(avl_set(AVLSet)),set(integer),_),X,Type,Res) :- !, | |
| 298 | (avl_fetch(int(X),AVLSet) -> | |
| 299 | create_texpr(truth,Type,[],Res) | |
| 300 | ; otherwise -> | |
| 301 | create_texpr(falsity,Type,[],Res) | |
| 302 | ). | |
| 303 | test_integer_membership(Set,X,Type,Res) :- | |
| 304 | is_interval_set(Set,Low,Up),!, | |
| 305 | ((Low=<X,X=<Up) -> | |
| 306 | create_texpr(truth,Type,[],Res) | |
| 307 | ; otherwise -> | |
| 308 | create_texpr(falsity,Type,[],Res) | |
| 309 | ). | |
| 310 | test_integer_membership(Set,X,Type,Res) :- | |
| 311 | is_global_integer_set(Set,GlobalSet),!, | |
| 312 | (element_of_global_set(int(X),GlobalSet) -> | |
| 313 | create_texpr(truth,Type,[],Res) | |
| 314 | ; otherwise -> | |
| 315 | create_texpr(falsity,Type,[],Res) | |
| 316 | ). | |
| 317 | ||
| 318 | is_interval_set(b(interval(b(Low,integer,_),b(Up,integer,_)),set(integer),_),Low,Up). | |
| 319 | ||
| 320 | is_global_integer_set(Set,GlobalSet) :- | |
| 321 | get_texpr_expr(Set,SetExpr), | |
| 322 | SetExpr = integer_set(GlobalSet), | |
| 323 | memberchk(GlobalSet,['NATURAL','NAT','INTEGER','INT']). | |
| 324 | ||
| 325 | is_true_constant(Expr) :- | |
| 326 | (is_truth(Expr); Expr=boolean_true). | |
| 327 | ||
| 328 | is_false_constant(Expr) :- | |
| 329 | (is_falsity(Expr); Expr=boolean_false). | |
| 330 | ||
| 331 | compare(Operator,LHS,RHS,Functor,Type,Res) :- | |
| 332 | b_integer_value(LHS,IsIntValueX,EX,NewLHS), | |
| 333 | b_integer_value(RHS,IsIntValueY,EY,NewRHS), | |
| 334 | ((IsIntValueX,IsIntValueY) -> | |
| 335 | (memberchk(Operator,['<','>','=<','>=','==','=\\=']) -> | |
| 336 | Call =.. [Operator,EX,EY], | |
| 337 | (Call -> create_texpr(truth,Type,[],Res); create_texpr(falsity,Type,[],Res)) | |
| 338 | ; otherwise -> | |
| 339 | add_internal_error('Internal error: Unexpected arithmetic comparison Operator: ', Operator), | |
| 340 | BExpr =.. [Functor,NewLHS,NewRHS], | |
| 341 | create_texpr(BExpr,Type,[],Res) | |
| 342 | ) | |
| 343 | ; otherwise -> | |
| 344 | BExpr =.. [Functor,NewLHS,NewRHS], | |
| 345 | create_texpr(BExpr,Type,[],Res) | |
| 346 | ). | |
| 347 | ||
| 348 | b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :- | |
| 349 | b_arithmetic_expression(BExpr,X),!, | |
| 350 | Res is X,IsIntValue=true, | |
| 351 | create_texpr(integer(Res),integer,[],NewBExpr). | |
| 352 | b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :- | |
| 353 | Res = BExpr,IsIntValue=false, | |
| 354 | NewBExpr=BExpr. | |
| 355 | ||
| 356 | b_arithmetic_expression(BExpr,Res) :- | |
| 357 | get_texpr_expr(BExpr,Expr), | |
| 358 | get_texpr_type(BExpr,integer), % only an integer expression | |
| 359 | b_arithmetic_expression1(Expr,Res). | |
| 360 | ||
| 361 | b_arithmetic_expression1(integer(X),X) :- !, | |
| 362 | number(X). | |
| 363 | b_arithmetic_expression1(unary_minus(E),Res) :- !, | |
| 364 | b_arithmetic_expression(E,ERes), | |
| 365 | Res = '-'(ERes). | |
| 366 | b_arithmetic_expression1(add(E1,E2),Res) :- !, | |
| 367 | b_arithmetic_expression(E1,E1Res), | |
| 368 | b_arithmetic_expression(E2,E2Res), | |
| 369 | Res = '+'(E1Res,E2Res). | |
| 370 | b_arithmetic_expression1(minus(E1,E2),Res) :- !, | |
| 371 | b_arithmetic_expression(E1,E1Res), | |
| 372 | b_arithmetic_expression(E2,E2Res), | |
| 373 | Res = '-'(E1Res,E2Res). | |
| 374 | b_arithmetic_expression1(multiplication(E1,E2),Res) :- !, | |
| 375 | b_arithmetic_expression(E1,E1Res), | |
| 376 | b_arithmetic_expression(E2,E2Res), | |
| 377 | Res = '*'(E1Res,E2Res). | |
| 378 | % it is not the same div as in Prolog X/Y will be rounded down | |
| 379 | %% b_arithmetic_expression1(div(E1,E2),Res) :- !, | |
| 380 | %% b_arithmetic_expression(E1,E1Res), | |
| 381 | %% b_arithmetic_expression(E2,E2Res), | |
| 382 | %% Res = '//'(E1Res,E2Res). |