substitute formulas in properties after parsing

src/storm-parsers/api/properties.cpp

@@ -58,7 +58,7 @@ namespace storm {
         std::vector <storm::jani::Property> parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional <std::set<std::string>> const &propertyFilter) {
             storm::parser::FormulaParser formulaParser(program);
             auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
-            return substituteConstantsInProperties(formulas, program.getConstantsSubstitution());
+            return substituteConstantsInProperties(formulas, program.getConstantsFormulasSubstitution());
         }
 
         std::vector <storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional <std::set<std::string>> const &propertyFilter) {

src/storm-parsers/parser/FormulaParser.cpp

@@ -32,18 +32,9 @@ namespace storm {
         }
 
         FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) {
-            this->addFormulasAsIdentifiers(program);
         }
 
         FormulaParser::FormulaParser(storm::prism::Program& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) {
-            this->addFormulasAsIdentifiers(program);
-        }
-
-        void FormulaParser::addFormulasAsIdentifiers(storm::prism::Program const& program) {
-            // Make the formulas of the program available to the parser.
-            for (auto const& formula : program.getFormulas()) {
-                this->addIdentifierExpression(formula.getName(), formula.getExpression());
-            }
         }
 
         FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) {

src/storm/storage/prism/Program.cpp

@@ -333,6 +333,14 @@ namespace storm {
             return constantsSubstitution;
         }
         
+        std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsFormulasSubstitution() const {
+            auto result = getConstantsSubstitution();
+            for (auto const& formula : this->getFormulas()) {
+                result.emplace(formula.getExpressionVariable(), formula.getExpression());
+            }
+            return result;
+        }
+        
         std::size_t Program::getNumberOfConstants() const {
             return this->getConstants().size();
         }

src/storm/storage/prism/Program.h

@@ -138,6 +138,13 @@ namespace storm {
              */
             std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
             
+            /*!
+             * Retrieves a mapping of all defined constants and formula variables to their defining expressions
+             *
+             * @return A mapping from constants and formulas to their expressions.
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsFormulasSubstitution() const;
+            
             /*!
              * Retrieves all constants defined in the program.
              *