[Maxima-commits] CVS: maxima/share/contrib/boolsimp boolsimp.lisp, 1.10, 1.11 rtest_boolsimp.mac, 1.7, 1.8

[Robert D. <rob...@us...>]

Update of /cvsroot/maxima/maxima/share/contrib/boolsimp
In directory sc8-pr-cvs7.sourceforge.net:/tmp/cvs-serv22701

Modified Files:
	boolsimp.lisp rtest_boolsimp.mac 
Log Message:
boolsimp.lisp: kill off existing translation properties and
fix a bug in flattening nary expressions.
rtest_boolsimp.mac: put in tests for translated functions and flattened nary expressions.

Index: boolsimp.lisp
===================================================================
RCS file: /cvsroot/maxima/maxima/share/contrib/boolsimp/boolsimp.lisp,v
retrieving revision 1.10
retrieving revision 1.11
diff -u -d -r1.10 -r1.11
--- boolsimp.lisp	23 May 2006 04:19:02 -0000	1.10
+++ boolsimp.lisp	10 Dec 2006 21:58:17 -0000	1.11
@@ -16,7 +16,7 @@
 ;  - flatten conditionals -- nested if --> if -- elseif -- elseif -- elseif -- else
 ;  - arithmetic on conditionals -- distribute arithmetic ops over if
 ;  - make up rules via tellsimp & friends for integrate / sum / diff applied to conditionals
-;  - knock out redundant clauses in simplification (i.e. if x => y then knock out y)
+;  - knock out redundant clauses in simplification (i.e. if x implies y then knock out y)
 
 ; Examples:
 ;
@@ -41,6 +41,11 @@
 ;
 ; Simplification of boolean expressions:
 ;
+; and and or are declared nary. The sole effect of this is to allow Maxima to
+; flatten nested expressions, e.g., a and (b and c) => a and b and c
+; (The nary declaration does not make and and or commutative, and and and or
+; are not otherwise declared commutative.)
+;
 ; and: if any argument simplifies to false, return false
 ;  otherwise omit arguments which simplify to true and simplify others
 ;  if only one argument remains, return it
@@ -115,6 +120,15 @@
 
 (in-package :maxima)
 
+; Kill off translation properties of conditionals and Boolean operators.
+; Ideally we could avoid calling MEVAL when arguments are declared Boolean.
+; We're not there yet.
+
+(remprop 'mcond 'translate)
+(remprop 'mand 'translate)
+(remprop 'mor 'translate)
+(remprop 'mnot 'translate)
+
 ; It's OK for MEVALATOMS to evaluate the arguments of MCOND.
 ; %MCOND already has this property.
 (defprop mcond t evok)
@@ -327,6 +341,36 @@
 
 (defun require-boolean (x) (cond ((or (not x) (eq x t)) x) (t nil)))
 
