I'm attempting to get Z3 to find all possible permutations of a sequence of fixed size that satisfy some constraints. However, I've run into a timeout error with the code I've developed so far:
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
; --------------- Basic Definitions -------------------
(declare-datatypes () ((Obj A B C)))
; --------------- Predicates -------------------------------
(define-sort MyList () (Seq Obj))
(define-fun in_list ((o Obj) (l MyList)) Bool (seq.contains l (seq.unit o)))
(define-fun permutation ((l1 MyList) (l2 MyList)) Bool
(forall ((o Obj)) (= (in_list o l1) (in_list o l2))))
; Two difference permutations of the same list
(declare-const l0 MyList)
(declare-const l1 MyList)
(assert (= 2 (seq.len l0)))
(assert (= 2 (seq.len l1)))
(assert (not (= l1 l0)))
(assert (permutation l0 l1))
; --------------- Verify -------------------
(check-sat)
(get-model)
It seems like this should be a pretty trivial solve (even a brute force should take milliseconds), so I'm pretty baffled what is causing the timeout. Any help?
You're running into limits of what Z3 can do when quantifiers are present.
You might want to look at this question: Defining a Theory of Sets with Z3/SMT-LIB2
In this case, the question is about general set operations, but I think you'll find the answers to apply to your case as well. (In short, disable MBQI, and see if you can use functions instead of sequences.)