.NET APIの文字列をZ3.exprにキャスト

Question

私は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型にキャストする必要があります。 ctxをContextとsortある

Answer 1

名lChildren[0]の変数（定数関数）ctx.MkConst(lChildren[0], sort)を呼び出すことによって作成することができるが、変数のソート/タイプである、例えば、それは整数のctx.IntSortかもしれません。

Z3は同じ名前の2つの変数、つまりctx.MkConstを同じ名前/ソートで2回呼び出すことができますが、最初の変数とは異なる新しい変数を作成することに注意してください。同じ変数がその構築時間よりも後に必要とされる場合、例えば、ハッシュテーブル（または辞書）に保存して、迅速な検索が可能にする必要があります。