Screamer

     http://groups.google.com/group/screamer/

     git clone git://github.com/nikodemus/screamer.git

     http://github.com/nikodemus/screamer

     (all-values
       (let ((x (either 1 2 3 4)))
         (if (oddp x)
             x
             (fail)))) ; => (1 3)

     ;;; Screamer already provides an-integer-between, so we'll
     ;;; call this by a different name.
     (defun an-int-between (min max)
       (if (> min max)
           (fail)
           (either min (an-int-between (1+ min) max))))
     
     (all-values (an-int-between 41 43)) ; => (41 42 43)

     ;;; Square numbers are numbers produced by multiplying an integer with itself.
     (defun a-square-number (min max)
       (let* ((x (an-integer-between 0 max))
              (square (* x x)))
         (if (<= min square max)
             square
             (fail))))
     
     (all-values (a-square-number 12 80)) ; => (16 25 36 49 64)

     (defun a-comedic-actor ()
       (list (either :tall :short) (either :thin :fat)))
     
     (defun a-comedy-duo ()
       (let ((a (a-comedic-actor))
             (b (a-comedic-actor)))
         (if (or (eq (first a) (first b))
                 (eq (second a) (second b)))
             (fail)
             (list a :and b))))
     
     (one-value (a-comedy-duo)) ; => ((:TALL :THIN) :AND (:SHORT :FAT))

     (let ((n 0))
       (list :numbers
             (all-values (let ((x (an-integer-between 0 3)))
                           (incf n)
                           x))
             :n n)) ; => (:NUMBERS (0 1 2 3) :N 4)

     (let ((m 0)
           (n 0))
       (list :numbers
             (all-values (let ((x (an-integer-between 0 3)))
                           (local
                             (incf n)
                             (global
                               (incf m)))
                           x))
             :m m
             :n n)) ; => (:NUMBERS (0 1 2 3) :M 4 :N 0)

     ;;; Make a variable
     (defparameter *v* (make-variable "The Answer"))
     
     ;;; It is initially unconstrained.
     *v* ; => ["The Answer"]
     
     ;;; Constrain it to be an integer.
     (assert! (integerpv *v*))
     
     *v* ; => ["The Answer" integer]
     
     ;;; Constrain 40 to be 2 less than *v*
     (assert! (=v 40 (-v *v* 2)))
     
     ;;; And we have our answer.
     *v* ; => 42

     (defparameter *x* (make-variable "X"))
     (defparameter *y* (make-variable "Y"))
     
     (assert! (integerpv *x*))
     (assert! (integerpv *y*))
     
     (assert! (=v 0 (+v *x* *y* 42)))
     
     (all-values (let ((x (an-integer-between -50 -30))
                       (y (an-integer-between 2 5)))
                   (assert! (=v *x* x))
                   (assert! (=v *y* y))
                   (list x y))) ; => ((-47 5) (-46 4) (-45 3) (-44 2))

     (assert! (=v *x* (an-integer-betweenv -50 -30)))
     (assert! (=v *y* (an-integer-betweenv 2 5)))
     
     (all-values
       (solution (list *x* *y*)
                 (static-ordering #'linear-force))) => ((-47 5) (-46 4) (-45 3) (-44 2))

     (local (incf (foo)))

— Macro: either &body expressions

Nondeterministically evaluates and returns the value of one of its expressions.

either takes any number of arguments. With no arguments, (either) is equivalent to (fail) and is thus deterministic. With one argument, (either expression) is equivalent to expression itself and is thus deterministic only when expression is deterministic. With two or more argument it is nondeterministic and can only appear in a nondeterministic context.

It sets up a choice point and evaluates the first expression returning its result. Whenever backtracking proceeds to this choice point, the next expression is evaluated and its result returned. When no more expressions remain, the current choice point is removed and backtracking continues to the next most recent choice point.

As an optimization, the choice point created for this expression is removed before the evaluation of the last expression so that a failure during the evaluation of the last expression will backtrack directly to the parent choice point of the either expression.

either is a special form, not a function. It is an error for the expression #'either to appear in a program.

— Function: fail

Backtracks to the most recent choise point. Equivalent to (either). Note that fail is deterministic function and thus it is permissible to reference #'fail, and write (funcall #'fail) or (apply #'fail). In nondeterministic contexts, the expression (fail) is optimized to generate inline backtracking code.

— Macro: all-values &body expressions

Evaluates expressions as an implicit progn and returns a list of all of the nondeterministic values returned by the last expression.

These values are produced by repeatedly evaluating the body and backtracking to produce the next value, until the body fails and yields no further values.

Accordingly, local side effects performed by the body while producing each value are undone before attempting to produce subsequent values, and all local side effects performed by the body are undone upon exit from all-values.

Returns the list containing nil if there are no expressions. An all-values expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the all-values expression appears in, the expressions are always in a nondeterministic context. An all-values expression itself is always deterministic. all-values is analogous to the bagof primitive in Prolog.

— Macro: one-value expression &optional default-expression

Returns the first value of a nondeterministic expression. expression is evaluated, deterministically returning only its first nondeterministic value, if any.

No further execution of expression is attempted after it successfully returns one value.

If expression does not return any nondeterministic values (i.e. it fails) then default-expression is evaluated and its value returned instead. default-expression defaults to (fail) if not present.

Local side effects performed by expression are undone when one-value returns, but local side effects performed by default-expression are not undone when one-value returns.

A one-value expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the one-value expression appears in, expression is always in a nondeterministic context, while default-expression is in whatever context the one-value expression appears.

A one-value expression is nondeterministic if default-expression is present and is nondeterministic, otherwise it is deterministic.

If default-expression is present and nondeterministic, and if expression fails, then it is possible to backtrack into the default-expression and for the one-value expression to nondeterministically return multiple times. one-value is analogous to the cut primitive (!) in Prolog.

— Macro: for-effects &body forms

Evaluates forms as an implicit progn in a nondeterministic context and returns nil.

The body is repeatedly backtracked to its first choice-point until the body fails.

Local side effects performed by forms are undone when for-effects returns.

A for-effects expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the for-effects expression appears in, forms are always in a nondeterministic context.

A for-effects expression is is always deterministic.

— Macro: ith-value i expression &optional default-expression

Returns the Ith value of a nondeterministic expression. expression is evaluated, deterministically returning only its Ith nondeterministic value, if any. I must be an integer. The first nondeterministic value returned by expression is numbered zero, the second one, etc. The Ith value is produced by repeatedly evaluating expression, backtracking through and discarding the first I values and deterministically returning the next value produced.

No further execution of expression is attempted after it successfully returns the desired value.

If expression fails before returning both the I values to be discarded, as well as the desired Ith value, then default-expression is evaluated and its value returned instead. default-expression defaults to (fail) if not present.

Local side effects performed by expression are undone when ith-value returns, but local side effects performed by default-expression and by I are not undone when ith-value returns.

An ith-value expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the ith-value expression appears in, expression is always in a nondeterministic context, while default-expression and I are in whatever context the ith-value expression appears.

An ith-value expression is nondeterministic if default-expression is present and is nondeterministic, or if I is nondeterministic. Otherwise it is deterministic.

If default-expression is present and nondeterministic, and if expression fails, then it is possible to backtrack into the default-expression and for the ith-value expression to nondeterministically return multiple times.

If I is nondeterministic then the ith-value expression operates nondeterministically on each value of I. In this case, backtracking for each value of expression and default-expression is nested in, and restarted for, each backtrack of I.

— Macro: print-values &body expressions

Evaluates expressions as an implicit progn and prints each of the nondeterministic values returned by the last expression in succession using print.

After each value is printed, the user is queried as to whether or not further values are desired. These values are produced by repeatedly evaluating the body and backtracking to produce the next value, until either the user indicates that no further values are desired or until the body fails and yields no further values.

Accordingly, local side effects performed by the body while producing each value are undone after printing each value, before attempting to produce subsequent values, and all local side effects performed by the body are undone upon exit from print-values, either because there are no further values or because the user declines to produce further values.

A print-values expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the print-values expression appears in, the expressions are always in a nondeterministic context. A print-values expression itself is always deterministic and always returns nil.

print-values is analogous to the standard top-level user interface in Prolog.

— Macro: possibly? &body forms

Evaluates forms as an implicit progn in nondeterministic context, returning true if the body ever yields true.

The body is repeatedly backtracked as long as it yields nil. Returns the first true value yielded by the body, or nil if body fails before yielding true.

Local side effects performed by the body are undone when possibly? returns.

A possibly? expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the possibly? expression appears in, its body is always in a nondeterministic context.

A possibly? expression is always deterministic.

— Macro: necessarily? &body forms

Evaluates forms as an implicit progn in nondeterministic context, returning true if the body never yields false.

The body is repeatedly backtracked as long as it yields true. Returns the last true value yielded by the body if it fails before yielding nil, otherwise returns nil.

Local side effects performed by the body are undone when necessarily? returns.

A necessarily? expression can appear in both deterministic and nondeterministic contexts. Irrespective of what context the necessarily? expression appears in, its body is always in a nondeterministic context.

A necessarily? expression is always deterministic.

— Macro: global &body expressions

Evaluates expressions in the same fashion as progn except that all setf and setq expressions lexically nested in its body result in global side effects which are not undone upon backtracking.

Note that this affects only side effects introduced explicitly via setf and setq. Side effects introduced by Common Lisp builtin functions such as rplaca are always global anyway.

Furthermore, it affects only occurrences of setf and setq which appear textually nested in the body of the global expression -- not those appearing in functions called from the body.

local and global expressions may be nested inside one another. The nearest surrounding declaration determines whether or not a given setf or setq results in a local or global side effect.

Side effects default to be global when there is no surrounding local or global expression. Global side effects can appear both in deterministic as well as nondeterministic contexts. In nondeterministic contexts, global as well as setf are treated as special forms rather than macros. This should be completely transparent to the user.

— Macro: local &body expressions

Evaluates expressions in the same fashion as progn except that all setf and setq expressions lexically nested in its body result in local side effects which are undone upon backtracking.

This affects only side effects introduced explicitly via setf and setq. Side effects introduced by either user defined functions or builtin Common Lisp functions such as rplaca are always global.

Behaviour of side effects introduced by macro-expansions such as incf depends on the exact macro-expansion. If (incf (foo)) expands using eg. set-foo, local is unable to undo the side-effect.

local does not currently distinguish between initially uninitialized and intialized places, such as unbound variables or hash-table keys with no prior values. As a result, an attempt to assign an unbound variable inside local will signal an error due to the system's attempt to first read the variable. Similarly, undoing a (setf gethash) when the key did not previously exist in the table will insert a nil into the table instead of doing a remhash.

local and global expressions may be nested inside one another. The nearest surrounding declaration determines whether or not a given setf or setq results in a local or global side effect.

Side effects default to be global when there is no surrounding local or global expression. Local side effects can appear both in deterministic as well as nondeterministic contexts though different techniques are used to implement the trailing of prior values for restoration upon backtracking. In nondeterministic contexts, local as well as setf are treated as special forms rather than macros. This should be completely transparent to the user.

— Function: a-boolean

Equivalent to (either t nil).

— Function: a-member-of sequence

Nondeterministically returns an element of sequence. The elements are returned in the order that they appear in sequence. The sequence must be either a list or a vector.

— Function: an-integer

Generator yielding integers in sequence 0, 1, -1, 2, -2, ...

— Function: an-integer-above low

Generator yielding integers starting from low and continuing sequentially in increasing direction.

— Function: an-integer-below high

Generator yielding integers starting from high and continuing sequentially in decreasing direction.

— Function: an-integer-between low high

Nondeterministically returns an integer in the closed interval [low, high]. The results are returned in ascending order. Both low and high must be integers. Fails if the interval does not contain any integers.

— Function: apply-nondeterministic function &rest arguments

Analogous to the cl:apply, except function can be either a nondeterministic function, or an ordinary deterministic function.

You must use apply-nondeterministic to apply a nondeterministic function. An error is signalled if a nondeterministic function object is used with cl:apply.

You can use apply-nondeterministic to apply either a deterministic or nondeterministic function, though even if all of the arguments are deterministic and function is a deterministic function object, the call expression will still be nondeterministic (with presumably a single value), since it is impossible to determine at compile time that a given call to apply-nondeterministic will be passed only deterministic function objects for function.

— Function: funcall-nondeterministic function &rest arguments

Analogous to cl:funcall, except function can be either a nondeterministic function, or an ordinary determinisitic function.

You must use funcall-nondeterministic to funcall a nondeterministic function. An error is signalled if you attempt to funcall a nondeterministic function object with cl:funcall.

You can use funcall-nondeterministic to funcall either a deterministic or nondeterministic function, though even if all of the arguments are deterministic and function is a deterministic function object, the call expression will still be nondeterministic (with presumably a single value), since it is impossible to determine at compile time that a given call to funcall-nondeterministic will be passed only deterministic function objects for function.

— Function: multiple-value-call-nondeterministic function-form &rest values-forms

Analogous to the cl:multiple-value-call, except function-form can evaluate to either a nondeterministic function, or an ordinary deterministic function.

You must use multiple-value-call-nondeterministic to multiple-value-call a nondeterministic function. An error is signalled if a nondeterministic function object is used with cl:multiple-value-call.

You can use multiple-value-call-nondeterministic to call either a deterministic or nondeterministic function, though even if all of the values-forms are deterministic and function-form evaluates to a deterministic function object, the call expression will still be nondeterministic (with presumably a single value), since it is impossible to determine at compile time that a given call to multiple-value-call-nondeterministic will be passed only deterministic function objects for function.

While multiple-value-call-nondeterministic appears to be a function, it is really a special-operator implemented by the code-walkers processing nondeterministic source contexts.

— Function: nondeterministic-function? x

Returns t if x is a nondeterministic function and nil otherwise.

#'foo returns a nondeterministic function object iff it is used in nondeterminisitc context and foo is either a nondeterministic lambda form, or the name of a nondeterministic function defined using screamer::defun.

Currently, if foo is a nondeterministic function defined using screamer::defun, #'foo and (symbol-function 'foo) in deterministic context will return an ordinary deterministic Common Lisp function, which will signal an error at runtime.

— Function: make-variable &optional name

Creates and returns a new variable. Variables are assigned a name which is only used to identify the variable when it is printed. If the parameter name is given then it is assigned as the name of the variable. Otherwise, a unique name is assigned. The parameter name can be any Lisp object.

— Function: value-of x

Returns x if x is not a variable. If x is a variable then value-of dereferences x and returns the dereferenced value. If x is bound then the value returned will not be a variable. If x is unbound then the value returned will be a variable which may be x itself or another variable which is shared with x.

— Function: bound? x

Returns t if x is not a variable or if x is a bound variable. Otherwise returns nil. bound? is analogous to the extra-logical predicates var and nonvar typically available in Prolog.

— Function: ground? x

The primitive ground? is an extension of the primitive bound? which can recursively determine whether an entire aggregate object is bound. Returns t if x is bound and either the value of x is atomic or all of the slots in the value of x are also bound. Otherwise returns nil.

— Macro: assert! x

Restricts x to t. No meaningful result is returned. The argument x can be either a variable or a non-variable.

This assertion may cause other assertions to be made due to noticers attached to x.

A call to assert! fails if x is known not to equal t prior to the assertion or if any of the assertions performed by the noticers result in failure.

Except for the fact that one cannot write #'assert!, assert! behaves like a function, even though it is implemented as a macro.

The reason it is implemented as a macro is to allow a number of compile time optimizations. Expressions like (assert! (notv x)), (assert! (numberpv x)) and (assert! (notv (numberv x))) are transformed into calls to functions internal to Screamer which eliminate the need to create the boolean variable(s) normally returned by functions like notv and numberpv. Calls to the functions numberpv, realpv, integerpv, memberv, booleanpv, =v, <v, <=v, >v, >=v, /=v, notv, funcallv, applyv and equalv which appear directly nested in a call to assert!, or directly nested in a call to notv which is in turn directly nested in a call to assert!, are similarly transformed.

— Macro: known? x

Restricts x to be a boolean. If x is equal to t after being restricted to be boolean, returns t. If x is equal to nil or if the value of x is unknown returns nil. The argument x can be either a variable or a non-variable.

The initial restriction to boolean may cause other assertions to be made due to noticers attached to x. A call to known? fails if x is known not to be boolean prior to the assertion or if any of the assertions performed by the noticers result in failure.

Restricting x to be boolean attaches a noticer on x so that any subsequent assertion which restricts x to be non-boolean will fail.

Except for the fact that one cannot write #'known?, known? behaves like a function, even though it is implemented as a macro.

The reason it is implemented as a macro is to allow a number of compile time optimizations. Expressions like (known? (notv x)), (known? (numberpv x)) and (known? (notv (numberpv x))) are transformed into calls to functions internal to Screamer which eliminate the need to create the boolean variable(s) normally returned by functions like notv and numberv. Calls to the functions numberpv, realpv, integerpv, memberv, booleanpv, =v, <v, <=v, v, >=v, /=v, notv, funcallv, applyv and equalv which appear directly nested in a call to known?, or directly nested in a call to notv which is in turn directly nested in a call to known?, are similarly transformed.

— Macro: decide x

Restricts x to a be boolean. After x is restricted a nondeterministic choice is made. For one branch, x is restricted to equal t and (decide x) returns t as a result. For the other branch, x is restricted to equal nil and (decide x) returns nil as a result. The argument x can be either a variable or a non-variable.

The initial restriction to boolean may cause other assertions to be made due to noticers attached to x. A call to decide immediately fails if x is known not to be boolean prior to the assertion or if any of the assertions performed by the noticers result in failure.

Restricting x to be boolean attaches a noticer on x so that any subsequent assertion which restricts x to be non-boolean will fail.

Except for implementation optimizations (decide x) is equivalent to:

          
            (EITHER (PROGN (ASSERT! X) T) (PROGN (ASSERT! (NOTV X)) NIL))

Except for the fact that one cannot write #'decide, decide behaves like a function, even though it is implemented as a macro.

The reason it is implemented as a macro is to allow a number of compile time optimizations. Expressions like (decide (notv x)), (decide (numberpv x)) and (decide (notv (numberpv x))) are transformed into calls to functions internal to Screamer which eliminate the need to create the boolean variable(s) normally returned by functions like notv and numberv. Calls to the functions numberpv, realpv, integerpv, memberpv, booleanpv, =v, <v, <=v, >v, >=v, /=v, notv, funcallv, applyv and equalv which appear directly nested in a call to decide, or directly nested in a call to notv which is in turn directly nested in a call to decide, are similarly transformed.

— Function: booleanpv x

The expression (booleanpv x) is an abbreviation for (memberv x '(t nil)).

— Function: numberpv x

Returns t if x is known to be numeric, nil if x is known to be non-numeric, and otherwise returns a new boolean variable v.

The values of x and v are mutually constrained via noticers so that v is equal to t if and only if x is known to be numeric and v is equal to nil if and only if x is known to be non-numeric.

• If x later becomes known to be numeric, a noticer attached to x restricts v to equal t. Likewise, if x later becomes known to be non-numeric, a noticer attached to x restricts v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x to be numeric. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x to be non-numeric.

— Function: realpv x

Returns t if x is known to be real, nil if x is known to be non-real, and otherwise returns a new boolean variable v.

The values of x and v are mutually constrained via noticers so that v is equal to t if and only if x is known to be real and v is equal to nil if and only if x is known to be non-real.

• If x later becomes known to be real, a noticer attached to x restricts v to equal t. Likewise, if x later becomes known to be non-real, a noticer attached to x restricts v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x to be real. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x to be non-real.

— Function: integerpv x

Returns t if x is known to be integer valued, and nil if x is known be non-integer value.

If it is not known whether or not x is integer valued when integerpv is called then integerpv creates and returns a new boolean variable v.

The values of x and v are mutually constrained via noticers so that v is equal to t if and only if x is known to be integer valued, and v is equal to nil if and only if x is known to be non-integer valued.

If x later becomes known to be integer valued, a noticer attached to x restricts v to equal t. Likewise, if x later becomes known to be non-integer valued, a noticer attached to x restricts v to equal nil.

Furthermore, if v ever becomes known to equal t then a noticer attached to v restricts x to be integer valued. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x to be non-integer valued.

— Function: memberv x sequence

Returns t if x is known to be a member of sequence (using the Common Lisp function eql as a test function), nil if x is known not to be a member of sequence, and otherwise returns a new boolean variable v.

When a new variable is created, the values of x and v are mutually constrained via noticers so that v is equal to t if and only if x is known to be a member of sequence and v is equal to nil if and only if x is known not to be a member of sequence.

• If x later becomes known to be a member of sequence, a noticer attached to x restricts v to equal t. Likewise, if x later becomes known not to be a member of sequence, a noticer attached to x restricts v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x to be a member of sequence. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x not to be a member of sequence.

The current implementation imposes two constraints on the parameter sequence. First, sequence must be bound when memberv is called. Second, sequence must not contain any unbound variables when memberv is called.

The value of parameter sequence must be a sequence, i.e. either a list or a vector.

— Function: equalv x y

Returns t if the aggregate object x is known to equal the aggregate object y, nil if the aggregate object x is known not to equal the aggregate object y, and a new boolean variable v if it is not known whether or not x equals y when equalv is called.

The values of x, y and v are mutually constraints via noticers so that v equals t if and only if x is known to equal y and v equals nil if and only if x is known not to equal y.

Noticers are attached to v as well as to all variables nested in both in x and y. When the noticers attached to variables nested in x and y detect that x is known to equal y they restrict v to equal t. Likewise, when the noticers attached to variables nested in x and y detect that x is known not to equal y they restrict v to equal nil.

Furthermore, if v later becomes known to equal t then x and y are unified. Likewise, if v later becomes known to equal nil then x and y are restricted to not be equal. This is accomplished by attaching noticers to the variables nested in x and y which detect when x becomes equal to y and fail.

The expression (known? (equalv x y)) is analogous to the extra-logical predicate == typically available in Prolog.

The expression (known? (notv (equalv x y))) is analogous to the extra-logical predicate \= typically available in Prolog.

The expression (assert! (equalv x y)) is analogous to Prolog unification.

The expression (assert! (notv (equalv x y))) is analogous to the disunification operator available in Prolog-II.

— Function: =v x &rest xs

Returns a boolean value which is constrained to be t if all of the arguments are numerically equal, and constrained to be nil if two or more of the arguments numerically differ.

This function takes one or more arguments. All of the arguments are restricted to be numeric.

Returns t when called with one argument. A call such as (=v x1 x2 ... xn) with more than two arguments behaves like a conjunction of two argument calls:

          
            (ANDV (=V X1 X2) ... (=V Xi Xi+1) ... (=V Xn-1 Xn))

When called with two arguments, returns t if x1 is known to be equal to x2 at the time of call, nil if x1 is known not to be equal to x2 at the time of call, and a new boolean variable v if is not known if the two values are equal.

Two numeric values are known to be equal only when they are both bound and equal according to the Common Lisp function =.

Two numeric values are known not to be equal when their domains are disjoint. Furthermore, two real values are known not to be equal when their ranges are disjoint, i.e. the upper bound of one is greater than the lower bound of the other.

When a new variable is created, the values of x1, x2, and v are mutually constrained via noticers so that v is equal to t if and only if x1 is known to be equal to x2, and v is equal to nil if and only if x1 is known not to be equal to x2.

• If it later becomes known that x1 is equal to x2 noticers attached to x1 and x2 restrict v to equal t. Likewise if it later becomes known that x1 is not equal to x2 noticers attached to x1 and x2 restrict v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x1 to be equal to x2. Likewise if v ever becomes known to equal nil then a noticer attached to v restricts x1 not to be equal to x2.
• If x1 is known to be real then the noticer attached to x2 continually restrict the upper bound of x1 to be no higher than the upper bound of x2 and the lower bound of x1 to be no lower than the lower bound of x2. Likewise for bounds of x1 if x2 is known to be real.

Restricting two values x1 and x2 to be equal is performed by attaching noticers to x1 and x2. These noticers continually restrict the domains of x1 and x2 to be equivalent sets (using the Common Lisp function = as a test function) as their domains are restricted.

Restricting two values x1 and x2 to not be equal is also performed by attaching noticers to x1 and x2. These noticers however do not restrict the domains or ranges of x1 or x2. They simply monitor their continually restrictions and fail when any assertion causes x1 to be known to be equal to x2.

— Function: /=v x &rest xs

Returns a boolean value which is constrained to be t if no two arguments are numerically equal, and constrained to be nil if any two or more arguments are numerically equal.

This function takes one or more arguments. All of the arguments are restricted to be numeric.

Returns t when called with one argument. A call such as (/=v x1 x2 ... xn) with more than two arguments behaves like a conjunction of two argument calls:

          
            (ANDV (/=V X1 X2) ... (/=V X1 Xn)
                  (/=V X2 X3) ... (/=V X2 Xn)
                  ...
                  (/=V Xi Xi+1 ... (/=V Xi Xn)
                  ...
                  (/=V Xn-1 xn))

When called with two arguments, returns t if x1 is known not to be equal to x2 at the time of call, nil if x1 is known to be equal to x2 at the time of call, and otherwise a new boolean variable v.

Two numeric values are known not to be equal when their domains are disjoint.

Two real values are known not to be equal when their ranges are disjoint, i.e. the upper bound of one is greater than the lower bound of the other.

Two numeric values are known to be equal only when they are both bound and equal according to the Common Lisp function =.

When a new variable is created, the values of x1, x2 and v are mutually constrained via noticers so that v is equal to t if and only if x1 is known not to be equal to x2 and v is equal to nil if and only if x1 is known to be equal to x2.

• If it later becomes known that x1 is not equal to x2, noticers attached to x1 and x2 restrict v to equal t. Likewise, if it later becomes known that x1 is equal to x2, noticers attached to x1 and x2 restrict v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x1 to not be equal to x2. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x1 to be equal to x2.

Restricting two values x1 and x2 to be equal is performed by attaching noticers to x1 and x2. These noticers continually restrict the domains of x1 and x2 to be equivalent sets (using the Common Lisp function = as a test function) as their domains are restricted. Furthermore, if x1 is known to be real then the noticer attached to x2 continually restrict the upper bound of x1 to be no higher than the upper bound of x2 and the lower bound of x1 to be no lower than the lower bound of x2. The noticer of x2 performs a symmetric restriction on the bounds of x1 if it is known to be real.

Restricting two values x1 and x2 to not be equal is also performed by attaching noticers to x1 and x2. These noticers however, do not restrict the domains or ranges of x1 or x2. They simply monitor their continually restrictions and fail when any assertion causes x1 to be known to be equal to x2.

— Function: <v x &rest xs

Returns a boolean value which is constrained to be t if each argument Xi is less than the following argument Xi+1 and constrained to be nil if some argument Xi is greater than or equal to the following argument Xi+1.

This function takes one or more arguments. All of the arguments are restricted to be real.

Returns t when called with one argument. A call such as (<v x1 x2 ... xn) with more than two arguments behaves like a conjunction of two argument calls:

          
            (ANDV (<V X1 X2) ... (<V Xi Xi+1 ) ... (<V XNn-1 Xn))

When called with two arguments, returns t if x1 is known to be less than x2 at the time of call, nil if x1 is known to be greater than or equal to x2 at the time of call, and otherwise a new boolean variable v.

A real value x1 is known to be less than a real value x2 if x1 has an upper bound, x2 has a lower bound and the upper bound of x1 is less than the lower bound of x2.

A real value x1 is known to be greater than or equal to a real value x2 if x1 has a lower bound, x2 has an upper bound and the lower bound of x1 is greater than or equal to the upper bound of x2.

When a new variable is created, the values of x1, x2 and v are mutually constrained via noticers so that v is equal to t if and only if x1 is known to be less than x2 and v is equal to nil if and only if x1 is known to be greater than or equal to x2.

• If it later becomes known that x1 is less than x2, noticers attached to x1 and x2 restrict v to equal t. Likewise, if it later becomes known that x1 is greater than or equal to x2, noticers attached to x1 and x2 restrict v to equal nil.
• If v ever becomes known to equal t then a noticer attached to v restricts x1 to be less than x2. Likewise, if v ever becomes known to equal nil then a noticer attached to v restricts x1 to be greater than or equal to x2.

Restricting a real value x1 to be less than a real value x2 is performed by attaching noticers to x1 and x2. The noticer attached to x1 continually restricts the lower bound of x2 to be no lower than the upper bound of x1 if x1 has an upper bound. The noticer attached to x2 continually restricts the upper bound of x1 to be no higher than the lower bound of x2 if x2 has a lower bound. Since these restrictions only guarantee that x1 be less than or equal to x2, the constraint that x1 be strictly less than x2 is enforced by having the noticers fail when both x1 and x2 become known to be equal.

Restricting a real value x1 to be greater than or equal to a real value x2 is performed by an analogous set of noticers without this last equality check.

— Function: a-booleanv &optional name

Returns a boolean variable.

— Function: a-realv &optional name

Returns a real variable.

— Function: a-real-abovev low &optional name

Returns a real variable whose value is constrained to be greater than or equal to low.

— Function: a-real-belowv high &optional name

Returns a real variable whose value is constrained to be less than or equal to high.

— Function: a-real-betweenv low high &optional name

Returns a real variable whose value is constrained to be greater than or equal to low and less than or equal to high. If the resulting real variable is bound, its value is returned instead. Fails if it is known that low is greater than high at the time of call.

The expression (a-real-betweenv low high) is an abbreviation for:

          
           (LET ((V (MAKE-VARIABLE)))
              (ASSERT! (REALPV V))
              (ASSERT! (>=V V LOW))
              (ASSERT! (<=V V HIGH))
              (VALUE-OF V))

— Function: an-integerv &optional name

Returns an integer variable.

— Function: an-integer-abovev low &optional name

Returns an integer variable whose value is constrained to be greater than or equal to low.

— Function: an-integer-belowv high &optional name

Returns an integer variable whose value is constrained to be less than or equal to high.

— Function: an-integer-betweenv low high &optional name

Returns an integer variable whose value is constrained to be greater than or equal to low and less than or equal to high. If the resulting integer variable is bound, its value is returned instead. Fails if it is known that there is no integer between low and high at the time of call.

The expression (an-integer-betweenv low high) is an abbreviation for:

          
           (LET ((V (MAKE-VARIABLE)))
              (ASSERT! (INTEGERPV V))
              (ASSERT! (>=V V LOW))
              (ASSERT! (<=V V HIGH))
              (VALUE-OF v))

— Variable: *maximum-discretization-range*

Discretize integer variables whose range is not greater than this number. Discretize all integer variables if nil. Must be an integer or nil.

— Variable: *minimum-shrink-ratio*

Ignore propagations which reduce the range of a variable by less than this ratio.

— Variable: *strategy*

Strategy to use for funcallv and applyv. Either :gfc for Generalized Forward Checking, or :ac for Arc Consistency. Default is :gfc.

— Function: purge function-name

Removes any information about function-name from Screamer's who-calls database.

— Function: unwedge-screamer

Removes any information about all user defined functions from Screamer's who-calls database.

— Variable: *dynamic-extent?*

Set to t to enable the dynamic extent optimization, nil to disable it. Default is platform dependent.

— Variable: *screamer-version*

The version of Screamer which is loaded. This is currently still 3.20, while we're considering how to express versions for this copy of Screamer in the future.

— Variable: *iscream?*

t if Screamer is running under ILisp/GNUEmacs with iscream.el loaded.