@ -1,4 +1,4 @@
# include "storm/storage/jani/traverser/ ArrayEliminator.h"
# include "storm/storage/jani/ArrayEliminator.h"
# include <unordered_map>
@ -10,6 +10,7 @@
# include "storm/storage/expressions/ExpressionManager.h"
# include "storm/exceptions/NotSupportedException.h"
# include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace jani {
@ -105,11 +106,188 @@ namespace storm {
}
virtual boost : : any visit ( storm : : expressions : : ArrayAccessExpression const & expression , boost : : any const & data ) override {
STORM_LOG_WARN ( " Array access expression on rhs of array assignment . This is not expected since nested arrays are currently not supported." ) ;
STORM_LOG_WARN ( " Found Array access expression within an array expression . This is not expected since nested arrays are currently not supported." ) ;
return 0 ;
}
} ;
class ArrayExpressionEliminationVisitor : public storm : : expressions : : ExpressionVisitor , public storm : : expressions : : JaniExpressionVisitor {
public :
typedef std : : shared_ptr < storm : : expressions : : BaseExpression const > BaseExprPtr ;
ArrayExpressionEliminationVisitor ( std : : unordered_map < storm : : expressions : : Variable , std : : vector < storm : : jani : : Variable const * > > const & replacements , std : : unordered_map < storm : : expressions : : Variable , std : : size_t > const & sizes ) : replacements ( replacements ) , arraySizes ( sizes ) { }
virtual ~ ArrayExpressionEliminationVisitor ( ) = default ;
storm : : expressions : : Expression eliminate ( storm : : expressions : : Expression const & expression , storm : : expressions : : Expression const & outOfBoundsExpression ) {
auto res = eliminate ( expression , false ) ;
if ( outOfBoundsError ) {
return outOfBoundsExpression ;
} else {
return res ;
}
}
storm : : expressions : : Expression eliminate ( storm : : expressions : : Expression const & expression , bool failIfOutOfBounds = true ) {
outOfBoundsError = false ;
// here, data is the accessed index of the most recent array access expression. Initially, there is none.
auto res = storm : : expressions : : Expression ( boost : : any_cast < BaseExprPtr > ( expression . accept ( * this , boost : : any ( ) ) ) ) ;
STORM_LOG_THROW ( ! failIfOutOfBounds | | ! outOfBoundsError , storm : : exceptions : : UnexpectedException , " Out of bounds array access occured while eliminating expression " < < expression ) ;
return res . simplify ( ) ;
}
virtual boost : : any visit ( storm : : expressions : : IfThenElseExpression const & expression , boost : : any const & data ) override {
// for the condition expression, outer array accesses should not matter.
BaseExprPtr conditionExpression = boost : : any_cast < BaseExprPtr > ( expression . getCondition ( ) - > accept ( * this , boost : : any ( ) ) ) ;
BaseExprPtr thenExpression = boost : : any_cast < BaseExprPtr > ( expression . getThenExpression ( ) - > accept ( * this , data ) ) ;
BaseExprPtr elseExpression = boost : : any_cast < BaseExprPtr > ( expression . getElseExpression ( ) - > accept ( * this , data ) ) ;
// If the arguments did not change, we simply push the expression itself.
if ( conditionExpression . get ( ) = = expression . getCondition ( ) . get ( ) & & thenExpression . get ( ) = = expression . getThenExpression ( ) . get ( ) & & elseExpression . get ( ) = = expression . getElseExpression ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : IfThenElseExpression ( expression . getManager ( ) , thenExpression - > getType ( ) , conditionExpression , thenExpression , elseExpression ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : BinaryBooleanFunctionExpression const & expression , boost : : any const & data ) override {
STORM_LOG_ASSERT ( data . empty ( ) , " BinaryBooleanFunctionExpressions should not be direct subexpressions of array access expressions. However, the expression " < < expression < < " is. " ) ;
BaseExprPtr firstExpression = boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , data ) ) ;
BaseExprPtr secondExpression = boost : : any_cast < BaseExprPtr > ( expression . getSecondOperand ( ) - > accept ( * this , data ) ) ;
// If the arguments did not change, we simply push the expression itself.
if ( firstExpression . get ( ) = = expression . getFirstOperand ( ) . get ( ) & & secondExpression . get ( ) = = expression . getSecondOperand ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : BinaryBooleanFunctionExpression ( expression . getManager ( ) , expression . getType ( ) , firstExpression , secondExpression , expression . getOperatorType ( ) ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : BinaryNumericalFunctionExpression const & expression , boost : : any const & data ) override {
STORM_LOG_ASSERT ( data . empty ( ) , " BinaryNumericalFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " < < expression < < " is. " ) ;
BaseExprPtr firstExpression = boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , data ) ) ;
BaseExprPtr secondExpression = boost : : any_cast < BaseExprPtr > ( expression . getSecondOperand ( ) - > accept ( * this , data ) ) ;
// If the arguments did not change, we simply push the expression itself.
if ( firstExpression . get ( ) = = expression . getFirstOperand ( ) . get ( ) & & secondExpression . get ( ) = = expression . getSecondOperand ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : BinaryNumericalFunctionExpression ( expression . getManager ( ) , expression . getType ( ) , firstExpression , secondExpression , expression . getOperatorType ( ) ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : BinaryRelationExpression const & expression , boost : : any const & data ) override {
STORM_LOG_ASSERT ( data . empty ( ) , " BinaryRelationExpression should not be direct subexpressions of array access expressions. However, the expression " < < expression < < " is. " ) ;
BaseExprPtr firstExpression = boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , data ) ) ;
BaseExprPtr secondExpression = boost : : any_cast < BaseExprPtr > ( expression . getSecondOperand ( ) - > accept ( * this , data ) ) ;
// If the arguments did not change, we simply push the expression itself.
if ( firstExpression . get ( ) = = expression . getFirstOperand ( ) . get ( ) & & secondExpression . get ( ) = = expression . getSecondOperand ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : BinaryRelationExpression ( expression . getManager ( ) , expression . getType ( ) , firstExpression , secondExpression , expression . getRelationType ( ) ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : VariableExpression const & expression , boost : : any const & data ) override {
if ( expression . getType ( ) . isArrayType ( ) ) {
STORM_LOG_THROW ( ! data . empty ( ) , storm : : exceptions : : NotSupportedException , " Unable to translate array variable to basic variable, since it does not seem to be within an array access expression. " ) ;
uint64_t index = boost : : any_cast < uint64_t > ( data ) ;
STORM_LOG_ASSERT ( replacements . find ( expression . getVariable ( ) ) ! = replacements . end ( ) , " Unable to find array variable " < < expression < < " in array replacements. " ) ;
auto const & arrayVarReplacements = replacements . at ( expression . getVariable ( ) ) ;
STORM_LOG_ASSERT ( index < arrayVarReplacements . size ( ) , " No replacement for array variable, since index " < < index < < " is out of bounds. " ) ;
return arrayVarReplacements [ index ] - > getExpressionVariable ( ) . getExpression ( ) . getBaseExpressionPointer ( ) ;
} else {
return expression . getSharedPointer ( ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : UnaryBooleanFunctionExpression const & expression , boost : : any const & data ) override {
STORM_LOG_ASSERT ( data . empty ( ) , " UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " < < expression < < " is. " ) ;
BaseExprPtr operandExpression = boost : : any_cast < BaseExprPtr > ( expression . getOperand ( ) - > accept ( * this , data ) ) ;
// If the argument did not change, we simply push the expression itself.
if ( operandExpression . get ( ) = = expression . getOperand ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : UnaryBooleanFunctionExpression ( expression . getManager ( ) , expression . getType ( ) , operandExpression , expression . getOperatorType ( ) ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : UnaryNumericalFunctionExpression const & expression , boost : : any const & data ) override {
STORM_LOG_ASSERT ( data . empty ( ) , " UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " < < expression < < " is. " ) ;
BaseExprPtr operandExpression = boost : : any_cast < BaseExprPtr > ( expression . getOperand ( ) - > accept ( * this , data ) ) ;
// If the argument did not change, we simply push the expression itself.
if ( operandExpression . get ( ) = = expression . getOperand ( ) . get ( ) ) {
return expression . getSharedPointer ( ) ;
} else {
return std : : const_pointer_cast < storm : : expressions : : BaseExpression const > ( std : : shared_ptr < storm : : expressions : : BaseExpression > ( new storm : : expressions : : UnaryNumericalFunctionExpression ( expression . getManager ( ) , expression . getType ( ) , operandExpression , expression . getOperatorType ( ) ) ) ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : BooleanLiteralExpression const & expression , boost : : any const & ) override {
return expression . getSharedPointer ( ) ;
}
virtual boost : : any visit ( storm : : expressions : : IntegerLiteralExpression const & expression , boost : : any const & ) override {
return expression . getSharedPointer ( ) ;
}
virtual boost : : any visit ( storm : : expressions : : RationalLiteralExpression const & expression , boost : : any const & ) override {
return expression . getSharedPointer ( ) ;
}
virtual boost : : any visit ( storm : : expressions : : ValueArrayExpression const & expression , boost : : any const & data ) override {
STORM_LOG_THROW ( ! data . empty ( ) , storm : : exceptions : : NotSupportedException , " Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression. " ) ;
uint64_t index = boost : : any_cast < uint64_t > ( data ) ;
STORM_LOG_ASSERT ( expression . size ( ) - > isIntegerLiteralExpression ( ) , " unexpected kind of size expression of ValueArrayExpression ( " < < expression . size ( ) - > toExpression ( ) < < " ). " ) ;
if ( index < static_cast < uint64_t > ( expression . size ( ) - > evaluateAsInt ( ) ) ) {
return expression . at ( index ) ;
} else {
outOfBoundsError = true ;
return expression . at ( 0 ) ;
}
}
virtual boost : : any visit ( storm : : expressions : : ConstructorArrayExpression const & expression , boost : : any const & data ) override {
STORM_LOG_THROW ( ! data . empty ( ) , storm : : exceptions : : NotSupportedException , " Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression. " ) ;
uint64_t index = boost : : any_cast < uint64_t > ( data ) ;
if ( expression . size ( ) - > containsVariables ( ) ) {
STORM_LOG_WARN ( " Ignoring length of constructorArrayExpression " < < expression < < " as it still contains variables. " ) ;
} else if ( index > = static_cast < uint64_t > ( expression . size ( ) - > evaluateAsInt ( ) ) ) {
outOfBoundsError = true ;
}
return expression . at ( index ) ;
}
virtual boost : : any visit ( storm : : expressions : : ArrayAccessExpression const & expression , boost : : any const & data ) override {
if ( expression . getSecondOperand ( ) - > containsVariables ( ) ) {
//get the size of the array expression
uint64_t size = MaxArraySizeExpressionVisitor ( ) . getMaxSize ( expression . getFirstOperand ( ) - > toExpression ( ) , arraySizes ) ;
STORM_LOG_THROW ( size > 0 , storm : : exceptions : : NotSupportedException , " Unable to get size of array expression for array access " < < expression < < " . " ) ;
uint64_t index = size - 1 ;
storm : : expressions : : Expression result = boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , index ) ) - > toExpression ( ) ;
while ( index > 0 ) {
- - index ;
result = storm : : expressions : : ite (
expression . getSecondOperand ( ) - > toExpression ( ) = = expression . getManager ( ) . integer ( index ) ,
boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , index ) ) - > toExpression ( ) ,
result ) ;
}
return result . getBaseExpressionPointer ( ) ;
} else {
uint64_t index = expression . getSecondOperand ( ) - > evaluateAsInt ( ) ;
return boost : : any_cast < BaseExprPtr > ( expression . getFirstOperand ( ) - > accept ( * this , index ) ) ;
}
}
private :
std : : unordered_map < storm : : expressions : : Variable , std : : vector < storm : : jani : : Variable const * > > const & replacements ;
std : : unordered_map < storm : : expressions : : Variable , std : : size_t > const & arraySizes ;
bool outOfBoundsError ;
} ;
class MaxArraySizeDeterminer : public ConstJaniTraverser {
public :
@ -127,7 +305,7 @@ namespace storm {
return result ;
}
virtual void traverse ( Assignment const & assignment , boost : : any const & data ) const override {
virtual void traverse ( Assignment const & assignment , boost : : any const & data ) override {
if ( assignment . lValueIsVariable ( ) & & assignment . getExpressionVariable ( ) . getType ( ) . isArrayType ( ) ) {
auto & map = * boost : : any_cast < MapPtr > ( data ) ;
std : : size_t newSize = MaxArraySizeExpressionVisitor ( ) . getMaxSize ( assignment . getAssignedExpression ( ) , map ) ;
@ -138,7 +316,7 @@ namespace storm {
}
}
virtual void traverse ( ArrayVariable const & variable , boost : : any const & data ) const override {
virtual void traverse ( ArrayVariable const & variable , boost : : any const & data ) override {
if ( variable . hasInitExpression ( ) ) {
auto & map = * boost : : any_cast < MapPtr > ( data ) ;
std : : size_t newSize = MaxArraySizeExpressionVisitor ( ) . getMaxSize ( variable . getInitExpression ( ) , map ) ;
@ -156,19 +334,21 @@ namespace storm {
typedef ArrayEliminatorData ResultType ;
ArrayVariableReplacer ( storm : : expressions : : ExpressionManager & expressionManager , bool keepNonTrivialArrayAccess ) : expressionManager ( expressionManager ) , keepNonTrivialArrayAccess ( keepNonTrivialArrayAccess ) { }
ArrayVariableReplacer ( storm : : expressions : : ExpressionManager & expressionManager , bool keepNonTrivialArrayAccess , std : : unordered_map < storm : : expressions : : Variable , std : : size_t > const & arrayVarToSizesMap ) : expressionManager ( expressionManager ) , keepNonTrivialArrayAccess ( keepNonTrivialArrayAccess ) , arraySizes ( arrayVarToSizesMap ) { }
virtual ~ ArrayVariableReplacer ( ) = default ;
ResultType replace ( Model & model , std : : unordered_map < storm : : expressions : : Variable , std : : size_t > const & arrayVarToSizesMap ) {
ResultType replace ( Model & model ) {
ResultType result ;
for ( auto const & arraySize : arrayVarToSizesMap ) {
arrayExprEliminator = std : : make_unique < ArrayExpressionEliminationVisitor > ( result . replacements , arraySizes ) ;
for ( auto const & arraySize : arraySizes ) {
result . replacements . emplace ( arraySize . first , std : : vector < storm : : jani : : Variable const * > ( arraySize . second , nullptr ) ) ;
}
traverse ( model , & result ) ;
return result ;
}
virtual void traverse ( Model & model , boost : : any const & data ) const override {
virtual void traverse ( Model & model , boost : : any const & data ) override {
// Insert fresh basic variables for global array variables
auto & replacements = boost : : any_cast < ResultType * > ( data ) - > replacements ;
@ -183,20 +363,20 @@ namespace storm {
auto & eliminatedArrayVariables = boost : : any_cast < ResultType * > ( data ) - > eliminatedArrayVariables ;
eliminatedArrayVariables . insert ( eliminatedArrayVariables . end ( ) , elVars . begin ( ) , elVars . end ( ) ) ;
// Make new variable replacements known to the expression eliminator
arrayExprEliminator = std : : make_unique < ArrayExpressionEliminationVisitor > ( replacements , arraySizes ) ;
for ( auto & aut : model . getAutomata ( ) ) {
traverse ( aut , data ) ;
}
// traverse remaining components
for ( auto & c : model . getConstants ( ) ) {
traverse ( c , data ) ;
}
// traversal of remaining components
if ( model . hasInitialStatesRestriction ( ) ) {
//model.setInitialStatesRestriction();
model . setInitialStatesRestriction ( arrayExprEliminator - > eliminate ( model . getInitialStatesRestriction ( ) ) ) ;
}
}
virtual void traverse ( Automaton & automaton , boost : : any const & data ) const override {
virtual void traverse ( Automaton & automaton , boost : : any const & data ) override {
// No need to traverse the init restriction.
// Insert fresh basic variables for local array variables
@ -212,23 +392,23 @@ namespace storm {
auto & eliminatedArrayVariables = boost : : any_cast < ResultType * > ( data ) - > eliminatedArrayVariables ;
eliminatedArrayVariables . insert ( eliminatedArrayVariables . end ( ) , elVars . begin ( ) , elVars . end ( ) ) ;
// Make new variable replacements known to the expression eliminator
arrayExprEliminator = std : : make_unique < ArrayExpressionEliminationVisitor > ( replacements , arraySizes ) ;
for ( auto & loc : automaton . getLocations ( ) ) {
JaniTraverser : : traverse ( loc , data ) ;
}
JaniTraverser : : traverse ( automaton . getEdgeContainer ( ) , data ) ;
}
void traverse ( Constant & constant , boost : : any const & data ) const {
if ( constant . isDefined ( ) ) {
// todo:
//traverse(constant.getExpression(), data);
if ( automaton . hasInitialStatesRestriction ( ) ) {
automaton . setInitialStatesRestriction ( arrayExprEliminator - > eliminate ( automaton . getInitialStatesRestriction ( ) ) ) ;
}
}
virtual void traverse ( OrderedAssignments & orderedAssignments , boost : : any const & data ) const override {
virtual void traverse ( OrderedAssignments & orderedAssignments , boost : : any const & data ) override {
auto const & replacements = boost : : any_cast < ResultType * > ( data ) - > replacements ;
// Replace array occurrences in LValues.
// Replace array occurrences in LValues and assigned expressions .
std : : vector < Assignment > newAssignments ;
uint64_t level = 0 ;
std : : unordered_map < storm : : expressions : : Variable , std : : vector < Assignment const * > > collectedArrayAccessAssignments ;
@ -253,12 +433,14 @@ namespace storm {
STORM_LOG_ASSERT ( assignment . getAssignedExpression ( ) . getType ( ) . isArrayType ( ) , " Assigning a non-array expression to an array variable... " ) ;
std : : vector < storm : : jani : : Variable const * > const & arrayVariableReplacements = replacements . at ( assignment . getExpressionVariable ( ) ) ;
for ( uint64_t index = 0 ; index < arrayVariableReplacements . size ( ) ; + + index ) {
auto arrayAccessExpression = std : : make_shared < storm : : expressions : : ArrayAccessExpression > ( expressionManager , assignment . getAssignedExpression ( ) . getType ( ) . getElementType ( ) , assignment . getAssignedExpression ( ) . getBaseExpressionPointer ( ) , expressionManager . integer ( index ) . getBaseExpressionPointer ( ) ) ;
newAssignments . emplace_back ( LValue ( * arrayVariableReplacements [ index ] ) , arrayAccessExpression - > toExpression ( ) , level ) ;
auto const & replacement = * arrayVariableReplacements [ index ] ;
auto arrayAccessExpression = std : : make_shared < storm : : expressions : : ArrayAccessExpression > ( expressionManager , assignment . getAssignedExpression ( ) . getType ( ) . getElementType ( ) , assignment . getAssignedExpression ( ) . getBaseExpressionPointer ( ) , expressionManager . integer ( index ) . getBaseExpressionPointer ( ) ) - > toExpression ( ) ;
arrayAccessExpression = arrayExprEliminator - > eliminate ( arrayAccessExpression , getOutOfBoundsValue ( replacement ) ) ;
newAssignments . emplace_back ( LValue ( replacement ) , arrayAccessExpression , level ) ;
}
continue ;
}
newAssignments . push _back( assignment ) ;
newAssignments . emplace _back( assignment . getLValue ( ) , arrayExprEliminator - > eliminate ( assignment . getAssignedExpression ( ) ) , assignment . getLevel ( ) ) ;
}
for ( auto const & arrayAssignments : collectedArrayAccessAssignments ) {
insertLValueArrayAccessReplacements ( arrayAssignments . second , replacements . at ( arrayAssignments . first ) , level , newAssignments ) ;
@ -276,7 +458,7 @@ namespace storm {
std : : string name = arrayVariable . getExpressionVariable ( ) . getName ( ) + " _at_ " + std : : to_string ( index ) ;
storm : : expressions : : Expression initValue ;
if ( arrayVariable . hasInitExpression ( ) ) {
initValue = std : : make_shared < storm : : expressions : : ArrayAccessExpression > ( expressionManager , arrayVariable . getExpressionVariable ( ) . getType ( ) . getElementType ( ) , arrayVariable . getInitExpression ( ) . getBaseExpressionPointer ( ) , expressionManager . integer ( index ) . getBaseExpressionPointer ( ) ) - > toExpression ( ) ;
initValue = arrayExprEliminator - > eliminate ( std : : make_shared < storm : : expressions : : ArrayAccessExpression > ( expressionManager , arrayVariable . getExpressionVariable ( ) . getType ( ) . getElementType ( ) , arrayVariable . getInitExpression ( ) . getBaseExpressionPointer ( ) , expressionManager . integer ( index ) . getBaseExpressionPointer ( ) ) - > toExpression ( ) ) ;
}
if ( arrayVariable . getElementType ( ) = = ArrayVariable : : ElementType : : Int ) {
storm : : expressions : : Variable exprVariable = expressionManager . declareIntegerVariable ( name ) ;
@ -324,31 +506,50 @@ namespace storm {
if ( onlyConstantIndices ) {
for ( auto const & aa : arrayAccesses ) {
LValue lvalue ( * arrayVariableReplacements . at ( aa - > getLValue ( ) . getArrayIndex ( ) . evaluateAsInt ( ) ) ) ;
newAssignments . emplace_back ( lvalue , aa - > getAssignedExpression ( ) , level ) ;
newAssignments . emplace_back ( lvalue , arrayExprEliminator - > eliminate ( a a - > getAssignedExpression ( ) ) , level ) ;
}
} else {
for ( uint64_t index = 0 ; index < arrayVariableReplacements . size ( ) ; + + index ) {
storm : : expressions : : Expression assignedExpression = arrayVariableReplacements [ index ] - > getExpressionVariable ( ) . getExpression ( ) ;
auto indexExpression = expressionManager . integer ( index ) ;
for ( auto const & aa : arrayAccesses ) {
assignedExpression = storm : : expressions : : ite ( aa - > getLValue ( ) . getArrayIndex ( ) = = indexExpression , aa - > getAssignedExpression ( ) , assignedExpression ) ;
assignedExpression = storm : : expressions : : ite ( aa - > getLValue ( ) . getArrayIndex ( ) = = indexExpression , arrayExprEliminator - > eliminate ( a a - > getAssignedExpression ( ) ) , assignedExpression ) ;
newAssignments . emplace_back ( LValue ( * arrayVariableReplacements [ index ] ) , assignedExpression , level ) ;
}
}
}
}
storm : : expressions : : Expression getOutOfBoundsValue ( Variable const & var ) const {
if ( var . hasInitExpression ( ) ) {
return var . getInitExpression ( ) ;
}
if ( var . isBooleanVariable ( ) ) {
return expressionManager . boolean ( false ) ;
}
if ( var . isBoundedIntegerVariable ( ) ) {
return var . asBoundedIntegerVariable ( ) . getLowerBound ( ) ;
}
if ( var . isUnboundedIntegerVariable ( ) ) {
return expressionManager . integer ( 0 ) ;
}
if ( var . isRealVariable ( ) ) {
return expressionManager . rational ( 0.0 ) ;
}
STORM_LOG_THROW ( false , storm : : exceptions : : UnexpectedException , " unhandled variabe type " ) ;
return storm : : expressions : : Expression ( ) ;
}
std : : unique_ptr < ArrayExpressionEliminationVisitor > arrayExprEliminator ;
storm : : expressions : : ExpressionManager & expressionManager ;
bool const keepNonTrivialArrayAccess ;
std : : unordered_map < storm : : expressions : : Variable , std : : size_t > const & arraySizes ;
} ;
} // namespace detail
ArrayEliminatorData ArrayEliminator : : eliminate ( Model & model , bool keepNonTrivialArrayAccess ) {
auto sizes = detail : : MaxArraySizeDeterminer ( ) . getMaxSizes ( model ) ;
ArrayEliminatorData result = detail : : ArrayVariableReplacer ( model . getExpressionManager ( ) , keepNonTrivialArrayAccess ) . replace ( model , sizes ) ;
ArrayEliminatorData result = detail : : ArrayVariableReplacer ( model . getExpressionManager ( ) , keepNonTrivialArrayAccess , sizes ) . replace ( model ) ;
model . finalize ( ) ;
return result ;
TimQu
7 years ago