Type Restrictions: numberpv realpv integerpv booleanpv memberv
Boolean: andv orv notv
Numeric: <v <=v >v >=v =v /=v +v -v *v /v minv maxv
Expression: equalv
Functions: funcallv applyv

Table 1: The constraint primitives provided by Screamer.

values|and return a variable as their result. The constraint primitive installs a constraint between the arguments and the returned variable stating that, under any interpretation of the variables involved, the value of the result variable must equal the corresponding Common Lisp primitive applied to the values of the arguments. As another example, the expression (<v x y) returns a variable z and adds the constraint z = (< x y). This constraint is satisfied when z is either t or nil depending on whether x is less than y. For the most part, each constraint primitive obeys the same calling convention as the corresponding Common Lisp primitive. Screamer performs a variety of optimizations to improve run time efficiency. In particular, if the value of a variable returned by a constraint primitive can be determined at the time the function is called then that value is returned directly without creating a new variable.

In Screamer, most constraints are of the form z = (f x1 : : : xn) where f is the Common Lisp primitive corresponding to some constraint primitive. Constraints of this form can imply type restrictions on the variables involved. For example, a constraint of the form z = (< x y) implies that z is Boolean", i.e., either t or nil. Furthermore, this constraint implies that x and y are numeric. In practice, a variable usually has a well defined type, e.g., it is known to be Boolean, known be real, known to be a cons cell, etc. Knowledge about the type of a variable has significant ramifications for the efficiency of Screamer's constraint satisfaction algorithms. Screamer has special procedures for inferring the types of variables. Because knowledge of the types of variables is important for efficiency, in contrast to the Common Lisp primitives and, or, and not which accept any arguments of any type, the Screamer constraint primitives andv, orv, and notv require their arguments to be Boolean. This allows the use of Boolean constraint satisfaction techniques for any constraints introduced by these primitives. Similarly, constraint predicates" return Boolean variables. For example, in contrast to the Common Lisp primitive member which can return the sub-list of the second argument whose head satisfies the equality check, the result of the memberv primitive is constrained to be Boolean.
Screamer includes the primitive assert! which

can be used to add constraints other than those added by the constraint primitives. Evaluating the expression (assert! x) constrains x to equal t. This can be used in conjunction with other constraint primitives to install a wide variety of constraints. For example, (assert! (<v x y)) effectively installs the constraint that x must be less than y.1 Certain constraint primitives in table 1, in conjunction with assert!, can be used to directly constrain the type of a variable. For example, evaluating (assert! (numberpv x)) effectively installs the constraint that x must be a number. Likewise evaluating (assert! (booleanpv x)) installs the constraint that x must be Boolean. This is effectively the same as evaluating (assert! (memberv x '(t nil))).

All constraints in Screamer are installed either by assert! or by one of the constraint primitives in table 1. A constraint installed by assert! states that a certain variable must have the value t. A constraint installed by a constraint primitive always has the form z = (f x1 : : : xn) where f is either a Common Lisp primitive or a slight variation on a Common Lisp primitive. The variations arise for constraint primitives such as orv and memberv where the semantics of the constraint version differs slightly from the semantics of the corresponding Common Lisp primitive as discussed above.

An attempt to add a constraint fails if Screamer determines that the resulting set of constraints would be unsatisfiable. For example, after evaluating (assert! (<v x 0)) a subsequent evaluation of (assert! (>v x 0)) will fail. A call to a constraint primitive can fail when it would generate a constraint inconsistent with known type information. For example, if x is known to be Boolean then an evaluation of (+v x y) will fail.

Constraint Propagation

In this section we discuss the five kinds of constraint propagation inference processes performed by Screamer. First, Screamer implements binding propagation, an incomplete inference technique sometimes called value propagation. Second, Screamer implements Boolean constraint propagation (BCP). This is an incomplete form of Boolean inference that can be viewed as a form of unit resolution. Third, Screamer implements generalized forward checking (GFC). This is a constraint propagation technique for discrete constraints used in the CHiP system. Fourth, Screamer implements bounds propagation on numeric variables. Such bounds propagation| when combined with the divide-and-conquer technique

1To mitigate the apparent inefficiency of this conceptually clean language design, the implementation optimizes most calls to assert!, such as the calls (assert! (notv (realpv x))) and (assert! (<=v x y)), to eliminate the creation of the intermediate Boolean variable(s) and the resulting local propagation.