Progress in smtrat-smtsolver interface

Former-commit-id: 2cee8a4968

src/solver/SmtratSmtSolver.cpp

@@ -0,0 +1,107 @@
+#include "src/solver/SmtratSmtSolver.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/NotSupportedException.h"
+#include "src/exceptions/InvalidStateException.h"
+
+#ifdef STORM_HAVE_SMTRAT
+#include "lib/smtrat.h"
+#endif 
+
+namespace storm {
+	namespace solver {
+
+        
+		SmtratSmtSolver::SmtratSmtSolver(storm::expressions::ExpressionManager& manager) : SmtSolver(manager)
+		{
+#ifndef STORM_HAVE_SMTRAT
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
+#else 
+                     // Construct the settingsManager.
+                    //smtrat::RuntimeSettingsManager settingsManager;
+                    
+                    // Construct solver.
+                    smtrat::RatOne* solver = new smtrat::RatOne();
+
+                    //std::list<std::pair<std::string, smtrat::RuntimeSettings*> > settingsObjects =
+                    smtrat::addModules( solver );
+
+                    // Introduce the settingsObjects from the modules to the manager.
+                    //settingsManager.addSettingsObject( settingsObjects );
+                    //settingsObjects.clear();
+#endif 
+                }  
+        
+		SmtratSmtSolver::~SmtratSmtSolver() {
+                    delete solver;
+                }
+
+		void SmtratSmtSolver::push()
+		{
+#ifndef STORM_HAVE_SMTRAT
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
+#else
+                    this->solver->push();
+#endif
+		}
+
+		void SmtratSmtSolver::pop()
+		{
+#ifndef STORM_HAVE_SMTRAT
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
+#else
+                    this->solver->pop();
+#endif		
+                }
+
+		void SmtratSmtSolver::pop(uint_fast64_t n)
+		{
+#ifndef STORM_HAVE_SMTRAT
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
+#else
+                    this->solver->pop(static_cast<unsigned int>(n));
+#endif
+		}
+
+		
+		SmtSolver::CheckResult SmtratSmtSolver::check()
+		{
+#ifdef STORM_HAVE_SMTRAT
+                    switch (this->solver->check()) {
+                        case smtrat::Answer::True:
+                            this->lastResult = SmtSolver::CheckResult::Sat;
+                            break;
+                        case smtrat::Answer::False:
+                            this->lastResult = SmtSolver::CheckResult::Unsat;
+                            break;
+                        case smtrat::Answer::Unknown:
+                            this->lastResult = SmtSolver::CheckResult::Unknown;
+                            break;
+                        default:
+                            // maybe exit
+                            this->lastResult = SmtSolver::CheckResult::Unknown;
+                            break;
+                    }
+                    return this->lastResult;
+#else
+			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
+                
+                void SmtratSmtSolver::add(const storm::RawPolynomial& pol, storm::CompareRelation cr) {
+                    this->solver->add(smtrat::FormulaT(pol, cr));
+                }
+                
+                template<>
+                smtrat::Model SmtratSmtSolver::getModel() const
+                {
+                    return this->solver->model();
+                }
+                
+                std::vector<smtrat::FormulasT> const& SmtratSmtSolver::getUnsatisfiableCores() const
+                {
+                    return this->solver->infeasibleSubsets();
+                }
+                
+
+        }
+}

src/solver/SmtratSmtSolver.h

@@ -0,0 +1,50 @@
+#ifndef STORM_SOLVER_SMTRATSMTSOLVER
+#define STORM_SOLVER_SMTRATSMTSOLVER
+#include "storm-config.h"
+#include "src/solver/SmtSolver.h"
+
+#ifdef STORM_HAVE_SMTRAT
+#include "lib/smtrat.h"
+#include "../adapters/carlAdapter.h"
+
+
+namespace storm {
+	namespace solver {
+		class SmtratSmtSolver : public SmtSolver {
+                private:
+                        smtrat::RatOne* solver;
+                        unsigned exitCode;
+                    
+		public:
+			SmtratSmtSolver(storm::expressions::ExpressionManager& manager);
+			virtual ~SmtratSmtSolver();
+
+			virtual void push() override;
+
+			virtual void pop() override;
+
+			virtual void pop(uint_fast64_t n) override;
+
+			virtual CheckResult check() override;
+#ifdef STORM_HAVE_CARL 
+                        void add(storm::RawPolynomial const&, storm::CompareRelation);
+                        
+                        template<typename ReturnType>
+                        ReturnType  getModel() const;
+                        
+                        std::vector<smtrat::FormulasT> const& getUnsatisfiableCores() const;
+                        
+                        
+                        
+                        
+                        
+#endif
+            
+            // The last result that was returned by any of the check methods.
+			CheckResult lastResult;
+		};
+	}
+}
+#endif
+
+#endif // STORM_SOLVER_SMTRATSMTSOLVER