From bf07feb812527d494f250106a9f1ad64fd3d0021 Mon Sep 17 00:00:00 2001
From: Niklas Krafczyk <niklas@uni-bremen.de>
Date: Tue, 23 May 2023 11:50:34 +0200
Subject: [PATCH 1/3] Fixing conversion warnings in LTL monitor

---
 src/libsfsmtest/monitors/ltlMonitor/ltlMonitor.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/libsfsmtest/monitors/ltlMonitor/ltlMonitor.cpp b/src/libsfsmtest/monitors/ltlMonitor/ltlMonitor.cpp
index 1144bd0..d13991e 100644
--- a/src/libsfsmtest/monitors/ltlMonitor/ltlMonitor.cpp
+++ b/src/libsfsmtest/monitors/ltlMonitor/ltlMonitor.cpp
@@ -83,8 +83,9 @@ size_t getEquivalenceClassForValuation(EquivalenceClassTable_t const &table, Ide
     std::unordered_map<Expression, bool> cache;
     auto const &base = table.base;
     std::vector<ssize_t> selectionVector;
-    for(size_t idx = 0; idx < base.size(); ++idx) {
-        if(std::get<bool>(evaluateValuationInExpression(valuation.getValuations(), base.at(idx)))) {
+    assert(base.size() < std::numeric_limits<ssize_t>::max());
+    for(ssize_t idx = 0; static_cast<size_t>(idx) < base.size(); ++idx) {
+        if(std::get<bool>(evaluateValuationInExpression(valuation.getValuations(), base.at(static_cast<size_t>(idx))))) {
             selectionVector.push_back(idx);
         }
     }
@@ -663,9 +664,9 @@ std::tuple<EquivalenceClassTable_t, PropertyMonitor> getEquivalenceClassTableAnd
         tableEntry.representative = Valuation{valuation.value()};
         tableEntry.inputEquivalenceClassId = inputEqClassMapping.at(idx);
         std::vector<ssize_t> cacheIndexes;
-        for(auto const idx : indexes) {
-            if(idx > 0) {
-                cacheIndexes.push_back(idx-1);
+        for(auto const expIdx : indexes) {
+            if(expIdx > 0) {
+                cacheIndexes.push_back(expIdx-1);
             }
         }
         table.vectorMap->operator[](cacheIndexes) = idx;
-- 
GitLab


From dfa079a2fdf525b06468329ad9dbf08d0c11e291 Mon Sep 17 00:00:00 2001
From: Niklas Krafczyk <niklas@uni-bremen.de>
Date: Tue, 23 May 2023 11:51:03 +0200
Subject: [PATCH 2/3] Splitting SolverInterface into stateless and stateful

---
 .../transformers/AbstractionTransformer.hpp   |   4 +-
 .../executables/sfsmMethod/sfsmMethod.cpp     |   4 +-
 ...ctedSfsmDistinguishingInputCalculation.cpp |   4 +-
 ...ctedSfsmDistinguishingInputCalculation.hpp |   4 +-
 .../checkers/ObservabilityChecker.cpp         |   2 +-
 .../checkers/ObservabilityChecker.hpp         |   6 +-
 .../checkers/RestrictednessChecker.cpp        |   6 +-
 .../checkers/TraceInclusionChecker.hpp        |   2 +-
 .../UnsatisfiableTransitionsChecker.cpp       |   2 +-
 .../UnsatisfiableTransitionsChecker.hpp       |   6 +-
 src/libsfsmtest/sfsm/SMTTools.cpp             | 231 +++++++-----------
 src/libsfsmtest/sfsm/SMTTools.hpp             |  93 +++++--
 src/libsfsmtest/sfsm/Sfsm.cpp                 |   2 +-
 src/libsfsmtest/sfsm/Sfsm.hpp                 |   4 +-
 src/libsfsmtest/sfsm/SfsmSolver.hpp           |   2 +-
 src/libsfsmtest/sfsm/State.cpp                |   2 +-
 src/libsfsmtest/sfsm/State.hpp                |   4 +-
 .../sfsm/TransitionRelationGenerator.cpp      |  14 +-
 .../sfsm/TransitionRelationGenerator.hpp      |   6 +-
 src/libsfsmtest/testgeneration/SfsmMethod.cpp |  32 +--
 src/libsfsmtest/testgeneration/SfsmMethod.hpp |   4 +-
 .../utils/algorithms/FindAllImplications.hpp  |   2 +-
 .../FindAllSatisfiableConjunctions.hpp        |   4 +-
 src/usage-demo/usage-demo.cpp                 |   4 +-
 24 files changed, 227 insertions(+), 217 deletions(-)

diff --git a/src/libsfsmtest/creators/transformers/AbstractionTransformer.hpp b/src/libsfsmtest/creators/transformers/AbstractionTransformer.hpp
index 6c43a88..29558b6 100644
--- a/src/libsfsmtest/creators/transformers/AbstractionTransformer.hpp
+++ b/src/libsfsmtest/creators/transformers/AbstractionTransformer.hpp
@@ -38,11 +38,11 @@ class AbstractionTransformer : public SfsmTransformer {
 protected:
     Expressions const abstractionExpressions;
     Expressions equivalenceClasses;
-    SolverInterface *solverInstance;
+    SolverServiceInterface *solverInstance;
 
 public:
 
-    AbstractionTransformer(Sfsm const *sfsmToTransform, Expressions const &paramAbstractionExpressions, SolverInterface *paramSolverInstance) :
+    AbstractionTransformer(Sfsm const *sfsmToTransform, Expressions const &paramAbstractionExpressions, SolverServiceInterface *paramSolverInstance) :
     SfsmTransformer(sfsmToTransform), abstractionExpressions(paramAbstractionExpressions), solverInstance(paramSolverInstance) {
         assert(not abstractionExpressions.empty());
         typedef std::pair<std::vector<ssize_t>, Expression> ConjunctionResult;
diff --git a/src/libsfsmtest/executables/sfsmMethod/sfsmMethod.cpp b/src/libsfsmtest/executables/sfsmMethod/sfsmMethod.cpp
index 4e21102..3013e23 100644
--- a/src/libsfsmtest/executables/sfsmMethod/sfsmMethod.cpp
+++ b/src/libsfsmtest/executables/sfsmMethod/sfsmMethod.cpp
@@ -42,7 +42,7 @@
 
 using namespace libfsmtest;
 
-static void printSfsmInfo(SFSMs::Sfsm *sfsm, SFSMs::SolverInterface *solver) {
+static void printSfsmInfo(SFSMs::Sfsm *sfsm, SFSMs::SolverServiceInterface *solver) {
     auto minimized = SFSMs::transformSfsm<SFSMs::MinimizedTransformer>(sfsm);
     std::cerr << "Reference model: ";
     std::cerr << (sfsm->isDeterministic() ? "deterministic" : "non-deterministic");
@@ -104,7 +104,7 @@ static void SfsmMethod(size_t additionalStates, std::string const &pathToCSV, st
         abstraction->accept(abstractionVisitor);
         abstractionVisitor.writeToFile();
     }
-    SFSMs::SolverInterface solver;
+    SFSMs::StatefulSolverService solver;
     auto result = SFSMs::sfsmMethod(*sfsm, additionalStates, props, &solver);
     //std::cout << "Test suite (size: " << result.size() << "):" << std::endl;
     for(auto const &trace : result) {
diff --git a/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.cpp b/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.cpp
index abfd8d9..67a9fc3 100644
--- a/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.cpp
+++ b/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.cpp
@@ -9,7 +9,7 @@
 
 namespace libfsmtest::SFSMs {
 
-static RestrictedSfsmDistinguishingInputCalculator::result_type calculateDistinguishingInputMap(Expressions const &guardConditions, Expressions const &outputExpressions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+static RestrictedSfsmDistinguishingInputCalculator::result_type calculateDistinguishingInputMap(Expressions const &guardConditions, Expressions const &outputExpressions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     std::vector<std::tuple<size_t, size_t, std::shared_future<SatisfyingValuationResult>>> resultPreparation;
     // Filter identifierDefinitions for outputs
     IdentifierDefinitions outputDefinitions;
@@ -146,7 +146,7 @@ static RestrictedSfsmDistinguishingInputCalculator::result_type calculateDisting
     return returnValue;
 }
 
-RestrictedSfsmDistinguishingInputCalculator::RestrictedSfsmDistinguishingInputCalculator(SolverInterface *paramSolverInstance)
+RestrictedSfsmDistinguishingInputCalculator::RestrictedSfsmDistinguishingInputCalculator(SolverServiceInterface *paramSolverInstance)
     : solverInstance(paramSolverInstance) { }
 
 RestrictedSfsmDistinguishingInputCalculator::result_type RestrictedSfsmDistinguishingInputCalculator::operator()(Sfsm const &sfsm) {
diff --git a/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.hpp b/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.hpp
index b2b8f70..90644bb 100644
--- a/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.hpp
+++ b/src/libsfsmtest/processing/RestrictedSfsmDistinguishingInputCalculation.hpp
@@ -33,9 +33,9 @@ class SolverInstance;
  */
 class RestrictedSfsmDistinguishingInputCalculator : public Processor<Sfsm, std::map<std::tuple<size_t, size_t>, Valuation>> {
 private:
-    SolverInterface *solverInstance;
+    SolverServiceInterface *solverInstance;
 public:
-    RestrictedSfsmDistinguishingInputCalculator(SolverInterface *solverInstance);
+    RestrictedSfsmDistinguishingInputCalculator(SolverServiceInterface *solverInstance);
     result_type operator()(Sfsm const &sfsm) override;
 };
 
diff --git a/src/libsfsmtest/processing/checkers/ObservabilityChecker.cpp b/src/libsfsmtest/processing/checkers/ObservabilityChecker.cpp
index 678c995..07c0b20 100644
--- a/src/libsfsmtest/processing/checkers/ObservabilityChecker.cpp
+++ b/src/libsfsmtest/processing/checkers/ObservabilityChecker.cpp
@@ -11,7 +11,7 @@
 
 namespace libfsmtest::SFSMs {
 
-ObservabilityChecker::ObservabilityChecker(SolverInterface *paramSolverInstance)
+ObservabilityChecker::ObservabilityChecker(SolverServiceInterface *paramSolverInstance)
     : solverInstance(paramSolverInstance) { }
 
 bool ObservabilityChecker::operator()(Sfsm const &sfsm) {
diff --git a/src/libsfsmtest/processing/checkers/ObservabilityChecker.hpp b/src/libsfsmtest/processing/checkers/ObservabilityChecker.hpp
index 2155f00..2722684 100644
--- a/src/libsfsmtest/processing/checkers/ObservabilityChecker.hpp
+++ b/src/libsfsmtest/processing/checkers/ObservabilityChecker.hpp
@@ -27,16 +27,16 @@
 #include "sfsm/State.hpp"
 
 namespace libfsmtest::SFSMs {
-class SolverInterface;
+class SolverServiceInterface;
 
 /**
  * A class checking an SFSM for transitions that can never be taken.
  */
 class ObservabilityChecker : public Processor<Sfsm, bool> {
 private:
-    SolverInterface *solverInstance;
+    SolverServiceInterface *solverInstance;
 public:
-    ObservabilityChecker(SolverInterface *solverInstance);
+    ObservabilityChecker(SolverServiceInterface *solverInstance);
     ~ObservabilityChecker() override = default;
 
     result_type operator()(Sfsm const &sfsm) override;
diff --git a/src/libsfsmtest/processing/checkers/RestrictednessChecker.cpp b/src/libsfsmtest/processing/checkers/RestrictednessChecker.cpp
index a9afcf9..21e5e39 100644
--- a/src/libsfsmtest/processing/checkers/RestrictednessChecker.cpp
+++ b/src/libsfsmtest/processing/checkers/RestrictednessChecker.cpp
@@ -16,7 +16,7 @@ namespace libfsmtest::SFSMs {
 RestrictednessChecker::RestrictednessChecker(Expressions const &atomicPropositions, SfsmSolver *paramSolverInstance)
  : APs(atomicPropositions), solverInstance(paramSolverInstance) { }
 
-bool inputSpacePartitioned(Expressions const &guardConditions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool inputSpacePartitioned(Expressions const &guardConditions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     auto notGuardConditions = makeLogicalNegation(makeLogicalDisjunction(guardConditions));
     if(isSatisfiable(makeLogicalConjunction(invariant, notGuardConditions), identifierDefinitions, solverInstance).has_value()) {
         std::cerr << "The guard conditions do not cover the whole input domain" << std::endl;
@@ -38,7 +38,7 @@ bool inputSpacePartitioned(Expressions const &guardConditions, Expression const
     return true;
 }
 
-bool alphabetsImplyAPs(Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &APs, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool alphabetsImplyAPs(Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &APs, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     std::vector<std::tuple<Expression, std::future<SatisfyingValuationResult>>> inOutResults;
     for(auto const &guardCondition : guardConditions) {
         for(auto const &outputExpression : outputExpressions) {
@@ -71,7 +71,7 @@ bool alphabetsImplyAPs(Expressions const &guardConditions, Expressions const &ou
     return true;
 }
 
-bool outputsDistinct(Expressions const &guardConditions, Expressions const &outputExpressions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool outputsDistinct(Expressions const &guardConditions, Expressions const &outputExpressions, Expression const &invariant, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     // Filter identifierDefinitions for outputs
     IdentifierDefinitions outputDefinitions;
     std::copy_if(identifierDefinitions.begin(), identifierDefinitions.end(), std::back_inserter(outputDefinitions), [](auto const &idDef) {
diff --git a/src/libsfsmtest/processing/checkers/TraceInclusionChecker.hpp b/src/libsfsmtest/processing/checkers/TraceInclusionChecker.hpp
index f4c4fe2..f774b0a 100644
--- a/src/libsfsmtest/processing/checkers/TraceInclusionChecker.hpp
+++ b/src/libsfsmtest/processing/checkers/TraceInclusionChecker.hpp
@@ -29,7 +29,7 @@
 #include "sfsm/State.hpp"
 
 namespace libfsmtest::SFSMs {
-class SolverInterface;
+class SolverServiceInterface;
 class SfsmSolver;
 
 /**
diff --git a/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.cpp b/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.cpp
index 91e501a..54fd5b4 100644
--- a/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.cpp
+++ b/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.cpp
@@ -29,7 +29,7 @@
 
 namespace libfsmtest::SFSMs {
 
-UnsatisfiableTransitionsChecker::UnsatisfiableTransitionsChecker(SolverInterface *paramSolverInstance)
+UnsatisfiableTransitionsChecker::UnsatisfiableTransitionsChecker(SolverServiceInterface *paramSolverInstance)
     : solverInstance(paramSolverInstance) { }
 
 UnsatisfiableTransitionsChecker::result_type
diff --git a/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.hpp b/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.hpp
index 61a370a..9f070ac 100644
--- a/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.hpp
+++ b/src/libsfsmtest/processing/checkers/UnsatisfiableTransitionsChecker.hpp
@@ -28,16 +28,16 @@ namespace libfsmtest::SFSMs {
 
 class Sfsm;
 class Transition;
-class SolverInterface;
+class SolverServiceInterface;
 
 /**
  * A class checking an SFSM for transitions that can never be taken.
  */
 class UnsatisfiableTransitionsChecker : public SfsmProcessor<std::vector<Transition const*>> {
 private:
-    SolverInterface *solverInstance;
+    SolverServiceInterface *solverInstance;
 public:
-    UnsatisfiableTransitionsChecker(SolverInterface *solverInstance);
+    UnsatisfiableTransitionsChecker(SolverServiceInterface *solverInstance);
     ~UnsatisfiableTransitionsChecker() override = default;
 
     result_type operator()(Sfsm const &sfsm) override;
diff --git a/src/libsfsmtest/sfsm/SMTTools.cpp b/src/libsfsmtest/sfsm/SMTTools.cpp
index 6a171d4..ab6330b 100644
--- a/src/libsfsmtest/sfsm/SMTTools.cpp
+++ b/src/libsfsmtest/sfsm/SMTTools.cpp
@@ -25,8 +25,14 @@
 
 namespace libfsmtest::SFSMs {
 
+static std::unique_ptr<StatefulSolverService> defaultSolver;
+
+SolverServiceInterface::SolverServiceInterface() = default;
+SolverServiceInterface::SolverServiceInterface(SolverServiceInterface &&) = default;
+SolverServiceInterface::~SolverServiceInterface() = default;
+
 #ifndef LIBSFSMTEST_PLATFORM_WINDOWS
-class SolverInterface::ProcessImpl {
+class StatefulSolverService::ProcessImpl {
 private:
     typedef std::decay_t<decltype(fork())> pid_t;
     typedef std::decay_t<decltype(open("", 0))> file_t;
@@ -189,29 +195,86 @@ public:
 };
 #endif
 
-SolverInterface::SolverInterface() : impl(new SolverInterface::ProcessImpl) { }
-SolverInterface::SolverInterface(SolverInterface &&other) 
+StatefulSolverService::SolverCleaner::SolverCleaner(StatefulSolverService *argSolver, bool argUsePushPop) : solver(argSolver), usePushPop(argUsePushPop) {
+    if(usePushPop) {
+        assert(solver != defaultSolver.get());
+        solver->callSolver("(push)", false);
+    }
+}
+StatefulSolverService::SolverCleaner::~SolverCleaner() {
+    if(solver != nullptr) {
+        if(usePushPop) {
+            assert(solver != defaultSolver.get());
+            solver->callSolver("(pop)", false);
+        } else {
+            assert(solver == defaultSolver.get());
+            solver->callSolver("(reset)", false);
+        }
+    }
+}
+StatefulSolverService::SolverCleaner::SolverCleaner(StatefulSolverService::SolverCleaner &&other) : solver(other.solver), usePushPop(other.usePushPop) {
+    other.solver = nullptr;
+}
+
+StatefulSolverService::StatefulSolverService() : impl(new StatefulSolverService::ProcessImpl) { }
+StatefulSolverService::StatefulSolverService(StatefulSolverService &&other) 
     : impl(std::move(other.impl)) {
     other.impl = nullptr;
 }
-SolverInterface::~SolverInterface() {
+StatefulSolverService::~StatefulSolverService() {
     delete this->impl;
 }
 
-SolverInterface &SolverInterface::operator=(SolverInterface &&other) {
+StatefulSolverService &StatefulSolverService::operator=(StatefulSolverService &&other) {
     this->impl = std::move(other.impl);
     other.impl = nullptr;
     return *this;
 }
 
-std::string SolverInterface::callSolver(std::string const &input, bool waitForOutput) {
+SolverServiceInterface &StatefulSolverService::operator=(SolverServiceInterface &&other) {
+    if(auto otherPtr = dynamic_cast<StatefulSolverService*>(&other);
+        otherPtr == nullptr) {
+        throw std::runtime_error("Move-assignment operator called with operand of different type");
+    } else {
+        return this->operator=(std::move(*otherPtr));
+    }
+}
+
+std::string StatefulSolverService::callSolver(std::string const &input, bool waitForOutput) {
     return this->impl->callSolver(input, waitForOutput);
 }
+QueryResult StatefulSolverService::callSolver(Expressions const &problem, Expressions const &queries) {
+    std::ostringstream solverInput;
+    for(auto const &expression : problem) {
+        solverInput << std::to_string(expression) << std::endl;
+    }
+    assert(problem.back() == makeFunctionCall({makeIdentifier("check-sat")}));
+
+    auto solverOutput = this->callSolver(solverInput.str(), true);
+    if(solverOutput.substr(0, 3) == "sat") {
+        std::unordered_map<Expression, Expression> result;
+        for(auto const &query : queries) {
+            Expressions queryResults = parseToExpressions(this->callSolver(std::to_string(query), true));
+            assert(queryResults.size() == 1);
+            result[query] = queryResults.front();
+        }
+        return result;
+    } else {
+        if(solverOutput.substr(0, 5) != "unsat") {
+            throw std::runtime_error("Solver returned neither `sat` nor `unsat`.\nSolver output: " + solverOutput);
+        }
+        return {};
+    }
+}
 
-bool SolverInterface::isRunning() const {
+bool StatefulSolverService::isRunning() const {
     return this->impl->processRunning();
 }
 
+StatefulSolverService::SolverCleaner StatefulSolverService::getCleaner(bool usePushPop) {
+    return StatefulSolverService::SolverCleaner(this, usePushPop);
+}
+
 Expression getSMTTypeExpression(IdentifierType::Type const &type) {
     class TypeToExpressionVisitor {
     public:
@@ -280,150 +343,32 @@ public:
     }
 };
 
-/*static Expression deduceAndGenerateLogicExpression(Expressions const &expressions*//*) {*/
-    // Are there integer functions?
-    // Are there real functions?
-    /*bool ints = std::any_of(identifierDefinitions.begin(), identifierDefinitions.end(), [](auto const &definition) {
-        auto const &[_, type] = definition;
-        return std::visit(SimpleTypeDetector<IdentifierType::SimpleBaseType::INTEGER>{}, type.getType());
-    });
-    bool reals = std::any_of(identifierDefinitions.begin(), identifierDefinitions.end(), [](auto const &definition) {
-        auto const &[_, type] = definition;
-        return std::visit(SimpleTypeDetector<IdentifierType::SimpleBaseType::REAL>{}, type.getType());
-    });
-    bool arrays = std::any_of(identifierDefinitions.begin(), identifierDefinitions.end(), [](auto const &definition) {
-        auto const &[_, type] = definition;
-        return std::visit(ComplexTypeDetector<IdentifierType::ComplexBaseType::ARRAY>{}, type.getType());
-    });*/
-    //std::string logic = "UFNIRA";
-    /*if (ints) {
-        if(reals) {
-            // ints and reals and (arrays or not arrays)
-            logic = "AUFNIRA";
-        } else {
-            if(arrays) {
-                // ints and not reals and arrays
-                logic = "AUFNIRA";
-            } else {
-                logic = "QF_UFNIA";
-            }
-        }
-    } else {
-        if(reals) {
-            if(arrays) {
-                // not ints and reals and arrays
-                logic = "AUFNIRA";
-            } else {
-                // not ints and reals and not arrays
-                logic = "QF_UFNRA";
-            }
-        } else {
-            if(arrays) {
-                // not ints and not reals and arrays
-                logic = "QF_AUFLIA";
-            } else {
-                // not ints and not reals and not arrays
-                logic = "QF_UF";
-            }
-        }
-    }*//*
-    return makeFunctionCall(makeIdentifier("set-logic"), {makeIdentifier(logic)});
-}*/
-static std::unique_ptr<SolverInterface> defaultSolver;
-
-template<typename Fn>
-class ScopeExitExecution {
-    Fn fn;
-public:
-    ScopeExitExecution(Fn &&paramFn) : fn(paramFn) { }
-    ScopeExitExecution(ScopeExitExecution const &) = delete;
-    ScopeExitExecution(ScopeExitExecution &&) = default;
-    ~ScopeExitExecution() {
-        fn();
-    }
-};
 
-class SolverCleanup {
-private:
-    SolverInterface *solver;
-    bool usePushPop;
-public:
-    SolverCleanup(SolverInterface *argSolver, bool argUsePushPop) : solver(argSolver), usePushPop(argUsePushPop) {
-        if(usePushPop) {
-            assert(solver != defaultSolver.get());
-            solver->callSolver("(push)", false);
-        }
-    }
-    ~SolverCleanup() = default;
-    void operator()() {
-        if(usePushPop) {
-            assert(solver != defaultSolver.get());
-            solver->callSolver("(pop)", false);
-        } else {
-            assert(solver == defaultSolver.get());
-            solver->callSolver("(reset)", false);
-        }
-    }
-};
-
-static std::pair<SolverInterface*, ScopeExitExecution<SolverCleanup>> setupSolverOrUseExisting(SolverInterface *solverInstance) {
+static std::pair<SolverServiceInterface*, StatefulSolverService::SolverCleaner> setupSolverOrUseExisting(SolverServiceInterface *solverInstance) {
     if(solverInstance == nullptr) {
         if(defaultSolver == nullptr) {
-            defaultSolver = std::make_unique<SolverInterface>();
+            defaultSolver = std::make_unique<StatefulSolverService>();
         }
+
         assert(defaultSolver != nullptr);
-        return {defaultSolver.get(), SolverCleanup(defaultSolver.get(), false)};
+        return {defaultSolver.get(), defaultSolver->getCleaner(false)};
     }
-    assert(solverInstance != nullptr);
-    return {solverInstance, SolverCleanup(solverInstance, true)};
-}
-
-static std::string checkSatAndQueryOnSat(std::string const &input, std::vector<std::string> const &queries, SolverInterface *solverInstance) {
-    auto [solver, popExec] = setupSolverOrUseExisting(solverInstance);
-    assert(solver == solverInstance or solver == defaultSolver.get());
-    solver->callSolver(input, false);
-    auto response = solver->callSolver("(check-sat)", true);
-    if(response.substr(0,3) == "sat") {
-        for(auto const &query : queries) {
-            response += solver->callSolver(query, true);
-        }
-    } else if(response.substr(0,5) != "unsat") {
-        throw std::runtime_error(std::string("Unexpected output from SMT solver: ") + response + "\nReferring to this problem:\n" + input + "\n");
+    if(auto statefulService = dynamic_cast<StatefulSolverService*>(solverInstance);
+        statefulService != nullptr) {
+        return {solverInstance, statefulService->getCleaner(true)};
+    } else {
+        return {solverInstance, StatefulSolverService::SolverCleaner(nullptr, false)};
     }
-    return response;
 }
 
-std::optional<std::unordered_map<Expression, Expression>> isSatisfiable(Expressions const &expressions, Expressions const &queries, SolverInterface *solverInstance) {
-    //auto logicExpression = deduceAndGenerateLogicExpression(expressions);
-
-    std::ostringstream output;
-    std::vector<std::string> queryList;
-    //output << std::to_string(logicExpression) << std::endl;
-    for(auto const &expression : expressions) {
-        output << std::to_string(expression) << std::endl;
-    }
-    for(auto const &query : queries) {
-        queryList.push_back(std::to_string(query));
-    }
-
-    auto solverOutput = checkSatAndQueryOnSat(output.str(), queryList, solverInstance);
-    if(solverOutput.substr(0, 3) == "sat") {
-        std::unordered_map<Expression, Expression> result;
-        Expressions queryResults = parseToExpressions(solverOutput.substr(3));
-        assert(queryResults.size() == queryList.size());
-        for(size_t index = 0; index < queryList.size(); ++index) {
-            result[queries.at(index)] = queryResults.at(index);
-        }
-        return result;
-    } else {
-        if(solverOutput.substr(0, 5) != "unsat") {
-            throw std::runtime_error("Solver returned neither `sat` nor `unsat`.\nSolver output: " + solverOutput);
-        }
-        return {};
-    }
+std::optional<std::unordered_map<Expression, Expression>> isSatisfiable(Expressions const &expressions, Expressions const &queries, SolverServiceInterface *solverInstance) {
+    Expressions problem(expressions);
+    problem.push_back(makeFunctionCall({makeIdentifier("check-sat")}));
+    auto [solver, cleaner] = setupSolverOrUseExisting(solverInstance);
+    return solver->callSolver(problem, queries);
 }
 
-std::optional<IdentifierValuations> isSatisfiable(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+std::optional<IdentifierValuations> isSatisfiable(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     auto getModelCall = makeFunctionCall({makeIdentifier("get-model")});
     std::vector<Expression> problemStatements;
     std::transform(identifierDefinitions.cbegin(), identifierDefinitions.cend(), std::back_inserter(problemStatements), [](auto const &identifierDefinition) {
@@ -553,17 +498,17 @@ Expression makeFunctionDeclaration(IdentifierDefinition const &functionDefinitio
     return makeFunctionCall(makeIdentifier("declare-fun"), resultPrep);
 }
 
-bool areEquivalent(Expression const &exp1, Expression const &exp2, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool areEquivalent(Expression const &exp1, Expression const &exp2, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     auto assertion = makeComparisonInequality(exp1, exp2);
     return not isSatisfiable(assertion, identifierDefinitions, solverInstance).has_value();
 }
 
-bool isImplication(Expression const &antecedent, Expression const &consequent, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool isImplication(Expression const &antecedent, Expression const &consequent, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     auto assertion = makeLogicalConjunction(antecedent, makeLogicalNegation(consequent));
     return not isSatisfiable(assertion, identifierDefinitions, solverInstance).has_value();
 }
 
-bool isAlwaysTrue(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance) {
+bool isAlwaysTrue(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance) {
     return not isSatisfiable(makeLogicalNegation(expression), identifierDefinitions, solverInstance);
 }
 
diff --git a/src/libsfsmtest/sfsm/SMTTools.hpp b/src/libsfsmtest/sfsm/SMTTools.hpp
index 87e36f3..1e2a2cc 100644
--- a/src/libsfsmtest/sfsm/SMTTools.hpp
+++ b/src/libsfsmtest/sfsm/SMTTools.hpp
@@ -33,11 +33,37 @@ namespace libfsmtest::SFSMs {
 typedef std::optional<IdentifierValuations> SatisfyingValuationResult;
 typedef std::optional<std::unordered_map<Expression, Expression>> QueryResult;
 
-class SolverInterface;
+/**
+ * An interface to a non-interactive solver service.
+ * 
+ * The contract is as follows: The client sends a problem and a set of queries
+ * to the service. The problem and the set of queries consists of s-expressions
+ * that can be interpreted by an SMT solver.  The last s-expression of the
+ * problem is `(check-sat)`. The solver service feeds this problem to an SMT
+ * solver. If the SMT solver returns "sat", the set of queries is applied.
+ * The service returns a `QueryResult` object that is equal to `std::nullopt`
+ * if the SMT solver returned something else than `sat` in response to the
+ * problem. Otherwise, if the SMT solver returned `sat`, the `QueryResult`
+ * object contains a map from query expressions to solver responses.
+ */
+class SolverServiceInterface {
+public:
+    SolverServiceInterface();
+    SolverServiceInterface(SolverServiceInterface const &) = delete;
+    SolverServiceInterface(SolverServiceInterface &&);
+    virtual ~SolverServiceInterface();
+
+    SolverServiceInterface &operator=(SolverServiceInterface const&) = delete;
+    virtual SolverServiceInterface &operator=(SolverServiceInterface &&) = 0;
+
+    virtual QueryResult callSolver(Expressions const &problem, Expressions const &queries) = 0;
+
+    virtual bool isRunning() const = 0;
+};
 
-[[nodiscard]] QueryResult isSatisfiable(Expressions const &expressions, Expressions const &queries /*= {}*/, SolverInterface *solverInstance);
+[[nodiscard]] QueryResult isSatisfiable(Expressions const &expressions, Expressions const &queries /*= {}*/, SolverServiceInterface *solverInstance);
 //[[nodiscard]] std::future<QueryResult> asyncIsSatisfiable(Expressions const &expressions, Expressions const &queries = {});
-[[nodiscard]] SatisfyingValuationResult isSatisfiable(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance);
+[[nodiscard]] SatisfyingValuationResult isSatisfiable(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance);
 //[[nodiscard]] std::future<SatisfyingValuationResult> asyncIsSatisfiable(Expression const &expression, IdentifierDefinitions const &identifierDefinitions);
 
 [[nodiscard]] Expression makeIdentifierDefinition(IdentifierDefinition const &id);
@@ -47,29 +73,68 @@ class SolverInterface;
 [[nodiscard]] Expression makeUniversallyQuantifiedFormula(IdentifierDefinitions const &quantifiedIdentifiers, Expression const &content);
 
 // Convenience functions for common checks
-[[nodiscard]] bool areEquivalent(Expression const &exp1, Expression const &exp2, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance);
-[[nodiscard]] bool isImplication(Expression const &antecedent, Expression const &consequent, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance);
-[[nodiscard]] bool isAlwaysTrue(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverInterface *solverInstance);
+[[nodiscard]] bool areEquivalent(Expression const &exp1, Expression const &exp2, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance);
+[[nodiscard]] bool isImplication(Expression const &antecedent, Expression const &consequent, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance);
+[[nodiscard]] bool isAlwaysTrue(Expression const &expression, IdentifierDefinitions const &identifierDefinitions, SolverServiceInterface *solverInstance);
 
 Expression getSMTTypeExpression(IdentifierType const &type);
 
-class SolverInterface {
+class StatefulSolverService : public SolverServiceInterface {
 private:
     class ProcessImpl;
 private:
     ProcessImpl *impl;
 public:
-    SolverInterface();
-    SolverInterface(SolverInterface const&) = delete;
-    SolverInterface(SolverInterface &&);
-    ~SolverInterface();
+    class SolverCleaner;
+public:
+    StatefulSolverService();
+    StatefulSolverService(StatefulSolverService const&) = delete;
+    StatefulSolverService(StatefulSolverService &&);
+    ~StatefulSolverService() override;
 
-    SolverInterface &operator=(SolverInterface const&) = delete;
-    SolverInterface &operator=(SolverInterface &&);
+    StatefulSolverService &operator=(StatefulSolverService const&) = delete;
+    StatefulSolverService &operator=(StatefulSolverService &&);
+    SolverServiceInterface &operator=(SolverServiceInterface &&) override;
 
     std::string callSolver(std::string const &input, bool waitForOutput);
+    QueryResult callSolver(Expressions const &problem, Expressions const &queries) override;
+
+    bool isRunning() const override;
+
+    SolverCleaner getCleaner(bool usePushPop);
+};
+
+class StatefulSolverService::SolverCleaner {
+private:
+    StatefulSolverService * solver;
+    bool usePushPop;
+public:
+    SolverCleaner(StatefulSolverService */*solver*/, bool /*usePushPop*/);
+    SolverCleaner(StatefulSolverService::SolverCleaner const &) = delete;
+    SolverCleaner(StatefulSolverService::SolverCleaner &&/*other*/);
+    ~SolverCleaner();
+};
+
+class StatelessSolverService : public SolverServiceInterface {
+private:
+    class ProcessImpl;
+private:
+    ProcessImpl *impl;
+protected:
+    std::string callSolver(std::string const &input);
+public:
+    StatelessSolverService();
+    StatelessSolverService(StatelessSolverService const&) = delete;
+    StatelessSolverService(StatelessSolverService &&);
+    ~StatelessSolverService() override;
+
+    StatelessSolverService &operator=(StatelessSolverService const&) = delete;
+    StatelessSolverService &operator=(StatelessSolverService &&);
+    SolverServiceInterface &operator=(SolverServiceInterface &&) override;
+
+    QueryResult callSolver(Expressions const &problem, Expressions const &queries) override;
 
-    bool isRunning() const;
+    bool isRunning() const override;
 };
 
 }
diff --git a/src/libsfsmtest/sfsm/Sfsm.cpp b/src/libsfsmtest/sfsm/Sfsm.cpp
index d59b33d..0dc9ac5 100644
--- a/src/libsfsmtest/sfsm/Sfsm.cpp
+++ b/src/libsfsmtest/sfsm/Sfsm.cpp
@@ -79,7 +79,7 @@ bool Sfsm::isDeterministic() const {
     });
 }
 
-bool Sfsm::isCompletelySpecified(SolverInterface *solverInstance) const {
+bool Sfsm::isCompletelySpecified(SolverServiceInterface *solverInstance) const {
     return std::all_of(states.begin(), states.end(), [&identifiers=this->identifiers, &invariant=this->invariant, &guardConditions=this->inputAlphabet, &solverInstance](const auto& s){
         return s.isCompletelySpecified(identifiers, invariant, guardConditions, solverInstance);
     });
diff --git a/src/libsfsmtest/sfsm/Sfsm.hpp b/src/libsfsmtest/sfsm/Sfsm.hpp
index 4296fef..6297227 100644
--- a/src/libsfsmtest/sfsm/Sfsm.hpp
+++ b/src/libsfsmtest/sfsm/Sfsm.hpp
@@ -41,7 +41,7 @@ typedef std::vector<libfsmtest::SFSMs::Expression> SymbolicOutputTrace;
 typedef std::vector<Valuation> ConcreteTrace;
 
 class SfsmVisitor;
-class SolverInterface;
+class SolverServiceInterface;
 class SfsmSolver;
 
 /**
@@ -97,7 +97,7 @@ public:
     
     [[nodiscard]] bool isDeterministic() const;
     
-    [[nodiscard]] bool isCompletelySpecified(SolverInterface *solverInstance) const;
+    [[nodiscard]] bool isCompletelySpecified(SolverServiceInterface *solverInstance) const;
     
     /**
      * The size of an FSM is the number of its states.
diff --git a/src/libsfsmtest/sfsm/SfsmSolver.hpp b/src/libsfsmtest/sfsm/SfsmSolver.hpp
index ad817ed..80ab2d2 100644
--- a/src/libsfsmtest/sfsm/SfsmSolver.hpp
+++ b/src/libsfsmtest/sfsm/SfsmSolver.hpp
@@ -30,7 +30,7 @@
 
 namespace libfsmtest::SFSMs {
 
-class SfsmSolver : public SolverInterface {
+class SfsmSolver : public StatefulSolverService {
 private:
     Sfsm const &sfsm;
     Expression const transitionRelationDefinition;
diff --git a/src/libsfsmtest/sfsm/State.cpp b/src/libsfsmtest/sfsm/State.cpp
index bef6e50..67fcfdf 100644
--- a/src/libsfsmtest/sfsm/State.cpp
+++ b/src/libsfsmtest/sfsm/State.cpp
@@ -62,7 +62,7 @@ bool State::isDeterministic() const {
 }
 
 
-bool State::isCompletelySpecified(IdentifierDefinitions const &identifiers, Expression const &invariant, std::vector<Sfsm::GuardCondition_t> const &guardConditions, SolverInterface *solverInstance) const {
+bool State::isCompletelySpecified(IdentifierDefinitions const &identifiers, Expression const &invariant, std::vector<Sfsm::GuardCondition_t> const &guardConditions, SolverServiceInterface *solverInstance) const {
     vector<Expression> inputs;
     std::transform(transitions.cbegin(), transitions.cend(), std::back_inserter(inputs), [&guardConditions](auto const &tr) {
         return guardConditions.at(tr.getInputId());
diff --git a/src/libsfsmtest/sfsm/State.hpp b/src/libsfsmtest/sfsm/State.hpp
index d134bc9..e82ce6d 100644
--- a/src/libsfsmtest/sfsm/State.hpp
+++ b/src/libsfsmtest/sfsm/State.hpp
@@ -33,7 +33,7 @@
 
 namespace libfsmtest::SFSMs {
 class SfsmVisitor;
-class SolverInterface;
+class SolverServiceInterface;
 
 /**
  * Class representing FSM states
@@ -83,7 +83,7 @@ public:
      *  IDs in this state's transitions refer to.
      * @note Events of the input alphabet are internally numbered by 0..lastInputId
      */
-    [[nodiscard]] bool isCompletelySpecified(IdentifierDefinitions const &identifiers, Expression const &invariant, Expressions const &guardConditions, SolverInterface *solverInstance) const;
+    [[nodiscard]] bool isCompletelySpecified(IdentifierDefinitions const &identifiers, Expression const &invariant, Expressions const &guardConditions, SolverServiceInterface *solverInstance) const;
     
     /**
      * Return true if the transitions of this state are
diff --git a/src/libsfsmtest/sfsm/TransitionRelationGenerator.cpp b/src/libsfsmtest/sfsm/TransitionRelationGenerator.cpp
index 02b2d81..4f9044f 100644
--- a/src/libsfsmtest/sfsm/TransitionRelationGenerator.cpp
+++ b/src/libsfsmtest/sfsm/TransitionRelationGenerator.cpp
@@ -100,7 +100,7 @@ Expression generateTransitionRelationForTransition(IdentifierDefinitions const &
     return generateTransitionExpression(transition.getSourceId(), guardCondition, outputExpression, transition.getTargetId());
 }
 
-Expressions generateAbstractTransitionRelationsForTransition(IdentifierDefinitions const &definitions, Transition const &transition, Expression const &invariant, Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &propositionEquivalenceClasses, SolverInterface *solverInstance) {
+Expressions generateAbstractTransitionRelationsForTransition(IdentifierDefinitions const &definitions, Transition const &transition, Expression const &invariant, Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &propositionEquivalenceClasses, SolverServiceInterface *solverInstance) {
     checkIdentifierNameValidity(definitions);
     Expressions abstractTransitionExpressions;
 
@@ -116,7 +116,7 @@ Expressions generateAbstractTransitionRelationsForTransition(IdentifierDefinitio
     return abstractTransitionExpressions;
 }
 
-Expression generateTransitionRelationForState(IdentifierDefinitions const &definitions, State const &state, Expressions const &guardConditions, Expressions const &outputExpressions, SolverInterface *solverInstance) {
+Expression generateTransitionRelationForState(IdentifierDefinitions const &definitions, State const &state, Expressions const &guardConditions, Expressions const &outputExpressions, SolverServiceInterface *solverInstance) {
     Expressions relsForTransitions;
     Expressions guardConditionsInState;
     auto const &transitions = state.getTransitions();
@@ -140,7 +140,7 @@ Expression generateTransitionRelationForState(IdentifierDefinitions const &defin
     return makeLogicalDisjunction(relsForTransitions);
 }
 
-Expression generateAbstractTransitionRelationForState(IdentifierDefinitions const &definitions, State const &state, Expression const &invariant, Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &propositionEquivalenceClasses, SolverInterface *solverInstance) {
+Expression generateAbstractTransitionRelationForState(IdentifierDefinitions const &definitions, State const &state, Expression const &invariant, Expressions const &guardConditions, Expressions const &outputExpressions, Expressions const &propositionEquivalenceClasses, SolverServiceInterface *solverInstance) {
     Expressions relsForTransitions;
     Expressions guardConditionsInState;
     auto const &transitions = state.getTransitions();
@@ -162,7 +162,7 @@ Expression generateAbstractTransitionRelationForState(IdentifierDefinitions cons
     return makeLogicalDisjunction(relsForTransitions);
 }
 
-Expression generateTransitionRelationForSfsm(Sfsm const &sfsm, SolverInterface *solverInstance) {
+Expression generateTransitionRelationForSfsm(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     Expressions relsForStates;
     IdentifierDefinitions const &definitions = sfsm.getIdentifierDefinitions();
     auto const &states = sfsm.getStates();
@@ -174,7 +174,7 @@ Expression generateTransitionRelationForSfsm(Sfsm const &sfsm, SolverInterface *
     return makeLogicalConjunction(makeLogicalDisjunction(relsForStates), sfsm.getInvariant());
 }
 
-Expression generateAbstractTransitionRelationForSfsm(Sfsm const &sfsm, Expressions const &propositionEquivalenceClasses, SolverInterface *solverInstance) {
+Expression generateAbstractTransitionRelationForSfsm(Sfsm const &sfsm, Expressions const &propositionEquivalenceClasses, SolverServiceInterface *solverInstance) {
     Expressions relsForStates;
     IdentifierDefinitions const &definitions = sfsm.getIdentifierDefinitions();
     auto const &states = sfsm.getStates();
@@ -200,7 +200,7 @@ Expression generateTransitionRelationCall(Sfsm const &sfsm, Expressions const &a
     return makeFunctionCall(makeIdentifier(TRANSITION_RELATION_IDENTIFIER), arguments);
 }
 
-Expression generateTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, SolverInterface *solverInstance) {
+Expression generateTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     auto const relation = generateTransitionRelationForSfsm(sfsm, solverInstance);
     IdentifierDefinitions parameters = {
         {PRE_STATE_IDENTIFIER,
@@ -223,7 +223,7 @@ Expression generateTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, SolverI
     {IdentifierType::SimpleType(IdentifierType::SimpleBaseType::BOOLEAN), IdentifierType::LocationInModel::OTHER}, parameters, relation);
 }
 
-Expression generateAbstractTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, Expressions const &propositionEquivalenceClasses, SolverInterface *solverInstance) {
+Expression generateAbstractTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, Expressions const &propositionEquivalenceClasses, SolverServiceInterface *solverInstance) {
     auto const relation = generateAbstractTransitionRelationForSfsm(sfsm, propositionEquivalenceClasses, solverInstance);
     IdentifierDefinitions parameters = {
         {PRE_STATE_IDENTIFIER,
diff --git a/src/libsfsmtest/sfsm/TransitionRelationGenerator.hpp b/src/libsfsmtest/sfsm/TransitionRelationGenerator.hpp
index 3ad41ae..3c4fbf6 100644
--- a/src/libsfsmtest/sfsm/TransitionRelationGenerator.hpp
+++ b/src/libsfsmtest/sfsm/TransitionRelationGenerator.hpp
@@ -35,12 +35,12 @@
 namespace libfsmtest::SFSMs {
 class Transition;
 class State;
-class SolverInterface;
+class SolverServiceInterface;
 
 Expression generateTransitionRelationForTransition(IdentifierDefinitions const &definitions, Transition const &transition);
 Expression generateTransitionRelationForState(IdentifierDefinitions const &definitions, State const &state);
-Expression generateTransitionRelationForSfsm(Sfsm const &sfsm, SolverInterface *solverInstance);
-Expression generateTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, SolverInterface *solverInstance);
+Expression generateTransitionRelationForSfsm(Sfsm const &sfsm, SolverServiceInterface *solverInstance);
+Expression generateTransitionRelationDefinitionForSfsm(Sfsm const &sfsm, SolverServiceInterface *solverInstance);
 
 // Expects arguments for the transition relation, where each argument
 // corresponds to one identifier in the SFSM. They are expected in the order
diff --git a/src/libsfsmtest/testgeneration/SfsmMethod.cpp b/src/libsfsmtest/testgeneration/SfsmMethod.cpp
index 1fd6a9d..3ce1ec3 100644
--- a/src/libsfsmtest/testgeneration/SfsmMethod.cpp
+++ b/src/libsfsmtest/testgeneration/SfsmMethod.cpp
@@ -218,7 +218,7 @@ private:
 public:
     MemoAbstractionDistinguishingTraceGenerator(Sfsm const &paramSfsm,
                                             Expressions const &paramPropositions,
-                                            SolverInterface *solverInstance)
+                                            SolverServiceInterface *solverInstance)
         : sfsm(*transformSfsm<AbstractionTransformer>(&paramSfsm, paramPropositions, solverInstance).release()),
           targets(sfsm) { }
 
@@ -265,7 +265,7 @@ public:
     }
 };
 
-std::vector<Index> satisfiableGuardConditions(Sfsm const &sfsm, SolverInterface *solverInstance) {
+std::vector<Index> satisfiableGuardConditions(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     std::vector<Index> result;
     auto const &guardConditions = sfsm.getGuardConditions();
     for(size_t index = 0; index < guardConditions.size(); ++index) {
@@ -276,7 +276,7 @@ std::vector<Index> satisfiableGuardConditions(Sfsm const &sfsm, SolverInterface
     return result;
 }
 
-std::vector<Index> reachableStates(Sfsm const &sfsm, SolverInterface *solverInstance) {
+std::vector<Index> reachableStates(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     std::vector<Index> reachedStates(1, sfsm.getInitialStateId());
     std::vector<Index> guardConditions = satisfiableGuardConditions(sfsm, solverInstance);
     return fixpointIteration(reachedStates, [&guardConditions,&sfsm](auto const &states) {
@@ -350,7 +350,7 @@ std::vector<std::pair<std::vector<ssize_t>, Expression>> pickHittingSetForInputE
     return result;
 }
 
-std::vector<ConcreteTrace> translateSymbolicTracesToConcreteTracesByEquivalenceClasses(Sfsm const &sfsm, std::vector<SymbolicInputTrace> const &symbolicTraces, SolverInterface *solverInstance) {
+std::vector<ConcreteTrace> translateSymbolicTracesToConcreteTracesByEquivalenceClasses(Sfsm const &sfsm, std::vector<SymbolicInputTrace> const &symbolicTraces, SolverServiceInterface *solverInstance) {
     auto const &identifierDefinitions = sfsm.getIdentifierDefinitions();
     auto const &invariant = sfsm.getInvariant();
     auto const guardConditions = sfsm.getGuardConditions();
@@ -416,7 +416,7 @@ static void eraseEverySecondElement(Container &c) {
     }
 }
 
-Valuation translateSymbolToValuation(IdentifierDefinitions const &definitions, Expression const &symbol, std::vector<Expression> forbiddenValuations, SolverInterface *solverInstance) {
+Valuation translateSymbolToValuation(IdentifierDefinitions const &definitions, Expression const &symbol, std::vector<Expression> forbiddenValuations, SolverServiceInterface *solverInstance) {
     SatisfyingValuationResult result;
     while(not result.has_value()) {
         result = isSatisfiable(makeLogicalConjunction(symbol, makeLogicalConjunction(makeLogicalNegation(forbiddenValuations))), definitions, solverInstance);
@@ -442,7 +442,7 @@ std::vector<ConcreteTrace> toInputTraces(Sfsm const &sfsm, std::vector<ConcreteT
     return result;
 }
 
-ConcreteTrace translateSymbolicTraceToConcreteTraceWithPreferrablyUniqueValuations(Sfsm const &sfsm, std::set<Valuation> const &forbiddenValuations, SymbolicInputTrace const &symbolicTrace, SolverInterface *solverInstance) {
+ConcreteTrace translateSymbolicTraceToConcreteTraceWithPreferrablyUniqueValuations(Sfsm const &sfsm, std::set<Valuation> const &forbiddenValuations, SymbolicInputTrace const &symbolicTrace, SolverServiceInterface *solverInstance) {
     auto const &invariant = sfsm.getInvariant();
     auto const &identifierDefinitions = sfsm.getIdentifierDefinitions();
     std::vector<Expression> forbiddenValuationExpressions;
@@ -457,7 +457,7 @@ ConcreteTrace translateSymbolicTraceToConcreteTraceWithPreferrablyUniqueValuatio
     return result;
 }
 
-std::vector<SymbolicTrace> translateConcreteTraceToSymbolicTraces(Sfsm const &sfsm, Index const &startState, ConcreteTrace const &trace, SolverInterface *solverInstance) {
+std::vector<SymbolicTrace> translateConcreteTraceToSymbolicTraces(Sfsm const &sfsm, Index const &startState, ConcreteTrace const &trace, SolverServiceInterface *solverInstance) {
     std::vector<std::pair<Index, SymbolicTrace>> worklist;
     std::vector<std::pair<Index, SymbolicTrace>> nextWorklist;
     worklist.emplace_back(startState, SymbolicTrace{});
@@ -525,7 +525,7 @@ std::vector<ConcreteTrace> crossConcatenateConcreteTraceSets(std::vector<Concret
     return result;
 }
 
-std::vector<ConcreteTrace> generateStateCover(Sfsm const &sfsm, std::vector<Index> const &statesToCover, SolverInterface *solverInstance) {
+std::vector<ConcreteTrace> generateStateCover(Sfsm const &sfsm, std::vector<Index> const &statesToCover, SolverServiceInterface *solverInstance) {
     auto const symbolicStateCover = getSymbolicStateCoverForStates(sfsm, statesToCover);
     return toInputTraces(sfsm, translateSymbolicTracesToConcreteTracesByEquivalenceClasses(sfsm, symbolicStateCover, solverInstance));
 }
@@ -560,7 +560,7 @@ std::vector<ConcreteTrace> generateDiscoveryTraces(Sfsm const &sfsm, std::vector
     return toInputTraces(sfsm, result);
 }
 
-std::vector<ConcreteTrace> generatePartOne(Sfsm const &sfsm, std::vector<Index> const &statesToCover, SolverInterface *solverInstance) {
+std::vector<ConcreteTrace> generatePartOne(Sfsm const &sfsm, std::vector<Index> const &statesToCover, SolverServiceInterface *solverInstance) {
     auto stateCover = generateStateCover(sfsm, statesToCover /* = reachableStates(sfsm) */, solverInstance);
     if(auto const envVarPtr = getenv("LIBSFSMTEST_TEST_SUITE_TEX");
         envVarPtr != nullptr) {
@@ -717,7 +717,7 @@ std::vector<ConcreteTrace> generatePartTwo(Sfsm const &sfsm, std::vector<Index>
     output << "}";
 }
 
-std::vector<ConjunctionResult> getSfsmEquivalenceClasses(Sfsm const &sfsm, Expressions const &propositions, SolverInterface *solverInstance) {
+std::vector<ConjunctionResult> getSfsmEquivalenceClasses(Sfsm const &sfsm, Expressions const &propositions, SolverServiceInterface *solverInstance) {
     auto const &identifierDefinitions = sfsm.getIdentifierDefinitions();
     auto const &invariant = sfsm.getInvariant();
     auto const &guardConditions = sfsm.getUsedGuardConditions();
@@ -743,7 +743,7 @@ Expressions getExpressionsFromConjunctionResults(std::vector<ConjunctionResult>
     return result;
 }
 
-std::vector<ConcreteTrace> generatePartThree(Sfsm const &sfsm, std::vector<Index> const &statesToCover, size_t stateDifference, Expressions const &propositions, SolverInterface *solverInstance) {
+std::vector<ConcreteTrace> generatePartThree(Sfsm const &sfsm, std::vector<Index> const &statesToCover, size_t stateDifference, Expressions const &propositions, SolverServiceInterface *solverInstance) {
     std::vector<ConjunctionResult> const equivalenceClasses 
         = getSfsmEquivalenceClasses(sfsm, propositions, solverInstance);
     auto const &identifierDefinitions = sfsm.getIdentifierDefinitions();
@@ -790,7 +790,7 @@ std::vector<ConcreteTrace> generatePartFour(Sfsm const &sfsm, std::vector<Index>
     std::unique_ptr<MemoizingSfsmSolver> abstSfsmSolver;
     std::unique_ptr<Sfsm> abstSfsm;
     if(abstract) {
-        abstSfsm = transformSfsm<AbstractionTransformer>(&sfsm, propositions, static_cast<SolverInterface*>(solverInstance));
+        abstSfsm = transformSfsm<AbstractionTransformer>(&sfsm, propositions, static_cast<SolverServiceInterface*>(solverInstance));
         abstSfsmSolver = std::make_unique<MemoizingSfsmSolver>(sfsm);
     }
     std::cerr << "Calculating the first part of the final test suite..." << std::endl;
@@ -951,7 +951,7 @@ std::vector<ConcreteTrace> generatePartFive(Sfsm const &sfsm, std::vector<Index>
     std::unique_ptr<MemoizingSfsmSolver> abstSfsmSolver;
     std::unique_ptr<Sfsm> abstSfsm;
     if(abstract) {
-        abstSfsm = transformSfsm<AbstractionTransformer>(&sfsm, propositions, static_cast<SolverInterface*>(solverInstance));
+        abstSfsm = transformSfsm<AbstractionTransformer>(&sfsm, propositions, static_cast<SolverServiceInterface*>(solverInstance));
         abstSfsmSolver = std::make_unique<MemoizingSfsmSolver>(sfsm);
     }
     std::cerr << "Calculating the second part of the final test suite..." << std::endl;
@@ -1127,7 +1127,7 @@ void filterPrefixes(IIter1 begin, IIter2 &&end, OIter &&out) {
     }
 }
 
-Sfsm removeInfeasibleTransitions(Sfsm const &sfsm, SolverInterface *solverInstance) {
+Sfsm removeInfeasibleTransitions(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     if(auto const unsatisfiableTransitions = applyProcessor<UnsatisfiableTransitionsChecker>(sfsm, solverInstance);
         not unsatisfiableTransitions.empty()) {
         std::cerr << "Warning: Found infeasible transitions:" << std::endl;
@@ -1274,7 +1274,7 @@ Sfsm removeInfeasibleTransitions(Sfsm const &sfsm, SolverInterface *solverInstan
     return sfsm;
 }
 
-Sfsm preprocessSfsm(Sfsm const &sfsm, SolverInterface *solverInstance) {
+Sfsm preprocessSfsm(Sfsm const &sfsm, SolverServiceInterface *solverInstance) {
     auto feasibleSfsm = removeInfeasibleTransitions(sfsm, solverInstance);
     return *transformSfsm<MinimizedTransformer>(&feasibleSfsm);
 }
@@ -1292,7 +1292,7 @@ std::vector<ConcreteTrace> calculateProtoWMethod(std::vector<ConcreteTrace> cons
     return prefixFreeWMethodTestSuite;
 }
 
-std::vector<ConcreteTrace> sfsmMethod(Sfsm const &sfsm, size_t stateDifference, Expressions const &propositions, SolverInterface *solverInstance) {
+std::vector<ConcreteTrace> sfsmMethod(Sfsm const &sfsm, size_t stateDifference, Expressions const &propositions, SolverServiceInterface *solverInstance) {
     Sfsm preprocessedSfsm = preprocessSfsm(sfsm, solverInstance);
     MemoizingSfsmSolver sfsmSolver(preprocessedSfsm);
     auto const statesToCover = reachableStates(preprocessedSfsm, solverInstance);
diff --git a/src/libsfsmtest/testgeneration/SfsmMethod.hpp b/src/libsfsmtest/testgeneration/SfsmMethod.hpp
index 922ace7..a1feb78 100644
--- a/src/libsfsmtest/testgeneration/SfsmMethod.hpp
+++ b/src/libsfsmtest/testgeneration/SfsmMethod.hpp
@@ -28,9 +28,9 @@
 
 namespace libfsmtest::SFSMs {
 class Sfsm;
-class SolverInterface;
+class SolverServiceInterface;
 
 std::vector<ConcreteTrace> generateStateCover(Sfsm const &sfsm);
-std::vector<ConcreteTrace> sfsmMethod(Sfsm const &sfsm, size_t stateDifference, Expressions const &propositions, SolverInterface *solverInstance);
+std::vector<ConcreteTrace> sfsmMethod(Sfsm const &sfsm, size_t stateDifference, Expressions const &propositions, SolverServiceInterface *solverInstance);
 }
 
diff --git a/src/libsfsmtest/utils/algorithms/FindAllImplications.hpp b/src/libsfsmtest/utils/algorithms/FindAllImplications.hpp
index 30236d2..2d1df8a 100644
--- a/src/libsfsmtest/utils/algorithms/FindAllImplications.hpp
+++ b/src/libsfsmtest/utils/algorithms/FindAllImplications.hpp
@@ -32,7 +32,7 @@
 namespace libfsmtest::SFSMs {
 
     typedef std::unordered_map<size_t, std::unordered_set<size_t>> ImplicationMap_t;
-    inline ImplicationMap_t findAllImplications(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &expressions, SolverInterface *solverInstance) {
+    inline ImplicationMap_t findAllImplications(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &expressions, SolverServiceInterface *solverInstance) {
         std::cerr << "[IMPLIC] Determinining implication relationships" << std::endl;
         ImplicationMap_t result;
         ImplicationMap_t impliedByMap;
diff --git a/src/libsfsmtest/utils/algorithms/FindAllSatisfiableConjunctions.hpp b/src/libsfsmtest/utils/algorithms/FindAllSatisfiableConjunctions.hpp
index 7d58899..0a429e4 100644
--- a/src/libsfsmtest/utils/algorithms/FindAllSatisfiableConjunctions.hpp
+++ b/src/libsfsmtest/utils/algorithms/FindAllSatisfiableConjunctions.hpp
@@ -37,7 +37,7 @@
 namespace libfsmtest::SFSMs {
 
     typedef std::map<ssize_t, std::unordered_set<ssize_t>> EquivalenceClassImplicationMap_t;
-    inline EquivalenceClassImplicationMap_t calculateImplicationMapForEquivalenceClasses(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &positiveExpressions, Expressions const &negativeExpressions, SolverInterface *solverInstance) {
+    inline EquivalenceClassImplicationMap_t calculateImplicationMapForEquivalenceClasses(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &positiveExpressions, Expressions const &negativeExpressions, SolverServiceInterface *solverInstance) {
         Expressions allExpressions = positiveExpressions;
         allExpressions.insert(allExpressions.end(), negativeExpressions.cbegin(), negativeExpressions.cend());
         auto implicationMap = findAllImplications(definitions, invariant, allExpressions, solverInstance);
@@ -59,7 +59,7 @@ namespace libfsmtest::SFSMs {
     }
 
     typedef std::vector<std::pair<std::vector<ssize_t>, Expression>> EquivalenceClassPartitioning_t;
-    inline EquivalenceClassPartitioning_t findAllSatisfiableConjunctions(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &expressions, SolverInterface *solverInstance) {
+    inline EquivalenceClassPartitioning_t findAllSatisfiableConjunctions(IdentifierDefinitions const &definitions, Expression const &invariant, Expressions const &expressions, SolverServiceInterface *solverInstance) {
         Expressions const &positiveExpressions = expressions;
         Expressions negatedExpressions;
         std::transform(positiveExpressions.cbegin(), positiveExpressions.cend(), std::back_inserter(negatedExpressions), [](auto const &expression) {
diff --git a/src/usage-demo/usage-demo.cpp b/src/usage-demo/usage-demo.cpp
index 306d775..fec487f 100644
--- a/src/usage-demo/usage-demo.cpp
+++ b/src/usage-demo/usage-demo.cpp
@@ -175,7 +175,7 @@ using namespace libfsmtest;
     brake.writeToFile();
     abstraction->accept(abstractBrake);
     abstractBrake.writeToFile();
-    libfsmtest::SFSMs::SolverInterface solver;
+    libfsmtest::SFSMs::StatefulSolverService solver;
     auto result = SFSMs::sfsmMethod(*sfsm, 0, props, &solver);
     std::cout << "Test suite POT (size: " << result.size() << "):" << std::endl;
     for(auto const &trace : result) {
@@ -185,7 +185,7 @@ using namespace libfsmtest;
 
 [[maybe_unused]] static void demo_SfsmMethod() {
     std::unique_ptr<SFSMs::Sfsm> sfsm = SFSMs::createSfsm<SFSMs::SfsmFromFileCreator>(RESOURCEPATH "brake/brake.csv");
-    libfsmtest::SFSMs::SolverInterface solver;
+    libfsmtest::SFSMs::StatefulSolverService solver;
     auto result = SFSMs::sfsmMethod(*sfsm, 0, {}, &solver);
     std::cout << "Test suite (size: " << result.size() << "):" << std::endl;
     for(auto const &trace : result) {
-- 
GitLab


From 1045bec0fe809e2e0b95211c93ce43066ef0ee78 Mon Sep 17 00:00:00 2001
From: Niklas Krafczyk <niklas@uni-bremen.de>
Date: Wed, 24 May 2023 11:36:37 +0200
Subject: [PATCH 3/3] Fixing regular expressions for integer and float

---
 src/libsfsmtest/sfsm/ExpressionEvaluation.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/libsfsmtest/sfsm/ExpressionEvaluation.cpp b/src/libsfsmtest/sfsm/ExpressionEvaluation.cpp
index 9eca15f..ebafe85 100644
--- a/src/libsfsmtest/sfsm/ExpressionEvaluation.cpp
+++ b/src/libsfsmtest/sfsm/ExpressionEvaluation.cpp
@@ -118,8 +118,8 @@ inline void dispatchLeftAssoc(EvalType &result, EvalType const &leftVal, OP &opC
 }
 
 static std::string const boolean{R"(true|false)"};
-static std::string const integer{R"(-?[0-9]*)"};
-static std::string const floating{R"(-?[0-9]*.[0-9]*)"};
+static std::string const integer{R"(-?[0-9]+)"};
+static std::string const floating{R"(-?[0-9]+\.[0-9]+)"};
 static std::string const all = (((std::string("(") += boolean) += std::string(")|(") += integer) += std::string(")|(") += floating) += std::string(")");
 static std::regex allRegex{all, std::regex::icase | std::regex::optimize | std::regex::ECMAScript};
 static std::regex operators{
-- 
GitLab