Z3找到的模型中的值的集合

我有一個類似的問題在這裏：How to print a Z3 Set object? 從中我無法知道如何在模型中打印集合的值。我有一個枚舉排序（Java代碼）：Z3找到的模型中的值的集合

EnumSort rSort = ctx.mkEnumSort（ctx.mkSymbol（「RES」），ctx.mkSymbol（「RES1」））;

從中我創建一組排序：

SetSort RSET = ctx.mkSetSort（rSort）

通過使用該組排序，我創建Z3恆定RID並定義一個簡單的會員表達：

BoolExpr c1 =（BoolExpr）ctx.mkSetMembership（rSort.getConsts（）[0]，rID）;

當c1可以滿足時，我希望在模型中看到rID的一個可能值。如果我嘗試使用const解釋（即，m.getConstInterp（e），其中e是來自模型的FuncDecl），我會得到：「非零的arity函數和數組具有FunctionInterpretations作爲模型，使用FuncInterp。」。

當我嘗試使用func解釋（即m.getFuncInterp（e））時，我得到「參數不是數組常量」。我在這裏做錯了什麼？是不是可以打印設置對象的值？或者，是否有更好的方式來表示一個可能包含多個排序值的變量？

來源

2014-04-08 fturkmen

集合在內部由數組表示，而這些數組又有模型的功能。 getConstInterp失敗，因爲rID是set-type（內部數組類型），它引發一個相應的異常。從例如目前還不清楚是什麼e是，但這裏是如何獲得在FuncInterp爲擺脫一個例子：

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，這可能是混亂的來源。

來源

2014-04-08 16:58:15

工作，謝謝！我意識到，如果我明確地將求解器設置爲QF_LIA，那麼會出現該錯誤。我沒有給出徹底的想法，但我認爲設置變量在LIA中不起作用。 – fturkmen

與處理集有關的另一個問題是集合上是否存在基數約束的實現？這裏（https://github.com/psuter/bapa-z3）我看到有一個Scala實現，但我不確定在Z3的其他實現中是否有任何實現。 – fturkmen

Z3找到的模型中的值的集合

回答

相關問題