search

BoiseState-AdaptLab / IEGenLib

Inspector/Executor Generation Library for manipulating sets and relations with uninterpreted function symbols.
BSD 2-Clause "Simplified" License
2 stars 4 forks source link

projectOut for UFs #49

Open riftEmber opened 3 years ago

riftEmber commented 3 years ago

"Now, when we do it in the presense of UFs we will need to run Tobi's new transitive closure as a first step. Then, if the tuple variable is used as a parameter to a UF we will need to remove that constraint. Then, we will need to use the existing code to finish it off." Work on branch projectout-ufs

riftEmber commented 3 years ago

Additional constraint that if the tuple variable is used as a parameter in a UF that also has other parameters, we should fail. In this case I'll make the method return null to be consistent with the existing projectOut method.