Procurando exemplos práticos de casos de uso SMT Z3 (como DbC) e alternativas de código aberto ao Z3?[fechado]

Question

Tenho me interessado e procurado exemplos práticos de uso do SMT Z3 (como DbC) com código e alternativas de código aberto para esta ferramenta.Então, na verdade, estou interessado em ferramentas de resolução formal Z3 semelhantes, mas:

• deve ser de código aberto
• fornecer interação de baixo nível (API) e de alto nível (script de texto)
• suporte SMT-LIB
• adequado (utilizável) em ferramentas/escrito em/para linguagens como Java, python, ruby, Vala e não Haskell
• possui ferramentas estáveis ​​(utilizáveis ​​na prática) baseadas nele, como projeto por contrato (DbC), verificação de tipo estático, etc.

De acordo com a página inicial do SMT-LIB (consulte o pacote bit.ly para obter detalhes), a lista de solucionadores SMT de 2010 é:"Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, SWORD, UCLID, veriT, Yices, Z3."

Por favor, dê algum feedback sobre o uso de qualquer um deles na prática (exemplos de código são os melhores)?

Finalmente, qualquer informação sobre comparação com as possibilidades do GHC seria útil, mas apenas no caso de haver um exemplo de implementação (não um "recurso" de linguagem).

Mais informações rápidas sobre Z3 aqui http://bit.ly/bundles/ewiger/1

Answer 1

Até onde sei, o CVC3 é o que mais se aproxima das suas necessidades, na medida em que:

1. Possui um conjunto de recursos semelhante ao do Z3.
2. Tem um Licença estilo BSD
3. É o solucionador subjacente para vários projetos existentes.

CVC3 tem ligações para C++ e Java e provavelmente outras linguagens.Em geral, acho que a API é muito mais difícil de usar do que a API (textual) idioma de entrada.Isso tem o benefício adicional de que, se você continuar com a linguagem SMT-LIB2, poderá mudar para uma ferramenta diferente posteriormente, se for necessário.Uma grande amostra de exemplos está disponível no site Site SMT-LIB.

Answer 2

Você perguntou sobre alternativas de código aberto ao Z3:

De acordo com SMT-Wikipedia em 2011-08, temos:

Com base nestas medidas, parece que os projetos mais vibrantes e bem organizados são OpenSMT, STP e CVC4.

Estou apenas verificando essas coisas - até agora, todos os três parecem razoáveis, além do CVC mais antigo -> quero dizer, CVC3.