Z3 .NET API для квантификатора существования

Я пытаюсь использовать Z3 .net API, чтобы получить выражение квантификатора существования. Ниже приведен мой код:

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();

'

Для программы я получил следующий результат:

(exists ((lamb Real))
 (! (and (> lamb 0.0)
      (= b0 true)
      (= b1 true)
      (>= (+ c lamb) 0.0)
      (<= (+ c lamb) 3.0)
      (>= c 0.0)
      (<= c 3.0))
 :skid skid2
 :qid Q2))
 Not reach

Мои вопросы: 1. В чем смысл ! в результате/ 2. По какой причине я не могу получить результат? 3. Может ли кто-нибудь предложить какие-либо боевые действия, соответствующие Z3 .NET　API　помимо API　меню на сайте Z3.

Большое спасибо!


.net z3 quantifiers
person user1402725    schedule 31.05.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Смысл функции (!...) — это аннотация, которая привязывает к выражению шаблоны и квантификаторы и идентификаторы Сколема. Когда эта линия

BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"), ctx.MkSymbol("skid2"));

меняется на

BoolExpr exist = ctx.MkExists(lamb, temp, 1);

то на выходе нет (!...) .

Я не могу воспроизвести результат UNSAT: когда я запускаю этот пример с Z3 4.0, я получаю SAT и следующую модель:

(define-fun lamb!0 () Real  1.0)
(define-fun c () Real  1.0)
(define-fun b1 () Bool true)
(define-fun b0 () Bool true)
person Christoph Wintersteiger    schedule 31.05.2012
comment
Спасибо за ваш ответ. Я попытался установить параметр Auto-config false. Теперь это работает. - person user1402725; 01.06.2012