Add support for boundary variables #160
Conversation
- add variable scope for BoundaryConstraints and IntegrityConstraints
| // The scope of the variable must be valid for the constraint domain. | ||
| match (scope, domain) { | ||
| ( | ||
| Scope::BoundaryConstraints, | ||
| ConstraintDomain::FirstRow | ConstraintDomain::LastRow, | ||
| ) | ||
| | ( | ||
| Scope::IntegrityConstraints, | ||
| ConstraintDomain::EveryRow | ConstraintDomain::EveryFrame(_), | ||
| ) => { | ||
| let key = (scope, variable_value); | ||
| if let Some(expr) = variable_roots.get(&key) { | ||
| match scope { | ||
| Scope::BoundaryConstraints => { | ||
| // TODO: deal with boundary conflict properly | ||
| Ok(ExprDetails::new( | ||
| expr.root_idx(), | ||
| expr.trace_segment(), | ||
| domain, | ||
| )) | ||
| } | ||
| Scope::IntegrityConstraints => Ok(*expr), | ||
| } |
There was a problem hiding this comment.
This can be addressed during #150, but it actually requires significant refactoring to do it cleanly
| integrity_constraints: | ||
| let a = 1 | ||
| enf clk' = clk + 1 | ||
| boundary_constraints: | ||
| enf clk.first = 0 | ||
| enf clk.last = a"; |
There was a problem hiding this comment.
Is it intentional to reverse the order of integrity and boundary constraints sections here?
There was a problem hiding this comment.
Oops, no! Good catch, thanks
There was a problem hiding this comment.
Oh wait, yes - it is. It needs to be reversed there in order to test defining the variable in the integrity_constraints and then using it in the boundary_constraints (out of scope)
There was a problem hiding this comment.
My mistake, I thought that it would work the other way around as well and you probably did it to make the example clearer but it wouldn't work the other way around.
This PR addresses #106. As mentioned in #150, I'd like to do some refactoring, including the symbol table, so I consider this implementation to be a preliminary version