Opened 16 years ago

Closed 16 years ago

#108 closed defect (fixed)

array problem in symbolic

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

Description

Run:

compare -verbose -simplify /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-seq_1_1_2.mmp -np 1 /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-par_1_1_2.mmp -np 2

and an exception is thrown. The cause is that the symbolic constant

matmat-seq_1_1_2_P0_S0_F1_V2

is supposed to have type real[X2][X1], but somehow it got type real[X2][X0].

Change History (2)

comment:1 by ywei, 16 years ago

Status: new → accepted

comment:2 by ywei, 16 years ago

Resolution: → fixed
Status: accepted → closed

Changed the way the type table stores symbolic array types in CVC3TheoremProver class. It doesn't throw that exception now. But as the length and complexity of the array increase, CVC3 use some other techniques to translate the array read/write, which change the expression structure and confuse the CVC3TheoremProver class. Need to work that out.

Note: See TracTickets for help on using tickets.