Unknown when working sequence of type StringSort

Question

I am trying to work with sequences (modeling SQL conditions, and need it to work with IN clauses of the form "US" in ImportCountries to see if two conditions can be True at the same time):

s = Solver()
test = Const('test', SeqSort(StringSort()))

expr1 = Contains(test, Unit(StringVal("US")))
expr2 = Not(Contains(test, Unit(StringVal("AE"))))

s.add(And(expr1 == True, expr2 == True))

print(s.check()) # Gives unknown.

Is this a limitation of Z3 or a limitation of my understanding or both?

trying the same with a Int sequence works as expected:

s = Solver()

test = Const('test', SeqSort(IntSort()))

expr1 = Contains(test, Unit(IntVal(1)))
expr2 = Not(Contains(test, Unit(IntVal(2))))

s.add(And(expr1 == True, expr2 == True))

print(s.check())
print(s.model())

Answer 1

You're not doing anything wrong. Looks like z3 is probably missing some internal "heuristics" to decide the string case. Note that when you mix strings and sequences the logic becomes semi-decidable: so this is a case where some internal rule failed to apply. But if the elements are integers, they handle it just fine.

As a point of reference, I tried your problem with CVC5 and it went through just fine. (i.e., CVC5 was able to answer your query in the affirmative.) Here's the SMTLib equivalent of your problem:

(set-option :produce-models true)
(set-logic ALL)
(define-fun s1 () (Seq String) (seq.unit "US"))
(define-fun s3 () (Seq String) (seq.unit "AE"))
(declare-fun s0 () (Seq String))
(define-fun s2 () Bool (seq.contains s0 s1))
(define-fun s4 () Bool (seq.contains s0 s3))
(define-fun s5 () Bool (not s4))
(define-fun s6 () Bool (and s2 s5))
(assert s6)
(check-sat)
(get-value (s0))

With z3 I get:

$ z3 a.smt2
unknown
(error "line 12 column 15: model is not available")

With CVC5 I get:

$ cvc5 a.smt2
sat
((s0 (seq.unit "US")))

You should report this at https://github.com/Z3Prover/z3/issues. While this isn't strictly speaking a bug, I'm sure the developers would love to know about it. (Don't forget to mention that CVC5 solves it just fine!) In the mean time, perhaps you can switch to using CVC5 instead.

Using multiple solvers on the same source

SMTLib is the lingua-franca of SMT solvers, i.e., all SMT solvers understand this format. (https://smtlib.cs.uiowa.edu). Unfortunately, it isn't suitable for end-user programming, this is why most people use higher-level bindings from different languages. Your example itself was in Python using the z3 bindings. There are also bindings from many other languages, and some of these aim to be solver-agnostic. i.e., you express your problem in the host-language, and tell the user to solve it using a given solver, and the infrastructure takes care of all the communication and resolves discrepancies (as best as they can!). When you are dealing with these sorts of problems, you might want to pick a system that allows for easy switching of solvers.

One such library is Haskell's SBV (https://hackage.haskell.org/package/sbv). As an example, here's how you'd code your problem in SBV in a solver agnostic way:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV
import qualified Data.SBV.List as L

problemInt :: ConstraintSet
problemInt = do test :: SList Integer <- sList "test"
                constrain $ 1 `L.elem`    test
                constrain $ 2 `L.notElem` test

problemString :: ConstraintSet
problemString = do test :: SList String <- sList "test"
                   constrain $ "US" `L.elem`    test
                   constrain $ "EN" `L.notElem` test

And now you can "run" it with the supported solvers of your choosing:

test :: IO ()
test = do solve z3   "Z3,   Int:"    problemInt
          solve cvc5 "CVC5, Int:"    problemInt
          solve z3   "Z3,   String:" problemString
          solve cvc5 "CVC5, String:" problemString
  where solve solver what problem = do putStrLn $ "\n== " ++ what ++ " version:"
                                       print =<< satWith solver problem

This produces:

*Main> test

== Z3,   Int: version:
Satisfiable. Model:
  test = [1] :: [Integer]

== CVC5, Int: version:
Satisfiable. Model:
  test = [1] :: [Integer]

== Z3,   String: version:
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory seq))

== CVC5, String: version:
Satisfiable. Model:
  test = ["US"] :: [String]

Allowing you to use these tools in a more productive manner.