
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.
valuesand 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 sublist 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 divideandconquer 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.