0

我在Visual Studio 2010（版本：10.0.30319.1 RTMREL）中用C#语言编写了以下程序，.net框架的版本是4.0.30319 RTMREL。编译时没有错误或警告，但在运行程序时会抛出异常。例外是“Z3_test_1.exe[2448] unhandled exception occurred in Microsoft .net framework”，其中 Z3_test_1.exe 是程序文件名。我使用的 Z3 证明器是 Z3 4.0 版本，在程序中我使用的是 Microsoft.Z3.dll 而不是 Microsoft.Z3V3.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 回答