+; The presence of OPERS tells SIMPLIFYA to call OPER-APPLY,
+; which calls NARY1 to flatten nested "and" and "or" expressions
+; (due to $NARY property of MAND and MOR, declared elsewhere).
+
+(put 'mand t 'opers)
+(put 'mor t 'opers)
+
+; NARY EXPRESSIONS NOT FLATTENED COMPLETELY AT PRESENT
+; BUG IS DUE TO STRANGENESS OF SPECIAL VARIABLE OPERS-LIST
+; WHICH IS MAINTAINED BY OPER-APPLY AND SUBSIDIARIES INCLUDING NARY1
+; DO NOT ATTEMPT TO MODIFY OPER-APPLY -- CHANGE ONLY NARY1
+; EVENTUALLY MOVE THIS CODE INTO SRC/ASUM.LISP
+
+(defun nary1 (e z)
+  (do
+    ((l (cdr e) (cdr l)) (ans) (some-change))
+
+    ((null l)
+     (if some-change
+       (nary1 (cons (car e) (nreverse ans)) z)
+       (let ((w (get (caar e) 'operators)))
+         (if w (funcall w e 1 z) (simpargs e z)))))
+
+    (setq
+      ans (if (and (not (atom (car l))) (eq (caaar l) (caar e)))
+            (progn
+              (setq some-change t)
+              (nconc (reverse (cdar l)) ans))
+            (cons (car l) ans)))))
+
 (putprop 'mnot 'simp-mnot 'operators)
 (putprop 'mand 'simp-mand 'operators)
 (putprop 'mor 'simp-mor 'operators)

Index: rtest_boolsimp.mac
===================================================================
RCS file: /cvsroot/maxima/maxima/share/contrib/boolsimp/rtest_boolsimp.mac,v
retrieving revision 1.7
retrieving revision 1.8
diff -u -d -r1.7 -r1.8
--- rtest_boolsimp.mac	5 May 2006 14:31:38 -0000	1.7
+++ rtest_boolsimp.mac	10 Dec 2006 21:58:17 -0000	1.8
@@ -94,6 +94,32 @@
 '(not not not not a);
 'a;
 
+/* Flattening nested expressions.
+ * Maxima "and" and "or" are not commutative, so order of arguments should be preserved.
+ * Flattening is a simplification => should happen in both simplification and evaluation.
+ */
+
+kill (all);
+done;
+
+('(x and b and ((h and d) and c) and y), [op (%%), args (%%)]);
+["and", [x, b, h, d, c, y]];
+
+('(x or b or ((h or d) or c) or y), [op (%%), args (%%)]);
+["or", [x, b, h, d, c, y]];
+
+'(x and b and ((h or d) or c) and (y and q and e));
+x and b and (h or d or c) and y and q and e;
+
+(x and b and ((h and d) and c) and y, [op (%%), args (%%)]);
+["and", [x, b, h, d, c, y]];
+
+(x or b or ((h or d) or c) or y, [op (%%), args (%%)]);
+["or", [x, b, h, d, c, y]];
+
+x and b and ((h or d) or c) and (y and q and e);
+x and b and (h or d or c) and y and q and e;
+
 /* Side-effects shouldn't happen in simplification (since arguments are not evaluated).
  */
 
@@ -433,3 +459,81 @@
 
 (L : [], (is(first (push (false, L))), if %% then %% else (is(first (push (true, L))), if %% then %% else (is(first (push (true, L))), if %% then %%))), [%%, L]);
 [true, [true, false]];
+
+/* Translation of conditionals and boolean expressions.
+ * Translating this file (rtest_boolsimp.mac) would be a good test,
+ * but the translator is too broken to translate all of the file.
+ */
+
+/* Leave this mode_declare for later.
+ * The effect which would be observable here would be
+ * to trigger an error if some argument is not true or false.
+ * But as it stands, the translation code doesn't exploit
+ * the boolean mode_declare in any way.
+mode_declare ([a%, b%, c%, d%], boolean);
+[[a%, b%, c%, d%]];
+ */
+
+/* Example from mailing list 2006/05/04, tnx Barton */
+
+(kill(f), f(x) := if x < 0 then -1 else 1, 0);
+0;
+
+f(a);
+'if a < 0 then -1 else 1;
+
+(translate(f), f(a));
+'if a < 0 then -1 else 1;
+
+/* Other examples of translated functions */
+
+(my_max (x, y, z) := if x > y and x > z then x elseif y > z then y else z, translate (my_max));
+[my_max];
+
+my_max (11, 33, 22);
+33;
+
+my_max (a + b, c, 1);
+'if a + b > c and a + b > 1 then a + b elseif c > 1 then c else 1;
+
+[assume (c < 1), my_max (a + b, c, 1), forget (c < 1)];
+[[c < 1], 'if a + b > c and a + b > 1 then a + b else 1, [c < 1]];
+
+(kill (aa, bb, cc, dd),
+ implies (a%, b%) := (not a%) or b%,
+ equivalent (a%, b%) := implies (a%, b%) and implies (b%, a%),
+ translate (implies, equivalent));
+[implies, equivalent];
+
+implies (aa and bb, cc or dd);
+not aa or not bb or cc or dd;
+
+implies (aa and bb, aa);
+not aa or not bb or aa;
+
+equivalent (aa, aa);
+(not aa or aa) and (not aa or aa);
+
+/* crime scene example from mailing list 2006/05/06 tnx Mario */
+
+(kill (all),
+ "=>" (r, s) := not r or s,
+ infix ("=>"),
+ implies (ante, conse, listvar) := block ([expr, npos, maxn, combis:[], bits, quot, div],
+    npos: length(listvar),
+    maxn: 2^npos - 1,
+    expr: not ante or conse,
+    for i:0 thru maxn do
+       (bits: [],
+        quot: i,
+        for j: 1 thru npos do
+           (div: divide (quot, 2),
+            quot: div[1],
+            bits: cons (listvar[j]=div[2], bits)),
+        combis: cons (subst ([1=true, 0=false], bits), combis)),
+    apply ("and", makelist (subst (k, expr), k, combis))), 0);
+0;
+
+implies ((p or q) and (q => r) and (p => s) and not r, s, [p, q, r, s]);
+true;
+