1

我在 .NET API 中创建了一个现有的 Z3 4.1 上下文，其中包含许多函数声明、排序声明、断言假设等。

在此上下文中使用所有现有声明解析 SMT-LIB2 字符串的最简洁方法是什么？具体来说，有没有办法遍历上下文中的所有声明？我在 Context 中没有看到任何允许我访问声明的方法。

目前，我正在执行以下操作：

Context z3 = new Context();

// ... declare sorts, add declarations (parsing other input files), add assertions, to z3 context

List<FuncDecl> decls = new List<FuncDecl>();
List<Symbol> names = new List<Symbol>();
string pstr; // smtlib2 string to be parsed populated elsewhere

// ... populate decls and names by iterating over my internal data structures with references to these declarations

BoolExpr prop = z3.ParseSMTLIB2String(pstr, null, null, names.ToArray(), decls.ToArray());

有没有办法从 z3 上下文本身获取所有这些声明和符号名称？它们都已经在 z3 对象中声明了。我宁愿这样做，也不愿遍历我的内部数据结构。

我可能错过了它，但我没有看到任何可以让我在 API 中执行此操作的内容。我正在成像类似于可通过 Solver.Assertions 获得的断言公式数组。

4

1 回答 1

1

您的解决方案看起来正确。decl 和名称可以在它们第一次出现时被收集，而不是为每次调用重新构建它们，这将消除每次调用对内部数据结构的迭代。请注意，如果您对 Z3 进行多次调用，则使用 SMT 解析器可能不是最有效的解决方案；如果可能的话，我建议直接构建 Z3 表达式而不是字符串（在这种情况下，可能还需要一个符号表）。

于 2012-10-26T10:19:25.330 回答