@@ -70,14 +70,21 @@ module DAELow:
7070 * Algorithm.Algorithm array (* Algorithms *)
7171
7272 datatype Variables = VARIABLES of CrefIndex list array (* HashTB, cref->indx*)
73- * Var array (* Array of variables *)
73+ * VariableArray (* Array of variables *)
7474 * int (* bucket size *)
7575 * int (* no. of vars *)
76+
7677datatype CrefIndex = CREFINDEX of Exp.ComponentRef * int
7778
7879(* array of Equations are expandable, to amortize the cost of adding
7980 ** equations in a more efficient manner
8081 *)
82+
83+
84+ datatype VariableArray = VARIABLE_ARRAY of int * (* no. elements *)
85+ int * (* array size *)
86+ Var option array
87+
8188datatype EquationArray = EQUATION_ARRAY of int * (* no. elements *)
8289 int * (* array size *)
8390 Equation option array
@@ -170,6 +177,12 @@ datatype EquationArray = EQUATION_ARRAY of int * (* no. elements *)
170177 relation list_equation:(Equation list ) => EquationArray
171178
172179
180+ relation vararray_nth:(VariableArray, int) => Var
181+ relation vararray_setnth:(VariableArray, int, Var) => VariableArray
182+ relation vararray_add:(VariableArray,Var) => VariableArray
183+ relation vararray_length: (VariableArray) => int
184+ relation vararray_list:(VariableArray) => Var list
185+
173186 relation is_non_state: VarKind => ()
174187 relation is_var_known : (Var list, Exp.ComponentRef) => bool
175188end (* End Module *)
@@ -453,11 +466,46 @@ end
453466 **)
454467relation var_list: (Variables) => Var list =
455468
456- rule array_list (vararr) => varlst
469+ rule vararray_list (vararr) => varlst
457470 --------------------------------------
458471 var_list(VARIABLES(_,vararr,_,_)) => varlst
459472end
460473
474+ (** relation vararray_list
475+ ** Transforms a VariableArray to a Var list
476+ **)
477+
478+ relation vararray_list:(VariableArray) => Var list =
479+
480+ axiom vararray_list(VARIABLE_ARRAY(0,_,arr)) => []
481+
482+ rule array_nth(arr,0) => SOME(elt)
483+ ------------------
484+ vararray_list(VARIABLE_ARRAY(1,_,arr)) => [elt]
485+
486+ rule n - 1 => lastpos &
487+ vararray_list2(arr,0,lastpos) => lst
488+ ---------------
489+ vararray_list(VARIABLE_ARRAY(n,size,arr)) => lst
490+ end
491+
492+ (** relation: vararray_list2
493+ ** Helper relation to vararray_list
494+ **)
495+
496+ relation vararray_list2:(Var option array,int,int) => Var list =
497+
498+ rule int_eq (pos,lastpos) => true &
499+ array_nth(arr,pos) => SOME(v)
500+ --------------------
501+ vararray_list2(arr,pos,lastpos) => [v]
502+
503+ rule pos + 1 => pos' &
504+ array_nth(arr,pos) => SOME(v) &
505+ vararray_list2(arr,pos',lastpos) => res
506+ ---------------------------------------
507+ vararray_list2(arr,pos,lastpos) => v::res
508+ end
461509
462510(** relation: dump_eqns
463511 ** Helper relation to dump.
@@ -1560,14 +1608,15 @@ end
15601608
15611609(**relation empty_vars
15621610 ** Returns a Variable datastructure that is empty.
1563- ** Using the bucketsize 100 .
1611+ ** Using the bucketsize 10000 and array size 1000 .
15641612 **)
15651613relation empty_vars: () => Variables =
15661614
15671615 rule array_create(10000,[]) => arr &
1568- list_array([]) => emptyarr
1616+ Util.list_fill(NONE,1000) => lst &
1617+ list_array(lst) => emptyarr
15691618 ------------------------
1570- empty_vars() => VARIABLES(arr,emptyarr, 10000,0)
1619+ empty_vars() => VARIABLES(arr,VARIABLE_ARRAY(0,1000, emptyarr) , 10000,0)
15711620end
15721621
15731622(** relation: merge_vars
@@ -1597,19 +1646,19 @@ relation add_var: (Var, Variables) => Variables =
15971646 not get_var(cr,vars) => (_,_) &
15981647 hash_component_ref(cr) => hval &
15991648 int_mod(hval,bsize) => indx &
1600- array_length (varr) => newpos &
1601- array_add (varr,v) => varr' &
1649+ vararray_length (varr) => newpos &
1650+ vararray_add (varr,v) => varr' &
16021651 array_nth(hashvec,indx)=> indexes &
16031652 array_setnth(hashvec,indx,CREFINDEX(cr,newpos)::indexes) => hashvec' &
1604- array_length (varr') => n'
1653+ vararray_length (varr') => n'
16051654 -----------------------------
16061655 add_var(v as VAR(cr,_,_,_,_,_,_,_,_,_,_),vars as VARIABLES(hashvec,varr,bsize,n))
16071656 => VARIABLES(hashvec',varr',bsize,n')
16081657
1609- rule (* adding when allready present => Updating value *)
1658+ rule (* adding when allready present => Updating value *)
16101659 get_var(cr,vars) => (v,indx) &
16111660 int_sub(indx,1) => indx' &
1612- array_setnth (varr,indx',newv) => varr'
1661+ vararray_setnth (varr,indx',newv) => varr'
16131662 -----------------------------------
16141663 add_var( newv as VAR(cr,_,_,_,_,_,_,_,_,_,_),vars as VARIABLES(hashvec,varr,bsize,n))
16151664 => VARIABLES(hashvec,varr',bsize,n)
@@ -1619,6 +1668,95 @@ relation add_var: (Var, Variables) => Variables =
16191668 add_var(_,_) => fail
16201669end
16211670
1671+ (** relation vararray_length
1672+ ** Returns the number of variable in the VariableArray
1673+ **)
1674+ relation vararray_length: (VariableArray) => int =
1675+
1676+ axiom vararray_length(VARIABLE_ARRAY(n,_,_)) => n
1677+
1678+ end
1679+
1680+ (** relation vararray_add
1681+ ** Adds a variable last to the VariableArray, increasing array size
1682+ ** if no space left by factor 1.4
1683+ **)
1684+ relation vararray_add:(VariableArray,Var) => VariableArray =
1685+
1686+ rule (* Have space to add array elt. *)
1687+ int_lt(n,size) => true &
1688+ n +1 => n' &
1689+ array_setnth(arr,n,SOME(v)) => arr'
1690+ -------------------------
1691+ vararray_add(VARIABLE_ARRAY(n,size,arr),v)
1692+ => VARIABLE_ARRAY(n',size,arr')
1693+
1694+ rule (* Do NOT have splace to add array elt. Expand with factor 1.4 *)
1695+ int_lt(n,size) => false &
1696+ int_real(size) => rsize &
1697+ real_mul(rsize,0.4) => rexpandsize &
1698+ real_int(rexpandsize) => expandsize &
1699+ int_add(expandsize,size) => newsize &
1700+ Util.array_expand(expandsize,arr,NONE) => arr' &
1701+ n + 1 => n' &
1702+ array_setnth(arr',n,SOME(v)) => arr''
1703+ ---------------------------------
1704+ vararray_add(VARIABLE_ARRAY(n,size,arr),v)
1705+ => VARIABLE_ARRAY(n',newsize,arr'')
1706+
1707+ rule print "-vararray_add failed\n"
1708+ --------------------
1709+ vararray_add(_,_) => fail
1710+ end
1711+
1712+ (** relation vararray_setnth
1713+ ** Set the n:th variable in the VariableArray to v.
1714+ **)
1715+
1716+ relation vararray_setnth:(VariableArray,
1717+ int, (* n *)
1718+ Var) (* v *)
1719+ => VariableArray =
1720+
1721+ rule int_lt(pos,size) => true &
1722+ array_setnth(arr,pos,SOME(v)) => arr'
1723+ -------------------------
1724+ vararray_setnth(VARIABLE_ARRAY(n,size,arr),pos,v)
1725+ => VARIABLE_ARRAY(n,size,arr')
1726+
1727+ rule print "-vararray_setnth failed\n"
1728+ -------------------------
1729+ vararray_setnth(_,_,_)
1730+ => fail
1731+ end
1732+
1733+ (** relation vararray_nth
1734+ ** Retrieve the n:th Var from VariableArray
1735+ **)
1736+ relation vararray_nth:(VariableArray,
1737+ int (* n *))
1738+ => Var =
1739+
1740+ rule int_lt(pos,n) => true &
1741+ array_nth(arr,pos) => SOME(v)
1742+ --------------
1743+ vararray_nth(VARIABLE_ARRAY(n,_,arr),pos) => v
1744+
1745+ rule int_lt(pos,n) => true &
1746+ array_nth(arr,pos) => NONE &
1747+ print "vararray_nth has NONE!!!\n"
1748+ --------------
1749+ vararray_nth(VARIABLE_ARRAY(n,_,arr),pos) => fail
1750+
1751+ rule print "-vararray_nth , pos : " & int_string(pos) => ps & print ps &
1752+ print "\n array_length:" & vararray_length(arr) => len &
1753+ int_string(len) => lens & print lens & print "\n" &
1754+ int_string(n) => ns &
1755+ print "n :" & print ns & print "\n"
1756+ --------------
1757+ vararray_nth(arr as VARIABLE_ARRAY(n,_,_),pos) => fail
1758+ end
1759+
16221760(** relation replace_var
16231761 ** Takes a 'Var' list and a 'Var' and replaces the var with the
16241762 ** same ComponentRef in Var list with Var
@@ -1681,21 +1819,21 @@ relation get_var: (Exp.ComponentRef, Variables) => (Var,int) =
16811819 int_mod(hval,bsize) => hashindx &
16821820 array_nth(hashvec,hashindx) => indexes &
16831821 get_var2(cr, indexes) => indx &
1684- array_nth (varr,indx) => (v as VAR(cr2,_,_,_,_,_,_,_,_,_,_)) &
1822+ vararray_nth (varr,indx) => (v as VAR(cr2,_,_,_,_,_,_,_,_,_,_)) &
16851823 Exp.cref_equal(cr,cr2) => true &
16861824 int_add(indx,1) => indx'
16871825 -----------------------------
16881826 get_var(cr,VARIABLES(hashvec,varr,bsize,n)) => (v,indx')
16891827
1690- rule
1691- hash_component_ref(cr) => hval &
1828+ rule hash_component_ref(cr) => hval &
16921829 int_mod(hval,bsize) => hashindx &
16931830 array_nth(hashvec,hashindx) => indexes &
16941831 get_var2(cr, indexes) => indx &
1695- array_nth(varr,indx) => (v as VAR(cr2,_,_,_,_,_,_,_,_,_,_)) &
1696- Exp.cref_equal(cr,cr2) => true &
1697- print "-get_var failed\n"
1698- --------------------
1832+ not vararray_nth(varr,indx) => (_) &
1833+ print "get var failed because vararray_nth failed, cr:" &
1834+ Exp.print_component_ref_str cr => str &
1835+ print str & print "\n"
1836+ -----------------
16991837 get_var(cr,VARIABLES(hashvec,varr,bsize,n)) => fail
17001838end
17011839(** relation get_var2
@@ -1710,7 +1848,6 @@ relation get_var2:(Exp.ComponentRef, CrefIndex list) => int =
17101848 rule get_var2(cr,vs) => res
17111849 ----------------------
17121850 get_var2(cr,v::vs) => res
1713-
17141851end
17151852
17161853(** relation: delete_var
@@ -1719,10 +1856,10 @@ end
17191856 **)
17201857relation delete_var: (Variables,Exp.ComponentRef) => Variables =
17211858
1722- rule array_list (varr) => varlst &
1859+ rule vararray_list (varr) => varlst &
17231860 delete_var2(cr,varlst) => varlst' &
17241861 empty_vars() => newvars &
1725- add_vars(varlst,newvars) => newvars'
1862+ add_vars(varlst' ,newvars) => newvars'
17261863 --------------------------------------------------
17271864 delete_var(VARIABLES(hashvec,varr,bsize,n),cr)
17281865 => newvars'
@@ -2357,32 +2494,12 @@ end
23572494 ** is a dummy variable, etc.
23582495 **)
23592496relation replace_dummy_der_others:(Equation, Variables) => (Equation, Variables) =
2360-
2361-
23622497 rule replace_dummy_der_others_exp(e1,vars) => (e1',vars') &
23632498 replace_dummy_der_others_exp(e2,vars') => (e2', vars'')
23642499 ---------------------------------------------------------------
23652500 replace_dummy_der_others(EQUATION(e1,e2),vars)
23662501 => (EQUATION(e1',e2'),vars'')
23672502
2368- rule not replace_dummy_der_others_exp(e1,vars) => (_,_) &
2369- replace_dummy_der_others_exp(e2,vars) => (e2', vars')
2370- ----------------------
2371- replace_dummy_der_others(EQUATION(e1,e2),vars)
2372- => (EQUATION(e1,e2'),vars')
2373-
2374- rule replace_dummy_der_others_exp(e1,vars) => (e1',vars') &
2375- not replace_dummy_der_others_exp(e2,vars) => (_, _)
2376- ----------------------
2377- replace_dummy_der_others(EQUATION(e1,e2),vars)
2378- => (EQUATION(e1',e2),vars')
2379-
2380- rule not replace_dummy_der_others_exp(e1,vars) => (_,_) &
2381- not replace_dummy_der_others_exp(e2,vars) => (_, _)
2382- ----------------------
2383- replace_dummy_der_others(EQUATION(e1,e2),vars)
2384- => (EQUATION(e1,e2),vars)
2385-
23862503 rule print "-replace_dummy_der_others failed\n"
23872504 ---------------------
23882505 replace_dummy_der_others(_,_) => fail
@@ -2472,6 +2589,7 @@ relation replace_dummy_der_others_exp: (Exp.Exp, Variables) => (Exp.Exp,Variable
24722589 _),vars)
24732590 => (Exp.CREF(dummyder,Exp.REAL),vars')
24742591
2592+ axiom replace_dummy_der_others_exp(e,vars) => (e,vars)
24752593end
24762594
24772595relation var_equal: (Var,Var) => bool =
0 commit comments