Scala ^ Z3 (Z3 версия 3.2) и parsesmtlib2string (...) не работают - PullRequest
Новая
       7

Scala ^ Z3 (Z3 версия 3.2) и parsesmtlib2string (...) не работают

2 голосов
/ 26 сентября 2011

При попытке реализовать тест с использованием parsesmtlib2string я обнаружил ошибку: 

println("Hello World!");
var smtlib2String = ""
smtlib2String += "(declare-fun x () bool)" + "\n"
smtlib2String += "(declare-fun y () bool)" + "\n"
smtlib2String += "(assert (= x y))" + "\n"
smtlib2String += "(assert (= x true))" + "\n"
//  smtlib2String += "(check-sat)" + "\n"
//  smtlib2String += "(model)" + "\n"
smtlib2String += "(exit)" + "\n"

val cfg = new Z3Config
val z3 = new Z3Context(cfg)

z3.parseSMTLIB2String(smtlib2String)

При комментировании "Check-sat" я получаю "неизвестно". При комментировании "модель" я получаю "неподдерживаемый".

Используя F # с Z3 3.2, я просто вернул бы Term, но в Scala типом возврата является Unit. Я просмотрел API Z3-C, но не нашел хорошего примера использования ist.

Итак, как лучше всего получить модель, используя smtlib2string?

Кстати: использование Scala ^ Z3 и построение Z3AST прекрасно работает, и я могу получить модель, используя .checkAndGetModel (). Приведенный выше код SMT-LIB2 прекрасно работает с методом F # .NET parsesmtlib2string.

Использование одного из «getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts» приводит к «Ошибка: анализатор (данные) недоступен».

Использование "getSMTLIBError.size" возвращает "0".

1 Ответ

2 голосов
/ 26 сентября 2011

Методы parseSMTLIB2[...] действительно должны были вернуть Z3AST, спасибо за сообщение о проблеме.Это исправлено в scalaz3-3.2.b.jar .Что касается использования парсера SMT-LIB 2, я сам новичок в этом, поэтому Лео, возможно, следует подтвердить, но я понимаю, что вы должны использовать его только для разбора формул, а не для выполнения команд, таких как (check-sat).

Вот пример, который работает для меня: 

import z3.scala._
val smtlib2String = """
  (declare-fun x () bool)
  (declare-fun y () bool)
  (assert (= x y))
  (assert (= x true))"""

val ctx = new Z3Context("MODEL" -> true)
val assertions = ctx.parseSMTLIB2String(smtlib2String)
println(assertions) // prints "(and (= x y) (= x true))"
ctx.assertCnstr(assertions)
println(ctx.checkAndGetModel._1) // prints "Some(true)", i.e. SAT

Теперь, если вы хотите программно восстановить модель для x, я понимаю, что единственный способ сделать это - этосоздайте символ для x перед синтаксическим анализом и передайте его анализатору, используя перегруженное определение метода parseSMTLIB2[...].Вот как вы это делаете: 

val ctx = new Z3Context("MODEL" -> true)
val xSym = ctx.mkStringSymbol("x") // should be the same symbol as in the SMT-LIB string
val assertions = ctx.parseSMTLIB2String(smtlib2String, Map(xSym -> ctx.mkBoolSort), Map.empty)
ctx.assertCnstr(assertions)
val model = ctx.checkAndGetModel._2
val xTree = ctx.mkConst(xSym, ctx.mkBoolSort) // need a tree to evaluate using the model
println(model.evalAs[Boolean](xTree)) // prints "Some(true)"

Надеюсь, это поможет.

(Опять же, может быть более простой способ сделать это, но я не знаю об этом. Парсингметоды напрямую связаны с их эквивалентом C, и единственный пример , который я смог найти , не показывает много.)

...