make storm compile when carl is not available

added settings for smt-lib solver


Former-commit-id: 7d1872267a

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -988,6 +988,7 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         storm::storage::SparseMatrix<double> SparseDtmcEliminationModelChecker<storm::RationalFunction>::FlexibleSparseMatrix::instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions){
             
@@ -1016,6 +1017,7 @@ namespace storm {
         storm::storage::SparseMatrix<double> SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions){
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Instantiation of flexible matrix is not supported for this type");
         }
+#endif
         
         
         template<typename ValueType>
@@ -1045,7 +1047,7 @@ namespace storm {
             
             return flexibleMatrix;
         }
-        
+#ifdef STORM_HAVE_CARL
         template<>
         bool SparseDtmcEliminationModelChecker<storm::RationalFunction>::checkRegion(storm::logic::Formula const& formula, std::vector<SparseDtmcEliminationModelChecker<storm::RationalFunction>::ParameterRegion> parameterRegions){
             //Note: this is an 'experimental' implementation
@@ -1318,13 +1320,14 @@ namespace storm {
             
             return false;
         }
-        
+
         template<typename ValueType>
         bool SparseDtmcEliminationModelChecker<ValueType>::checkRegion(storm::logic::Formula const& formula, std::vector<SparseDtmcEliminationModelChecker<ValueType>::ParameterRegion> parameterRegions){
             
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type");
         }
-        
+
+#endif        
         template class SparseDtmcEliminationModelChecker<double>;
         
 #ifdef STORM_HAVE_CARL

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -21,19 +21,21 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
             virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
-            
+
+#ifdef STORM_HAVE_CARL
             struct ParameterRegion{
                 storm::Variable variable;
                 storm::RationalFunction::CoeffType lowerBound;
                 storm::RationalFunction::CoeffType upperBound;
             };
+
             
             /*!
              * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions
              * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals)
              */
             bool checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
-            
+#endif            
             
             
         private:
@@ -66,6 +68,7 @@ namespace storm {
                  */
                 bool hasSelfLoop(storm::storage::sparse::state_type state);
                 
+#ifdef STORM_HAVE_CARL
                 /*!
                  * Instantiates the matrix, i.e., evaluate the occurring functions according to the given substitution of the variables
                  * 
@@ -74,7 +77,7 @@ namespace storm {
                  * @return A matrix with constant (double) entries
                  */
                 storm::storage::SparseMatrix<double> instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions);
-                
+#endif         
                 
             private:
                 std::vector<row_type> data;

src/settings/SettingsManager.cpp

@@ -27,6 +27,7 @@ namespace storm {
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
 			this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
+            this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::Smt2SmtSolverSettings(*this)));
 			this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::TopologicalValueIterationEquationSolverSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::ParametricSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::SparseDtmcEliminationModelCheckerSettings(*this)));
@@ -511,6 +512,10 @@ namespace storm {
             return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
 		}
 
+        storm::settings::modules::Smt2SmtSolverSettings const& smt2SmtSolverSettings() {
+            return dynamic_cast<storm::settings::modules::Smt2SmtSolverSettings const&>(manager().getModule(storm::settings::modules::Smt2SmtSolverSettings::moduleName));
+        }
+
 		storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings() {
 			return dynamic_cast<storm::settings::modules::TopologicalValueIterationEquationSolverSettings const&>(manager().getModule(storm::settings::modules::TopologicalValueIterationEquationSolverSettings::moduleName));
 		}

src/settings/SettingsManager.h

@@ -28,6 +28,7 @@
 #include "src/settings/modules/BisimulationSettings.h"
 #include "src/settings/modules/GlpkSettings.h"
 #include "src/settings/modules/GurobiSettings.h"
+#include "src/settings/modules/Smt2SmtSolverSettings.h"
 #include "src/settings/modules/ParametricSettings.h"
 #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
