From a412ac2a6033454cad1e1f83af51065f0689cc64 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Jun 2015 22:14:52 +0200
Subject: [PATCH] Progress in smtrat-smtsolver interface

Former-commit-id: 2cee8a49680ab9c4db8c31f5885b5cad6b4ea206
---
 src/solver/SmtratSmtSolver.cpp | 107 +++++++++++++++++++++++++++++++++
 src/solver/SmtratSmtSolver.h   |  50 +++++++++++++++
 2 files changed, 157 insertions(+)
 create mode 100644 src/solver/SmtratSmtSolver.cpp
 create mode 100644 src/solver/SmtratSmtSolver.h

diff --git a/src/solver/SmtratSmtSolver.cpp b/src/solver/SmtratSmtSolver.cpp
new file mode 100644
index 000000000..ca6e8942d
--- /dev/null
+++ b/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();
+                }
+                
+
+        }
+}
diff --git a/src/solver/SmtratSmtSolver.h b/src/solver/SmtratSmtSolver.h
new file mode 100644
index 000000000..22bfa08e7
--- /dev/null
+++ b/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
\ No newline at end of file