Which quantifier elimination technique does TPA-QE use?

usi-verification-and-security / golem

Solver for Constrained Horn Clauses

MIT License

34 stars 7 forks source link

Which quantifier elimination technique does TPA-QE use? #35

Closed dong-yf closed 1 year ago

dong-yf commented 1 year ago

As stated above, thank you

blishko commented 1 year ago

Hi @dong-yf , using QE option for TPA is not recommended at the moment. Our quantifier elimination algorithm is currently based on model-based projection (MBP).