Opened 16 years ago

Closed 16 years ago

#109 closed defect (fixed)

unknown expression type

Reported by: Stephen Siegel Owned by: ywei
Priority: major Milestone:
Component: Administration Version: 1.0
Keywords: symbolic CVC3 convert Cc:

Description

Seems to be problem in symbolic package when converting from CVC expression back to symbolic expression. The CVC expression printed in the error message below appears to be correct.

By the way, where does the name _BD1TY0 come from?

The command was

compare -verbose -simplify /Users/siegel/Documents/workspace/MiniMP/examples/simpleArray/simpleArraySpec.mmp -np 1 /Users/siegel/Documents/workspace/MiniMP/examples/simpleArray/simpleArrayImpl.mmp -np 1

java.lang.RuntimeException: Unknown or unimplemented expression type: (((_BD1TY0 >= 0) AND (_BD1TY0 < 1)) => ((simpleArraySpec_V0 WITH [0] := 1)[_BD1TY0] = (simpleArrayImpl_V0 WITH [0] := 1)[_BD1TY0]))
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:883)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:863)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:655)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.equalsExpression(SymUniverse.java:1300)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.equals(DynamicFactory.java:204)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:122)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:252)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:172)
	at edu.udel.cis.vsl.minimp.MiniMP.compareEquivalence(MiniMP.java:476)
	at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:503)
No violation at this state.

Change History (2)

comment:1 by ywei, 16 years ago

Status: new → accepted

The name _BD1TY0 is generated within CVC3. I didn't quite remember what it represents.

comment:2 by ywei, 16 years ago

Resolution: → fixed
Status: accepted → closed

Bug fixed. The forall expression can now be converted back to symbolic expression correctly.

Note: See TracTickets for help on using tickets.