0

Visual Studio 2010 (バージョン: 10.0.30319.1 RTMREL) で C# 言語を使用して次のプログラムを作成しました。.net フレームワークのバージョンは 4.0.30319 RTMREL です。コンパイル時にエラーや警告は発生しませんが、プログラムの実行時に例外がスローされます。例外は、「Z3_test_1.exe [2448] 未処理の例外が Microsoft .net フレームワークで発生しました」ということです。ここで、Z3_test_1.exe はプログラム ファイル名です。私が使用した Z3 プルーバーはバージョン Z3 4.0 で、プログラムでは Microsoft.Z3V3.dll ではなく Microsoft.Z3.dll を使用しました。

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Z3;
//using Microsoft.Z3V3;

namespace Z3_test_1
{
    class Program
    {
        static void Main(string[] args)
        {
                using (Context ctx = new Context())
                {
                    RealExpr c = ctx.MkRealConst("c");
                    BoolExpr Eqzero = ctx.MkGt(c,ctx.MkReal(0));    
                    BoolExpr Gezero = ctx.MkGe(c,ctx.MkReal(0));
                    BoolExpr Lttwo = ctx.MkLt(c,ctx.MkReal(2));
                    BoolExpr Gtthree = ctx.MkGt(c,ctx.MkReal(3)); 
                    BoolExpr b1 = ctx.MkBoolConst("b1");
                    BoolExpr b2 = ctx.MkBoolConst("b2");
                    BoolExpr b3 = ctx.MkBoolConst("b3");
                    BoolExpr b0 = ctx.MkBoolConst("b0");   

                    RealExpr[] lamb=new RealExpr[1];
                    lamb[0]=ctx.MkRealConst("lamb");
                    BoolExpr  temp=ctx.MkAnd(ctx.MkGt(lamb[0],ctx.MkReal(0)),ctx.MkEq(b0,ctx.MkTrue()),ctx.MkEq(b1,ctx.MkTrue()),ctx.MkGe(ctx.MkAdd(c,lamb[0]),ctx.MkReal(0)),ctx.MkLe(ctx.MkAdd(c,lamb[0]),ctx.MkReal(3)),ctx.MkGe(c,ctx.MkReal(0)),ctx.MkLe(c,ctx.MkReal(3)));   
                    BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"),ctx.MkSymbol("skid2"));
                    Console.WriteLine(exist.ToString());
                    Solver s1 = ctx.MkSolver();
                    s1.Assert(exist);
                    if (s1.Check() == Status.SATISFIABLE){
                        Console.WriteLine("get pre");
                        Console.Write(s1);
                    }
                    else
                    {
                        Console.WriteLine("Not reach");
                    }
                    Console.ReadKey();
                }   

            }
        }
    }
4

1 に答える 1

1

私はあなたのエラーを再現しようとしました。テストは私にとってはうまくいきます。私にとってはうまくいったので、Leoが指摘したのと同じコンパイルの問題だと思います。微妙な問題は、x64 環境または他のラウンドから x86 アセンブリを参照すると、ランタイム エラーが発生し始めることです。確実な方法は、コンパイラ (csc.exe) に渡す引数に /platform 指示を追加することです。

于 2012-06-05T17:32:51.740 に答える