fix nested quantifiers if both are equal

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.

1 stars 0 forks source link

fix nested quantifiers if both are equal #14

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

there are expressions of the form (forall (a) ((forall (b)(...)))) in your current translation. these expression can be rewritten into a single quantified expression. please extend the forall() functions of TermQuant to optimize such expressions.

jonnybest commented 12 years ago

fixed in 1841b262c0935c353156c9509bb81278a00d7f64