1. Aug 18, 2017
  2. Aug 17, 2017
    • Matthew Fernandez's avatar
      add issue 'enable -Wshadow' · 60e2b9ac
      Matthew Fernandez authored
      60e2b9ac
    • Matthew Fernandez's avatar
      librumur: enable referencing of quantified variables within forall · 8bd2aa47
      Matthew Fernandez authored
      This works, but it makes me slightly nervous that the Var of a quantified
      variable is only sustained by shared_ptrs of ExprIDs related to where it is
      referenced. I.e. Once we traverse out of parsing the forall expression, the
      enclosing scope is closed and the Var is destroyed if it hasn't been referenced.
      On the one hand, this seems fine and might even help us later in detecting
      useless quantification. On the other hand, the lifetime of this Var object is
      quite slippery.
      8bd2aa47
    • Matthew Fernandez's avatar
      librumur: fix: remove accidentally shadowing field · c89084bd
      Matthew Fernandez authored
      Well that was a rude surprise. VarDecl lookups in the symbol table failed
      mysteriously and debugging indicated they had no name. Some digging revealed we
      were accidentally shadowing Decl::name.
      
      It is pretty surprising to me that -Wall -Wextra does not enable -Wshadow, which
      would have caught this. Unfortunately we can't turn it on right now because it
      sprays warnings about the constructors that shadow class members with their
      arguments. Sigh. I guess I'll have to refactor this before turning it on.
      c89084bd
    • Matthew Fernandez's avatar
      librumur: introduce new Var type · 55fa3302
      Matthew Fernandez authored
      This expression is used for referring to variables (either parts of the state or
      local variables). I'm still not sure this is the natural solution. It feels like
      this and ExprID should be a single class, but we'll see how it goes.
      55fa3302
    • Matthew Fernandez's avatar
      librumur: implement forall expressions · 15208239
      Matthew Fernandez authored
      Note that you can't currently reference the quantified variables within the
      forall expression as explained in the FIXME comment.
      15208239
  3. Aug 14, 2017
  4. Aug 13, 2017
  5. Aug 12, 2017
  6. Aug 11, 2017
  7. Aug 10, 2017
  8. Aug 09, 2017
    • Matthew Fernandez's avatar
      librumur: support for enum types · 5a0f2a92
      Matthew Fernandez authored
      The implementation of these departs somewhat from CMurphi. Where CMurphi
      implements each member of each enum as a separate value (i.e. enum members in
      distinct enums will still have different numerical representations), we simply
      implement enums as C would. We'll need to do a little more work to prevent
      accidental comparison of distinct enum values, but this representation should
      allow us to more efficiently encode enum values in the state. This only matters
      for input models that contain large enum types, but empirically it seems like
      this is much more common than one might think. E.g. see [0].
      
      The EnumValue class and related symbol table declaration implemented in this
      commit is a bit awkward. It would be nice to implement this in a cleaner way,
      but I couldn't immediately think of a better alternative.
      
        [0]: https://bitbucket.org/jderick/preach/commits/e7cecfc142253799bdf5d5cc5ed60015ec5cd0a8
      5a0f2a92
    • Matthew Fernandez's avatar
      abeb93ee