How can I restrict the domain of a sort in Z3 to a single value?

I'm using the following rule in my Z3 program to make s the only possible value of sort S.

(assert (forall ((t S)) (= t s)))

However, the above formula makes Z3 report the following error:

Z3: ERROR: WARN开发者_StackOverflow中文版ING: failed to find a pattern for quantifier (quantifier id: k!8)

What is the right way to make sure that the domain of a particular sort has only a single value?

The message

Z3: ERROR: WARNING: failed to find a pattern for quantifier (quantifier id: k!8)

is misleading. This is just an warning, the “ERROR” word is there by accident. This was fixed, and will be available in the next release. The warning just tells the user that the E-matching module will ignore the quantifier. However, Z3 uses many engines to process quantified formulas. The MBQI module can handle this quantified formula, and build satisfying assignments for problems such as:

(declare-sort S)

(declare-fun s () S)

(assert (forall ((t S)) (= t s)))

(declare-fun a () S)

(declare-fun b () S)

(assert (= a b))

(check-sat)

(model)

That being said, the quantified formula above is not the best way to specify a sort with a single element. You can use datatypes to encode enumeration types. For example, the following command defines a sort S with elements e1 … en. (declare-datatypes ((S e1 e2 … en))) A sort with only one element can be specified using: (declare-datatypes ((S e))) The following example is unsatisfiable:

(declare-datatypes ((S elem)))

(declare-const a S)

(declare-const b S)

(assert (not (= a b)))

(check-sat)