tests/rtest_boolean.mac

   1 (kill (all), 0);
   2 0;
   3
   4 /* Test simplification of boolean expressions.
   5  * '(...) expressions are simplified but not evaluated.
   6  */
   7
   8 ['("and" ()), '("or" ())];      /* analogous to * and + with no arguments */
   9 [true, false];
  10
  11 /* These values are supposed to be ignored in quoted expressions '(...).
  12  */
  13 (a : true, b : false, c : true, 0);
  14 0;
  15
  16 ('(a and b), [op (%%), args (%%)]);
  17 ["and", '[a, b]];
  18
  19 ('(a or b), [op (%%), args (%%)]);
  20 ["or", '[a, b]];
  21
  22 ('(not a), [op (%%), args (%%)]);
  23 ["not", '[a]];
  24
  25 ('(a and b or c and d), [op (%%), args (%%)]);
  26 ["or", ['(a and b), '(c and d)]];
  27
  28 ('((a or b) and (c or d)), [op (%%), args (%%)]);
  29 ["and", ['(a or b), '(c or d)]];
  30
  31 '(a and true);
  32 'a;
  33
  34 '(a and false);
  35 false;
  36
  37 '(a or true);
  38 true;
  39
  40 '(a or false);
  41 'a;
  42
  43 '[true and true, true and false, true or true, true or false, false and true, false and false, false or true, false or false];
  44 [true, false, true, true, false, false, true, false];
  45
  46 '((a or true) and (b or true));
  47 true;
  48
  49 '(a and true or b and true);
  50 '(a or b);
  51
  52 '(a or b or c or false);
  53 '(a or b or c);
  54
  55 '(a and b and c and true);
  56 '(a and b and c);
  57
  58 '(not (a and b));
  59 '((not a) or (not b));
  60
  61 '(not a and b);
  62 '((not a) and b);
  63
  64 '(not (a or b));
  65 '((not a) and (not b));
  66
  67 '(not (a or b or c or d or e));
  68 '((not a) and (not b) and (not c) and (not d) and (not e));
  69
  70 '(not (a and b and c and d and e));
  71 '((not a) or (not b) or (not c) or (not d) or (not e));
  72
  73 '(not (a or b and c or d and e));
  74 '((not a) and ((not b) or (not c)) and ((not d) or (not e)));
  75
  76 '(not (a and not b or c and not d and not e));
  77 '(((not a) or b) and ((not c) or d or e));
  78
  79 '(not a or b);
  80 '((not a) or b);
  81
  82 '(not not a);
  83 'a;
  84
  85 '(not not not a);
  86 '(not a);
  87
  88 '(not not not not a);
  89 'a;
  90
  91 /* Flattening nested expressions.
  92  * Maxima "and" and "or" are not commutative, so order of arguments should be preserved.
  93  * Flattening is a simplification => should happen in both simplification and evaluation.
  94  */
  95
  96 kill (all);
  97 done;
  98
  99 ('(x and b and ((h and d) and c) and y), [op (%%), args (%%)]);
 100 ["and", [x, b, h, d, c, y]];
 101
 102 ('(x or b or ((h or d) or c) or y), [op (%%), args (%%)]);
 103 ["or", [x, b, h, d, c, y]];
 104
 105 '(x and b and ((h or d) or c) and (y and q and e));
 106 x and b and (h or d or c) and y and q and e;
 107
 108 (x and b and ((h and d) and c) and y, [op (%%), args (%%)]);
 109 ["and", [x, b, h, d, c, y]];
 110
 111 (x or b or ((h or d) or c) or y, [op (%%), args (%%)]);
 112 ["or", [x, b, h, d, c, y]];
 113
 114 x and b and ((h or d) or c) and (y and q and e);
 115 x and b and (h or d or c) and y and q and e;
 116
 117 /* Side-effects shouldn't happen in simplification (since arguments are not evaluated).
 118  */
 119
 120 (kill (a, b, c), 0);
 121 0;
 122
 123 ('((a : true) and (b : false) and (c : foo ())), [op (%%), args (%%), a, b, c]);
 124 ["and", '[a : true, b : false, c : foo ()], 'a, 'b, 'c];
 125
 126 ('(not (a : true)), [op (%%), args (%%), a]);
 127 ["not", '[a : true], 'a];
 128
 129 /* Miscellaneous tests.
 130  */
 131 expr: '(a > b and (equal (c, d) or e = 1) and not f <= g or notequal (h, %pi));
 132 '(a > b and (equal (c, d) or e = 1) and f > g or notequal (h, %pi));
 133
 134 '(a > b and b > c and true or a < b and b < c and true or false or not true);
 135 '((a > b and b > c) or (a < b and b < c));
 136
 137 '(not not not not a > b);
 138 '(a > b);
 139
 140 '(not not not not not a > b);
 141 '(a <= b);
 142
 143 '(not not not false and not not not not true);
 144 true;
 145
 146 '(not foo (a));
 147 ''(funmake ("not", '[foo (a)]));
 148
 149 '[is (not a > b or false), is (not a > b or true), is (not a > b and false)];
 150 '[is (a <= b), true, false];
 151
 152 '['is (not a > b or false), 'is (not a > b or true), 'is (not a > b and false)];
 153 '['is (a <= b), true, false];
 154
 155 '[maybe (not a > b or false), maybe (not a > b or true), maybe (not a > b and false)];
 156 '[maybe (a <= b), true, false];
 157
 158 '['maybe (not a > b or false), 'maybe (not a > b or true), 'maybe (not a > b and false)];
 159 '['maybe (a <= b), true, false];
 160
 161 /* Test evaluation of boolean expressions.
 162  * Evaluate the arguments and simplify.
 163  */
 164
 165 ["and" (), "or" ()];      /* analogous to * and + with no arguments */
 166 [true, false];
 167
 168 (a and b, [op (%%), args (%%)]);
 169 ["and", '[a, b]];
 170
 171 (a or b, [op (%%), args (%%)]);
 172 ["or", '[a, b]];
 173
 174 (not a, [op (%%), args (%%)]);
 175 ["not", '[a]];
 176
 177 (a and b or c and d, [op (%%), args (%%)]);
 178 ["or", ['(a and b), '(c and d)]];
 179
 180 ((a or b) and (c or d), [op (%%), args (%%)]);
 181 ["and", ['(a or b), '(c or d)]];
 182
 183 a and true;
 184 'a;
 185
 186 a and false;
 187 false;
 188
 189 a or true;
 190 true;
 191
 192 a or false;
 193 'a;
 194
 195 (a or true) and (b or true);
 196 true;
 197
 198 a and true or b and true;
 199 '(a or b);
 200
 201 a or b or c or false;
 202 '(a or b or c);
 203
 204 a and b and c and true;
 205 '(a and b and c);
 206
 207 not (a and b);
 208 '((not a) or (not b));
 209
 210 not a and b;
 211 '((not a) and b);
 212
 213 not (a or b);
 214 '((not a) and (not b));
 215
 216 not (a or b or c or d or e);
 217 '((not a) and (not b) and (not c) and (not d) and (not e));
 218
 219 not (a and b and c and d and e);
 220 '((not a) or (not b) or (not c) or (not d) or (not e));
 221
 222 not (a or b and c or d and e);
 223 '((not a) and ((not b) or (not c)) and ((not d) or (not e)));
 224
 225 not (a and not b or c and not d and not e);
 226 '(((not a) or b) and ((not c) or d or e));
 227
 228 not a or b;
 229 '((not a) or b);
 230
 231 not not a;
 232 'a;
 233
 234 not not not a;
 235 '(not a);
 236
 237 not not not not a;
 238 'a;
 239
 240 /* Side-effects should happen in evaluation.
 241  */
 242
 243 ((a : true) and (b : true) and (c : foo ()), [%%, a, b, c]);
 244 [foo (), true, true, foo ()];
 245
 246 (not (a : bar ()), [%%, a]);
 247 ['(not bar ()), bar ()];
 248
 249 (kill (a, b, c), 0);
 250 0;
 251
 252 /* Miscellaneous tests.
 253  */
 254 expr: a > b and (equal (c, d) or e = 1) and not f <= g or notequal (h, %pi);
 255 '(a > b and equal (c, d) and f > g or notequal (h, %pi));
 256
 257 ''expr, e=1;
 258 '(a > b and equal (c, d) and f > g or notequal (h, %pi));
 259
 260 ''expr, e=1, h=%e;
 261 true;
 262
 263 ''expr, e=1, h=%pi;
 264 '(a > b and equal (c, d) and f > g);
 265
 266 ''expr, e=89, f = g + 1;
 267 '(a > b and equal (c, d) or notequal (h, %pi));
 268
 269 (assume (notequal (c, d), equal (f, 100), g < 0), 0);
 270 0;
 271
 272 ''expr, e = 1;
 273 '(notequal (h, %pi));
 274
 275 a > b and b > c and true or a < b and b < c and true or false or not true;
 276 '((a > b and b > c) or (a < b and b < c));
 277
 278 not not not not a > b;
 279 '(a > b);
 280
 281 not not not not not a > b;
 282 '(a <= b);
 283
 284 not not not false and not not not not true;
 285 true;
 286
 287 /* is-evaluation of conditionals.
 288  * is(foo) => true, false, and unknown or error (depending on prederror flag).
 289  */
 290
 291 ev (is (a > b or a > c), prederror=false);
 292 unknown;
 293
 294 errcatch (ev (is (a > b or a > c), prederror=true));
 295 [];
 296
 297 [is (not a > b or true), is (not a > b and false), 'is (not a > b or true), 'is (not a > b and false)];
 298 [true, false, true, false];
 299
 300 [maybe (not a > b or false), maybe (not a > b or true), maybe (not a > b and false)];
 301 [unknown, true, false];
 302
 303 ['maybe (not a > b or false), 'maybe (not a > b or true), 'maybe (not a > b and false)];
 304 ['maybe (a <= b), true, false];
 305
 306 is (not a > b or true);
 307 true;
 308
 309 is (not a > b and false);
 310 false;
 311
 312 ev (maybe (not a > b or false), prederror=false);
 313 unknown;
 314
 315 ev (maybe (not a > b or false), prederror=true);
 316 unknown;
 317
 318 ev (maybe (not a > b), a = 100.0, b = 1000/3);
 319 true;
 320
 321 ev (maybe (not a > b), b = 100.0, a = 1000/3);
 322 false;
 323
 324 (kill (aa, bb, cc, dd),
 325  implies (a%, b%) := (not a%) or b%,
 326  equivalent (a%, b%) := implies (a%, b%) and implies (b%, a%),
 327  translate (implies, equivalent));
 328 [implies, equivalent];
 329
 330 /* output not fully simplified -- these next two tests show bugs */
 331
 332 implies (aa and bb, cc or dd);
 333 not (aa) or not (bb) or cc or dd;
 334
 335 implies (aa and bb, aa);
 336 not (aa) or not (bb) or aa;
 337
 338 equivalent (aa, aa);
 339 (not aa or aa) and (not aa or aa);
 340
 341 /* crime scene example from mailing list 2006/05/06 tnx Mario */
 342
 343 (kill (all),
 344  "=>" (r, s) := not r or s,
 345  infix ("=>"),
 346  implies (ante, conse, listvar) := block ([expr, npos, maxn, combis:[], bits, quot, div],
 347     npos: length(listvar),
 348     maxn: 2^npos - 1,
 349     expr: not ante or conse,
 350     for i:0 thru maxn do
 351        (bits: [],
 352         quot: i,
 353         for j: 1 thru npos do
 354            (div: divide (quot, 2),
 355             quot: div[1],
 356             bits: cons (listvar[j]=div[2], bits)),
 357         combis: cons (subst ([1=true, 0=false], bits), combis)),
 358     apply ("and", makelist (subst (k, expr), k, combis))), 0);
 359 0;
 360
 361 implies ((p or q) and (q => r) and (p => s) and not r, s, [p, q, r, s]);
 362 true;
 363
 364 /* charfun examples following email discussion circa 2007-03-23 */
 365
 366 (kill (x, y, z), expr : charfun (-1 < x and x < 1));
 367 '(charfun (-1 < x and x < 1));
 368
 369 [ev (expr, x = 1/2), ev (expr, x = -3/2)];
 370 [1, 0];
 371
 372 expr : charfun (x > 0 or y > 0);
 373 '(charfun (x > 0 or y > 0));
 374
 375 [ev (expr, x = 1/2), ev (expr, x = -3/2), ev (expr, x = -3/2, y = -3/4)];
 376 [1, '(charfun (y > 0)), 0];
 377
 378 /* ensure that arguments to is and maybe are evaluated exactly once */
 379
 380 (kill (aa, bb, cc),
 381  aa : bb : cc,
 382  cc : 1234,
 383  is (aa = bb));
 384 true;
 385
 386 is (aa = 'cc and bb = 'cc);
 387 true;
 388
 389 is ('aa = 'bb);
 390 false;
 391
 392 maybe (aa = bb);
 393 true;
 394
 395 maybe (aa = 'cc and bb = 'cc);
 396 true;
 397
 398 maybe ('aa = 'bb);
 399 false;
 400
 401 /* SF bug [ 1726148 ] maybe with prederror : true */
 402
 403 (kill (a), ev (maybe (a), prederror = true));
 404 unknown;
 405
 406 ev (maybe (a or false), prederror = true);
 407 unknown;
 408