在Z3 .NET API设置逻辑

这是一个非常小的例子，显示我有一个问题：在Z3 .NET API设置逻辑

class Z3Tester 
    { 
     private Context cICtx; 
     private Solver cISolver; 

     static void Main(string[] args) 
     { 
      Z3Tester lZ3Tester = new Z3Tester(); 
      lZ3Tester.Test_Z3(); 
     } 

     public void Test_Z3() 
     { 
      BoolExpr lA = cICtx.MkBoolConst("A"); 
      BoolExpr lB = cICtx.MkBoolConst("B"); 
      cISolver.Push(); 
      BoolExpr lConstraint1 = cICtx.MkBoolConst("Constraint1"); 
      cISolver.AssertAndTrack(lA, lConstraint1); 
      cISolver.ToString(); 
      cISolver.Check(lConstraint1); 
     } 

     public Z3Tester() 
     { 
      cICtx = new Context(new Dictionary<string, string>() { { "proof", "true" } }); 
      using (cICtx) 
       this.cISolver = cICtx.MkSolver("QF_FD");

在此代码时，我给cISolver.Check(lConstraint1);线来我得到的AccessViolationException ...。

来源

2017-08-16 Amir Ebrahimi

创建使用指定逻辑配置的求解器对象。 –

有在上下文对象中的方法，（在Context.cs）：

public Solver MkSolver(string logic)

它创建一个使用指定的逻辑结构的解算器的对象。

来源

2017-08-16 15:42:06

我想在Z3 .Net API中设置逻辑。为此，我使用Public Solver MkSolver（字符串逻辑）' 函数将逻辑设置为“QF_FD”。但是当我这样做以后的代码时，我想使用的功能，如： Solver.Push（）或 Solver.Check（boolExpr）我得到的错误： SystemAccessViolationException：... 我究竟做错了什么？ –

您可以调用其他函数（而不是解算器相关的函数），例如获取版本字符串？如果你不能，这很可能是系统拒绝加载的本地库的一个问题（出于各种原因）。 –

所以你说的是，如果我设置求解器的逻辑，我不能使用我之前提到的一些函数？ –

在Z3 .NET API设置逻辑

回答

相关问题