@@ -312,6 +313,13 @@ namespace storm {
          */
 		storm::settings::modules::GurobiSettings const& gurobiSettings();
 
+        /*!
+        * Retrieves the settings of the SMT-LIBv2 SMT solver.
+        *
+        * @return the settings of SMT-LIBv2 SMT solver.
+        */
+        storm::settings::modules::Smt2SmtSolverSettings const& smt2SmtSolverSettings();
+
 		/*!
 		* Retrieves the settings of the topological value iteration-based equation solver.
 		*

src/settings/modules/Smt2SmtSolverSettings.cpp

@@ -0,0 +1,48 @@
+#include "src/settings/modules/Smt2SmtSolverSettings.h"
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string Smt2SmtSolverSettings::moduleName = "smt2smtsolver";
+            const std::string Smt2SmtSolverSettings::solverCommandOption = "solvercommand";
+            const std::string Smt2SmtSolverSettings::exportSmtLibScriptOption = "exportSmtLibScript";
+            
+            Smt2SmtSolverSettings::Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, solverCommandOption, true, "If set, this command is used to call the solver and to let the solver know that it should read SMT-LIBv2 commands from standard input. If not set, only a SMT-LIB script file might be exported.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("command", "path to the solver + command line arguments.").setDefaultValueString("").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportSmtLibScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build());
+            }
+            
+            bool Smt2SmtSolverSettings::isSolverCommandSet() const{
+                return this->getOption(solverCommandOption).getHasOptionBeenSet();
+            }
+
+            std::string Smt2SmtSolverSettings::getSolverCommand() const{
+                return this->getOption(solverCommandOption).getArgumentByName("command").getValueAsString();
+            }
+
+
+            bool Smt2SmtSolverSettings::isExportSmtLibScriptSet() const{
+                return this->getOption(exportSmtLibScriptOption).getHasOptionBeenSet();
+            }
+
+
+            std::string Smt2SmtSolverSettings::getExportSmtLibScriptPath() const{
+                return this->getOption(solverCommandOption).getArgumentByName("path").getValueAsString();
+            }
+
+
+            bool Smt2SmtSolverSettings::check() const {
+                if (isSolverCommandSet() || isExportSmtLibScriptSet()) {
+                //TODO check if paths are valid
+   
+                }
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/Smt2SmtSolverSettings.h

@@ -0,0 +1,65 @@
+#ifndef STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_
+#define STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for interaction with SMT-LIBv2 solvers.
+             */
+            class Smt2SmtSolverSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new set of Smt2SmtSolver settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager);
+                
+                /*!
+                 * Retrieves whether the solver command has been set.
+                 *
+                 * @return True iff the solver command has been set.
+                 */
+                bool isSolverCommandSet() const;
+
+                /*!
+                * Retrieves the solver command i.e. the path and the command line arguments for the solver.
+                *
+                * @return The solver command to be used
+                */
+                std::string getSolverCommand() const;
+                
+                /*!
+                * Retrieves whether the SMT-LIBv2 script should be exportet to a file.
+                *
+                * @return True iff the SMT-LIBv2 script should be exportet to a file.
+                */
+                bool isExportSmtLibScriptSet() const;
+
+                /*!
+                * Retrieves the path where the SMT-LIBv2 script file should be exportet to.
+                *
+                * @return the path where the SMT-LIBv2 script file should be exportet to.
+                */
+                std::string getExportSmtLibScriptPath() const;
+
+                bool check() const override;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                // Define the string names of the options as constants.
+                static const std::string solverCommandOption;
+                static const std::string exportSmtLibScriptOption;
+            };
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_ */

src/solver/Smt2SmtSolver.cpp

@@ -1,12 +1,13 @@
 #include "src/solver/Smt2SmtSolver.h"
 
+#include "src/settings/SettingsManager.h"
 #include "src/exceptions/NotSupportedException.h"
-#include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/IllegalArgumentException.h"
+#include "src/exceptions/IllegalFunctionCallException.h"
 #include "utility/macros.h"
 #include "adapters/CarlAdapter.h"
-#include "exceptions/IllegalArgumentException.h"
-#include "exceptions/IllegalFunctionCallException.h"
 
 namespace storm {
     namespace solver {
@@ -99,7 +100,14 @@ namespace storm {
 
         SmtSolver::CheckResult Smt2SmtSolver::check() {
             writeCommand("( check-sat )");
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
+                // todo get the result
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            }
+            else{
+                STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\"");
+                return SmtSolver::CheckResult::Unknown;
+            }
         }
 
         SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
@@ -114,9 +122,19 @@ namespace storm {
 #endif
 
         void Smt2SmtSolver::init() {
-            //hard coded output file.. for now
-            commandFile.open("/home/tim/Desktop/smtlibcommand.txt", std::ios::trunc);
-            STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
+            if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
+                //todo call the solver!
+                std::string cmd = storm::settings::smt2SmtSolverSettings().getSolverCommand();
+            }
+            else{
+                STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
+            }
+
+            if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){
+                STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
+                commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc);
+                STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
+            }
 
             //some initial commands
             writeCommand("( set-logic QF_NRA )");