Запись полей в z3 - PullRequest
Новая
       27

Запись полей в z3

1 голос
/ 11 июля 2019

запись модели по типу данных в z3

, если два типа данных записи имеют одно и то же поле, например, 

 UNI_MSG : record
    Cmd : UNI_CMD;
    Proc : NODE;
    HomeProc : boolean;
    Data : DATA;
  end;

  INV_CMD : enum {INV_None, INV_Inv, INV_InvAck};

  INV_MSG : record
    Cmd : INV_CMD;
  end;

  RP_CMD : enum {RP_None, RP_Replace};

  RP_MSG : record
    Cmd : RP_CMD;
  end;

и UNI_MSG, и RP_MSG имеют поля Cmd. когда я использую поле Cmd переменной записи UNI_MSG, я не знаю, как используйте его, потому что переменная RP_CMD также имеет поле Cmd. Код z3 выглядит следующим образом: 

; This example illustrates basic arithmetic and 
; uninterpreted functions
(declare-datatypes () ((CACHE_STATE CACHE_I CACHE_S CACHE_E)))
(declare-datatypes () ((NODE_CMD NODE_None NODE_Get NODE_GetX)))
(declare-datatypes () ((UNI_CMD UNI_None UNI_Get UNI_GetX UNI_Put UNI_PutX UNI_Nak)))
(declare-datatypes () ((INV_CMD INV_None INV_Inv INV_InvAck)))
(declare-datatypes () ((RP_CMD RP_None RP_Replace)))
(declare-datatypes () ((WB_CMD WB_None WB_Wb)))
(declare-datatypes () ((SHWB_CMD SHWB_None SHWB_ShWb SHWB_FAck)))
(declare-datatypes () ((NAKC_CMD NAKC_None NAKC_Nakc)))
(define-sort NODE () Int)
(define-sort DATA () Int)
(define-sort boolean () Bool)
(declare-datatypes () ((Record_0 (mk-Record_0 (Cmd NAKC_CMD)))))
(declare-datatypes () ((Record_1 (mk-Record_1 (Data DATA)
(HomeProc boolean)
(Proc NODE)
(Cmd SHWB_CMD)))))

(declare-datatypes () ((Record_2 (mk-Record_2 (HomeInvSet boolean)
(InvSet (Array  NODE  boolean))
(HomeShrSet boolean)
(ShrSet (Array  NODE  boolean))
(ShrVld boolean)
(HomeHeadPtr boolean)
(HeadPtr NODE)
(HeadVld boolean)
(Dirty boolean)
(Local boolean)
(Pending boolean)))))

(declare-datatypes () ((Record_3 (mk-Record_3 (CacheData DATA)
(CacheState CACHE_STATE)
(InvMarked boolean)
(ProcCmd NODE_CMD)))))


(declare-datatypes () ((Record_4 (mk-Record_4 (CurrData DATA)
( NakcMsg (  Record_0))
( ShWbMsg (  Record_1))
( WbMsg (  Record_1))
( HomeRpMsg (  Record_0))
( RpMsg (Array  NODE  Record_0))
( HomeInvMsg (  Record_0))
( InvMsg (Array  NODE  Record_0))
( HomeUniMsg (  Record_1))
( UniMsg (Array  NODE  Record_1))
(MemData DATA)
( Dir (  Record_2))
( HomeProc (  Record_3))
( Proc (Array  NODE  Record_3))))))


(declare-const Sta  ( Record_4)) 

(assert (= (Cmd (select (UniMsg Sta)  1 )) UNI_Nak))

(check-sat)

Ошибка вызвана тем, что запись_0 и запись_1 имеют поле Cmd.

1 Ответ

0 голосов
/ 11 июля 2019

Вы можете обойти это, переименовав их в Cmd0, Cmd1 и т. Д.

SMTLib фактически позволяет использовать одно и то же имя в полях с другими типами, но система типов слишком слаба и требует, чтобы для ее обхода использовались надписи. Если вы действительно хотите сохранить имя, опубликуйте (намного!) Уменьшенную версию этой проблемы, чтобы мы могли показать вам, как это сделать. Но на практике переименование является лучшим (и самым простым!) Способом.

...