Dat3M icon indicating copy to clipboard operation
Dat3M copied to clipboard

Relation Model Implementation

Open CapZTr opened this issue 1 year ago • 0 comments

This PR is related to #732 and contains the following:

  1. Implementation of RelationModel, a representation of relations in Dartagnan dedicated for better witness generation, and the corresponding "RelationModelManager" that is responsible for construction of RelationModel and computation of derived relations.
  2. Support of witness generation for showing relations defined in the model vmm.cat. Users may pass --witness.relationsToShow=r1,r2,r3... into the command to have witness for corresponding relations.
  3. Add Local and Assert events to witness graph. But note code of this part is temporary and needs to be refined, which will be done in the next step: implementation of EventModel...

CapZTr avatar Oct 25 '24 07:10 CapZTr