Reported by Len Hamey. The following test program provides a minimal reconstruction. The problem appears to be that one of the aux-PropagateAssertion rule is not generated in case the condition of the two rules starts with the same prefix.

module simplify3
imports libstratego-lib

signature
constructors
Var : String -> Exp
Geq : Exp * Exp -> Exp
Leq : Exp * Exp -> Exp
Lt : Exp * Exp -> Exp
Int : IntConst -> Exp
False : Exp
True : Exp

strategies

main =
test-suite(!“simplify”
, test-propagate-assert1
)

test-propagate-assert1 =
apply-test(!“test-propagate-assert1”
, propagate-assert
, ![ Leq(Var("x"),Int("1")), Geq(Var("x"),Int("1"))]
, ![Leq(Var("x"),Int("1")), Geq(Var("x"),Int("1"))]
)

simplify = propagate-assert

propagate-assert =
all(propagate-assert)
; try(PropagateAssertion)
; try(use-assertion-leq)

bugfix = id

use-assertion-lt =
Lt(?e1,Int(?i))
; rules(
PropagateAssertion :
Geq(e1,Int(j)) -> False() where bugfix; (j,i)
)

use-assertion-leq =
Leq(?e1,Int(?i))
; rules(
PropagateAssertion :
Geq(e1,Int(j)) -> False() where bugfix; (j,i)
)

debug-simplify = debug

Submitted on 13 November 2006 at 15:51