Permalink
Browse files

document and fix MINV and MAXV

  Previously argument wasn't constrained to be real in the single argument
  case, and which also returned the variable and not its value, even if bound.
  • Loading branch information...
1 parent 992b28a commit ea26255d94dd81a893eaba3e4ba42e89fdca5446 @nikodemus committed Nov 1, 2011
Showing with 57 additions and 7 deletions.
  1. +0 −2 TODO
  2. +2 −0 doc/screamer.texinfo
  3. +44 −4 screamer.lisp
  4. +11 −1 tests.lisp
View
2 TODO
@@ -33,8 +33,6 @@
******* Restricts vs constrains.
******* Don't talk about noticers: they're an implementation detail.
***** Still missing exported symbols:
-******* minv
-******* maxv
******* apply-substitution
******* linear-force
******* divide-and-conquer-force
View
2 doc/screamer.texinfo
@@ -461,6 +461,8 @@ of Screamer.
@include include/fun-screamer-integerpv.texinfo
@include include/fun-screamer-memberv.texinfo
@include include/fun-screamer-notv.texinfo
+@include include/fun-screamer-minv.texinfo
+@include include/fun-screamer-maxv.texinfo
@include include/fun-screamer-equalv.texinfo
@include include/fun-screamer-plus-v.texinfo
@include include/fun-screamer---v.texinfo
View
48 screamer.lisp
@@ -6025,14 +6025,54 @@ or X2 equals one."
(if (null xs) (/v2 1 x) (/v-internal x xs)))
(defun minv-internal (x xs)
- (if (null xs) x (minv-internal (minv2 x (first xs)) (rest xs))))
+ (cond ((null xs)
+ (assert!-realpv x)
+ (value-of x))
+ (t
+ (minv-internal (minv2 x (first xs)) (rest xs)))))
+
+(defun minv (x &rest xs)
+ "Constrains its arguments to be real. If called with a single argument,
+returns its value. If called with multiple arguments, behaves as if a
+combination of two argument calls:
+
+ \(MINV X1 X2 ... Xn) == (MINV (MINV X1 X2) ... Xn)
+
+If called with two arguments, and either is known to be less than or equal to
+the other, returns the value of that argument. Otherwise returns a real variable
+V, mutually constrained with the arguments:
+
+ * Minimum of the values of X1 and X2 is constrained to equal V. This
+ includes constraining their bounds appropriately. If it becomes know that
+ cannot be true. FAIL is called.
-(defun minv (x &rest xs) (if (null xs) x (minv-internal x xs)))
+ * If both arguments are integers, V is constrained to be an integer."
+ (minv-internal x xs))
(defun maxv-internal (x xs)
- (if (null xs) x (maxv-internal (maxv2 x (first xs)) (rest xs))))
+ (cond ((null xs)
+ (assert!-realpv x)
+ (value-of x))
+ (t
+ (maxv-internal (maxv2 x (first xs)) (rest xs)))))
+
+(defun maxv (x &rest xs)
+ "Constrains its arguments to be real. If called with a single argument,
+returns its value. If called with multiple arguments, behaves as if a
+combination of two argument calls:
+
+ \(MAXV X1 X2 ... Xn) == (MAXV (MAXV X1 X2) ... Xn)
+
+If called with two arguments, and either is known to be greater than or equal
+to the other, returns the value of that argument. Otherwise returns a real
+variable V, mutually constrained with the arguments:
+
+ * Maximum of the values of X1 and X2 is constrained to equal V. This
+ includes constraining their bounds appropriately. If it becomes know that
+ cannot be true. FAIL is called.
-(defun maxv (x &rest xs) (if (null xs) x (maxv-internal x xs)))
+ * If both arguments are integers, V is constrained to be an integer."
+ (maxv-internal x xs))
;;; Lifted Arithmetic Comparison Functions (KNOWN? optimized)
View
12 tests.lisp
@@ -186,4 +186,14 @@
(assert! x)
(assert! y)
(assert! (notv z))
- (value-of n)))))
+ (value-of n)))))
+
+(deftest test-minv.1 ()
+ (is (= 42
+ (let ((x (a-member-ofv '(:a 42))))
+ (minv x)))))
+
+(deftest test-maxv.1 ()
+ (is (= 42
+ (let ((x (a-member-ofv '(:a 42))))
+ (maxv x)))))

0 comments on commit ea26255

Please sign in to comment.