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

Updates To Union Operator in IEGenLib #160

Open tpops opened 2 years ago

tpops commented 2 years ago

Union operation on two sets creates a new set with disjunct of conjunctions from both sets. For instance:

S3 := S1 U S2
S3 { Conjs(S1), Conjs(S2)}

There are is a special case however when the Union is not necessarily a disjunct of conjunction. This is a case where the Convex Hull of both sets is equal to the union. In this case, a single conjunction can be used to describe the Union.

In a case where the union is non-convex, we revert back to a union as a disjunction of conjunctions.

What needs to be implemented

tpops commented 2 years ago

Marking this as invalid as there is no need to modify the Union Operator, codegen can directly support Union and Omega Integration was expanded to take unions as well.