Yes, I do. Z3, CVC3 and Yices all support "structured values" in the sense that is algebraic datatypes. The "empty theory" is ambiguous in the SMT solver community. It could mean "yes" or it could mean the theory of equality. Not sure if some lump in the theory of equality with uninterpreted functions too, but I wouldn't be surprised.
I have an implementation of Oliviera's and Nieuwenhuis's SMT(T) framework on planet if he's interested in adding more theories. I implemented equality of uninterpreted functions a while back but I don't think that's part of the PLaneT release. Let me know if that's the plan. Test generation is really just satisfying assignments to some (negated) property that you wanted to hold, but didn't. Say you change your implementation and the whole correctness checking is hard. Well, throw in that satisfying assignment - it might hit the bug again. -Ian ----- Original Message ----- From: "John Clements" <[email protected]> To: "Racket-users Users" <[email protected]> Sent: Wednesday, June 20, 2012 12:30:18 PM GMT -05:00 US/Canada Eastern Subject: [racket] Experience with SMT solvers for test generation? Does anyone on this list have experience with SMT solvers and their use in test-generation tools like DART and SAGE? I have a student that's interested in this stuff, and it looks to me like most of the existing SMT solvers focus on theories of arithmetic, rather than structured values. I have a faint sense that what SMT solvers call "empty theory" may in fact suffice for the kinds of things I have in mind, but I'd like to hear from someone who knows more about it. Thanks in advance! John ____________________ Racket Users list: http://lists.racket-lang.org/users ____________________ Racket Users list: http://lists.racket-lang.org/users
