在 .Net API 中将字符串转换为 Z3.expr答案

【问题标题】：Casting string to Z3.expr in .Net API在 .Net API 中将字符串转换为 Z3.expr
【发布时间】：2016-12-29 18:20:07
【问题描述】：

我有一个字符串变量，我需要将其转换为 Expr 类型。我正在使用 Z3 .Net API。这可能吗？

编辑

List<Node<string>> lChildren = new List<Node<string>>(); 
//...   
switch (pNode.Data)
{ 
    //...
    case ">=": 
    { 
        lResult = lZ3Solver.GreaterOrEqualOperator(
            lChildren[0].Data, 
            int.Parse(lChildren[1].Data)
        );

GreaterOrEqualOperator 的第一个参数是Expr 类型。在这种情况下，我需要将当前字符串类型转换为 Expr 类型。

【问题讨论】：

需要贴出相关代码部分
List> lChildren = new List>(); ... switch (pNode.Data) { ...case ">=": { lResult = lZ3Solver.GreaterOrEqualOperator(lChildren[0].Data, int.Parse(lChildren[1].Data)); 'GreaterOrEqualOperator' 的第一个参数是 Expr 类型。在这种情况下，我需要将当前字符串类型转换为 Expr 类型。
将评论移至 OP 的问题。

标签： c# z3

【解决方案1】：

可以通过调用ctx.MkConst(lChildren[0], sort) 来创建名称为lChildren[0] 的变量（常量函数），其中ctx 是Context，sort 是变量的排序/类型，例如，它可以是ctx.IntSort 用于整数。

请注意，Z3 允许两个同名变量，即第二次以相同的名称/排序调用ctx.MkConst，将创建一个与第一个不同的新变量。如果在构建时间之后需要相同的变量，则需要将其保存在其他地方，例如，在允许快速查找的哈希表（或字典）中。

【讨论】：