Skip to content
Snippets Groups Projects
Commit a6cbf8e2 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Simplify inside choose predicates

parent 0ce50b8a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/scala/inox/transformers/SimplifierWithPC.scala
+ 3
− 1
View file @ a6cbf8e2
...@@ -94,7 +94,9 @@ trait SimplifierWithPC extends Transformer { self => ...@@ -94,7 +94,9 @@ trait SimplifierWithPC extends Transformer { self =>
case e if path implies not(e) => (BooleanLiteral(false).copiedFrom(e), true) case e if path implies not(e) => (BooleanLiteral(false).copiedFrom(e), true)
case c @ Choose(res, BooleanLiteral(true)) if hasInstance(res.tpe) == Some(true) => (c, true) case c @ Choose(res, BooleanLiteral(true)) if hasInstance(res.tpe) == Some(true) => (c, true)
case c: Choose => (c, false) case Choose(res, pred) =>
val (rp, _) = simplify(pred, path withBound res)
(Choose(res, rp).copiedFrom(e), false)
case Lambda(params, body) => case Lambda(params, body) =>
val (rb, _) = simplify(body, path withBounds params) val (rb, _) = simplify(body, path withBounds params)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment