search

salmans / Razor

5 stars 0 forks source link

Two Open Questions About Relaxed (aka Collapsed) Mode #71

Closed thedotmatrix closed 9 years ago

thedotmatrix commented 9 years ago

Right now, the mode will only "collapse at infinity." That is, when we reach the end of a skolem bound, and encounter an existential, we deliberately force the fresh element to be collapsed with the previously created element. This works just fine without any bugs or major performance issues.

Two open questions:

  1. Without unforced collapses at the SMT layer, we will not return possibly "unexpected models." For the ALAS example, an unexpected model may be when the stranger grants himself the key as an employee. Do unforced collapses / unexpected models really enlighten the user on anything interesting? If not, there's no reason to allow unforced collapses in this case.
  2. Does allowing unforced collapses at the SMT layer enable us to return more models than the current Collapsed Mode would?

@salmans, @dandougherty I think this summarizes what is left open from our discussion. Feel free to comment to add or correct me.

thedotmatrix commented 9 years ago

This issue is best discussed #38 . Adding point 2 from here.