From 1976a412986ffcb2392619ed8600e4302cc8d5c4 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 17 Apr 2019 14:07:15 +0200
Subject: [PATCH] Reworked solver integration

---
 src/storm-dft/api/storm-dft.cpp               |  5 +++-
 .../modelchecker/dft/DFTASFChecker.cpp        | 26 ++++++++++++-------
 .../modelchecker/dft/DFTASFChecker.h          | 10 ++++++-
 3 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp
index 32796b7e8..961b5fd5d 100644
--- a/src/storm-dft/api/storm-dft.cpp
+++ b/src/storm-dft/api/storm-dft.cpp
@@ -47,7 +47,10 @@ namespace storm {
         analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
             storm::modelchecker::DFTASFChecker smtChecker(dft);
             smtChecker.convert();
-            std::vector<storm::solver::SmtSolver::CheckResult> results = smtChecker.toSolver();
+            smtChecker.toSolver();
+            std::vector<storm::solver::SmtSolver::CheckResult> results;
+
+            results.push_back(smtChecker.checkTleNeverFailedQuery());
 
             if (printOutput) {
                 // TODO add suitable output function, maybe add query descriptions for better readability
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index da5daa574..5c26ca08f 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -429,10 +429,12 @@ namespace storm {
             storm::utility::closeFile(stream);
         }
 
-        std::vector<storm::solver::SmtSolver::CheckResult> DFTASFChecker::toSolver() {
-            std::vector<storm::solver::SmtSolver::CheckResult> resultVector;
+        void DFTASFChecker::toSolver() {
+            // First convert the DFT
+            convert();
+
             std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
-            std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(
+            solver = storm::utility::solver::SmtSolverFactory().create(
                     *manager);
             //Add variables to manager
             for (auto const &timeVarEntry : timePointVariables) {
@@ -453,19 +455,23 @@ namespace storm {
             for (auto const &constraint : constraints) {
                 solver->add(constraint->toExpression(varNames, manager));
             }
-            // Set backtracking marker to check several properties without reconstructing DFT encoding
-            solver->push();
 
-            //TODO put different queries in separate functions for further modularization
+        }
+
+        storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() {
+            STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
 
+            // Set backtracking marker to check several properties without reconstructing DFT encoding
+            solver->push();
             // Constraint that toplevel element will not fail (part of constraint 13)
             std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
                     timePointVariables.at(dft.getTopLevelIndex()), notFailed);
-            solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
-            resultVector.push_back(solver->check());
+            solver->add(tleNeverFailedConstr->toExpression(varNames,
+                                                           std::make_shared<storm::expressions::ExpressionManager>(
+                                                                   solver->getManager())));
+            storm::solver::SmtSolver::CheckResult res = solver->check();
             solver->pop();
-
-            return resultVector;
+            return res;
         }
     }
 }
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
index 097ca0732..bf448b0ba 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
@@ -37,7 +37,7 @@ namespace storm {
             void convert();
             void toFile(std::string const&);
 
-            std::vector<storm::solver::SmtSolver::CheckResult> toSolver();
+            void toSolver();
             
         private:
             uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
@@ -115,8 +115,16 @@ namespace storm {
              * This corresponds to constraints (9), (10) and (11)
              */
             void addMarkovianConstraints();
+
+            /**
+             * Check if the TLE of the DFT never fails
+             *
+             * @return  "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown"
+             */
+            storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery();
             
             storm::storage::DFT<ValueType> const& dft;
+            std::shared_ptr<storm::solver::SmtSolver> solver = 0;
             std::vector<std::string> varNames;
             std::unordered_map<uint64_t, uint64_t> timePointVariables;
             std::vector<std::shared_ptr<SmtConstraint>> constraints;