Solver cannot deal with string literals

[seizethedave]

A query like this:

WordBag:
    state words : Set<String>

    query containsPassword()
        "password" in words

produces this error when run in synthesis mode:

.
.
.
  File "/Users/dgrant/Dev/cozy/cozy/cozy/solver.py", line 617, in visit_EBinOp
    v1 = self.visit(e.e1, env)
  File "/Users/dgrant/Dev/cozy/cozy/cozy/solver.py", line 824, in visit
    return super().visit(e, *args)
  File "/Users/dgrant/Dev/cozy/cozy/cozy/common.py", line 182, in visit
    return getattr(self, visit_func)(x, *args, **kwargs)
  File "/Users/dgrant/Dev/cozy/cozy/cozy/solver.py", line 431, in visit_EStr
    raise NotImplementedError("cannot encode string literal {}".format(repr(s.val)))
NotImplementedError: cannot encode string literal 'password'

...because Z3 doesn't (currently) deal with strings.

[Calvin-L]

An easy and correct (although perhaps suboptimal) fix would be for Cozy to automatically transform string literals into uninterpreted extern declarations before starting synthesis.

[mernst]

Another workaround is to use an extern declaration for a function that compares against a string literal, as in
extern is_issue_tracking(x : String) : Bool = "({x} == \"issue_tracking\")"