Значения набора в модели, найденной Z3

Question

У меня есть аналогичный вопрос: How to print a Z3 Set object? , из которого я не мог понять, как печатать значения набора в модели. У меня есть одно перечисление рода (код в Java):

• EnumSort rSort = ctx.mkEnumSort (ctx.mkSymbol ("Рес"), ctx.mkSymbol ("res1"));

, из которого я создаю множество рода:

• SetSort RSet = ctx.mkSetSort (rSort)

С помощью этого набора то, я создаю Z3 постоянной Rid и определим простое выражение членство:

• BoolExpr c1 = (BoolExpr) ctx.mkSetMembership (rSort.getConsts() [0], РИД);

Когда c1 выполнимо, я хотел бы увидеть одно возможное значение для rID в модели. Если я попытаюсь интерпретировать константу (т. Е. M.getConstInterp (e), где e - это FuncDecl из модели), я получаю: «Функции ненулевой функции arity и функции массивов имеют функции Functionterterretretations в качестве модели. Используйте FuncInterp.».

Когда я пытаюсь интерпретировать func (т. Е. M.getFuncInterp (e)), я получаю «Аргумент не был константой массива». Я здесь что-то не так? Невозможно ли напечатать значения заданного объекта? Альтернативно, есть ли лучший способ представления переменной, которая может содержать несколько значений из сортировки?

Answer 1

Установки внутренне представлены массивами, которые, в свою очередь, функционируют как модели. getConstInterp терпит неудачу, потому что rID имеет тип set ​​(внутренний тип массива) и генерирует исключение. На примере это не ясно, что e есть, но вот пример того, как получить в FuncInterp для Rid:

Context ctx = new Context(cfg); 

EnumSort rSort = ctx.mkEnumSort(ctx.mkSymbol("res"), ctx.mkSymbol("res1")); 
SetSort rSet = ctx.mkSetSort(rSort); 
Expr rID = ctx.mkConst("rID", rSet); 
BoolExpr c1 = (BoolExpr)ctx.mkSetMembership(rSort.getConsts()[0], rID); 

Solver s = ctx.mkSolver(); 
s.add(c1); 
Status status = s.check(); 
Model m = s.getModel(); 

System.out.println(status); 
System.out.println("Model = " + m); 

FuncInterp fi = m.getFuncInterp(rID.getFuncDecl()); 
System.out.println("fi="+ fi); 

Обратите внимание, что вызов getFuncInterp получает FuncDecl константы Rid, которые могут быть источник путаницы.