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: WARNING: 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)
The equality operator in SMT-LIB generally requires, unsurprisingly, that its operands be of the same type. For example, this is an error: (set-logic QF_LIRA) (declare-fun a () Bool) (declare-fun b () ...
I m playing around with Z3 s QBVF solver, and wondering if it s possible to extract values from an existential assertion. To wit, let s say I have the following: (assert (exists ((x (_ BitVec 16))) (...
I am trying to use Z3 to reason about substrings, and have come across some non-intuitive behavior. Z3 returns sat when asked to determine if xy appears within xy , but it returns unknown when ...
Is it possible to label Z3 scopes (SMTLib2 syntax) and to then pop back to a specific one? For example: (push foo) ; ... (push) ; ... (pop foo) ; pops two scopes I know that I can pop two scopes ...
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: ...
Has anyone tried proving Z3 with Z3 itself? Is it even possible, to prove that Z3 is correct, using Z3? More theoretical, is it possible to prove that tool X is correct, using X itself?
The SMTLib2 directive (get-info all-statistics) displays several numbers, e.g. num. conflicts: 4 num. propagations: 0 (binary: 0) num. qa. inst: 23 In order to test different ...
I am trying to use the Z3 SMT solver for my projects. However it seems there is a mismatch of the Visual Studio versions, which caused my troubles. My Visual Studio 2008 reports that The ...